X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=149fd90ec4389dfb47015cbb16dc2803e976fcf3;hb=c43f710f5e23e940114b1623329f650814e783af;hp=82f0005f5eaf08af13187c769ba2323da61205e0;hpb=9e781c8957ff049e7bba65e1d611e5f007b02fb5;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 82f0005f5..149fd90ec 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -114,49 +114,49 @@ let test_for_lifting ~ids_to_inner_types =
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ALambda (id,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ALetIn (id,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.AAppl (id,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false) 
+          with Not_found -> false) 
     | C.AConst (id,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false) 
+          with Not_found -> false) 
     | C.AMutInd (id,_,_,_) -> false
     | C.AMutConstruct (id,_,_,_,_) -> 
        (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
         (* oppure: false *)
     | C.AMutCase (id,_,_,_,_,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.AFix (id,_,_) ->
           (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
     | C.ACoFix (id,_,_) ->
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
-          with notfound -> false)
+          with Not_found -> false)
 ;;
 
 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
@@ -184,7 +184,7 @@ let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
                C.ARel (idr,idref,n,b) ->
                  let sort = 
                    (try Hashtbl.find ids_to_inner_sorts idr 
-                    with notfound -> "Type") in 
+                    with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     K.Premise 
                       { K.premise_id = gen_id seed;
@@ -209,7 +209,6 @@ let flat seed p =
     else 
       let p1 =
         { p with
-          K.proof_id = gen_id seed;
           K.proof_context = []; 
           K.proof_apply_context = []
         } in
@@ -282,7 +281,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
           K.conclude_args = [K.Term t];
           K.conclude_conclusion = 
               try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-              with notfound -> None
+              with Not_found -> None
         };
     }
 ;;
@@ -303,7 +302,7 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
           K.conclude_conclusion = 
             try Some 
              (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-            with notfound -> 
+            with Not_found -> 
               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
                  None -> None
               | Some t -> 
@@ -315,44 +314,50 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
 
 let build_decl_item seed id n s ~ids_to_inner_sorts =
  let module K = Content in
-  let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
-  if sort = "Prop" then
-     `Hypothesis
-       { K.dec_name = name_of n;
-         K.dec_id = gen_id seed; 
-         K.dec_inductive = false;
-         K.dec_aref = id;
-         K.dec_type = s
-       }
-  else 
-     `Declaration
-       { K.dec_name = name_of n;
-         K.dec_id = gen_id seed; 
-         K.dec_inductive = false;
-         K.dec_aref = id;
-         K.dec_type = s
-       }
+  try
+   let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
+   if sort = "Prop" then
+      `Hypothesis
+        { K.dec_name = name_of n;
+          K.dec_id = gen_id seed; 
+          K.dec_inductive = false;
+          K.dec_aref = id;
+          K.dec_type = s
+        }
+   else 
+      `Declaration
+        { K.dec_name = name_of n;
+          K.dec_id = gen_id seed; 
+          K.dec_inductive = false;
+          K.dec_aref = id;
+          K.dec_type = s
+        }
+  with
+   Not_found -> assert false
 ;;
 
 let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
-  let sort = Hashtbl.find ids_to_inner_sorts id in
-  if sort = "Prop" then
-     `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
-  else 
-     `Definition
-       { K.def_name = name_of n;
-         K.def_id = gen_id seed; 
-         K.def_aref = id;
-         K.def_term = t
-       }
+  try
+   let sort = Hashtbl.find ids_to_inner_sorts id in
+   if sort = "Prop" then
+      `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+   else 
+      `Definition
+        { K.def_name = name_of n;
+          K.def_id = gen_id seed; 
+          K.def_aref = id;
+          K.def_term = t
+        }
+  with
+   Not_found -> assert false
 
 (* the following function must be called with an object of sort
 Prop. For debugging purposes this is tested again, possibly raising an 
 Not_a_proof exception *)
 
-and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
-  let rec aux ?(name = None) t =
+and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
+  let rec aux ?name t =
   let module C = Cic in
   let module K = Content in
   let module C2A = Cic2acic in
@@ -380,7 +385,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
     | C.ALambda (id,n,s,t) -> 
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = "Prop" then 
-          let proof = aux t ~name:None in
+          let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
                match proof.K.proof_conclude.K.conclude_args with
@@ -430,7 +435,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
           let subproofs = 
             match args_to_lift with
                 [_] -> List.map aux args_to_lift 
-            | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
+            | _ -> List.map (aux ~name:"H") args_to_lift in
           let args = build_args seed li subproofs 
                  ~ids_to_inner_types ~ids_to_inner_sorts in
             { K.proof_name = name;
@@ -445,7 +450,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                   K.conclude_conclusion = 
                      try Some 
                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                     with notfound -> None
+                     with Not_found -> None
                  };
             })
     | C.AConst (id,uri,exp_named_subst) as t ->
