weak equality on meta used when replacing.

updated to the new goal_proof

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index e12b1f8a7a1b23591749e6de244da6804152e15b..b71f5e5b6fbd7002191d354ab996e7b5e8f7da12 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -73,7 +73,7 @@ let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
 type new_proof = 
-  Equality.goal_proof * Equality.proof * Subst.substitution * Cic.metasenv
+  Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
 type result =
   | ParamodulationFailure of string
   | ParamodulationSuccess of new_proof
@@ -942,8 +942,8 @@ let print_goals goals =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*  let names = names_of_context ctx in*)
-(*  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);*)
+  let names = names_of_context ctx in
+  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
@@ -954,9 +954,12 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
         | Some (subst, equality ) ->
+            prerr_endline 
+              ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
+            prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
-            Some (goalproof, p, subst, cicmenv)
+            Some (goalproof, p, id, subst, cicmenv)
         | None -> None)
   | _ -> None
 ;;
@@ -999,7 +1002,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
         | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ 
             when left = right && iseq uri -> 
             let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
-            true, Some (goalproof, reflproof, Subst.empty_subst,m)
+            true, Some (goalproof, reflproof, 0, Subst.empty_subst,m)
         | goal::_ ->
             (match check_if_goal_is_subsumed env (snd active) goal with
             | None -> false,None
@@ -1249,7 +1252,7 @@ let check_if_goal_is_identity env = function
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
     when left = right && iseq uri ->
       let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
-      Some (goalproof, reflproof,Subst.empty_subst,m)
+      Some (goalproof, reflproof, 0, Subst.empty_subst,m)
   | _ -> None
 ;;                              
     
@@ -1747,7 +1750,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 1000 in
-      let max_time = Unix.gettimeofday () +.  120. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in
     let finish = Unix.gettimeofday () in
@@ -1757,9 +1760,11 @@ let saturate
   | ParamodulationFailure s ->
       raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
   | ParamodulationSuccess 
-    (goalproof,newproof,subsumption_subst, proof_menv) ->
+    (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
       prerr_endline "OK, found a proof!";
-      prerr_endline (Equality.pp_proof names goalproof newproof);
+      prerr_endline 
+        (Equality.pp_proof names goalproof newproof subsumption_subst
+          subsumption_id type_of_goal);
       prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
@@ -1791,11 +1796,13 @@ let saturate
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) proof_menv 
       in
-prerr_endline ("RIMPIAZZATO CON " ^ match free_meta with None -> "?" | Some m -> CicPp.ppterm m);
-
       let replace where = 
+        (* we need this fake equality since the metas of the hypothesis may be
+         * with a real local context *)
         ProofEngineReduction.replace_lifting 
-          ~equality:(=) ~what ~with_what ~where
+          ~equality:(fun x y -> 
+            match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false)
+          ~what ~with_what ~where
       in
       let goal_proof = replace goal_proof in
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
@@ -1842,7 +1849,8 @@ prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
         | CicTypeChecker.AssertFailure _ 
         | Invalid_argument "list_fold_left2" as exn ->
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-(*            prerr_endline (CicPp.pp goal_proof names); *)
+            prerr_endline (CicPp.pp goal_proof names); 
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
             raise exn
       in
       let proof, real_metasenv =