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, isar_proof, |
50 max_new_mono_instances, type_enc, lam_trans, isar_proof, |
51 isar_shrink_factor, preplay_timeout, ...} : params) |
51 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 () => |
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, sound = true, |
65 relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), |
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), |
66 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, slicing = false, |
68 isar_shrink_factor = isar_shrink_factor, slicing = false, |
69 timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} |
69 timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} |
70 val problem = |
70 val problem = |
71 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
71 {state = state, goal = goal, subgoal = i, subgoal_count = n, |