1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
6 signature LUCAS_INTERPRETER =
8 datatype next_step_result =
9 Next_Step of Istate.T * Proof.context * Tactic.T
10 | Helpless | End_Program of Istate.T (*TODO ?needed when..*)* Tactic.T
11 val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
14 datatype input_tactic_result =
15 Safe_Step of Istate.T * Proof.context * Tactic.T
16 | Unsafe_Step of Istate.T * Proof.context * Tactic.T
17 | Not_Locatable (*TODO rm..*) of string
18 val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
19 -> Tactic.T -> input_tactic_result
21 datatype input_term_result = Found_Step of Calc.T | Not_Derivable (**)
22 val locate_input_term: Calc.T -> term -> input_term_result (**)
25 find_next_step calls do_next and is called by by_tactic;
26 by_tactic and do_next are mutually recursive via by_tactic..Apply_Method'
28 val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post
29 val do_next: Calc.T -> string * Calc.state_post
32 datatype expr_val1 = (* constructors for tests only *)
33 Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
34 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
37 val assoc2str: expr_val1 -> string
39 (* ---- for Doc/Lucas-Interpreter ------------------------------------------------------------- *)
40 val check_Seq_up: Istate.pstate -> term -> term
41 datatype expr_val = Accept_Tac of Tactic.T * Istate.pstate * Proof.context
42 | Reject_Tac | Term_Val of term
44 val scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val
45 val scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val
46 val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val
47 val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val
48 val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
50 val check_Let_up: Istate.pstate -> term -> term * term
51 val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Calc.state_post
53 val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
54 val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
55 val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
56 val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
58 val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
63 structure LI(**): LUCAS_INTERPRETER(**) =
71 (*** auxiliary functions ***)
73 fun check_Let_up ({path, ...}: pstate) prog =
74 case TermC.sub_at (drop_last path) prog of
75 Const (\<^const_name>\<open>Let\<close>,_) $ _ $ (Abs (i, T, body)) => (TermC.mk_Free (i, T), body)
76 | t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ UnparseC.term t ^ "\"")
77 fun check_Seq_up ({path, ...}: pstate) prog =
78 case TermC.sub_at (drop_last path) prog of
79 Const (\<^const_name>\<open>Tactical.Chain\<close>,_) $ _ $ e2=> e2
80 | t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ UnparseC.term t ^ "\"")
83 (*** determine a next tactic within a program ***)
85 datatype next_step_result = Next_Step of Istate.T * Proof.context * Tactic.T
86 | Helpless | End_Program of Istate.T * Tactic.T (*contains prog_result, without asms*)
88 (** scan to a Prog_Tac **)
90 datatype expr_val = (* "ExprVal" in the sense of denotational semantics *)
91 Reject_Tac (* tactic is found but NOT acknowledged, scan is continued *)
92 | Accept_Tac of (* tactic is found and acknowledged, scan is stalled *)
93 Tactic.T * (* Prog_Tac is applicable_in cstate *)
94 Istate.pstate * (* created by application of Tactic.T, for resuming execution *)
95 Proof.context (* created by application of Tactic.T *)
96 | Term_Val of (* Prog_Expr is found and evaluated, scan is continued *)
97 term; (* value of Prog_Expr, for updating environment *)
99 (* check if a prog_tac found in a program is applicable_in *)
100 fun check_tac ((pt, p), ctxt) ist (prog_tac, form_arg) =
102 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
105 Tactic.Subproblem _ => (*might involve problem refinement etc*)
107 val m' = snd (Sub_Problem.tac_from_prog pt prog_tac)
109 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
112 (case Solve_Step.check m (pt, p) of
114 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),
115 Tactic.insert_assumptions m' ctxt)
121 scan_dn, go_scan_up, scan_up scan for find_next_step.
122 (1) scan_dn is recursive descent depth first strictly from L to R;
123 (2) go_scan_up goes to the parent node and calls (3);
124 (3) scan_up resumes according to the interpreter-state.
125 Call of (2) means that there was an applicable Prog_Tac below = before.
127 fun scan_dn cc (ist as {act_arg, ...}) (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ e $ a) =
128 (case scan_dn cc (ist|> path_down_form ([L, R], a)) e of
129 Reject_Tac => Term_Val act_arg
130 | (*Accept_Tac*) goback => goback)
131 | scan_dn cc (ist as {act_arg, ...}) (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e) =
132 (case scan_dn cc (ist |> path_down [R]) e of
133 Reject_Tac => Term_Val act_arg
134 | (*Accept_Tac*) goback => goback)
136 | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
137 scan_dn cc (ist |> path_down_form ([L, R], a)) e
138 | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
139 scan_dn cc (ist |> path_down [R]) e
141 | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a) =
142 (case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
143 Term_Val v => scan_dn cc (ist |> path_down_form ([L, R], a) |> set_act v) e2
144 | (*Accept_Tac*) goback => goback)
145 | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2) =
146 (case scan_dn cc (ist |> path_down [L, R]) e1 of
147 Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
148 | (*Accept_Tac*) goback => goback)
150 | scan_dn cc ist (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))) =
151 (case scan_dn cc (ist |> path_down [L, R]) e of
152 Term_Val res => scan_dn cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
153 | (*Accept_Tac*) goback => goback)
155 | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ a) =
156 if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
157 then scan_dn cc (ist |> path_down_form ([L, R], a)) e
158 else Term_Val act_arg
159 | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
160 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
161 then scan_dn cc (ist |> path_down [R]) e
162 else Term_Val act_arg
164 |scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $e1 $ e2 $ a) =
165 (case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
166 Accept_Tac lme => Accept_Tac lme
167 | _ => scan_dn cc (ist |> path_down_form ([L, R], a)) e2)
168 | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $e1 $ e2) =
169 (case scan_dn cc (ist |> path_down [L, R]) e1 of
170 Accept_Tac lme => Accept_Tac lme
171 | _ => scan_dn cc (ist |> path_down [R]) e2)
173 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ c $ e1 $ e2) =
174 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
175 then scan_dn cc (ist |> path_down [L, R]) e1
176 else scan_dn cc (ist |> path_down [R]) e2
178 | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t (*fall-through*) =
179 if Tactical.contained_in t
180 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
182 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
183 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
184 | (Program.Tac prog_tac, form_arg) =>
185 (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |");
186 check_tac cc ist (prog_tac, form_arg))
188 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) =
189 if path = [R] (*root of the program body*) then
192 else raise ERROR "LItool.find_next_step without result"
193 else scan_up pcc (ist |> path_up) (go_up path sc)
194 (* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
195 and scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ $ _) = go_scan_up pcc ist
196 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _) = go_scan_up pcc ist
198 | scan_up (pcc as (_, cc)) ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ _) =
199 (case scan_dn cc (ist |> path_down [L, R]) e of
200 Accept_Tac ict => Accept_Tac ict
201 | Reject_Tac => go_scan_up pcc ist
202 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
203 | scan_up (pcc as (_, cc)) ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
204 (case scan_dn cc (ist |> path_down [R]) e of
205 Accept_Tac ict => Accept_Tac ict
206 | Reject_Tac => go_scan_up pcc ist
207 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
209 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
210 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _) = go_scan_up pcc ist
211 | scan_up (pcc as (sc, cc)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _) =
213 val e2 = check_Seq_up ist sc
215 case scan_dn cc (ist |> path_up_down [R]) e2 of
216 Accept_Tac ict => Accept_Tac ict
217 | Reject_Tac => go_scan_up pcc (ist |> path_up)
218 | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)
221 | scan_up (pcc as (sc, cc)) ist (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _) =
223 val (i, body) = check_Let_up ist sc
225 case scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body of
226 Accept_Tac ict => Accept_Tac ict
227 | Reject_Tac => go_scan_up pcc (ist |> path_up)
228 | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)
230 | scan_up pcc ist (Abs _(*2*)) = go_scan_up pcc ist
231 | scan_up pcc ist (Const (\<^const_name>\<open>Let\<close>(*3*), _) $ _ $ (Abs _)) = go_scan_up pcc ist
233 | scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
234 (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ _) =
235 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
237 case scan_dn cc (ist |> path_down [L, R]) e of
238 Accept_Tac ict => Accept_Tac ict
239 | Reject_Tac => go_scan_up pcc ist
240 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)
242 go_scan_up pcc (ist (*|> set_found*))
243 | scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
244 (Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
245 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
247 case scan_dn cc (ist |> path_down [R]) e of
248 Accept_Tac ict => Accept_Tac ict
249 | Reject_Tac => go_scan_up pcc ist
250 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)
254 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
255 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up pcc ist
256 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*3*), _) $ _ ) = go_scan_up pcc ist
258 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
260 | scan_up _ _ t = raise ERROR ("scan_up not impl for " ^ UnparseC.term t)
262 (* scan program until an applicable tactic is found *)
263 fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
265 scan_dn cc (trans_scan_dn ist) (Program.body_of prog)
266 else go_scan_up (prog, cc) (trans_scan_up ist)
267 | scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern";
269 (* find the next applicable Prog_Tac in a prog *)
270 fun find_next_step (Rule.Prog prog) (ptp as (pt, pos as (p, _))) (Pstate ist) ctxt =
271 (case scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) of
272 Accept_Tac (tac, ist, ctxt) =>
273 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
274 | Term_Val prog_result =>
275 (case LItool.parent_node pt pos of
278 val (_, pblID, _) = get_obj g_spec pt p';
280 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
282 | _ => End_Program (Pstate ist, Tactic.End_Detail' (TermC.empty,[])))
283 | Reject_Tac => Helpless)
284 | find_next_step _ _ ist _ =
285 raise ERROR ("find_next_step: not impl for " ^ Istate.string_of ist);
288 (*** locate an input tactic within a program ***)
290 datatype input_tactic_result =
291 Safe_Step of Istate.T * Proof.context * Tactic.T
292 | Unsafe_Step of Istate.T * Proof.context * Tactic.T
293 | Not_Locatable of string
295 (*all functions ending with "1" are supposed to be replaced by those without "1"*)
296 datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
297 Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
298 Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac*)
299 | Accept_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
300 Istate.pstate * (* the current state, returned for resuming execution *)
301 Proof.context * (* updated according to evaluation of Prog_Tac *)
302 Tactic.T (* Prog_Tac is associated to Tactic.input *)
303 | Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
304 term (* value of Prog_Expr, for updating environment *)
306 fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
307 | assoc2str (Term_Val1 _) = "Term_Val1"
308 | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
312 (** check a Prog_Tac: is it associated to Tactic ? **)
314 fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =
315 case LItool.associate pt ctxt (tac, prog_tac) of
316 LItool.Associated (m, v', ctxt)
317 => Accept_Tac1 (ist |> set_subst_true (form_arg, v') |> set_found, ctxt, m)
318 | LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
319 => Accept_Tac1 (ist |> set_subst_false (form_arg, v') |> set_found, ctxt, m)
320 | LItool.Not_Associated =>
321 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
322 AssOnly => Term_Val1 act_arg
324 case Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) of
325 Applicable.Yes m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
326 | Applicable.No _ => Term_Val1 act_arg)
328 (** scan to a Prog_Tac **)
330 (* scan is strictly first L, then R; tacticals have 2 args at maximum *)
331 fun scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ e $ a) =
332 (case scan_dn1 cct (ist |> path_down_form ([L, R], a)) e of goback => goback)
333 | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e) =
334 (case scan_dn1 cct (ist |> path_down [R]) e of goback => goback)
336 | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
337 scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
338 | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
339 scan_dn1 cct (ist |> path_down [R]) e
341 | scan_dn1 (cct as (cstate, _, _)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a) =
342 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
343 Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
344 | Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist
345 |> path_down_form ([L, R], a) |> trans_env_act ist') e2
347 | scan_dn1 (cct as (cstate, _, _)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2) =
348 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
349 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
350 | Reject_Tac1 (ist', ctxt', tac') =>
351 scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
354 | scan_dn1 cct ist (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))) =
355 (case scan_dn1 cct (ist |> path_down [L, R]) e of
356 Reject_Tac1 (ist', _, _) =>
357 scan_dn1 cct (ist' |> path_down [R, D] |> upd_env (TermC.mk_Free (id, T)) |> trans_ass ist) b
359 scan_dn1 cct (ist |> path_down [R, D] |> upd_env'' (TermC.mk_Free (id, T), v)) b
362 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
363 (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ a) =
364 if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
365 then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
366 else Term_Val1 act_arg
367 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
368 (Const (\<^const_name>\<open>Tactical.While\<close>(*2*),_) $ c $ e) =
369 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
370 then scan_dn1 cct (ist |> path_down [R]) e
371 else Term_Val1 act_arg
373 | scan_dn1 cct (ist as {or = ORundef, ...}) (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $e1 $ e2 $ a) =
374 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
376 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
378 (case scan_dn1 cct (ist |> path_down [L, L, R] |> upd_env'' (a, v) |> set_or AssGen) e1 of
380 scan_dn1 cct (ist |> path_down [L, R] |> upd_env'' (a, v) |> set_or AssGen) e2
383 | Reject_Tac1 _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return Reject_Tac1")
385 | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $e1 $ e2) =
386 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
387 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
390 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>, _) $ c $ e1 $ e2) =
391 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
392 then scan_dn1 cct (ist |> path_down [L, R]) e1
393 else scan_dn1 cct (ist |> path_down [R]) e2
395 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) t =
396 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
398 case LItool.check_leaf "locate" ctxt eval (get_subst ist) t of
399 (Program.Expr _, form_arg) =>
400 Term_Val1 (Rewrite.eval_prog_expr ctxt eval
401 (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
402 | (Program.Tac prog_tac, form_arg) =>
403 check_tac1 cct ist (prog_tac, form_arg)
405 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
406 if 1 < length path then
407 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog)
408 else Term_Val1 act_arg
409 (* scan is strictly to R, because at L there was a expr_val *)
410 and scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
411 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _) = go_scan_up1 pcct ist
413 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
414 (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
415 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
416 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
418 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
419 (case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
420 Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
421 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
424 (*all has been done in (*2*) below*)
425 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
426 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
427 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _ ) =
429 val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
431 case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 of
432 Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
433 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
437 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _) =
439 val (i, body) = check_Let_up ist prog
440 in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body of
441 Accept_Tac1 iss => Accept_Tac1 iss
442 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
443 | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
445 | scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist
446 | scan_up1 pcct ist (Const (\<^const_name>\<open>Let\<close>(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
448 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
449 (t as Const (\<^const_name>\<open>Tactical.While\<close>(*1*),_) $ c $ e $ a) =
450 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update' a (get_act_env ist)) c)
452 case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
453 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
455 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
457 else go_scan_up1 pcct (ist |> set_form a)
458 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
459 (t as Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
460 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
462 case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
463 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
464 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
466 else go_scan_up1 pcct ist
468 | scan_up1 pcct ist (Const (\<^const_name>\<open>If\<close>, _) $ _ $ _ $ _) = go_scan_up1 pcct ist
470 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
471 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
472 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
474 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.If\<close>,_) $ _ $ _ $ _) = go_scan_up1 pcct ist
476 | scan_up1 _ _ t = raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term t)
478 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Pstate (ist as {path, ...})) =
479 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_step IN solve*)p
480 then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
481 else go_scan_up1 (prog, cctt) ist
482 | scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
484 (*locate an input tactic within a program*)
485 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
486 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
487 Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
489 Safe_Step (Pstate ist, ctxt, tac')
490 else Unsafe_Step (Pstate ist, ctxt, tac')
491 | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
492 | err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err))
493 | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
496 (*** locate an input formula within a program ***)
498 datatype input_term_result = Found_Step of Calc.T | Not_Derivable
500 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
502 val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
503 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
504 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
505 val {ppc, ...} = MethodC.from_store ctxt mI;
506 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
507 val srls = LItool.get_simplifier (pt, pos)
508 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
509 (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
510 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
511 val ini = LItool.implicit_take prog env;
512 val pos = start_new_level pos
516 let (* implicit Take *)
517 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
518 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos)
520 ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
524 val (tac', ist', ctxt') =
525 case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
526 Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
527 | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \<rightarrow> " ^ strs2str' mI)
531 let (* explicit Take *)
532 val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
533 val (pos, c, _, pt) = Solve_Step.add show_add (ist', ctxt') (pt, pos)
535 ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
537 | add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
539 val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
540 val (pos, c, _, pt) = Solve_Step.add add (ist', ctxt') (pt, pos)
542 ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
545 raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
548 | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
550 val parent_pos = par_pblobj pt p
551 val ctxt = Ctree.get_ctxt pt pos
552 val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
554 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
555 Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
556 | End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
557 | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
559 if parent_pos = [] then
561 val tac = Tactic.Check_Postcond' (pI, prog_res)
562 val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
563 val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (is, sub_ctxt) (pt, (parent_pos, Res))
565 ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
568 let (*resume program of parent PblObj, transfer result of Subproblem-program*)
569 val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
570 (Pstate i, c) => (i, c)
571 | _ => raise ERROR "LI.by_tactic Check_Postcond': uncovered case get_loc"
572 val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
573 val tac = Tactic.Check_Postcond' (pI, prog_res')
574 val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
575 val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (ist', ctxt') (pt, (parent_pos, Res))
577 ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
580 | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
581 | by_tactic tac_ ic (pt, pos) =
583 val pos = next_in_prog' pos
584 val (pos', c, _, pt) = Solve_Step.add_general tac_ ic (pt, pos);
586 ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, ic))], c, (pt, pos')))
588 (*find_next_step from program, by_tactic will update Ctree*)
589 and do_next (ptp as (pt, pos as (p, p_))) =
590 if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) then
591 ("helpless", ([], [], (pt, (p, p_))))
594 val thy' = get_obj g_domID pt (par_pblobj pt p);
595 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
597 case find_next_step sc (pt, pos) ist ctxt of
598 Next_Step (ist, ctxt, tac) =>
599 by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
600 | End_Program (ist, tac) => (*TODO RM ..*)
602 Tactic.End_Detail' res =>
603 ("ok", ([(Tactic.End_Detail,
604 Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
605 | _ => (*.. RM*) by_tactic tac (ist, ctxt) ptp
607 | Helpless => ("helpless", Calc.state_empty_post)
611 compare inform with ctree.form at current pos by nrls;
612 if found, embed the derivation generated during comparison
613 if not, let the mat-engine compute the next Calc.result
615 TODO: find code in common with complete_solve
617 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
619 val fo = Calc.current_formula ptp
620 val ctxt = Ctree.get_ctxt pt pos
621 val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
622 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
623 val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
628 val tacis' = map (State_Steps.make_single rew_ord erls) der;
629 val (c', ptp) = Derive.embed tacis' ptp;
630 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
632 if pos = ([], Pos.Res) (*TODO: we should stop earlier with trying subproblems *)
633 then ("no derivation found", (tacis, c, ptp): Calc.state_post)
636 val msg_cs' as (_, (tacis, c', ptp)) = (*LI.*)do_next ptp; (*<---------------------*)
637 val (_, (tacis, c'', ptp)) = case tacis of
638 ((Tactic.Subproblem _, _, _) :: _) =>
640 val ptp as (pt, pos as (p, _)) = Specify.do_all ptp (*<--------------------*)
641 val mI = Ctree.get_obj Ctree.g_metID pt p
642 val (ist, ctxt) = (Istate.empty, Ctree.get_ctxt pt pos)
644 by_tactic (Tactic.Apply_Method' (mI, NONE, ist, ctxt)) (ist, ctxt) ptp
647 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
650 (* Locate a step in a program, which has been determined by input of a term *)
651 fun locate_input_term (pt, pos) tm =
653 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
654 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
656 case compare_step ([], [], (pt, pos_pred)) tm of
657 ("no derivation found", _) => Not_Derivable
658 | ("ok", (_, _, cstate)) =>
660 | _ => raise ERROR "compare_step: uncovered case"