1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
6 signature LUCAS_INTERPRETER =
8 datatype input_tactic_result =
9 Safe_Step of Istate.T * Proof.context * Tactic.T
10 | Unsafe_Step of Istate.T * Proof.context * Tactic.T
11 | Not_Locatable of string
12 val locate_input_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context -> Tactic.T
13 -> input_tactic_result
15 datatype next_tactic_result =
16 Next_Step of Istate.T * Proof.context * Tactic.T
17 | Helpless | End_Program of Istate.T * Tactic.T
18 val find_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
21 (*TODO input_formula_result = Found_Step of Ctree.state | Not_Derivable *)
22 datatype input_formula_result =
23 Found_Step of Ctree.state * Istate.T * Proof.context
24 | Not_Derivable of Chead.calcstate'
25 (*TODOlocate_input_formula: Ctree.state -> term -> input_formula_result *)
26 val locate_input_formula: Rule.program -> Ctree.state -> Istate.T -> Proof.context -> term
27 -> input_formula_result
30 find_next_tactic calls do_next and is called by by_tactic;
31 by_tactic and do_next are mutually recursive via by_tactic Apply_Method'
33 val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> string * Chead.calcstate'
34 val do_next: Ctree.state -> string * Chead.calcstate'
36 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
38 Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
39 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
41 val assoc2str: expr_val1 -> string
42 (* ---- for paper on Lucas-Interpretation ------------------------------------------- --------- *)
43 val at_location: TermC.path -> term -> term
44 val check_Seq_up: Istate.pstate -> term -> term
45 datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate * Proof.context
46 | Reject_Tac2 | Term_Val2 of term
48 val scan_dn2: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val2
49 val scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val2
50 val go_scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val2
51 val scan_to_tactic2: term * (Ctree.state * Proof.context) -> Istate.T -> expr_val2
52 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
53 val go_up: TermC.path -> term -> term
54 val check_Let_up: Istate.pstate -> term -> term * term
55 val compare_step: Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
57 val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
58 val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
59 val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
60 val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
62 val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
63 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
67 structure LucinNEW(**): LUCAS_INTERPRETER(**) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)
75 (*** auxiliary functions ***)
77 (*go to a location in a program and fetch the resective sub-term*)
78 fun at_location [] t = t
79 | at_location (D :: p) (Abs(_, _, body)) = at_location (p : TermC.path) body
80 | at_location (L :: p) (t1 $ _) = at_location p t1
81 | at_location (R :: p) (_ $ t2) = at_location p t2
82 | at_location l _ = error ("at_location: no " ^ TermC.path2str l);
84 if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)
86 fun check_Let_up ({path, ...}: pstate) prog =
87 case at_location (drop_last path) prog of
88 Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (TermC.mk_Free (i, T), body)
89 | t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ Rule.term2str t ^ "\"")
90 fun check_Seq_up ({path, ...}: pstate) prog =
91 case at_location (drop_last path) prog of
92 Const ("Tactical.Chain",_) $ _ $ e2=> e2
93 | t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ Rule.term2str t ^ "\"")
96 (*** locate an input tactic within a program ***)
98 datatype input_tactic_result =
99 Safe_Step of Istate.T * Proof.context * Tactic.T
100 | Unsafe_Step of Istate.T * Proof.context * Tactic.T
101 | Not_Locatable of string
103 datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
104 Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
105 Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac2*)
106 | Accept_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
107 Istate.pstate * (* the current state, returned for resuming execution *)
108 Proof.context * (* updated according to evaluation of Prog_Tac *)
109 Tactic.T (* Prog_Tac is associated to Tactic.input *)
110 | Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
111 term (* value of Prog_Expr, for updating environment *)
112 fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
113 | assoc2str (Term_Val1 _) = "Term_Val1"
114 | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
117 (** interpret a Prog_Tac: is it associated to Tactic ? **)
119 fun interpret_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (form_arg, prog_tac) =
120 case Lucin.associate pt ctxt (tac, prog_tac) of
121 (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
122 Lucin.Ass (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_true (form_arg, v'), ctxt, m)
123 | Lucin.Ass_Weak (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_false (form_arg, v'), ctxt, m)
126 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
127 AssOnly => Term_Val1 act_arg
129 case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
130 Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
131 | Applicable.Notappl _ => Term_Val1 act_arg)
133 (** scan to a Prog_Tac **)
135 fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =
136 (case scan_dn1 cct (ist |> path_down_form ([L, R], a)) e of goback => goback)
137 | scan_dn1 cct ist (Const ("Tactical.Try"(*2*), _) $ e) =
138 (case scan_dn1 cct (ist |> path_down [R]) e of goback => goback)
140 | scan_dn1 cct ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
141 scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
142 | scan_dn1 cct ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
143 scan_dn1 cct (ist |> path_down [R]) e
145 | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
146 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
147 Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
148 | Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist
149 |> path_down_form ([L, R], a) |> trans_env_act ist') e2
151 | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $e1 $ e2) =
152 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
153 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
154 | Reject_Tac1 (ist', ctxt', tac') =>
155 scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
158 | scan_dn1 cct ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =
159 (case scan_dn1 cct (ist |> path_down [L, R]) e of
160 Reject_Tac1 (ist', _, _) =>
161 scan_dn1 cct (ist' |> path_down [R, D] |> upd_env (TermC.mk_Free (id, T)) |> trans_ass ist) b
163 scan_dn1 cct (ist |> path_down [R, D] |> upd_env'' (TermC.mk_Free (id, T), v)) b
166 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
167 (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
168 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval
169 (subst_atomic (ist |> get_act_env |> Env.update' a) c)
170 then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
171 else Term_Val1 act_arg
172 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
173 (Const ("Tactical.While"(*2*),_) $ c $ e) =
174 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
175 then scan_dn1 cct (ist |> path_down [R]) e
176 else Term_Val1 act_arg
178 | scan_dn1 cct (ist as {or = ORundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
179 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
181 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
183 (case scan_dn1 cct (ist |> path_down [L, L, R] |> upd_env'' (a, v) |> set_or AssGen) e1 of
185 scan_dn1 cct (ist |> path_down [L, R] |> upd_env'' (a, v) |> set_or AssGen) e2
188 | Reject_Tac1 _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return Reject_Tac1")
190 | scan_dn1 cct ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
191 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
192 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
195 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
196 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
197 then scan_dn1 cct (ist |> path_down [L, R]) e1
198 else scan_dn1 cct (ist |> path_down [R]) e2
200 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) t =
201 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
203 case Lucin.interpret_leaf "locate" ctxt eval (get_subst ist) t of
204 (Program.Expr _, form_arg) =>
205 Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
206 (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
207 | (Program.Tac prog_tac, form_arg) =>
208 interpret_tac1 cct ist (form_arg, prog_tac)
210 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
212 then scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
213 else Term_Val1 act_arg
214 and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
215 | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
217 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
218 (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
219 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
220 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
222 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
223 (case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
224 Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
225 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
228 (*all has been done in (*2*) below*)
229 | scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
230 | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
231 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =
233 val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
235 case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 of
236 Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
237 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
241 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =
243 val (i, body) = check_Let_up ist prog
244 in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body of
245 Accept_Tac1 iss => Accept_Tac1 iss
246 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
247 | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
249 | scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist
250 | scan_up1 pcct ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
252 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
253 (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
254 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update' a (get_act_env ist)) c)
256 case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
257 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
259 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
261 else go_scan_up1 pcct (ist |> set_form a)
262 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
263 (t as Const ("Tactical.While"(*2*), _) $ c $ e) =
264 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
266 case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
267 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
268 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
270 else go_scan_up1 pcct ist
272 | scan_up1 pcct ist (Const ("If", _) $ _ $ _ $ _) = go_scan_up1 pcct ist
274 | scan_up1 pcct ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
275 | scan_up1 pcct ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
276 | scan_up1 pcct ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
278 | scan_up1 pcct ist (Const ("Tactical.If",_) $ _ $ _ $ _) = go_scan_up1 pcct ist
280 | scan_up1 _ _ t = error ("scan_up1 not impl for t= " ^ Rule.term2str t)
282 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
283 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_tactic IN solve*)p
284 then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
285 else go_scan_up1 (prog, cctt) ist
286 | scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
288 (*locate an input tactic within a program*)
289 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
290 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
291 Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
293 then Safe_Step (Istate.Pstate ist, ctxt, tac')
294 else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
295 | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
296 | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
297 | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
300 (*** determine a next tactic by executing the program ***)
302 datatype next_tactic_result = Next_Step of Istate.T * Proof.context * Tactic.T
303 | Helpless | End_Program of Istate.T * Tactic.T (*contains prog_result, without asms*)
305 (** scan to a Prog_Tac **)
307 datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics *)
308 Reject_Tac2 (* tactic is found but NOT acknowledged, scan is continued *)
309 | Accept_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
310 Tactic.T * (* Prog_Tac is applicable_in cstate *)
311 Istate.pstate * (* created by application of Tactic.T, for resuming execution *)
312 Proof.context (* created by application of Tactic.T *)
313 | Term_Val2 of (* Prog_Expr is found and evaluated, scan is continued *)
314 term; (* value of Prog_Expr, for updating environment *)
317 scan_dn2, go_scan_up2, scan_up2 scan for find_next_tactic.
318 (1) scan_dn2 is recursive descent;
319 (2) go_scan_up2 goes to the parent node and calls (3);
320 (3) scan_up2 resumes according to the interpreter-state.
321 Call of (2) means that there was an applicable Prog_Tac below
323 fun scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
324 (case scan_dn2 cc (ist|> path_down_form ([L, R], a)) e of
325 Reject_Tac2 => Term_Val2 act_arg
326 | (*Accept_Tac2*) goback => goback)
327 | scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
328 (case scan_dn2 cc (ist |> path_down [R]) e of
329 Reject_Tac2 => Term_Val2 act_arg
330 | (*Accept_Tac2*) goback => goback)
332 | scan_dn2 cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
333 scan_dn2 cc (ist |> path_down_form ([L, R], a)) e
334 | scan_dn2 cc ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
335 scan_dn2 cc (ist |> path_down [R]) e
337 | scan_dn2 cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
338 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
339 Term_Val2 v => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act v) e2 (*UPD*)
340 | (*Accept_Tac2*) goback => goback)
341 | scan_dn2 cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
342 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
343 Term_Val2 v => scan_dn2 cc (ist |> path_down [R] |> set_act v) e2
344 | (*Accept_Tac2*) goback => goback)
346 | scan_dn2 cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
347 (case scan_dn2 cc (ist |> path_down [L, R]) e of
348 Term_Val2 res => scan_dn2 cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
349 | (*Accept_Tac2*) goback => goback)
351 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
352 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
353 then scan_dn2 cc (ist |> path_down_form ([L, R], a)) e
354 else Term_Val2 act_arg
355 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
356 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
357 then scan_dn2 cc (ist |> path_down [R]) e
358 else Term_Val2 act_arg
360 |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
361 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
362 Accept_Tac2 lme => Accept_Tac2 lme
363 | _ => scan_dn2 cc (ist |> path_down_form ([L, R], a)) e2)
364 | scan_dn2 cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
365 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
366 Accept_Tac2 lme => Accept_Tac2 lme
367 | _ => scan_dn2 cc (ist |> path_down [R]) e2)
369 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
370 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
371 then scan_dn2 cc (ist |> path_down [L, R]) e1
372 else scan_dn2 cc (ist |> path_down [R]) e2
374 | scan_dn2 ((pt, p), ctxt) (ist as {eval, ...}) t =
375 if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])
377 case Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t of
378 (Program.Expr s, _) => Term_Val2 s
379 | (Program.Tac stac, a') =>
381 val (m, m') = Lucin.stac2tac_ pt (Proof_Context.theory_of ctxt) stac
383 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
384 Tactic.Subproblem _ =>
385 Accept_Tac2 (m', ist |> set_subst_reset (a', Tactic.result m'), ctxt)
387 (case Applicable.applicable_in p pt m of
388 Applicable.Appl m' => Accept_Tac2 (m',
389 ist |> set_subst_reset (a', Tactic.result m'), Tactic.insert_assumptions m' ctxt)
393 (*makes Reject_Tac2 to Term_Val2*)
394 fun go_scan_up2 (pcc as (sc, _)) (ist as {path, act_arg, finish, ...}) =
397 scan_up2 pcc (ist |> path_up) (go_up path sc)
398 else (*interpreted to end*)
399 if finish = Skip_ then Term_Val2 act_arg else Reject_Tac2
400 and scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
401 | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
403 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
404 (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
405 Accept_Tac2 lr => Accept_Tac2 lr
406 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
407 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
408 (*no appy_: there was already a stac below*)
409 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
410 (case scan_dn2 cc (ist |> path_down [R]) e of
411 Accept_Tac2 lr => Accept_Tac2 lr
412 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
413 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
415 | scan_up2 pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
416 | scan_up2 pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist
417 | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("Tactical.Chain"(*3*), _) $ _) =
419 then go_scan_up2 pcc (ist |> path_up)
422 val e2 = check_Seq_up ist sc
424 case scan_dn2 cc (ist |> path_up_down [R]) e2 of
425 Accept_Tac2 lr => Accept_Tac2 lr
426 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
427 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
430 | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
432 then go_scan_up2 pcc (ist |> path_up)
435 val (i, body) = check_Let_up ist sc
437 case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
438 Accept_Tac2 lre => Accept_Tac2 lre
439 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
440 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
442 | scan_up2 pcc ist (Abs _(*2*)) = go_scan_up2 pcc ist
443 | scan_up2 pcc ist (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) =
446 (*no appy_: never causes Reject_Tac2 -> Helpless*)
447 | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
448 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
450 case scan_dn2 cc (ist |> path_down [L, R]) e of
451 Accept_Tac2 lr => Accept_Tac2 lr
452 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
453 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
455 go_scan_up2 pcc (ist |> set_appy Skip_)
456 (*no appy_: never causes Reject_Tac2 - Helpless*)
457 | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
458 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
460 case scan_dn2 cc (ist |> path_down [R]) e of
461 Accept_Tac2 lr => Accept_Tac2 lr
462 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
463 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
465 go_scan_up2 pcc (ist |> set_appy Skip_)
467 | scan_up2 pcc ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
468 | scan_up2 pcc ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist
469 | scan_up2 pcc ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up2 pcc ist
471 | scan_up2 pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
473 | scan_up2 _ _ t = error ("scan_up2 not impl for " ^ Rule.term2str t)
475 (* scan program until an applicable tactic is found *)
476 fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
478 then scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog)
479 else go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_)
480 | scan_to_tactic2 _ _ = raise ERROR "scan_to_tactic2: uncovered pattern";
482 (* decide for the next applicable Prog_Tac *)
483 fun find_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt =
484 (case scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) of
485 Accept_Tac2 (tac, ist, ctxt) =>
486 Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
487 | Term_Val2 prog_result =>
488 (case par_pbl_det pt p of
491 val (_, pblID, _) = get_obj g_spec pt p';
493 End_Program (Istate.Pstate ist, Tactic.Check_Postcond' (pblID, (prog_result, [(*???*)])))
495 | _ => End_Program (Istate.Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))
496 | Reject_Tac2 => Helpless)
497 | find_next_tactic _ _ is _ =
498 raise ERROR ("find_next_tactic: not impl for " ^ Istate.istate2str is);
501 (*** locate an input formula in the program ***)
503 datatype input_formula_result =
504 Found_Step of Ctree.state * Istate.T * Proof.context
505 | Not_Derivable of Chead.calcstate'
507 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
509 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
510 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
511 | _ => error "LucinNEW.by_tactic Apply_Method': uncovered case get_obj"
512 (*l*) val {ppc, ...} = Specify.get_met mI;
513 (*l*) val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
514 (*l*) val itms = Specify.hack_until_review_Specify_1 mI itms
515 val thy = Celem.assoc_thy (get_obj g_domID pt p);
516 val srls = Lucin.get_simplifier (pt, pos)
517 val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of
518 (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
519 | _ => error "LucinNEW.by_tactic Apply_Method': uncovered case init_pstate"
520 val ini = Lucin.init_form thy scr env;
525 val pos = start_new_level pos
526 val tac_ = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
527 val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)
529 ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))
533 val pt = update_env pt (fst pos) (SOME (is, ctxt))
534 val (_, (tacis, c, ptp)) = do_next (pt, pos)
535 in ("ok", (tacis @ [(Tactic.Apply_Method mI,
536 Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp))
539 | by_tactic (Tactic.Check_Postcond' (pI, (prog_res, _))) _ (pt, pos as (p, _)) =
541 val pp = par_pblobj pt p
542 val thy = Celem.assoc_thy (get_obj g_domID pt pp);
543 val (ist, ctxt) = get_loc pt pos
544 val asm = (case get_obj g_tac pt p of (*collects and instantiates asms*)
545 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
546 | _ => get_assumptions_ pt pos)
547 val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
552 val is = Istate.Pstate (ist |> the_pstate
553 |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
554 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt) (pp, Res) pt;
555 in ("ok", ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_)))) end
557 let (*resume script of parent PblObj, transfer value of subpbl-script*)
558 val thy = Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt (lev_up p)));
560 val (pst', ctxt') = case get_loc pt (pp, Frm) of
561 (Istate.Pstate pst', ctxt') => (pst', ctxt')
562 | _ => error "by_tactic Check_Postcond' script of parpbl: uncovered case get_loc"
563 val ctxt'' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt'
564 val is = Istate.Pstate (pst' |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
565 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt'') (pp, Res) pt;
566 in ("ok", ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_)))) end
568 | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
569 | by_tactic tac_ is (pt, pos) =
571 val pos = next_in_prog' pos
572 val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
574 ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')))
576 (*find_next_tactic from program, by_tactic will update Ctree*)
577 and do_next (ptp as (pt, pos as (p, p_))) =
578 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
579 then ("helpless", ([], [], (pt, (p, p_))))
582 val thy' = get_obj g_domID pt (par_pblobj pt p);
583 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
585 case find_next_tactic sc (pt, pos) ist ctxt of
586 Next_Step (ist, ctxt, tac) =>
587 by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
588 | End_Program (ist, tac) =>
590 Tactic.End_Detail' res =>
591 ("ok", ([(Tactic.End_Detail,
592 Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
593 | _ => by_tactic tac (ist, ctxt) ptp
595 | Helpless => ("helpless", Chead.e_calcstate')
599 compare inform with ctree.form at current pos by nrls;
600 if found, embed the derivation generated during comparison
601 if not, let the mat-engine compute the next ctree.form.
603 Code's structure is copied from complete_solve
604 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
605 all_modspec etc. has to be inserted at Subproblem'
607 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
611 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
612 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
613 | _ => Rule.e_term (*on PblObj is fo <> ifo*);
614 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
615 val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls
616 val (found, der) = Inform.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
621 val tacis' = map (Inform.mk_tacis rew_ord erls) der;
622 val (c', ptp) = Generate.embed_deriv tacis' ptp;
623 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
625 if pos = ([], Pos.Res) (*TODO: we should stop earlier with trying subproblems *)
626 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
629 val msg_cs' as (_, (tacis, c', ptp)) = do_next ptp; (*<---------------------*)
630 val (_, (tacis, c'', ptp)) = case tacis of
631 ((Tactic.Subproblem _, _, _)::_) =>
633 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
634 val mI = Ctree.get_obj Ctree.g_metID pt p
636 by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) (Istate.e_istate, ContextC.e_ctxt) ptp
639 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
643 handle a user-input formula, which may be a CAS-command, too.
644 * CAS-command: create a calchead, and do 1 step
645 * formula, which is no CAS-command:
646 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
647 collect all the Prog_Tac applied by the way; ...???TODO?
648 If "no derivation found" then check_error_patterns.
649 ALTERNATIVE: check_error_patterns _within_ compare_step: seems too expensive
651 (* vvvv vvvvvv vvvv NEW args for compare_step *)
652 fun locate_input_formula (Rule.Prog _) ((pt, pos) : Ctree.state) (_ : Istate.T) (_ : Proof.context) tm =
654 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
655 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
657 (*TODO: use prog, istate, ctxt in compare_step ...*)
658 case compare_step ([], [], (pt, pos_pred)) tm of
659 ("no derivation found", calcstate') => Not_Derivable calcstate'
660 | ("ok", (_, _, cstate as (pt', pos'))) =>
661 Found_Step (cstate, get_istate pt' pos', get_ctxt pt' pos')
662 | _ => raise ERROR "compare_step: uncovered case"
664 | locate_input_formula _ _ _ _ _ = error ""