fixed demodulation of goal

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index cfada50855c633a2f1532f1fb6cac2774282eef8..6ab9f59e28206cdd47331ccd91bdf055d1fb038b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/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 
@@ -2011,7 +2009,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 +2027,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 +2045,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 =