45 end |
45 end |
46 |
46 |
47 fun print silent f = if silent then () else Output.urgent_message (f ()) |
47 fun print silent f = if silent then () else Output.urgent_message (f ()) |
48 |
48 |
49 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, |
49 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, |
50 max_new_mono_instances, type_enc, lam_trans, isar_proof, |
50 max_new_mono_instances, type_enc, strict, lam_trans, |
51 isar_shrink_factor, preplay_timeout, ...} : params) |
51 isar_proof, isar_shrink_factor, preplay_timeout, ...} : params) |
52 silent (prover : prover) timeout i n state facts = |
52 silent (prover : prover) timeout i n state facts = |
53 let |
53 let |
54 val _ = |
54 val _ = |
55 print silent (fn () => |
55 print silent (fn () => |
56 "Testing " ^ n_facts (map fst facts) ^ |
56 "Testing " ^ n_facts (map fst facts) ^ |
59 val {goal, ...} = Proof.goal state |
59 val {goal, ...} = Proof.goal state |
60 val facts = |
60 val facts = |
61 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
61 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
62 val params = |
62 val params = |
63 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
63 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
64 provers = provers, type_enc = type_enc, sound = true, |
64 provers = provers, type_enc = type_enc, strict = strict, |
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), |
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), |
66 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, |
66 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, |
67 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
67 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
68 isar_shrink_factor = isar_shrink_factor, slice = false, |
68 isar_shrink_factor = isar_shrink_factor, slice = false, |
69 minimize = SOME false, timeout = timeout, |
69 minimize = SOME false, timeout = timeout, |