X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=c964e3a78c882f525df690c230ec60e18abd1eb4;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=b748afec7357c55270d9ec38fb6a67752be70b28;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index b748afec7..c964e3a78 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -298,7 +298,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   returns true if target is subsumed by some equality in table
 *)
 let subsumption env table target =
-  let _, (ty, left, right, _), tmetas, _ = target in
+  let _, _, (ty, left, right, _), tmetas, _ = target in
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
@@ -324,14 +324,15 @@ let subsumption env table target =
   in
   let rec ok what = function
     | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl ->
+    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching metasenv context what other ugraph in
+                Inference.matching (metasenv @ menv @ m) context what other ugraph
+	      in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
               r
@@ -348,18 +349,26 @@ let subsumption env table target =
           ok what tl
   in
   let r, subst = ok right leftr in
-  if r then
-    true, subst
-  else
-    let rightr =
-      match right with
-      | Cic.Meta _ -> []
-      | _ ->
-          let rightc = get_candidates Matching table right in
-          find_all_matches ~unif_fun:Inference.matching
-            metasenv context ugraph 0 right ty rightc
-    in
-    ok left rightr
+  let r, s =
+    if r then
+      true, subst
+    else
+      let rightr =
+	match right with
+	  | Cic.Meta _ -> []
+	  | _ ->
+              let rightc = get_candidates Matching table right in
+		find_all_matches ~unif_fun:Inference.matching
+		  metasenv context ugraph 0 right ty rightc
+      in
+	ok left rightr
+  in
+    (if r then 
+       debug_print 
+	 (lazy
+	    (Printf.sprintf "SUBSUMPTION! %s\n%s\n"
+	       (Inference.string_of_equality target) (Utils.print_subst s))));
+    r, s
 ;;
 
 
@@ -553,26 +562,47 @@ let rec demodulation_equality newmeta env table sign target =
     !maxmeta, res
   in
   let res = demodulation_aux metasenv' context ugraph table 0 left in
-  match res with
-  | Some t ->
-      let newmeta, newtarget = build_newtarget true t in
-      if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
-        (Inference.meta_convertibility_eq target newtarget) then
-          newmeta, newtarget
-      else
-        demodulation_equality newmeta env table sign newtarget
-  | None ->
-      let res = demodulation_aux metasenv' context ugraph table 0 right in
-      match res with
-      | Some t ->
-          let newmeta, newtarget = build_newtarget false t in
-          if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+  let newmeta, newtarget = 
+    match res with
+    | Some t ->
+	let newmeta, newtarget = build_newtarget true t in
+	  if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
             (Inference.meta_convertibility_eq target newtarget) then
-              newmeta, newtarget
-          else
-              demodulation_equality newmeta env table sign newtarget
-      | None ->
-          newmeta, target
+	      newmeta, newtarget
+	  else
+            demodulation_equality newmeta env table sign newtarget
+    | None ->
+	let res = demodulation_aux metasenv' context ugraph table 0 right in
+	  match res with
+	  | Some t ->
+	      let newmeta, newtarget = build_newtarget false t in
+		if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+		  (Inference.meta_convertibility_eq target newtarget) then
+		    newmeta, newtarget
+		else
+		  demodulation_equality newmeta env table sign newtarget
+	  | None ->
+	      newmeta, target
+  in
+  (* newmeta, newtarget *)
+  (* tentiamo di ridurre usando CicReduction.normalize *)
+  let w, p, (ty, left, right, o), m, a = newtarget in
+  let left' = ProofEngineReduction.simpl context left in
+  let right' = ProofEngineReduction.simpl context right in
+  let newleft =
+    if !Utils.compare_terms left' left = Utils.Lt then left' else left in
+  let newright = 
+    if !Utils.compare_terms right' right = Utils.Lt then right' else right in
+  if newleft != left || newright != right then (
+    debug_print
+      (lazy
+	 (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n"
+	    (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right)
+	    (CicPp.ppterm right')))
+  );
+  let w' = Utils.compute_equality_weight ty newleft newright in
+  let o' = !Utils.compare_terms newleft newright in
+  newmeta, (w', p, (ty, newleft, newright, o'), m, a)
 ;;