X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=42703045d0019616b041af03fd1031d02ab66f4f;hb=ba9a57375b50e0527bf0d48f189f7e3129bbe99f;hp=b0aa00e890021aa93d00a4e38340efe283697cab;hpb=92d100db14a01e3fb70a7d5151ac1e60d5a782a0;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index b0aa00e89..42703045d 100644
--- 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,12 @@ let weight_of_term ?(consider_metas=true) term =
 ;;
 
 
+let compute_equality_weight ty left right =
+  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+  (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
 (* 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:
@@ -397,3 +403,19 @@ let rec lpo t1 t2 =
 
 (* settable by the user... *)
 let compare_terms = ref nonrec_kbo;;
+
+
+type equality_sign = Negative | Positive;;
+
+let string_of_sign = function
+  | Negative -> "Negative"
+  | Positive -> "Positive"
+;;
+
+
+type pos = Left | Right 
+
+let string_of_pos = function
+  | Left -> "Left"
+  | Right -> "Right"
+;;