(*
for debugging
let check_equation env equation msg =
- let w, proof, (eq_ty, left, right, order), metas, args = equation in
+ let w, proof, (eq_ty, left, right, order), metas = equation in
let metasenv, context, ugraph = env in
let metasenv' = metasenv @ metas in
try
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-let symbols_of_equality (_, _, (_, left, right, _), _, _) =
+let symbols_of_equality (_, _, (_, left, right, _), _) =
let m1 = symbols_of_term left in
let m =
TermMap.fold
m
;;
-module OrderedEquality = struct
+(* griggio *)
+module OrderedEquality = struct
type t = Inference.equality
let compare eq1 eq2 =
match meta_convertibility_eq eq1 eq2 with
| true -> 0
| false ->
- let w1, _, (ty, left, right, _), _, a = eq1
- and w2, _, (ty', left', right', _), _, a' = eq2 in
+ let w1, _, (ty, left, right, _), m1 = eq1
+ and w2, _, (ty', left', right', _), m2 = eq2 in
match Pervasives.compare w1 w2 with
+ | 0 ->
+ let res = (List.length m1) - (List.length m2) in
+ if res <> 0 then res else Pervasives.compare eq1 eq2
+ | res -> res
+end
+
+(*
+module OrderedEquality = struct
+ type t = Inference.equality
+
+ let minor eq =
+ let w, _, (ty, left, right, o), _ = eq in
+ match o with
+ | Lt -> Some left
+ | Le -> assert false
+ | Gt -> Some right
+ | Ge -> assert false
+ | Eq
+ | Incomparable -> None
+
+ let compare eq1 eq2 =
+ let w1, _, (ty, left, right, o1), m1 = eq1
+ and w2, _, (ty', left', right', o2), m2 = eq2 in
+ match Pervasives.compare w1 w2 with
| 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 Failure "hd" -> Pervasives.compare eq1 eq2
- )
- | res -> res
+ (match minor eq1, minor eq2 with
+ | Some t1, Some t2 ->
+ fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
+ | Some _, None -> -1
+ | None, Some _ -> 1
+ | _,_ ->
+ (List.length m2) - (List.length m1) )
+ | res -> res
+
+ let compare eq1 eq2 =
+ match compare eq1 eq2 with
+ 0 -> Pervasives.compare eq1 eq2
+ | res -> res
end
+*)
module EqualitySet = Set.Make(OrderedEquality);;
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
- let w,_,_,_,_ = hd in
+ let w,_,_,_ = hd in
let passive_table =
Indexing.remove_index passive_table hd
in (Positive, hd),
)
| _ ->
symbols_counter := !symbols_ratio;
- (* let set_selection set = EqualitySet.min_elt set in *)
- let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in
+ let set_selection set = EqualitySet.min_elt set in
+ (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *)
if EqualitySet.is_empty neg_set then
- let current = set_selection pos_list in
+ let current = set_selection pos_set in
let passive =
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
in
(Positive, current), passive
else
- let current = set_selection neg_list in
+ let current = set_selection neg_set in
let passive =
(remove current neg_list, EqualitySet.remove current neg_set),
(pos_list, pos_set),
let neg, pos = infer_positive table tl in
neg, res @ pos
in
+ let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+ maxmeta := maxm;
let curr_table = Indexing.index Indexing.empty current in
- let neg, pos = infer_positive curr_table active_list in
+ let neg, pos =
+ infer_positive curr_table ((sign,copy_of_current)::active_list)
+ in
if Utils.debug_metas then
ignore(List.map
(function current ->
try
let found =
List.find
- (fun (w, proof, (ty, left, right, ordering), m, a) ->
+ (fun (w, proof, (ty, left, right, ordering), m) ->
fst (CicReduction.are_convertible context left right ugraph))
negative
in
let active_list, newa =
List.fold_right
(fun (s, equality) (res, newn) ->
- let ew, _, _, _, _ = equality in
+ let ew, _, _, _ = equality in
if ew < min_weight then
(s, equality)::res, newn
else
let backward_simplify_passive env new_pos new_table min_weight passive =
let (nl, ns), (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
- let ew, _, _, _, _ = equality in
+ let ew, _, _, _ = equality in
if ew < min_weight then
equality::resl, ress, newn
else
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _, _ = e in
+ let ew, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) (snd new')
in
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _, _ = e in
+ let ew, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) (snd new')
in
;;
let is_commutative_law eq =
- let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+ let w, proof, (eq_ty, left, right, order), metas = snd eq in
match left,right with
Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
let module HL = HelmLibraryObjects in
let module I = Inference in
let metasenv, context, ugraph = env in
- let _, proof, (ty, left, right, _), metas, args = equality in
+ let _, proof, (ty, left, right, _), metas = equality in
let eqterm =
C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
let gproof, gmetas, gterm = goal in
debug_print
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
+ let _, proof, _, _ = current in
ParamodulationSuccess (Some proof, env)
) else (
debug_print
if res then
let proof =
match goal' with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | Some goal -> let _, proof, _, _ = goal in Some proof
| None -> None
in
ParamodulationSuccess (proof, env)
let proof =
match goal with
| Some goal ->
- let _, proof, _, _, _ = goal in Some proof
+ let _, proof, _, _ = goal in Some proof
| None -> None
in
ParamodulationSuccess (proof, env)
| _ -> assert false
in
( prerr_endline "esco qui";
+ (*
let s = Printf.sprintf "actives:\n%s\n"
(String.concat "\n"
((List.map
(string_of_equality ~env)
(let x,y,_ = passive in (fst x)@(fst y)))) in
prerr_endline s;
- prerr_endline sp;
+ prerr_endline sp; *)
ParamodulationSuccess (proof, env))
else
given_clause_fullred_aux dbd env goals theorems passive active
" LOCALMAX: " ^ string_of_int !Indexing.local_max ^
" #ACTIVES: " ^ string_of_int (size_of_active active) ^
" #PASSIVES: " ^ string_of_int (size_of_passive passive));
- if (size_of_active active) mod 54 = 0 then
+(*
+ if (size_of_active active) mod 50 = 0 then
(let s = Printf.sprintf "actives:\n%s\n"
(String.concat "\n"
((List.map
(string_of_equality ~env)
(let x,y,_ = passive in (fst x)@(fst y)))) in
prerr_endline s;
- prerr_endline sp);
+ prerr_endline sp); *)
let time1 = Unix.gettimeofday () in
let (_,context,_) = env in
let selection_estimate = get_selection_estimate () in
forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
match res with
| None ->
+ (* weight_age_counter := !weight_age_counter + 1; *)
given_clause_fullred dbd env goals theorems passive active
| Some (sign, current) ->
if (sign = Negative) && (is_identity env current) then (
debug_print
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
+ let _, proof, _, _ = current in
ParamodulationSuccess (Some proof, env)
) else (
debug_print
| true, goal ->
let proof =
match goal with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | Some goal -> let _, proof, _, _ = goal in Some proof
| None -> None
in
ParamodulationSuccess (proof, env)
print_endline (PP.pp proof names);
let newmetasenv =
List.fold_left
- (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+ (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
in
let _ =
(*try*)
projects / helm.git / blobdiff