Most warnings turned into errors and avoided

[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 2613efefd1044fd9fee7a067711346c9201ccd1d..d5f35a3a321c16929177d4af525239dfcac334dc 100644 (file)
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -131,8 +131,8 @@ let compare_weights (h1, w1) (h2, w2) =
           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 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,_ ->
@@ -376,6 +382,8 @@ module LPO (B : Terms.Blob) = struct
       | Terms.Leaf _, Terms.Node _  -> true (* we assume unary constants 
                             are smaller than constants with higher arity *)
       | Terms.Node _, Terms.Leaf _ -> false
+      | Terms.Node [],_
+      | _,Terms.Node [] -> assert false
       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
           if List.exists (lpo_le s) tl2 then true
           else
@@ -395,85 +403,23 @@ module LPO (B : Terms.Blob) = struct
                     else false
                 in 
                 compare_args tl1 tl2
+            | _ -> assert false
            end
+   in
+    Hashtbl.add cache (s,t) res; res
   ;;
 
-  let new_lpo s t =
+  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
   ;;
     
 
-  let rec lpo s t =
-    match s,t with
-      | s, t when eq_foterm s t ->
-          XEQ
-      | Terms.Var _, Terms.Var _ ->
-          XINCOMPARABLE
-      | _, Terms.Var i ->
-          if (List.mem i (Terms.vars_of_term s)) then XGT
-          else XINCOMPARABLE
-      | Terms.Var i,_ ->
-          if (List.mem i (Terms.vars_of_term t)) then XLT
-          else XINCOMPARABLE
-      | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
-          let rec ge_subterm t ol = function
-            | [] -> (false, ol)
-            | x::tl ->
-                let res = lpo x t in
-                match res with
-                  | XGT | XEQ -> (true,res::ol)
-                  | o -> ge_subterm t (o::ol) tl
-          in
-          let (res, l_ol) = ge_subterm t [] tl1 in
-            if res then XGT
-            else let (res, r_ol) = ge_subterm s [] tl2 in
-              if res then XLT
-              else begin
-                let rec check_subterms t = function
-                  | _,[] -> true
-                  | o::ol,_::tl ->
-                      if o = XLT then check_subterms t (ol,tl)
-                      else false
-                  | [], x::tl ->
-                      if lpo x t = XLT then check_subterms t ([],tl)
-                      else false
-                in
-                match aux_ordering B.compare hd1 hd2 with
-                  | XGT -> if check_subterms s (r_ol,tl2) then XGT
-                    else XINCOMPARABLE
-                  | XLT -> if check_subterms t (l_ol,tl1) then XLT
-                    else XINCOMPARABLE
-                  | XEQ -> 
-                     (try
-                      let lex = List.fold_left2
-                        (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
-                        XEQ tl1 tl2
-                      in
-                 (match lex with
-                    | XGT ->
-                        if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
-                      else XINCOMPARABLE
-                    | XLT ->
-                        if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
-                      else XINCOMPARABLE
-                    | o -> o)   
-                      with Invalid_argument _ -> (* assert false *)
-                              XINCOMPARABLE)
-              | XINCOMPARABLE -> XINCOMPARABLE
-              | _ -> assert false
-          end
-      | _,_ -> aux_ordering B.compare s t
-            
-  ;;
-  
-  let lpo s t = new_lpo s t 
-(* 
-      if res = lpo s t then res
-      else assert false *)
-
   let compare_terms = compare_terms lpo;;
 
   let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;