From 821485bdc469482d0f29ac2d1e6c6dd1a6a94661 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Apr 2009 16:13:37 +0000
Subject: [PATCH] fixed bug, demodulation was keeping results not strictly
 smaller

---
 .../tactics/paramodulation/indexing.ml        | 39 +++++++++----------
 helm/software/components/tactics/tactics.mli  |  2 +-
 2 files changed, 19 insertions(+), 22 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index b5d683dc9..97e45522d 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -360,7 +360,7 @@ let find_matches metasenv context ugraph lift_amount term termty =
   can be either Founif.matching or Inference.unification
 *)
 (* XXX termty unused *)
-let rec find_all_matches ?(unif_fun=Founif.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -368,7 +368,16 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
-  let cmp = !Utils.compare_terms in
+  let cmp x y = 
+          let r = !Utils.compare_terms x y in
+(*
+          prerr_endline (
+                  CicPp.ppterm x ^ "   " ^
+                  Utils.string_of_comparison r ^ "   " ^ 
+                       CicPp.ppterm y ); 
+*)
+          r
+  in
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> []
@@ -409,12 +418,14 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
                 let c' = apply_subst s c
                 and other' = apply_subst s other in
                 let order = cmp c' other' in
-                if order <> U.Lt && order <> U.Le then
+                if (demod && order = U.Gt) ||
+                   (not demod && (order <> U.Lt && order <> U.Le)) 
+                then
                   res::(find_all_matches ~unif_fun metasenv context ugraph
                           lift_amount term termty tl)
                 else
                   find_all_matches ~unif_fun metasenv context ugraph
-                    lift_amount term termty tl
+                     lift_amount term termty tl
           with
           | Founif.MatchingFailure
           | CicUnification.UnificationFailure _
@@ -424,10 +435,10 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
 ;;
 
 let find_all_matches 
-  ?unif_fun metasenv context ugraph lift_amount term termty l 
+  ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
 =
     find_all_matches 
-      ?unif_fun metasenv context ugraph lift_amount term termty l 
+      ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
   (*prerr_endline "CANDIDATES:";
   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
@@ -1247,7 +1258,7 @@ let rec demodulation_all_aux
       let termty, ugraph = C.Implicit None, ugraph in
       let res =
         find_all_matches 
-          ~unif_fun:Founif.matching
+          ~unif_fun:Founif.matching ~demod:true
             metasenv context ugraph lift_amount term termty candidates
       in
       match term with
@@ -1285,20 +1296,6 @@ let demod_all steps bag env table goal =
         let new_goals = 
           List.map (build_newg bag context goal Equality.Demodulation) res 
         in
-        (* we need this cause an equation E like
-            F ?x => F ?y
-           can add a meta for y in a goal without instantiating it
-            P (F true) ----> P (F ?y)
-           and this may cause duplicated in metasenvs
-           demodulating again with E
-        *)
-        let bag, new_goals =
-          List.fold_right
-            (fun g (bag,acc) ->
-              let bag, g = Equality.fix_metas_goal bag g in
-              bag, g::acc)
-          new_goals (bag,[])
-        in
         let visited, bag, res = aux steps visited bag (new_goals @ rest) in
         visited, bag, goal :: res
   in
diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index ca340f7d1..310cf42ef 100644
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 23 10:59:57 CEST 2009 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Apr 28 17:14:45 CEST 2009 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyP : term:Cic.term -> ProofEngineTypes.tactic
-- 
2.39.2