;;
*)
-let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
let m1 = symbols_of_term left in
let m =
TermMap.fold
;;
-let weight_of_equality (_, (ty, left, right, _), _, _) =
- let meta_number = ref 0 in
- let weight_of t =
- let weight, ml = weight_of_term t in
- meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
- weight
- in
- (weight_of ty) + (weight_of left) + (weight_of right), meta_number
-;;
-
-
module OrderedEquality = struct
type t = Inference.equality
match meta_convertibility_eq eq1 eq2 with
| true -> 0
| false ->
- let _, (ty, left, right, _), _, _ = eq1
- and _, (ty', left', right', _), _, _ = eq2 in
-(* let w1, m1 = weight_of_equality eq1 *)
-(* and w2, m2 = weight_of_equality eq2 in *)
- let weight_of t = fst (weight_of_term ~consider_metas:false t) in
- let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
- and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+ let w1, _, (ty, left, right, _), _, a = eq1
+ and w2, _, (ty', left', right', _), _, a' = eq2 in
+(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
+(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
+(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
match Pervasives.compare w1 w2 with
- | 0 -> Pervasives.compare eq1 eq2
-(* let res = Pervasives.compare m1 m2 in *)
-(* if res = 0 then Pervasives.compare eq1 eq2 else res *)
+ | 0 ->
+ let res = (List.length a) - (List.length a') in
+ if res <> 0 then res else (
+ try
+ let res = Pervasives.compare (List.hd a) (List.hd a') in
+ if res <> 0 then res else Pervasives.compare eq1 eq2
+ with _ -> Pervasives.compare eq1 eq2
+(* match a, a' with *)
+(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(* let res = Pervasives.compare i j in *)
+(* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(* | _, _ -> Pervasives.compare eq1 eq2 *)
+ )
| res -> res
end
try
let found =
List.find
- (fun (proof, (ty, left, right, ordering), m, a) ->
+ (fun (w, proof, (ty, left, right, ordering), m, a) ->
fst (CicReduction.are_convertible context left right ugraph))
negative
in
maxmeta := newmeta;
if is_identity env newcurrent then
if sign = Negative then Some (sign, newcurrent)
- else (Inference.delete_proof newcurrent; None)
+ else None
else
Some (sign, newcurrent)
in
if ok then res else None
| Some (Positive, c) ->
if Indexing.in_index active_table c then
- (Inference.delete_proof c; None)
+ None
else
match passive_table with
| None -> res
| Some passive_table ->
- if Indexing.in_index passive_table c then
- (Inference.delete_proof c; None)
+ if Indexing.in_index passive_table c then None
else res
(* | Some (s, c) -> if find_duplicate s c all then None else res *)
List.fold_left
(fun s e ->
if not (Inference.is_identity env e) then
- if EqualitySet.mem e s then
- (Inference.delete_proof e; s)
- else
- EqualitySet.add e s
- else
- (Inference.delete_proof e; s))
+ if EqualitySet.mem e s then s
+ else EqualitySet.add e s
+ else s)
EqualitySet.empty new_pos
in
let new_pos = EqualitySet.elements new_pos_set in
let is_duplicate =
match passive_table with
| None ->
- (fun e ->
- let ok = not (Indexing.in_index active_table e) in
- if not ok then Inference.delete_proof e;
- ok)
+ (fun e -> not (Indexing.in_index active_table e))
| Some passive_table ->
(fun e ->
- let ok = not ((Indexing.in_index active_table e) ||
- (Indexing.in_index passive_table e)) in
- if not ok then Inference.delete_proof e;
- ok)
+ not ((Indexing.in_index active_table e) ||
+ (Indexing.in_index passive_table e)))
in
new_neg, List.filter is_duplicate new_pos
if List.mem (s, eq) res then
res, tbl
else if (is_identity env eq) || (find eq res) then (
- Inference.delete_proof eq;
res, tbl
) (* else if (find eq res) then *)
(* res, tbl *)
List.fold_right
(fun (s, eq) (n, p) ->
if (s <> Negative) && (is_identity env eq) then (
- Inference.delete_proof eq;
(n, p)
) else
if s = Negative then eq::n, p
let env = (metasenv, context, ugraph) in
try
let term_equality = equality_of_term meta_proof goal in
- let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+ let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
let active = make_active () in
let passive = make_passive [term_equality] equalities in
Printf.printf "\ncurrent goal: %s\n"