X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=c8ff783c3eafab71d645e5bc13005682259a62ae;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=2c51fe7f80331d23c800fdab42fa9dc78e073bd2;hpb=79d584e8f049226ec9cf68e9e06880ed0d95af51;p=helm.git

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index 2c51fe7f8..c8ff783c3 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -78,7 +78,7 @@ let rec occur uri =
     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
     | C.Cast (te,ty) -> (occur uri te)
     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
-    | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
+    | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t)
     | C.Appl l -> 
         List.fold_left 
           (fun b a -> 
@@ -103,7 +103,7 @@ let get_id =
     | C.AProd (id,_,_,_) -> id
     | C.ACast (id,_,_) -> id
     | C.ALambda (id,_,_,_) -> id
-    | C.ALetIn (id,_,_,_) -> id
+    | C.ALetIn (id,_,_,_,_) -> id
     | C.AAppl (id,_) -> id
     | C.AConst (id,_,_) -> id
     | C.AMutInd (id,_,_,_) -> id
@@ -145,7 +145,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
           with Not_found -> false)
-    | C.ALetIn (id,_,_,_) -> 
+    | C.ALetIn (id,_,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
@@ -274,7 +274,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
     }
 ;;
 
-let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
+let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let module C = Cic in
   let module K = Content in
@@ -294,8 +294,9 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
                  None -> None
               | Some t -> 
-                  if is_intro then Some (C.AProd ("gen"^id,n,s,t))
-                  else Some (C.ALetIn ("gen"^id,n,s,t)))
+                 match ty with
+                    None -> Some (C.AProd ("gen"^id,n,s,t))
+                  | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t)))
         };
     }
 ;;
@@ -360,7 +361,7 @@ let infer_dependent ~headless context metasenv = function
                   (n <> Cic.Anonymous && fstorder src, t) :: 
                   aux (CicSubstitution.subst 
                         (Deannotate.deannotate_term t) tgt) tl
-              | _ -> assert false
+              | _ -> List.map (fun s -> false,s) (t::tl)
        in
        (false, he) :: aux hety tl
      with CicTypeChecker.TypeCheckerFailure _ -> assert false
@@ -369,16 +370,19 @@ let infer_dependent ~headless context metasenv = function
 let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
   let module C = Cic in
   let module K = Content in
-  let rec aux =
+  let rec aux n =
     function
       [] -> [],[]
     | (dep, t)::l1 -> 
-       let subproofs,args = aux l1 in
-        if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+       let need_lifting =
+        test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in
+       let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in
+        if need_lifting then
           let new_subproof = 
             acic2content 
               seed context metasenv 
-               ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+               ~name:("H" ^ string_of_int n) ~ids_to_inner_types
+               ~ids_to_inner_sorts t in
           let new_arg = 
             K.Premise
               { K.premise_id = gen_id premise_prefix seed;
@@ -423,7 +427,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
-			 CicEnvironment.get_obj CicUniv.empty_ugraph uri
+			 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
 		       in
 			 match o with 
 			   | Cic.InductiveDefinition (l,_,_,_) -> l 
@@ -444,7 +448,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
              | _ -> (K.Term (dep,t))) in
           subproofs,hd::args
   in 
-  match (aux (infer_dependent ~headless context metasenv l)) with
+  match (aux 1 (infer_dependent ~headless context metasenv l)) with
     [p],args -> 
       [{p with K.proof_name = None}], 
         List.map 
@@ -456,7 +460,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
 
 and
 
-build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
@@ -470,7 +474,8 @@ build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_ty
         { K.def_name = name_of n;
           K.def_id = gen_id definition_prefix seed; 
           K.def_aref = id;
-          K.def_term = t
+          K.def_term = t;
+          K.def_type = ty
         }
   with
    Not_found -> assert false
@@ -525,14 +530,16 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
                   proof'.K.proof_context
             }
           in
-          generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
+          generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types
         else 
           raise Not_a_proof 
-    | C.ALetIn (id,n,s,t) ->
+    | C.ALetIn (id,n,s,ty,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = `Prop then
-          let proof = (* XXX TIPAMI!!! *)
-            aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t 
+          let proof =
+            aux
+             ((Some (n,
+              Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t 
           in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -544,17 +551,17 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
             { proof' with
                K.proof_name = None;
                K.proof_context = 
-                 ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
+                 ((build_def_item seed context metasenv (get_id s) n s ty ids_to_inner_sorts
                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
                  ::proof'.K.proof_context;
             }
           in
-          generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
+          generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types
         else 
           raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
-           seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try rewrite 
            seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
@@ -605,7 +612,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+          (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 	     match o with
 		 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
@@ -773,7 +780,7 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+          (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
 	     match o with
                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
                | _ -> assert false
@@ -878,21 +885,31 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
           } 
   | _ -> raise NotApplicable
 
-and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts =
   match li with
     | ((Cic.AConst _) as he)::tl
     | ((Cic.AMutInd _) as he)::tl
     | ((Cic.AMutConstruct _) as he)::tl when 
-       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
-       !hide_coercions ->
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
+       (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+       | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+       && !hide_coercions ->
+        let cpos,sats =
+          match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+          | None -> assert false
+          | Some (_,_,_,sats,cpos) -> cpos, sats
         in
-          acic2content 
-            seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+        let x = List.nth tl cpos in
+        let _,rest = 
+          try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] 
+        in
+        if rest = [] then
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           x
+        else
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           (Cic.AAppl (id,x::rest))
     | _ -> raise NotApplicable
 
 and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
@@ -939,7 +956,8 @@ and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_s
               { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method =
-                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI then
+                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+                 || LibraryObjects.is_eq_ind_URI uri then
                   "RewriteLR"
                  else
                   "RewriteRL";
@@ -1036,7 +1054,7 @@ let map_conjectures
               K.dec_aref = get_id t;
               K.dec_type = t
             })
-     | (id,Some (name,Cic.ADef t)) ->
+     | (id,Some (name,Cic.ADef (t,ty))) ->
          Some
           (* We should call build_def_item, but we have not computed *)
           (* the inner-types ==> we always produce a declaration     *)
@@ -1044,7 +1062,8 @@ let map_conjectures
              { K.def_name = name_of name;
                K.def_id = gen_id definition_prefix seed; 
                K.def_aref = get_id t;
-               K.def_term = t
+               K.def_term = t;
+               K.def_type = ty
              })
    ) context
  in
@@ -1072,7 +1091,7 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) =
               K.dec_aref = get_id t;
               K.dec_type = t
             })
-     | (id,Some (name,Cic.ADef t)) ->
+     | (id,Some (name,Cic.ADef (t,ty))) ->
          Some
           (* We should call build_def_item, but we have not computed *)
           (* the inner-types ==> we always produce a declaration     *)
@@ -1080,7 +1099,8 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) =
              { K.def_name = name_of name;
                K.def_id = id; 
                K.def_aref = get_id t;
-               K.def_term = t
+               K.def_term = t;
+               K.def_type = ty
              })
    ) context
  in
@@ -1102,12 +1122,12 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
           `Def (K.Const,ty,
            build_def_item 
              seed [] (Deannotate.deannotate_conjectures conjectures) 
-             (get_id bo) (C.Name n) bo 
+             (get_id bo) (C.Name n) bo ty
              ~ids_to_inner_sorts ~ids_to_inner_types))
     | 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 
+           build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
                ~ids_to_inner_sorts ~ids_to_inner_types))
     | C.AConstant (id,_,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
@@ -1117,7 +1137,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
     | 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
+           build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
                ~ids_to_inner_sorts ~ids_to_inner_types))
     | C.AVariable (id,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,