in
let in_weight = round (howmany *. ratio /. (ratio +. 1.))
and in_age = round (howmany /. (ratio +. 1.)) in
- debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
+ debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
let symbols, card =
match active with
| (Negative, e)::_ ->
let f sign equality (resl, ress, newn) =
let ew, _, _, _, _ = equality in
if ew < min_weight then
-(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *)
+(* let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *)
equality::resl, ress, newn
else
match forward_simplify env (sign, equality) (new_pos, new_table) with
if !time_limit = 0. || !processed_clauses = 0 then
passive
else if !elapsed_time > !time_limit then (
- debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
- !time_limit !elapsed_time);
+ debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
+ !time_limit !elapsed_time));
make_passive [] []
) else if kept > selection_estimate then (
- debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
+ debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
"(kept: %d, selection_estimate: %d)\n")
- kept selection_estimate);
+ kept selection_estimate));
prune_passive selection_estimate active passive
) else
passive
given_clause env passive active
| Some (sign, current) ->
if (sign = Negative) && (is_identity env current) then (
- debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
- (string_of_equality ~env current));
+ debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+ (string_of_equality ~env current)));
ParamodulationSuccess (Some current, env)
) else (
- debug_print "\n================================================";
- debug_print (Printf.sprintf "selected: %s %s"
+ debug_print (lazy "\n================================================");
+ debug_print (lazy (Printf.sprintf "selected: %s %s"
(string_of_sign sign)
- (string_of_equality ~env current));
+ (string_of_equality ~env current)));
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
if !time_limit = 0. || !processed_clauses = 0 then
passive
else if !elapsed_time > !time_limit then (
- debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
- !time_limit !elapsed_time);
+ debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
+ !time_limit !elapsed_time));
make_passive [] []
) else if kept > selection_estimate then (
- debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
+ debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
"(kept: %d, selection_estimate: %d)\n")
- kept selection_estimate);
+ kept selection_estimate));
prune_passive selection_estimate active passive
) else
passive
given_clause_fullred env passive active
| Some (sign, current) ->
if (sign = Negative) && (is_identity env current) then (
- debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
- (string_of_equality ~env current));
+ debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+ (string_of_equality ~env current)));
ParamodulationSuccess (Some current, env)
) else (
- debug_print "\n================================================";
- debug_print (Printf.sprintf "selected: %s %s"
+ debug_print (lazy "\n================================================");
+ debug_print (lazy (Printf.sprintf "selected: %s %s"
(string_of_sign sign)
- (string_of_equality ~env current));
+ (string_of_equality ~env current)));
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
processed_clauses := !processed_clauses + (kept - 1 - k);
let _ =
- debug_print (
+ debug_print (lazy (
Printf.sprintf "active:\n%s\n"
(String.concat "\n"
((List.map
(fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e)) (fst active)))))
+ (string_of_equality ~env e)) (fst active))))))
in
let _ =
match new' with
| neg, pos ->
- debug_print (
+ debug_print (lazy (
Printf.sprintf "new':\n%s\n"
(String.concat "\n"
((List.map
(string_of_equality ~env e)) neg) @
(List.map
(fun e -> "Positive " ^
- (string_of_equality ~env e)) pos))))
+ (string_of_equality ~env e)) pos)))))
in
match contains_empty env new' with
| false, _ ->
else
let equalities =
let equalities = equalities @ library_equalities in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality equalities)));
- debug_print "SIMPLYFYING EQUALITIES...";
+ (List.map string_of_equality equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let active = others @ others_simpl in
let tbl =
let res =
List.rev (List.map snd (simpl (Positive, hd) others []))
in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality res)));
+ (List.map string_of_equality res))));
res
in
let active = make_active () in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let _, context, ty = CicUtil.lookup_meta goal' metasenv in
- debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
+ debug_print (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
Cic.Meta (maxm+1, irl),
(maxm+1, context, ty)::metasenv,
ty
maxmeta := maxm+2;
let equalities =
let equalities = equalities @ library_equalities in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality equalities)));
- debug_print "SIMPLYFYING EQUALITIES...";
+ (List.map string_of_equality equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let active = others @ others_simpl in
let tbl =
let res =
List.rev (List.map snd (simpl (Positive, hd) others []))
in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality res)));
+ (List.map string_of_equality res))));
res
in
let active = make_active () in
in
match res with
| ParamodulationSuccess (Some goal, env) ->
- debug_print "OK, found a proof!";
+ debug_print (lazy "OK, found a proof!");
let proof = Inference.build_proof_term goal in
let names = names_of_context context in
let newmetasenv =
let ty, ug =
CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
in
- debug_print (CicPp.pp proof [](* names *));
- debug_print
+ debug_print (lazy (CicPp.pp proof [](* names *)));
+ debug_print (lazy
(Printf.sprintf
"\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
(CicPp.pp type_of_goal names) (CicPp.pp ty names)
(string_of_bool
(fst (CicReduction.are_convertible
- context type_of_goal ty ug))));
+ context type_of_goal ty ug)))));
let equality_for_replace i t1 =
match t1 with
| C.Meta (n, _) -> n = i
~what:[goal'] ~with_what:[proof]
~where:meta_proof
in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
(match uri with Some uri -> UriManager.string_of_uri uri
| None -> "")
(print_metasenv newmetasenv)
(CicPp.pp real_proof [](* names *))
- (CicPp.pp term_to_prove names));
+ (CicPp.pp term_to_prove names)));
((uri, newmetasenv, real_proof, term_to_prove), [])
with CicTypeChecker.TypeCheckerFailure _ ->
- debug_print "THE PROOF DOESN'T TYPECHECK!!!";
- debug_print (CicPp.pp proof names);
+ debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
+ debug_print (lazy (CicPp.pp proof names));
raise (ProofEngineTypes.Fail
"Found a proof, but it doesn't typecheck")
in
- debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time);
+ debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
newstatus
| _ ->
raise (ProofEngineTypes.Fail "NO proof found")
projects / helm.git / blobdiff