ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / cicRecord.ml

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml
index 7348a61fcb85534bf75e544c7413d783c67d6718..a251bad87c5b5530b8253f0c8f221e51d5e3b6d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicRecord.ml
+++ b/helm/ocaml/cic_proof_checking/cicRecord.ml
@@ -23,90 +23,69 @@
  * 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
-    
-    
+let generate_one_proj uri params paramsno fields t i =
+ 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 paramsno in
+ let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in
+  Some
+   (mk_lambdas params
+     (Cic.Lambda (Cic.Name "w", recty,
+       Cic.MutCase (uri,0,outtype, Cic.Rel 1, 
+        [mk_lambdas fields (Cic.Rel i)]))))
 
-  
+let projections_of uri field_names =
+ let buri = UriManager.buri_of_uri uri in
+ let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+  match obj with
+     Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
+      assert (params = []); (* general case not implemented *)
+      let leftparams,ty =
+       let rec aux =
+        function
+           0,ty -> [],ty
+         | n,Cic.Prod (Cic.Name name,s,t) ->
+            let leftparams,ty = aux (n - 1,t) in
+             (name,s)::leftparams,ty
+         | _,_ -> assert false
+       in
+        aux (paramsno,ty)
+      in
+      let fields =
+       let rec aux =
+        function
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl)
+         | _,_ -> assert false
+       in
+        aux ((CicSubstitution.lift 1 ty),field_names)
+      in
+       let rec aux i =
+        function
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl ->
+            (match generate_one_proj uri leftparams paramsno fields s i with
+                Some p ->
+                 let puri =
+                  UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+                 in
+                  (puri,name,p) ::
+                    aux (i - 1)
+                     (CicSubstitution.subst
+                       (Cic.Appl
+                         (Cic.Const (puri,[]) ::
+                           CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
+                       ) t, tl)
+              | None -> assert false)
+         | _,_ -> assert false
+       in
+        aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
+   | _ -> assert false