module IntSet = Set.Make(OrderedInt)
-let compute_equality_weight ty left right =
+let compute_equality_weight (ty,left,right,o) =
+ let factor = 1 in
+ match o with
+ | Lt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ w + (factor * (List.length m)) ;
+ | Le -> assert false
+ | Gt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w + (factor * (List.length m)) ;
+ | Ge -> assert false
+ | Eq
+ | Incomparable ->
+ let w1, m1 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ let w2, m2 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+;;
+
+(* old
+let compute_equality_weight (ty,left,right,o) =
let metasw = ref 0 in
let weight_of t =
let w, m = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false t) in
- metasw := !metasw + (2 * (List.length m)) ;
+ metasw := !metasw + (1 * (List.length m)) ;
w
in
(* Warning: the following let cannot be expanded since it forces the
right evaluation order!!!! *)
- let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+ let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+ (* let w = weight_of (Cic.Appl [ty;left;right]) in *)
w + !metasw
;;
-
+*)
(* returns a "normalized" version of the polynomial weight wl (with type
* weight list), i.e. a list sorted ascending by meta number,