ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ef6999ca0887e65f5ad4036ca7320763d6693cda..72699f7e3cb2b584da6617a278a1b1f611945abd 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -122,7 +122,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
           with Not_found -> false) 
     | C.AMeta (id,_,_) -> 
          (try 
-            Hashtbl.find ids_to_inner_sorts id = "Prop"
+            Hashtbl.find ids_to_inner_sorts id = `Prop
           with Not_found -> assert false)
     | C.ASort (id,_) -> false
     | C.AImplicit _ -> raise NotImplemented
@@ -300,7 +300,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts =
    with Not_found -> None
  in
  match sort with
- | Some "Prop" ->
+ | Some `Prop ->
     `Hypothesis
       { K.dec_name = name_of n;
         K.dec_id = gen_id declaration_prefix seed; 
@@ -343,9 +343,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
             (match t with 
                C.ARel (idr,idref,n,b) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts idr 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts idr 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     K.Premise 
                       { K.premise_id = gen_id premise_prefix seed;
                         K.premise_xref = idr;
@@ -355,9 +356,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  else (K.Term t)
              | C.AConst(id,uri,[]) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts id 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     K.Lemma 
                       { K.lemma_id = gen_id lemma_prefix seed;
                         K.lemma_name = UriManager.name_of_uri uri;
@@ -366,18 +368,17 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  else (K.Term t)
              | C.AMutConstruct(id,uri,tyno,consno,[]) ->
                  let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts id 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
+                   (try
+                     Hashtbl.find ids_to_inner_sorts id 
+                    with Not_found -> `Type (CicUniv.fresh())) in 
+                 if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
                         CicEnvironment.get_obj CicUniv.empty_ugraph uri
                       in
                         match o with 
-                             Cic.Constant _ -> assert false
-                          | Cic.Variable _ -> assert false
-                          | Cic.CurrentProof _ -> assert false
-                          | Cic.InductiveDefinition (l,_,_) -> l 
+                          | Cic.InductiveDefinition (l,_,_,_) -> l 
+                           | _ -> assert false
                       ) in
                     let (_,_,_,constructors) = 
                       List.nth inductive_types tyno in 
@@ -410,7 +411,7 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
-   if sort = "Prop" then
+   if sort = `Prop then
        (let p = 
         (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
        in 
@@ -438,17 +439,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
     match t with 
       C.ARel (id,idref,n,b) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.AVar (id,uri,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.AMeta (id,n,l) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types 
         else raise Not_a_proof
     | C.ASort (id,s) -> raise Not_a_proof
@@ -457,7 +458,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
     | C.ACast (id,v,t) -> aux v
     | C.ALambda (id,n,s,t) -> 
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = `Prop then 
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -477,7 +478,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -532,13 +533,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             })
     | C.AConst (id,uri,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then
+        if sort = `Prop then
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
     | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = `Prop then 
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
@@ -548,7 +549,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
                | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> l,n 
+               | Cic.InductiveDefinition (l,_,n,_) -> l,n 
           ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
@@ -602,6 +603,9 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         let proofs = 
           List.map 
             (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+        let fun_name = 
+          List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no 
+        in
         let decreasing_args = 
           List.map (function (_,_,n,_,_) -> n) funs in
         let jo = 
@@ -622,7 +626,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                 [ K.Premise
                   { K.premise_id = gen_id premise_prefix seed; 
                     K.premise_xref = jo.K.joint_id;
-                    K.premise_binder = Some "tiralo fuori";
+                    K.premise_binder = Some fun_name;
                     K.premise_n = Some no;
                   }
                 ];
@@ -694,10 +698,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let inductive_types,noparams =
           (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
             match o with
-                Cic.Constant _ -> assert false
-               | Cic.Variable _ -> assert false
-               | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> (l,n) 
+               | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
+               | _ -> assert false
           ) in
         let rec split n l =
           if n = 0 then ([],l) else
@@ -729,9 +731,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   let idarg = get_id arg in
                   let sortarg = 
                     (try (Hashtbl.find ids_to_inner_sorts idarg)
-                     with Not_found -> "Type") in
+                     with Not_found -> `Type (CicUniv.fresh())) in
                   let hdarg = 
-                    if sortarg = "Prop" then
+                    if sortarg = `Prop then
                       let (co,bo) = 
                         let rec bc = 
                           function 
@@ -814,8 +816,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   else 
                     let aid = get_id a in
                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
-                      with Not_found -> "Type") in
-                    if asort = "Prop" then
+                      with Not_found -> `Type (CicUniv.fresh())) in
+                    if asort = `Prop then
                       K.ArgProof (aux a)
                     else K.Term a in
                 hd::(ma_aux (n-1) tl) in
@@ -916,7 +918,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let seed = ref 0 in
   function
-      C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
+      C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
         (gen_id object_prefix seed, params,
           Some
            (List.map
@@ -925,27 +927,27 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
           `Def (K.Const,ty,
             build_def_item seed (get_id bo) (C.Name n) bo 
              ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (_,_,n,Some bo,ty,params) ->
+    | C.AConstant (_,_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Const,ty,
              build_def_item seed (get_id bo) (C.Name n) bo 
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (id,_,n,None,ty,params) ->
+    | C.AConstant (id,_,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Const,
              build_decl_item seed id (C.Name n) ty 
                ~ids_to_inner_sorts))
-    | C.AVariable (_,n,Some bo,ty,params) ->
+    | C.AVariable (_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Var,ty,
              build_def_item seed (get_id bo) (C.Name n) bo
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AVariable (id,n,None,ty,params) ->
+    | C.AVariable (id,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Var,
              build_decl_item seed id (C.Name n) ty
               ~ids_to_inner_sorts))
-    | C.AInductiveDefinition (id,l,params,nparams) ->
+    | C.AInductiveDefinition (id,l,params,nparams,_) ->
          (gen_id object_prefix seed, params, None,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
@@ -959,6 +961,7 @@ and
       fun (_,n,b,ty,l) ->
         `Inductive
           { K.inductive_id = gen_id inductive_prefix seed;
+            K.inductive_name = n;
             K.inductive_kind = b;
             K.inductive_type = ty;
             K.inductive_constructors = build_constructors seed l