41 else |
41 else |
42 "") |
42 "") |
43 end |
43 end |
44 |
44 |
45 fun test_theorems ({debug, verbose, overlord, atps, full_types, |
45 fun test_theorems ({debug, verbose, overlord, atps, full_types, |
46 relevance_threshold, relevance_convergence, theory_relevant, |
46 relevance_threshold, relevance_convergence, |
47 defs_relevant, isar_proof, isar_shrink_factor, |
47 defs_relevant, isar_proof, isar_shrink_factor, ...} |
48 ...} : params) |
48 : params) |
49 (prover : prover) explicit_apply timeout subgoal state |
49 (prover : prover) explicit_apply timeout subgoal state |
50 name_thms_pairs = |
50 name_thms_pairs = |
51 let |
51 let |
52 val _ = |
52 val _ = |
53 priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") |
53 priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") |
54 val params = |
54 val params = |
55 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
55 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
56 full_types = full_types, explicit_apply = explicit_apply, |
56 full_types = full_types, explicit_apply = explicit_apply, |
57 relevance_threshold = relevance_threshold, |
57 relevance_threshold = relevance_threshold, |
58 relevance_convergence = relevance_convergence, |
58 relevance_convergence = relevance_convergence, |
59 theory_relevant = theory_relevant, defs_relevant = defs_relevant, |
59 max_relevant_per_iter = NONE, theory_relevant = NONE, |
60 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
60 defs_relevant = defs_relevant, isar_proof = isar_proof, |
61 timeout = timeout, minimize_timeout = timeout} |
61 isar_shrink_factor = isar_shrink_factor, timeout = timeout, |
|
62 minimize_timeout = timeout} |
62 val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
63 val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
63 val {context = ctxt, facts, goal} = Proof.goal state |
64 val {context = ctxt, facts, goal} = Proof.goal state |
64 val problem = |
65 val problem = |
65 {subgoal = subgoal, goal = (ctxt, (facts, goal)), |
66 {subgoal = subgoal, goal = (ctxt, (facts, goal)), |
66 relevance_override = {add = [], del = [], only = false}, |
67 relevance_override = {add = [], del = [], only = false}, |
96 timeout. *) |
97 timeout. *) |
97 val fudge_msecs = 250 |
98 val fudge_msecs = 250 |
98 |
99 |
99 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." |
100 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." |
100 | minimize_theorems |
101 | minimize_theorems |
101 (params as {debug, verbose, overlord, atps as atp :: _, full_types, |
102 (params as {debug, atps = atp :: _, full_types, isar_proof, |
102 relevance_threshold, relevance_convergence, theory_relevant, |
103 isar_shrink_factor, minimize_timeout, ...}) |
103 defs_relevant, isar_proof, isar_shrink_factor, |
|
104 minimize_timeout, ...}) |
|
105 i n state name_thms_pairs = |
104 i n state name_thms_pairs = |
106 let |
105 let |
107 val thy = Proof.theory_of state |
106 val thy = Proof.theory_of state |
108 val prover = get_prover_fun thy atp |
107 val prover = get_prover_fun thy atp |
109 val msecs = Time.toMilliseconds minimize_timeout |
108 val msecs = Time.toMilliseconds minimize_timeout |