From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 14:27:20 +0000 (+0000)
Subject: is_identity -> is_weak_identity
X-Git-Tag: 0.4.95@7852~970
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c93b71e6c429cd13ed4d223c4379174bfdb8e74d;p=helm.git

is_identity -> is_weak_identity
---

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 0b3ec04a8..34c601b35 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -592,7 +592,9 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     !maxmeta, res 
   in
 
-  let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
+  let res = 
+    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
+  in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 
     match res with
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 7ddfd86fc..da4ef7826 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -438,21 +438,22 @@ let check_for_deep_subsumption env active_table eq =
 
 (** simplifies current using active and passive *)
 let forward_simplify bag eq_uri env current (active_list, active_table) =
+  prerr_endline (Equality.string_of_equality ~env current);
   let _, context, _ = env in
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
-    if Equality.is_identity env newcurrent then None else Some newcurrent
+    if Equality.is_weak_identity newcurrent then None else Some newcurrent
   in
-  let rec demod current =
+  let demod current =
     if Utils.debug_metas then
       ignore (Indexing.check_target bag context current "demod0");
     let res = demodulate active_table current in
-      if Utils.debug_metas then
-        ignore ((function None -> () | Some x -> 
-                   ignore (Indexing.check_target bag context x "demod1");()) res);
+    if Utils.debug_metas then
+      ignore ((function None -> () | Some x -> 
+      ignore (Indexing.check_target bag context x "demod1");()) res);
     res
   in 
   let res = demod current in
@@ -556,7 +557,7 @@ let backward_simplify_active
       (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
            (res, (id_of_eq eq)::pruned),tbl 
-         else if (Equality.is_identity env eq) || (find eq res) then (
+         else if (Equality.is_weak_identity eq) || (find eq res) then (
            (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
@@ -746,7 +747,10 @@ let rec simpl bag eq_uri env e others others_simpl =
          if Equality.is_weak_identity e then t else Indexing.index t e) 
       Indexing.empty active
   in
-  let res = forward_simplify bag eq_uri env e (active, tbl) in
+  let res = 
+    if Equality.is_weak_identity e then None else 
+      forward_simplify bag eq_uri env e (active, tbl) 
+  in
     match others with
       | hd::tl -> (
           match res with
@@ -1077,6 +1081,7 @@ let given_clause
           ParamodulationSuccess p
       | None -> 
 *)
+
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
@@ -1084,6 +1089,7 @@ let given_clause
                   let goals = 
                     infer_goal_set_with_current bag env current goals active 
                   in
+
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
 (*                   prerr_endline "fwd/back simpl"; *)
                   let rec simplify new' active passive =
@@ -1103,6 +1109,7 @@ let given_clause
                   let active, passive, new' = 
                     simplify new' active passive
                   in
+
 (*                   prerr_endline "simpl goal with new"; *)
                   let goals = 
                     let a,b,_ = build_table new' in