some fixes

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 1968f017c9d36967cea9a43df3bf2a6ed5a73b40..f2ece4baa9f8478716212d4bf13e89d42b5b40ff 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -88,16 +88,28 @@ let weight_of_term ?(consider_metas=true) term =
 ;;
 
 
+module OrderedInt = struct
+  type t = int
+
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(OrderedInt)
+
 let compute_equality_weight ty left right =
+(*   let metasw = ref IntSet.empty in *)
   let metasw = ref 0 in
   let weight_of t =
     let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
 (*     let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
 (*     metasw := !metasw + mw; *)
     metasw := !metasw + (2 * (List.length m));
+(*     metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
     w
   in
-  (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
+  (weight_of ty) + (weight_of left) + (weight_of right) +
+    !metasw
+(*     (4 * IntSet.cardinal !metasw) *)
 ;;
 
 
@@ -227,7 +239,7 @@ let compare_weights ?(normalize=false)
 ;;
 
 
-let rec aux_ordering t1 t2 =
+let rec aux_ordering ?(recursion=true) t1 t2 =
   let module C = Cic in
   let compare_uris u1 u2 =
     let res =
@@ -259,7 +271,7 @@ let rec aux_ordering t1 t2 =
   | C.MutConstruct _, _ -> Lt
   | _, C.MutConstruct _ -> Gt
 
-  | C.Appl l1, C.Appl l2 ->
+  | C.Appl l1, C.Appl l2 when recursion ->
       let rec cmp t1 t2 =
         match t1, t2 with
         | [], [] -> Eq
@@ -271,10 +283,13 @@ let rec aux_ordering t1 t2 =
             else o
       in
       cmp l1 l2
+  | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
+      aux_ordering h1 h2
         
   | t1, t2 ->
-      Printf.printf "These two terms are not comparable:\n%s\n%s\n\n"
-        (CicPp.ppterm t1) (CicPp.ppterm t2);
+      debug_print (
+        Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
+          (CicPp.ppterm t1) (CicPp.ppterm t2));
       Incomparable
 ;;
 
@@ -300,6 +315,68 @@ let nonrec_kbo t1 t2 =
 ;;
 
 
+let rec kbo t1 t2 =
+(*   debug_print ( *)
+(*     Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
+(*   if t1 = t2 then *)
+(*     Eq *)
+(*   else *)
+    let aux = aux_ordering ~recursion:false in
+    let w1 = weight_of_term t1
+    and w2 = weight_of_term t2 in
+    let rec cmp t1 t2 =
+      match t1, t2 with
+      | [], [] -> Eq
+      | _, [] -> Gt
+      | [], _ -> Lt
+      | hd1::tl1, hd2::tl2 ->
+          let o =
+(*             debug_print ( *)
+(*               Printf.sprintf "recursion kbo on %s %s" *)
+(*                 (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *)
+            kbo hd1 hd2
+          in
+          if o = Eq then cmp tl1 tl2
+          else o
+    in
+    let comparison = compare_weights ~normalize:true w1 w2 in
+(*     debug_print ( *)
+(*       Printf.sprintf "Weights are: %s %s: %s" *)
+(*         (string_of_weight w1) (string_of_weight w2) *)
+(*         (string_of_comparison comparison)); *)
+    match comparison with
+    | Le ->
+        let r = aux t1 t2 in
+(*         debug_print ("HERE! " ^ (string_of_comparison r)); *)
+        if r = Lt then Lt
+        else if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+              if cmp tl1 tl2 = Lt then Lt else Incomparable
+          | _, _ ->  Incomparable
+        ) else Incomparable
+    | Ge ->
+        let r = aux t1 t2 in
+        if r = Gt then Gt
+        else if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+              if cmp tl1 tl2 = Gt then Gt else Incomparable
+          | _, _ ->  Incomparable
+        ) else Incomparable
+    | Eq ->
+        let r = aux t1 t2 in
+        if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+(*               if cmp tl1 tl2 = Gt then Gt else Incomparable *)
+              cmp tl1 tl2
+          | _, _ ->  Incomparable
+        ) else r 
+    | res -> res
+;;
+          
+
 let names_of_context context = 
   List.map
     (function