ocaml 3.09 transition

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index b748afec7357c55270d9ec38fb6a67752be70b28..c964e3a78c882f525df690c230ec60e18abd1eb4 100644 (file)
--- 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)
 ;;