added record generation module

diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend
index 09359d63abce95456750ef404864745456409bfb..105cfe4d94597653df66c92f25b99400154f7e00 100644 (file)
--- 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 de106143cb3af8497221e557ad4a72b48c5def2f..63d79e14ea6abedbb51d300148dba28b06986700 100644 (file)
--- 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 (file)
index 0000000..7348a61
--- /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
+    
+    
+
+