62 (if blocking then "." |
62 (if blocking then "." |
63 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
63 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
64 |
64 |
65 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, |
65 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, |
66 timeout, expect, ...}) |
66 timeout, expect, ...}) |
67 mode minimize_command only {state, goal, subgoal, subgoal_count, facts} |
67 mode minimize_command only learn |
68 name = |
68 {state, goal, subgoal, subgoal_count, facts} name = |
69 let |
69 let |
70 val ctxt = Proof.context_of state |
70 val ctxt = Proof.context_of state |
71 val hard_timeout = Time.+ (timeout, timeout) |
71 val hard_timeout = Time.+ (timeout, timeout) |
72 val birth_time = Time.now () |
72 val birth_time = Time.now () |
73 val death_time = Time.+ (birth_time, hard_timeout) |
73 val death_time = Time.+ (birth_time, hard_timeout) |
91 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
91 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
92 |> commas |
92 |> commas |
93 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
93 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
94 " proof (of " ^ string_of_int (length facts) ^ "): ") "." |
94 " proof (of " ^ string_of_int (length facts) ^ "): ") "." |
95 |> Output.urgent_message |
95 |> Output.urgent_message |
96 fun learn prover = |
|
97 mash_learn_proof ctxt params prover (prop_of goal) |
|
98 (map untranslated_fact facts) |
|
99 fun really_go () = |
96 fun really_go () = |
100 problem |
97 problem |
101 |> get_minimizing_prover ctxt mode learn name params minimize_command |
98 |> get_minimizing_prover ctxt mode learn name params minimize_command |
102 |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} => |
99 |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} => |
103 print_used_facts used_facts |
100 print_used_facts used_facts |
186 val {facts = chained, goal, ...} = Proof.goal state |
183 val {facts = chained, goal, ...} = Proof.goal state |
187 val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
184 val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
188 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
185 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
189 val reserved = reserved_isar_keyword_table () |
186 val reserved = reserved_isar_keyword_table () |
190 val css = clasimpset_rule_table_of ctxt |
187 val css = clasimpset_rule_table_of ctxt |
191 val facts = |
188 val all_facts = |
192 nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts |
189 nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts |
193 concl_t |
190 concl_t |
194 val _ = () |> not blocking ? kill_provers |
191 val _ = () |> not blocking ? kill_provers |
195 val _ = case find_first (not o is_prover_supported ctxt) provers of |
192 val _ = case find_first (not o is_prover_supported ctxt) provers of |
196 SOME name => error ("No such prover: " ^ name ^ ".") |
193 SOME name => error ("No such prover: " ^ name ^ ".") |
206 val facts = facts ~~ (0 upto num_facts - 1) |
203 val facts = facts ~~ (0 upto num_facts - 1) |
207 |> map (translate num_facts) |
204 |> map (translate num_facts) |
208 val problem = |
205 val problem = |
209 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
206 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
210 facts = facts} |
207 facts = facts} |
211 val launch = launch_prover params mode minimize_command only |
208 fun learn prover = |
|
209 mash_learn_proof ctxt params prover (prop_of goal) all_facts |
|
210 val launch = launch_prover params mode minimize_command only learn |
212 in |
211 in |
213 if mode = Auto_Try orelse mode = Try then |
212 if mode = Auto_Try orelse mode = Try then |
214 (unknownN, state) |
213 (unknownN, state) |
215 |> fold (fn prover => fn accum as (outcome_code, _) => |
214 |> fold (fn prover => fn accum as (outcome_code, _) => |
216 if outcome_code = someN then accum |
215 if outcome_code = someN then accum |
230 | NONE => |
229 | NONE => |
231 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice) |
230 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice) |
232 provers |
231 provers |
233 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) |
232 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) |
234 in |
233 in |
235 facts |
234 all_facts |
236 |> (case is_appropriate_prop of |
235 |> (case is_appropriate_prop of |
237 SOME is_app => filter (is_app o prop_of o snd) |
236 SOME is_app => filter (is_app o prop_of o snd) |
238 | NONE => I) |
237 | NONE => I) |
239 |> relevant_facts ctxt params (hd provers) max_max_facts fact_override |
238 |> relevant_facts ctxt params (hd provers) max_max_facts fact_override |
240 hyp_ts concl_t |
239 hyp_ts concl_t |