52 fn accum as SOME _ => accum |
52 fn accum as SOME _ => accum |
53 | NONE => if member (op =) codes candidate then SOME candidate else NONE) |
53 | NONE => if member (op =) codes candidate then SOME candidate else NONE) |
54 ordered_outcome_codes |
54 ordered_outcome_codes |
55 |> the_default unknownN |
55 |> the_default unknownN |
56 |
56 |
57 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = |
57 fun prover_description verbose name num_facts = |
58 (quote name, |
58 (quote name, |
59 (if verbose then |
59 if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "") |
60 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
|
61 else |
|
62 "") ^ |
|
63 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
|
64 (if blocking then "." |
|
65 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
|
66 |
60 |
67 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode |
61 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode |
68 output_result minimize_command only learn |
62 output_result minimize_command only learn |
69 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
63 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
70 let |
64 let |
74 val _ = spying spy (fn () => (state, subgoal, name, "Launched")); |
68 val _ = spying spy (fn () => (state, subgoal, name, "Launched")); |
75 val birth_time = Time.now () |
69 val birth_time = Time.now () |
76 val death_time = Time.+ (birth_time, hard_timeout) |
70 val death_time = Time.+ (birth_time, hard_timeout) |
77 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
71 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
78 val num_facts = length facts |> not only ? Integer.min max_facts |
72 val num_facts = length facts |> not only ? Integer.min max_facts |
79 |
|
80 fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal |
|
81 |
73 |
82 val problem = |
74 val problem = |
83 {comment = comment, state = state, goal = goal, subgoal = subgoal, |
75 {comment = comment, state = state, goal = goal, subgoal = subgoal, |
84 subgoal_count = subgoal_count, |
76 subgoal_count = subgoal_count, |
85 factss = factss |
77 factss = factss |
193 outcome |
185 outcome |
194 |> Async_Manager.break_into_chunks |
186 |> Async_Manager.break_into_chunks |
195 |> List.app Output.urgent_message |
187 |> List.app Output.urgent_message |
196 in (outcome_code, state) end |
188 in (outcome_code, state) end |
197 else |
189 else |
198 (Async_Manager.thread SledgehammerN birth_time death_time (desc ()) |
190 (Async_Manager.thread SledgehammerN birth_time death_time |
|
191 (prover_description verbose name num_facts) |
199 ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go); |
192 ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go); |
200 (unknownN, state)) |
193 (unknownN, state)) |
201 end |
194 end |
202 |
195 |
203 val auto_try_max_facts_divisor = 2 (* FUDGE *) |
196 val auto_try_max_facts_divisor = 2 (* FUDGE *) |