Porting to ocaml 5

[helm.git] / matita / components / ng_paramodulation / orderings.ml

diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml
index b457832453dd5582b5d44c95c9c292fb68578ac0..8da829e750df1e71daff86dde4b93b8cab9d1c4e 100644 (file)
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -130,9 +130,9 @@ let compare_weights (h1, w1) (h2, w2) =
       | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
           if var1 = var2 then
             let diffs = (w1 - w2) + diffs in
-            let r = Pervasives.compare w1 w2 in
-            let lt = lt or (r < 0) in
-            let gt = gt or (r > 0) in
+            let r = Stdlib.compare w1 w2 in
+            let lt = lt || (r < 0) in
+            let gt = gt || (r > 0) in
               if lt && gt then XINCOMPARABLE else
                 aux hdiff (lt, gt) diffs tl1 tl2
           else if var1 < var2 then
@@ -208,7 +208,7 @@ module NRKBO (B : Terms.Blob) = struct
   let name = "nrkbo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
@@ -224,7 +224,7 @@ exception UnificationFailure of string Lazy.t;;
       in
       match s, t with
         | s, t when eq_foterm s t -> subst
-        | Terms.Var i, Terms.Var j
+        | Terms.Var i, Terms.Var _j
             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
             let subst = FoSubst.build_subst i t subst in
               subst
@@ -290,7 +290,7 @@ module KBO (B : Terms.Blob) = struct
   let name = "kbo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
@@ -356,17 +356,23 @@ module LPO (B : Terms.Blob) = struct
   let name = "lpo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
   let compute_unit_clause_weight = compute_unit_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
+  (*CSC: beware! Imperative cache! *)
+  let cache = Hashtbl.create 101
+
   let rec lpo_le s t = 
     eq_foterm s t || lpo_lt s t 
   
   and lpo_lt s t =
+    try Hashtbl.find cache (s,t)
+    with
+    Not_found -> let res =
     match s,t with
       | _, Terms.Var _ -> false
       | Terms.Var i,_ ->
@@ -399,13 +405,18 @@ module LPO (B : Terms.Blob) = struct
                 compare_args tl1 tl2
             | _ -> assert false
            end
+   in
+    Hashtbl.add cache (s,t) res; res
   ;;
 
   let lpo s t =
+    let res =
     if eq_foterm s t then XEQ
     else if lpo_lt s t then XLT
     else if lpo_lt t s then XGT
     else XINCOMPARABLE
+    in
+     Hashtbl.clear cache; res
   ;;