type result =
| Failure
- | Success of Cic.term option * environment
+ | Success of Inference.equality option * environment
;;
;;
*)
-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
let contains_empty env (negative, positive) =
let metasenv, context, ugraph = env in
try
- let (proof, _, _, _) =
+ 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
- true, Some proof
+ true, Some found
with Not_found ->
false, None
;;
Indexing.demodulation !maxmeta env table current in
maxmeta := newmeta;
if is_identity env newcurrent then
- if sign = Negative then Some (sign, newcurrent) else None
+ if sign = Negative then Some (sign, newcurrent)
+ else None
else
Some (sign, newcurrent)
in
match passive_table with
| None -> res
| Some passive_table ->
- if Indexing.in_index passive_table c then None else res
+ if Indexing.in_index passive_table c then None
+ else res
(* | Some (s, c) -> if find_duplicate s c all then None else res *)
let new_pos_set =
List.fold_left
(fun s e ->
- if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+ if not (Inference.is_identity env e) then
+ 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 -> not (Indexing.in_index active_table e))
+ | None ->
+ (fun e -> not (Indexing.in_index active_table e))
| Some passive_table ->
- (fun e -> not ((Indexing.in_index active_table e) ||
- (Indexing.in_index passive_table e)))
+ (fun e ->
+ not ((Indexing.in_index active_table e) ||
+ (Indexing.in_index passive_table e)))
in
new_neg, List.filter is_duplicate new_pos
let active, newa =
List.fold_right
(fun (s, eq) (res, tbl) ->
- if (is_identity env eq) || (find eq res) then
+ if List.mem (s, eq) res then
+ res, tbl
+ else if (is_identity env eq) || (find eq res) then (
res, tbl
+ ) (* else if (find eq res) then *)
+(* res, tbl *)
else
(s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
active_list ([], Indexing.empty_table ()),
List.fold_right
(fun (s, eq) (n, p) ->
- if (s <> Negative) && (is_identity env eq) then
+ if (s <> Negative) && (is_identity env eq) then (
(n, p)
- else
+ ) else
if s = Negative then eq::n, p
else n, eq::p)
newa ([], [])
Printf.printf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current);
print_newline ();
- let proof, _, _, _ = current in
- Success (Some proof, env)
+ Success (Some current, env)
) else (
print_endline "\n================================================";
Printf.printf "selected: %s %s"
let t2 = Unix.gettimeofday () in
infer_time := !infer_time +. (t2 -. t1);
- let res, proof = contains_empty env new' in
+ let res, goal = contains_empty env new' in
if res then
- Success (proof, env)
+ Success (goal, env)
else
let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' (* ~passive *) active in
(* (EqualitySet.elements ps)))); *)
(* print_newline (); *)
given_clause env passive active
- | true, proof ->
- Success (proof, env)
+ | true, goal ->
+ Success (goal, env)
)
;;
Printf.printf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current);
print_newline ();
- let proof, _, _, _ = current in
- Success (Some proof, env)
+ Success (Some current, env)
) else (
print_endline "\n================================================";
Printf.printf "selected: %s %s"
| false, _ ->
let passive = add_to_passive passive new' in
given_clause_fullred env passive active
- | true, proof ->
- Success (proof, env)
+ | true, goal ->
+ Success (goal, env)
)
;;
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"
match res with
| Failure ->
Printf.printf "NO proof found! :-(\n\n"
- | Success (Some proof, env) ->
- Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
- (PP.pp proof (names_of_context context))
- (finish -. start);
-(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
-(* " demodulate: %.9f\n subsumption: %.9f\n") *)
-(* fs_time_info.build_all fs_time_info.demodulate *)
-(* fs_time_info.subsumption; *)
+ | Success (Some goal, env) ->
+ Printf.printf "OK, found a proof!\n";
+ let proof = Inference.build_term_proof goal in
+ print_endline (PP.pp proof (names_of_context context));
+ print_endline (string_of_float (finish -. start));
| Success (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
projects / helm.git / blobdiff