78 |
78 |
79 fun print silent f = if silent then () else writeln (f ()) |
79 fun print silent f = if silent then () else writeln (f ()) |
80 |
80 |
81 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, |
81 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, |
82 type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, |
82 type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, |
83 minimize, preplay_timeout, ...} : params) |
83 minimize, preplay_timeout, induction_rules, ...} : params) |
84 silent (prover : prover) timeout i n state goal facts = |
84 silent (prover : prover) timeout i n state goal facts = |
85 let |
85 let |
86 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ |
86 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ |
87 (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") |
87 (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") |
88 |
88 |
89 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) |
89 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) |
90 val params = |
90 val params = |
91 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, |
91 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, |
92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
94 max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), |
94 induction_rules = induction_rules, max_facts = SOME (length facts), |
95 max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, |
95 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
96 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
97 compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = false, |
98 expect = ""} |
98 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} |
99 val problem = |
99 val problem = |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
101 factss = [("", facts)], found_proof = I} |
101 factss = [("", facts)], found_proof = I} |
102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
103 message} = |
103 message} = |