equal
deleted
inserted
replaced
17 |
17 |
18 type isar_preplay_data |
18 type isar_preplay_data |
19 |
19 |
20 val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome |
20 val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome |
21 val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context |
21 val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context |
22 val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step -> |
22 val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method -> |
23 play_outcome |
23 isar_step -> play_outcome |
24 val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step -> |
24 val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list -> |
25 (proof_method * play_outcome) list |
25 isar_step -> (proof_method * play_outcome) list |
26 val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> |
26 val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> |
27 isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit |
27 isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit |
28 val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome |
28 val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome |
29 val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> |
29 val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> |
30 play_outcome Lazy.lazy |
30 play_outcome Lazy.lazy |
124 |> subst_free subst |
124 |> subst_free subst |
125 |> Skip_Proof.make_thm thy |
125 |> Skip_Proof.make_thm thy |
126 end |
126 end |
127 |
127 |
128 (* may throw exceptions *) |
128 (* may throw exceptions *) |
129 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) = |
129 fun raw_preplay_step_for_method ctxt chained timeout meth |
|
130 (Prove (_, xs, _, t, subproofs, facts, _, _)) = |
130 let |
131 let |
131 val goal = |
132 val goal = |
132 (case xs of |
133 (case xs of |
133 [] => t |
134 [] => t |
134 | _ => |
135 | _ => |
148 end) |
149 end) |
149 |
150 |
150 val assmsp = |
151 val assmsp = |
151 resolve_fact_names ctxt facts |
152 resolve_fact_names ctxt facts |
152 |>> append (map (thm_of_proof ctxt) subproofs) |
153 |>> append (map (thm_of_proof ctxt) subproofs) |
|
154 |>> append chained |
153 |
155 |
154 fun prove () = |
156 fun prove () = |
155 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
157 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
156 HEADGOAL (tac_of_proof_method ctxt assmsp meth)) |
158 HEADGOAL (tac_of_proof_method ctxt assmsp meth)) |
157 handle ERROR msg => error ("Preplay error: " ^ msg) |
159 handle ERROR msg => error ("Preplay error: " ^ msg) |
160 in |
162 in |
161 if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); |
163 if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); |
162 play_outcome |
164 play_outcome |
163 end |
165 end |
164 |
166 |
165 fun preplay_isar_step_for_method ctxt timeout meth = |
167 fun preplay_isar_step_for_method ctxt chained timeout meth = |
166 try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed |
168 try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed |
167 |
169 |
168 val min_preplay_timeout = seconds 0.002 |
170 val min_preplay_timeout = seconds 0.002 |
169 |
171 |
170 fun preplay_isar_step ctxt timeout0 hopeless step = |
172 fun preplay_isar_step ctxt chained timeout0 hopeless step = |
171 let |
173 let |
172 fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step) |
174 fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step) |
173 fun get_time (_, Played time) = SOME time |
175 fun get_time (_, Played time) = SOME time |
174 | get_time _ = NONE |
176 | get_time _ = NONE |
175 |
177 |
176 val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless |
178 val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless |
177 in |
179 in |
192 |
194 |
193 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data |
195 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data |
194 (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = |
196 (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = |
195 let |
197 let |
196 fun lazy_preplay meth = |
198 fun lazy_preplay meth = |
197 Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step) |
199 Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step) |
198 val meths_outcomes = meths_outcomes0 |
200 val meths_outcomes = meths_outcomes0 |
199 |> map (apsnd Lazy.value) |
201 |> map (apsnd Lazy.value) |
200 |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths |
202 |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths |
201 in |
203 in |
202 preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) |
204 preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) |