59 if name = metisN then Metis_Method (type_enc, lam_trans) |
59 if name = metisN then Metis_Method (type_enc, lam_trans) |
60 else if name = smtN then SMT2_Method |
60 else if name = smtN then SMT2_Method |
61 else raise Fail ("unknown proof_method: " ^ quote name) |
61 else raise Fail ("unknown proof_method: " ^ quote name) |
62 val used_facts = facts |> map fst |
62 val used_facts = facts |> map fst |
63 in |
63 in |
64 (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts |
64 (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout |
65 state subgoal meth [meth] of |
65 facts state subgoal meth [meth] of |
66 play as (_, Played time) => |
66 play as (_, Played time) => |
67 {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, |
67 {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, |
68 preplay = Lazy.value play, |
68 preplay = Lazy.value play, |
69 message = |
69 message = |
70 fn play => |
70 fn play => |
71 let |
71 let |
|
72 val ctxt = Proof.context_of state |
72 val (_, override_params) = extract_proof_method params meth |
73 val (_, override_params) = extract_proof_method params meth |
73 val one_line_params = |
74 val one_line_params = |
74 (play, proof_banner mode name, used_facts, minimize_command override_params name, |
75 (play, proof_banner mode name, used_facts, minimize_command override_params name, |
75 subgoal, subgoal_count) |
76 subgoal, subgoal_count) |
76 val num_chained = length (#facts (Proof.goal state)) |
77 val num_chained = length (#facts (Proof.goal state)) |
77 in |
78 in |
78 one_line_proof_text num_chained one_line_params |
79 one_line_proof_text ctxt num_chained one_line_params |
79 end, |
80 end, |
80 message_tail = ""} |
81 message_tail = ""} |
81 | play => |
82 | play => |
82 let |
83 let |
83 val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut) |
84 val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut) |