@@ -460,76 +465,59 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
+        let inductive_types =
+           (match CicEnvironment.get_obj uri with
+               Cic.Constant _ -> assert false
+             | Cic.Variable _ -> assert false
+             | Cic.CurrentProof _ -> assert false
+             | Cic.InductiveDefinition (l,_,_) -> l 
+           ) in
+        let (_,_,_,constructors) = List.nth inductive_types typeno in 
         let teid = get_id te in
-        let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
-        (match 
-          (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
-           with notfound -> None)
-         with
-             Some tety -> (* we must lift up the argument *)
+        let pp = List.map2 
+          (fun p (name,_) -> (K.ArgProof (aux ~name p))) 
+           patterns constructors in
+        let apply_context,term =
+          (match 
+            (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
+             with Not_found -> None)
+           with
+             Some tety -> 
                let p = (aux te) in
-               { K.proof_name = Some "name";
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = flat seed p;
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with notfound -> None  
-                   }
-               }
-           | None ->
-               { K.proof_name = name;
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = [];
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with notfound -> None 
-                   }
-               }
-         )  
-    | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> 
-        let proof = (aux bo) in (* must be recursive !! *)
-          { K.proof_name = name;
-            K.proof_id   = gen_id seed;
-            K.proof_context = [`Proof proof]; 
-            K.proof_apply_context = [];
-            K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
-                K.conclude_aref = id;
-                K.conclude_method = "Exact";
-                K.conclude_args =
-                [ K.Premise
-                  { K.premise_id = gen_id seed; 
-                    K.premise_xref = proof.K.proof_id;
-                    K.premise_binder = proof.K.proof_name;
-                    K.premise_n = Some 1;
-                  }
-                ];
-                K.conclude_conclusion =
-                   try Some 
-                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
-              }
+               (flat seed p, 
+                K.Premise
+		 { K.premise_id = gen_id seed; 
+                   K.premise_xref = p.K.proof_id;
+                   K.premise_binder = p.K.proof_name;
+                   K.premise_n = None
+                 })
+           | None -> [],K.Term te) in
+        { K.proof_name = name;
+          K.proof_id   = gen_id seed;
+          K.proof_context = []; 
+          K.proof_apply_context = apply_context;
+          K.proof_conclude = 
+            { K.conclude_id = gen_id seed; 
+              K.conclude_aref = id;
+              K.conclude_method = "Case";
+              K.conclude_args = 
+                (K.Aux (UriManager.string_of_uri uri))::
+                (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+              K.conclude_conclusion = 
+                try Some 
+                  (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+                with Not_found -> None  
+             }
         }
     | C.AFix (id, no, funs) -> 
         let proofs = 
-          List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
+          List.map 
+            (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+        let decreasing_args = 
+          List.map (function (_,_,n,_,_) -> n) funs in
         let jo = 
           { K.joint_id = gen_id seed;
-            K.joint_kind = `Recursive;
+            K.joint_kind = `Recursive decreasing_args;
             K.joint_defs = proofs
           } 
         in
@@ -552,39 +540,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
-              }
-        } 
-    | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> 
-        let proof = (aux bo) in (* must be recursive !! *)
-          { K.proof_name = name;
-            K.proof_id   = gen_id seed;
-            K.proof_context = [`Proof proof]; 
-            K.proof_apply_context = [];
-            K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
-                K.conclude_aref = id;
-                K.conclude_method = "Exact";
-                K.conclude_args =
-                [ K.Premise
-                  { K.premise_id = gen_id seed; 
-                    K.premise_xref = proof.K.proof_id;
-                    K.premise_binder = proof.K.proof_name;
-                    K.premise_n = Some 1;
-                  }
-                ];
-                K.conclude_conclusion =
-                   try Some 
-                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
         } 
     | C.ACoFix (id,no,funs) -> 
         let proofs = 
