Cleaned a bit

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 6880f6d18c177d3849fd284e8bab30e9165c7723..28fbe15073ae2fc32abf0dbfeda32e0e15726e2b 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -18,6 +18,15 @@ module Orderings (B : Terms.Blob) = struct
   module Pp = Pp.Pp(B)
 
   type weight = int * (int * int) list;;
+
+let rec eq_foterm x y =
+    x == y ||
+    match x, y with
+    | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+    | Terms.Var i, Terms.Var j -> i = j
+    | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
+    | _ -> false
+  ;;
   
   let string_of_weight (cw, mw) =
     let s =
@@ -224,7 +233,7 @@ let compute_goal_weight (_,l, _, _) =
 
   let rec lpo s t =
     match s,t with
-      | s, t when s = t ->
+      | s, t when eq_foterm s t ->
           XEQ
       | Terms.Var _, Terms.Var _ ->
           XINCOMPARABLE
@@ -282,76 +291,18 @@ let compute_goal_weight (_,l, _, _) =
             
   ;;
 
-let rec lpo_old t1 t2 =
-  match t1, t2 with
-  | t1, t2 when t1 = t2 -> XEQ
-  | t1, (Terms.Var m) ->
-      if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE
-  | (Terms.Var m), t2 ->
-      if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE
-  | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> (
-      let res =
-        let f o r t =
-          if r then true else
-            match lpo_old t o with
-            | XGT | XEQ -> true
-            | _ -> false
-        in
-        let res1 = List.fold_left (f t2) false tl1 in
-        if res1 then XGT
-        else let res2 = List.fold_left (f t1) false tl2 in
-        if res2 then XLT
-        else XINCOMPARABLE
-      in
-      if res <> XINCOMPARABLE then
-        res
-      else
-        let f o r t =
-          if not r then false else
-            match lpo_old o t with
-            | XGT -> true
-            | _ -> false
-        in
-        match aux_ordering hd1 hd2 with
-        | XGT ->
-            let res = List.fold_left (f t1) true tl2 in
-            if res then XGT
-            else XINCOMPARABLE
-        | XLT ->
-            let res = List.fold_left (f t2) true tl1 in
-            if res then XLT
-            else XINCOMPARABLE
-        | XEQ -> (
-            let lex_res =
-              try
-                List.fold_left2
-                  (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2)
-                  XEQ tl1 tl2
-              with Invalid_argument _ ->
-                XINCOMPARABLE
-            in
-            match lex_res with
-            | XGT ->
-                if List.fold_left (f t1) true tl2 then XGT
-                else XINCOMPARABLE
-            | XLT ->
-                if List.fold_left (f t2) true tl1 then XLT
-                else XINCOMPARABLE
-            | _ -> XINCOMPARABLE
-          )
-        | _ -> XINCOMPARABLE
-    )
-  | t1, t2 -> aux_ordering t1 t2
-;;
-
   let compare_terms x y = 
       match nonrec_kbo x y with
-(*       match lpo x y with *)
         | XINCOMPARABLE -> Terms.Incomparable
         | XGT -> Terms.Gt
         | XLT -> Terms.Lt
         | XEQ -> Terms.Eq
         | _ -> assert false
-  ;; 
+  ;;
+
+  let profiler = HExtlib.profile ~enable:true "compare_terms";;
+  let compare_terms x y =
+    profiler.HExtlib.profile (compare_terms x) y
+  ;;
 
 end