commented out a line to help paramodulation.

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index cfada50855c633a2f1532f1fb6cac2774282eef8..3bc8eb25bf2cfb13fce3641b6b40cf793d80ecc1 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -628,12 +628,7 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
     | None -> None
     | Some ((_, _), pt) -> Some pt
   in
-  let demodulate table goal = 
-    let changed, newmeta, newgoal =
-      Indexing.demodulation_goal !maxmeta env table goal in
-    maxmeta := newmeta;
-    changed, newgoal
-  in
+  let demodulate table goal = Indexing.demodulation_goal env table goal in
   let changed, goal =
     match passive_table with
     | None -> demodulate active_table goal
@@ -1274,8 +1269,8 @@ let simplify_goal_set env goals passive active =
   in
   let simplified =
     List.fold_left
-      (fun acc g -> 
-        match simplify_goal env g ~passive active with 
+      (fun acc goal -> 
+        match simplify_goal env goal ~passive active with 
         | _, g -> if find g acc then acc else g::acc)
       [] active_goals
   in
@@ -1314,6 +1309,9 @@ let infer_goal_set env active goals =
         let selected = hd in
         let passive_goals = tl in
         let new' = Indexing.superposition_left env (snd active) selected in
+        let metasenv, context, ugraph = env in
+        let names = names_of_context context in
+        List.iter (fun (_,_,x) -> prerr_endline ("X: " ^ CicPp.pp x names)) new';
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in 
@@ -1768,11 +1766,6 @@ let saturate
           (ProofEngineHelpers.compare_metasenvs 
             ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
-      let free_metas = 
-        List.filter (fun i -> i <> goalno)
-          (ProofEngineHelpers.compare_metasenvs 
-            ~oldmetasenv:metasenv ~newmetasenv:proof_menv)
-      in
       let goal_proof, side_effects_t = 
         let initial = Equality.build_proof_term newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
@@ -1802,8 +1795,12 @@ let saturate
       let goal_proof = replace goal_proof in
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
          * what mi pare buono, sostituisce solo le meta farlocche *)
-        prerr_endline (CicPp.pp goal_proof names);
       let side_effects_t = List.map replace side_effects_t in
+      let free_metas = 
+        List.filter (fun i -> i <> goalno)
+          (ProofEngineHelpers.compare_metasenvs 
+            ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
+      in
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1829,18 +1826,24 @@ let saturate
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
       let _ = 
-        let ty,_ =
+        try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
             CicUniv.empty_ugraph
-        in
-        ty
+        with 
+        | CicUtil.Meta_not_found _ 
+        | CicTypeChecker.TypeCheckerFailure _ 
+        | CicTypeChecker.AssertFailure _ 
+        | Invalid_argument "list_fold_left2" as exn ->
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+            prerr_endline (CicPp.pp goal_proof names);
+            raise exn
       in
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
       let open_goals = 
-        match free_meta with Some (Cic.Meta (m,_)) -> [m] | _ -> [] 
+        match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
@@ -2011,7 +2014,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 *)
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = 
+let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
   let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -2029,11 +2032,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
       (fun tbl eq -> Indexing.index tbl eq) 
       Indexing.empty equalities 
   in
-  let _, newmeta,(newproof,newmetasenv, newty) = 
+  let changed,(newproof,newmetasenv, newty) = 
     Indexing.demodulation_goal 
-      maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
   in
-  if newmeta != maxm then
+  if changed then
     begin
       let opengoal = Cic.Meta(maxm,irl) in
       let proofterm,_ = 
@@ -2047,11 +2050,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
             extended_status in
         (status,maxm::newgoals)
     end
-  else if newty = ty then
+  else (* if newty = ty then *)
     raise (ProofEngineTypes.Fail (lazy "no progress"))
-  else ProofEngineTypes.apply_tactic 
+  (*else ProofEngineTypes.apply_tactic 
     (ReductionTactics.simpl_tac ~pattern) 
-    initialstatus
+    initialstatus*)
 ;;
 
 let demodulate_tac ~dbd ~pattern =