From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Apr 2009 16:13:37 +0000 (+0000)
Subject: fixed bug, demodulation was keeping results not strictly smaller
X-Git-Tag: make_still_working~4042
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=821485bdc469482d0f29ac2d1e6c6dd1a6a94661;p=helm.git

fixed bug, demodulation was keeping results not strictly smaller
---

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