-          List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
+          List.map 
+            (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
         let jo = 
           { K.joint_id = gen_id seed;
-            K.joint_kind = `Recursive;
+            K.joint_kind = `CoRecursive;
             K.joint_defs = proofs
           } 
         in
@@ -607,16 +572,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
                 K.conclude_conclusion =
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                  with notfound -> None
+                  with Not_found -> None
               };
         } 
      in 
      let id = get_id t in
      generate_conversion seed false id t1 ~ids_to_inner_types
-in aux ~name:name t
+in aux ?name t
 
 and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
-  let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
+  let aux ?name = acic2content seed  ~ids_to_inner_types ~ids_to_inner_sorts in
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -663,7 +628,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
         let subproofs = 
           match args_to_lift with
             [_] -> List.map aux args_to_lift 
-          | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
+          | _ -> List.map (aux ~name:"H") args_to_lift in
         prerr_endline "****** end subproofs *******"; flush stderr;
         let other_method_args = 
           build_args seed other_args subproofs 
@@ -715,7 +680,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
                                 (  prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; 
                                 let (context,body) = bc (t,t1) in
                                 (ce::context,body))
-                            | _ , t -> ([],aux t ~name:None) in
+                            | _ , t -> ([],aux t) in
                         bc (ty,arg) in
                       K.ArgProof
                        { bo with
@@ -735,19 +700,19 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_aref = id;
                 K.conclude_method = "ByInduction";
                 K.conclude_args =
-                  K.Aux no_constructors 
+                  K.Aux (string_of_int no_constructors) 
                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
                   ::method_args@other_method_args;
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None  
+                   with Not_found -> None  
               }
           } 
   | _ -> raise NotApplicable
 
 and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
-  let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
+  let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -791,7 +756,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                   with notfound -> None
+                   with Not_found -> None
               }
           } 
       else raise NotApplicable
@@ -801,6 +766,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
 let map_conjectures
  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
 =
+ let module K = Content in
  let context' =
   List.map
    (function
@@ -808,13 +774,26 @@ let map_conjectures
      | (id,Some (name,Cic.ADecl t)) ->
          id,
           Some
-           (build_decl_item seed (get_id t) name t
-            ~ids_to_inner_sorts)
+           (* We should call build_decl_item, but we have not computed *)
+           (* the inner-types ==> we always produce a declaration      *)
+           (`Declaration
+             { K.dec_name = name_of name;
+               K.dec_id = gen_id seed; 
+               K.dec_inductive = false;
+               K.dec_aref = get_id t;
+               K.dec_type = t
+             })
      | (id,Some (name,Cic.ADef t)) ->
          id,
           Some
-           (build_def_item seed (get_id t) name t
-            ~ids_to_inner_sorts ~ids_to_inner_types)
+           (* We should call build_def_item, but we have not computed *)
+           (* the inner-types ==> we always produce a declaration     *)
+           (`Definition
+              { K.def_name = name_of name;
+                K.def_id = gen_id seed; 
+                K.def_aref = get_id t;
+                K.def_term = t
+              })
    ) context
  in
   (id,n,context',ty)