68 (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
68 (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
69 else |
69 else |
70 let |
70 let |
71 val ctxt = Proof.context_of state |
71 val ctxt = Proof.context_of state |
72 |
72 |
73 val fact_names = map fst used_facts |
73 val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst |
74 val {facts = chained, goal, ...} = Proof.goal state |
74 val {facts = chained, goal, ...} = Proof.goal state |
75 val goal_t = Logic.get_goal (Thm.prop_of goal) i |
75 val goal_t = Logic.get_goal (Thm.prop_of goal) i |
76 |
76 |
77 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
77 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
78 | try_methss ress [] = |
78 | try_methss ress [] = |
91 subproofs = [], |
91 subproofs = [], |
92 facts = ([], fact_names), |
92 facts = ([], fact_names), |
93 proof_methods = meths, |
93 proof_methods = meths, |
94 comment = ""} |
94 comment = ""} |
95 in |
95 in |
96 (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of |
96 (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of |
97 (res as (meth, Played time)) :: _ => |
97 (res as (meth, Played time)) :: _ => |
98 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
98 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
99 if not minimize orelse is_metis_method meth then |
99 if not minimize orelse is_metis_method meth then |
100 (used_facts, res) |
100 (used_facts, res) |
101 else |
101 else |
111 end |
111 end |
112 in |
112 in |
113 try_methss [] methss |
113 try_methss [] methss |
114 end) |
114 end) |
115 |> (fn (used_facts, (meth, play)) => |
115 |> (fn (used_facts, (meth, play)) => |
116 (used_facts |> not (proof_method_distinguishes_chained_and_direct meth) |
116 (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) |
117 ? filter_out (fn (_, (sc, _)) => sc = Chained), |
|
118 (meth, play))) |
|
119 |
117 |
120 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, |
118 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, |
121 expect, induction_rules, ...}) mode writeln_result only learn |
119 expect, induction_rules, ...}) mode writeln_result only learn |
122 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = |
120 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = |
123 let |
121 let |
124 val ctxt = Proof.context_of state |
122 val ctxt = Proof.context_of state |
125 |
123 |
126 val hard_timeout = Time.scale 5.0 timeout |
124 val hard_timeout = Time.scale 5.0 timeout |
127 val _ = spying spy (fn () => (state, subgoal, name, "Launched")); |
125 val _ = spying spy (fn () => (state, subgoal, name, "Launched")) |
128 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
126 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
129 val num_facts = length facts |> not only ? Integer.min max_facts |
127 val num_facts = length facts |> not only ? Integer.min max_facts |
130 val induction_rules = |
128 val induction_rules = |
131 the_default (if is_ho_atp ctxt name then Include else Exclude) induction_rules |
129 the_default (if is_ho_atp ctxt name then Include else Exclude) induction_rules |
132 |
130 |