version 0.7.1

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 4a20f5c3d80eb1547d88801d88d4741c96965f9e..d6454f2027d4799fdf2dd49bf1ade2bdd685f24d 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -7,8 +7,8 @@ let print_metasenv metasenv =
 ;;
 
 
-let print_subst subst =
-  String.concat "\n"
+let print_subst ?(prefix="\n") subst =
+  String.concat prefix
     (List.map
        (fun (i, (c, t, ty)) ->
           Printf.sprintf "?%d -> %s : %s" i
@@ -83,6 +83,19 @@ let weight_of_term ?(consider_metas=true) term =
 ;;
 
 
+let compute_equality_weight ty left right =
+  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));
+    w
+  in
+  (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
+;;
+
+
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,
  * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
@@ -406,3 +419,10 @@ let string_of_sign = function
   | Positive -> "Positive"
 ;;
 
+
+type pos = Left | Right 
+
+let string_of_pos = function
+  | Left -> "Left"
+  | Right -> "Right"
+;;