+let debug = true;;
+
+let debug_print = if debug then prerr_endline else ignore;;
+
+
let print_metasenv metasenv =
String.concat "\n--------------------------\n"
(List.map (fun (i, context, term) ->
;;
-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
;;
+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:
| Positive -> "Positive"
;;
+
+type pos = Left | Right
+
+let string_of_pos = function
+ | Left -> "Left"
+ | Right -> "Right"
+;;