From 3130208e2889643252cc835925b38042d6055d5d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jun 2005 16:48:11 +0000 Subject: [PATCH] added record generation module --- helm/ocaml/cic_proof_checking/.depend | 2 + helm/ocaml/cic_proof_checking/Makefile | 3 +- helm/ocaml/cic_proof_checking/cicRecord.ml | 112 +++++++++++++++++++++ 3 files changed, 116 insertions(+), 1 deletion(-) create mode 100644 helm/ocaml/cic_proof_checking/cicRecord.ml diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 09359d63a..105cfe4d9 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -22,3 +22,5 @@ cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \ cicPp.cmi cicEnvironment.cmi cicElim.cmi cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \ cicPp.cmx cicEnvironment.cmx cicElim.cmi +cicRecord.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicRecord.cmi +cicRecord.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicRecord.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index de106143c..63d79e14e 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -14,7 +14,8 @@ INTERFACE_FILES = \ cicMiniReduction.mli \ cicReduction.mli \ cicTypeChecker.mli \ - cicElim.mli + cicElim.mli \ + cicRecord.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml new file mode 100644 index 000000000..7348a61fc --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicRecord.ml @@ -0,0 +1,112 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type record_spec = + string * (string * Cic.term) list * Cic.term * (string * Cic.term) list + +let rec_ty uri leftno = + let rec_ty = Cic.MutInd (uri,0,[]) in + if leftno = 0 then rec_ty else + Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0)) + +let inductive_of_record (suri,params,ty,fields) = + let uri = UriManager.uri_of_string suri in + let name = UriManager.name_of_uri uri in + let leftno = List.length params in + let constructor_ty = + List.fold_right ( + fun (name, ty) acc -> + Cic.Prod (Cic.Name name, ty, acc)) + (params @ fields) (CicSubstitution.lift (List.length fields) + (rec_ty uri leftno)) + in + let ty = + List.fold_right ( + fun (name,ty) t -> + Cic.Prod(Cic.Name name,ty, t) + ) params ty + in + let types = [name,true,ty,["mk_" ^ name,constructor_ty]] in + let obj = + Cic.InductiveDefinition (types, [],leftno,[`Class `Record]) + in + let ugraph = + CicTypeChecker.typecheck_mutual_inductive_defs uri + (types, [], leftno) CicUniv.empty_ugraph + in + types, leftno, obj, ugraph + +let projections_of (suri,params,ty,fields) = + let uri = UriManager.uri_of_string suri in + let buri = UriManager.buri_of_uri uri in + let name = UriManager.name_of_uri uri in + let leftno = List.length params in + let ty = + List.fold_right ( + fun (name,ty) t -> + Cic.Prod(Cic.Name name,ty, t) + ) params ty + in + let mk_lambdas l start = + List.fold_right (fun (name,ty) acc -> + Cic.Lambda (Cic.Name name,ty,acc)) l start + in + let recty = rec_ty uri leftno in + let _,projections,_ = + let qualify name = buri ^ "/" ^ name ^ ".con" in + let mk_oty toapp typ = + Cic.Lambda (Cic.Name "w", recty, ( + let l,_ = + List.fold_right (fun (name,_) (acc,i) -> + let u = UriManager.uri_of_string (qualify name) in + (Cic.Appl ([Cic.Const (u,[])] @ + CicUtil.mk_rels leftno i @ [Cic.Rel i])) + :: acc, i+1 + ) toapp ([],1) + in + List.fold_left ( + fun res t -> CicSubstitution.subst t res + ) (CicSubstitution.lift_from (List.length toapp + 1) 1 typ) l)) + in + let toapp = try List.tl (List.rev fields) with Failure _-> [] in + List.fold_right ( + fun (name, typ) (i, acc, toapp) -> + let start = + Cic.Lambda(Cic.Name "x", recty, + Cic.MutCase (uri,0,CicSubstitution.lift 1 (mk_oty toapp typ), + Cic.Rel 1, + [CicSubstitution.lift 1 + (mk_lambdas fields (Cic.Rel i))])) + in + i+1, ((qualify name, name, mk_lambdas params start) :: acc) , + if toapp <> [] then List.tl toapp else [] + ) + fields (1, [], toapp) + in + projections + + + + -- 2.39.2