1 (* Title: interpreter for scripts
2 Author: Walther Neuper 2000
3 (c) due to copyright terms
6 signature LUCAS_INTERPRETER_DEL =
9 type step = Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
11 Ass of Tactic.T * term * Proof.context
12 | AssWeak of Tactic.T * term * Proof.context
14 val associate: Ctree.ctree -> Proof.context -> Tactic.T -> term -> ass
16 (* can these functions be local to Lucin or part of LItools ? *)
17 val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
18 val init_form : 'a -> Rule.program -> (term * term) list -> term option
19 val tac_2tac : Tactic.T -> Tactic.input
20 val init_scrstate : Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
22 val get_simplifier : Ctree.state -> Rule.rls
23 (*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Istate.T * Proof.context) * Rule.program
24 (*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
25 Rule.rls * (Istate.T * Proof.context) * Rule.program
26 val rule2thm'' : Rule.rule -> Celem.thm''
27 val rule2rls' : Rule.rule -> string
28 val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
29 (*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
30 val upd_env_opt : LTool.env -> term option * term -> LTool.env
31 val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
32 val tac_2res : Tactic.T -> term
33 val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
34 val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
35 val handle_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
36 string -> Rule.theory' -> Rule.rls -> LTool.env -> term option -> term -> term ->
37 term option * LTool.stacexpr
39 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
41 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
42 val get_stac : 'a -> term -> term option
43 val is_spec_pos : Ctree.pos_ -> bool
44 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
45 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
49 (* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *)
50 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
52 structure Lucin(**): LUCAS_INTERPRETER_DEL(**) =
55 (*TODO open Celem for L,R,D;
56 the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
59 (* data for creating a new node in ctree; designed for use as:
60 fun ass* scrstate steps = / ... case ass* scrstate steps of /
61 Assoc (scrstate, steps) => ... ass* scrstate steps *)
62 type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
63 WN190713 COMPARE: taci list, see papernote #139 *)
64 Tactic.T (*transformed from associated tac *)
65 * Generate.mout (*result with indentation etc. *)
66 * ctree (*containing node created by tac_ + resp. scrstate *)
67 * pos' (*position in ctree; ctree * pos' is the proofstate *)
68 * pos' list; (*of ctree-nodes probably cut (by fst tac_)
69 WN190713 COMPARE: pos' list also in calcstate'*)
71 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
72 | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
73 fun rule2rls' (Rule.Rls_ rls) = Rule.id_rls rls
74 | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
76 (*check if there are tacs for rewriting only*)
77 fun rew_only ([]:step list) = true
78 | rew_only (((Tactic.Rewrite' _ ,_,_,_,_))::ss) = rew_only ss
79 | rew_only (((Tactic.Rewrite_Inst' _ ,_,_,_,_))::ss) = rew_only ss
80 | rew_only (((Tactic.Rewrite_Set' _ ,_,_,_,_))::ss) = rew_only ss
81 | rew_only (((Tactic.Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss
82 | rew_only (((Tactic.Calculate' _ ,_,_,_,_))::ss) = rew_only ss
83 | rew_only (((Tactic.Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
84 | rew_only (((Tactic.End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
87 (* functions for the environment stack: NOT YET IMPLEMENTED
88 fun accessenv id es = the (assoc ((top es) : LTool.env, id))
89 handle _ => error ("accessenv: " ^ free2str id ^ " not in LTool.env");
90 fun updateenv id vl (es : LTool.env stack) =
91 (push (overwrite(top es, (id, vl))) (pop es)) : LTool.env stack;
92 fun pushenv id vl (es : LTool.env stack) =
93 (push (overwrite(top es, (id, vl))) es) : LTool.env stack;
94 val popenv = pop : LTool.env stack -> LTool.env stack;
97 fun de_esc_underscore str =
100 | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
101 in (implode o scan o Symbol.explode) str end;
103 (*.get argument of first stactic in a script for init_form.*)
104 fun get_stac thy (_ $ body) =
106 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
107 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
108 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
109 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
110 | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a
111 | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a
112 | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
113 | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
114 | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
115 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
116 | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
117 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
118 | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a
119 | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a
120 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
121 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
122 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
123 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
124 | get_t y (Abs (_,_,e)) a = get_t y e a*)
125 | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
126 get_t y e1 a (*don't go deeper without evaluation !*)
127 | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
128 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
130 | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
131 | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
132 | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
133 | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
134 | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
135 | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
136 | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
137 | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
138 | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
139 | get_t _ (Const ("Script.Calculate",_) $ _ ) a = SOME a
141 | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
142 | get_t _ (Const ("Script.Substitute",_) $ _ ) a = SOME a
144 | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
146 | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
147 in get_t thy body Rule.e_term end
148 | get_stac _ t = error ("get_stac: no fun-def. for " ^ Rule.term2str t);
150 fun init_form thy (Rule.Prog sc) env =
151 (case get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
152 | init_form _ _ _ = error "init_form: no match";
154 (*WN020526: not clear, when a is available in ass_up for eval_true*)
155 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
156 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
157 thus "NONE" must be set at the end of currying (ill designed anyway)*)
158 fun upd_env_opt env (SOME a, v) = LTool.upd_env env (a, v)
159 | upd_env_opt env (NONE, _) =
160 ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);
162 type dsc = typ; (* <-> nam..unknow in Descript.thy *)
164 (*.create the actual parameters (args) of script: their order
165 is given by the order in met.pat .*)
166 (*WN.5.5.03: ?: does this allow for different descriptions ???
167 ?: why not taken from formal args of script ???
168 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
169 (* val (thy, mI, itms) = (thy, metID, itms);
171 val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
172 fun itms2args _ mI itms =
174 val mvat = Model.max_vt itms
175 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
176 val itms = filter (okv mvat) itms
177 fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
178 fun itm2arg itms (_,(d,_)) =
179 case find_first (test_dsc d) itms of
180 NONE => error ("itms2args: '" ^ Rule.term2str d ^ "' not in itms")
181 | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
182 (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
183 penv postponed; presently penv holds already LTool.env for script*)
184 val pats = (#ppc o Specify.get_met) mI
185 val _ = if pats = [] then raise ERROR errmsg else ()
186 in (flat o (map (itm2arg itms))) pats end;
188 (* convert a script-tac 'stac' to 'tac' for users;
189 for "Script.SubProblem" also create a 'tac_' for internal use. FIXME separate?
190 if stac is an initac, then convert to a 'tac_' (as required in appy).
191 arg ctree for pushing the thy specified in rootpbl into subpbls *)
192 fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ thmID $ _ $ _) =
194 val tid = HOLogic.dest_string thmID
195 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
196 | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
198 val tid = HOLogic.dest_string thmID
199 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
200 | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _) =
201 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
202 | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
203 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
204 | stac2tac_ _ _ (Const ("Script.Calculate", _) $ op_ $ _) =
205 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
206 | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
207 | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =
208 (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
209 | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $
210 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
211 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
212 | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
214 (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
215 | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
217 val (dI, pI, mI) = LTool.dest_spec spec'
218 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
219 val ags = TermC.isalist2list ags';
224 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
225 (* Chead.match_ags : theory -> pat list -> term list -> ori list
226 ^^^ variables ^^^ values *)
227 handle ERROR "actual args do not match formal args"
228 => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
229 val pI' = Specify.refine_ori' pors pI;
230 in (pI', pors (* refinement over models with diff.prec only *),
231 (hd o #met o Specify.get_pbt) pI') end
232 else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
233 handle ERROR "actual args do not match formal args"
234 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
235 val (fmz_, vals) = Chead.oris2fmz_vals pors;
236 val {cas,ppc,thy,...} = Specify.get_pbt pI
237 val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
238 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
239 val ctxt = ContextC.initialise dI vals
242 NONE => LTool.pblterm dI pI
243 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
244 val f = LTool.subpbl (strip_thy dI) pI
245 in (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
247 | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
249 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
253 Tactic.T (* SubProblem gets args instantiated in associate *)
254 * term (* for itr_arg, result in ets *)
255 * Proof.context (* separate from Tactic.T like in loacte_input_tactic *)
256 | AssWeak of Tactic.T * term * Proof.context
259 (* check if tac_ is associated with stac.
260 Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
262 (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
263 (2) check if term t (the result has been calculated from) in tac_
264 has been changed (see "datatype tac_"); if yes, recalculate result
265 TODO.WN120106 recalculate impl.only for Substitute'
267 pt : ctree for pushing the thy specified in rootpbl into subpbls
268 d : unused (planned for data for comparison)
269 tac_ : from user (via applicable_in); to be compared with ...
270 stac : found in program
272 Ass : associated: e.g. thmID in stac = thmID in m
273 +++ arg in stac = arg in m
274 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
275 NotAss : e.g. thmID in stac/=/thmID in m (not =)
277 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
278 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms'))) stac =
280 (Const ("Script.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
281 if thmID = HOLogic.dest_string thmID_
284 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
285 else AssWeak (m, f', ContextC.insert_assumptions asms' ctxt)
286 else ((*tracing"3### associate ..NotAss";*) NotAss)
287 | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
288 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
289 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
290 else AssWeak (m, f', ContextC.insert_assumptions asms' ctxt)
293 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms'))) stac =
295 (Const ("Script.Rewrite", _) $ thmID_ $ _ $ f_) =>
296 if thmID = HOLogic.dest_string thmID_
299 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
300 else AssWeak (m, f', ContextC.insert_assumptions asms' ctxt)
302 | (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
303 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
306 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
307 else AssWeak (m, f', ContextC.insert_assumptions asms' ctxt)
310 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')))
311 (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =
312 if Rule.id_rls rls = HOLogic.dest_string rls_
315 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
316 else AssWeak (m ,f', ContextC.insert_assumptions asms' ctxt)
318 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')))
319 (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =
320 if Rule.id_rls rls = HOLogic.dest_string rls_
323 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
324 else AssWeak (m ,f', ContextC.insert_assumptions asms' ctxt)
326 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')))
327 (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =
328 if Rule.id_rls rls = HOLogic.dest_string rls_
331 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
332 else AssWeak (m ,f', ContextC.insert_assumptions asms' ctxt)
334 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')))
335 (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =
336 if Rule.id_rls rls = HOLogic.dest_string rls_
339 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
340 else AssWeak (m ,f', ContextC.insert_assumptions asms' ctxt)
342 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _))) stac =
344 (Const ("Script.Calculate",_) $ op__ $ f_) =>
345 if op_ = HOLogic.dest_string op__
348 then Ass (m, f', ctxt)
349 else AssWeak (m ,f', ctxt)
351 | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
352 let val thy = Celem.assoc_thy "Isac";
354 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
355 (assoc_rls (HOLogic.dest_string rls_))
358 then Ass (m, f', ctxt)
359 else AssWeak (m ,f', ctxt)
362 | (Const ("Script.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
363 let val thy = Celem.assoc_thy "Isac";
365 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
366 (assoc_rls (HOLogic.dest_string rls_))
369 then Ass (m, f', ctxt)
370 else AssWeak (m ,f', ctxt)
374 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)))
375 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
377 then Ass (m, consts_chkd, ctxt)
379 | associate _ ctxt (m as Tactic.Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) =
381 | associate _ ctxt (m as Tactic.Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term, ctxt)
382 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =
383 if f = t then Ass (m, f', ctxt)
384 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
385 if foldl and_ (true, map TermC.contains_Var subte)
387 let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
388 in if t = t' then error "associate: Substitute' not applicable to val of Expr"
389 else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
391 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
392 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
393 | NONE => error "associate: Substitute' not applicable to val of Expr")
395 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
396 | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _))
397 (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
399 val (dI, pI, mI) = LTool.dest_spec spec'
400 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
401 val ags = TermC.isalist2list ags';
406 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
407 handle ERROR "actual args do not match formal args"
408 => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
409 val pI' = Specify.refine_ori' pors pI;
410 in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
412 else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
413 handle ERROR "actual args do not match formal args"
414 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
415 val (fmz_, vals) = Chead.oris2fmz_vals pors;
416 val {cas, ppc, thy, ...} = Specify.get_pbt pI
417 val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
418 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
419 val ctxt = ContextC.initialise dI vals
422 NONE => LTool.pblterm dI pI
423 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
424 val f = LTool.subpbl (strip_thy dI) pI
426 if domID = dI andalso pblID = pI
427 then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ContextC.e_ctxt(*TODO rm*), f), f, ctxt)
430 | associate _ _ m _ =
432 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
433 ^ "@@@ tac_ = " ^ Tactic.tac_2str m)
437 fun tac_2tac (Tactic.Refine_Tacitly' (pI, _, _, _, _)) = Tactic.Refine_Tacitly pI
438 | tac_2tac (Tactic.Model_Problem' (_, _, _)) = Tactic.Model_Problem
439 | tac_2tac (Tactic.Add_Given' (t, _)) = Tactic.Add_Given t
440 | tac_2tac (Tactic.Add_Find' (t, _)) = Tactic.Add_Find t
441 | tac_2tac (Tactic.Add_Relation' (t, _)) = Tactic.Add_Relation t
443 | tac_2tac (Tactic.Specify_Theory' dI) = Tactic.Specify_Theory dI
444 | tac_2tac (Tactic.Specify_Problem' (dI, _)) = Tactic.Specify_Problem dI
445 | tac_2tac (Tactic.Specify_Method' (dI, _, _)) = Tactic.Specify_Method dI
447 | tac_2tac (Tactic.Rewrite' (_, _, _, _, thm, _, _)) = Tactic.Rewrite thm
448 | tac_2tac (Tactic.Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Tactic.Rewrite_Inst (Selem.subst2subs sub, thm)
450 | tac_2tac (Tactic.Rewrite_Set' (_, _, rls, _, _)) = Tactic.Rewrite_Set (Rule.id_rls rls)
451 | tac_2tac (Tactic.Detail_Set' (_, _, rls, _, _)) = Tactic.Detail_Set (Rule.id_rls rls)
453 | tac_2tac (Tactic.Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
454 Tactic.Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
455 | tac_2tac (Tactic.Detail_Set_Inst' (_, _, sub, rls, _, _)) =
456 Tactic.Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
458 | tac_2tac (Tactic.Calculate' (_, op_, _, _)) = Tactic.Calculate (op_)
459 | tac_2tac (Tactic.Check_elementwise' (_, pred, _)) = Tactic.Check_elementwise pred
461 | tac_2tac (Tactic.Or_to_List' _) = Tactic.Or_to_List
462 | tac_2tac (Tactic.Take' term) = Tactic.Take (Rule.term2str term)
463 | tac_2tac (Tactic.Substitute' (_, _, subte, _, _)) = Tactic.Substitute (Selem.subte2sube subte)
464 | tac_2tac (Tactic.Tac_ (_, _, id, _)) = Tactic.Tac id
466 | tac_2tac (Tactic.Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Tactic.Subproblem (domID, pblID)
467 | tac_2tac (Tactic.Check_Postcond' (pblID, _)) = Tactic.Check_Postcond pblID
468 | tac_2tac Tactic.Empty_Tac_ = Tactic.Empty_Tac
469 | tac_2tac m = error ("tac_2tac: not impl. for "^(Tactic.tac_2str m));
471 fun make_rule thy t =
472 let val ct = Thm.global_cterm_of thy (HOLogic.Trueprop $ t)
473 in Rule.Thm (Rule.term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
475 fun rep_tac_ (Tactic.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) =
477 val b = @{term False};
478 val subs' = Selem.subst_to_subst' subs;
479 val sT' = type_of subs';
481 val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
482 $ subs' $ HOLogic.mk_string thmID $ b $ f;
483 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
484 | rep_tac_ (Tactic.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
487 val b = if put then @{term True} else @{term False};
488 val lhs = Const ("Script.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
489 $ HOLogic.mk_string thmID $ b $ f;
490 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
491 | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
493 val b = @{term False};
494 val subs' = Selem.subst_to_subst' subs;
495 val sT' = type_of subs';
497 val lhs = Const ("Script.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
498 $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
499 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
500 | rep_tac_ (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) =
503 val b = if put then @{term True} else @{term False};
504 val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
505 $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
506 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
507 | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
510 val lhs = Const ("Script.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
511 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
512 | rep_tac_ (Tactic.Check_elementwise' (_, _, (t', _))) = (Rule.Erule, (Rule.e_term, t'))
513 | rep_tac_ (Tactic.Subproblem' (_, _, _, _, _, t')) = (Rule.Erule, (Rule.e_term, t'))
514 | rep_tac_ (Tactic.Take' t') = (Rule.Erule, (Rule.e_term, t'))
515 | rep_tac_ (Tactic.Substitute' (_, _, _, t, t')) = (Rule.Erule, (t, t'))
516 | rep_tac_ (Tactic.Or_to_List' (t, t')) = (Rule.Erule, (t, t'))
517 | rep_tac_ m = error ("rep_tac_: not impl.for " ^ Tactic.tac_2str m)
519 fun tac_2res m = (snd o snd o rep_tac_) m;
521 (* create the initial interpreter state
522 from the items of the guard and the formal arguments of the partial_function.
523 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
524 (a) fmz is given by a math author
525 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
526 (c) modelling creates an itm list from ori list + possible user input
527 (d) specifying a theory might add some items and create a guard for the partial_function
528 (e) fun relate_args creates an environment for evaluating the partial_function.
529 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
530 * Since the arguments of the partial_function have no description (see Descript.thy),
531 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
532 * pairing formal arguments with itm's follows the sequence
533 * Thus the resulting sequence-relation can be ambiguous.
534 * Ambiguities are done by rearranging fmz_ or the formal arguments.
535 * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
538 val errmsg = "ERROR: found no actual arguments for prog. of "
539 fun msg_miss sc metID caller f formals actuals =
540 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
541 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
542 "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
544 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
545 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
546 fun msg_miss_type sc metID f formals actuals =
547 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
548 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
549 "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
550 "\" doesn't mach an actual arg.\nwith:\n" ^
551 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
552 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
553 " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
554 fun msg_ambiguous sc metID f aas formals actuals =
555 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
556 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
557 "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
558 "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
559 "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
561 "formals: " ^ Rule.terms2str formals ^ "\n" ^
562 "actuals: " ^ Rule.terms2str actuals
563 fun trace_init metID =
565 then tracing("@@@ program " ^ strs2str metID)
567 fun trace_istate env =
569 then tracing("@@@ istate " ^ Celem.env2str env)
572 fun init_scrstate ctxt itms metID =
574 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
576 if metID = ["IntegrierenUndKonstanteBestimmen2"]
578 [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
579 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
580 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
581 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
582 (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
583 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
584 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
585 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
587 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
588 val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
589 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
590 val (scr, sc) = (case (#scr o Specify.get_met) metID of
591 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
592 | _ => raise ERROR ("init_scrstate with " ^ Celem.metID2str metID))
593 val formals = LTool.formal_args sc
594 fun assoc_by_type f aa =
595 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
596 [] => error (msg_miss_type sc metID f formals actuals)
598 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
599 fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
600 | relate_args env [] _ = env (*may drop Find?*)
601 | relate_args env (f::ff) (aas as (a::aa)) =
602 if type_of f = type_of a
603 then relate_args (env @ [(f, a)]) ff aa
605 let val (f, a) = assoc_by_type f aas
606 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
607 val env = relate_args [] formals actuals;
608 val _ = trace_istate env;
609 val {pre, prls, ...} = Specify.get_met metID;
610 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
611 val ctxt = ctxt |> ContextC.insert_assumptions pres;
612 in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
615 fun get_simplifier (pt, (p, _)) =
617 val p' = Ctree.par_pblobj pt p
618 val metID = Ctree.get_obj Ctree.g_metID pt p'
619 val {srls, ...} = Specify.get_met metID
622 (* decide, where to get script/istate from:
623 (* 1 *) from PblObj.LTool.env: at begin of script if no init_form
624 (* 2 *) from PblObj/PrfObj: if stac is in the middle of the script
625 (* 3 *) from rls/PrfObj: in case of detail a ruleset DEPRECATED in favour of inter_steps *)
626 fun from_pblobj_or_detail' _ (p, p_) pt = (* DEPRECATED ??? *)
627 if member op = [Pbl, Met] p_
628 then case get_obj g_env pt p of
629 NONE => error "from_pblobj_or_detail': no istate"
632 val metID = get_obj g_metID pt p
633 val {srls, ...} = Specify.get_met metID
634 in (srls, is, (#scr o Specify.get_met) metID) end
636 let val (pbl, p', rls') = par_pbl_det pt p
638 then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
640 val metID = get_obj g_metID pt p'
641 val {srls, ...} = Specify.get_met metID
642 in (srls, get_loc pt (p, p_), (#scr o Specify.get_met) metID) end
643 else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in inform, determine_next_tactic*)
644 (Rule.e_rls(*!!!*), get_loc pt (p,p_), (* 3 *)
646 Rule.Rls {scr = scr,...} => scr
647 | Rule.Seq {scr = scr,...} => scr
648 | Rule.Rrls {scr =rfuns,...} => rfuns
649 | Rule.Erls => error "from_pblobj_or_detail' with Erls")
652 fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
654 val p' = par_pblobj pt p
655 val thy = Celem.assoc_thy thy'
657 (case get_obj I pt p' of
658 PblObj {meth = itms, ...} => itms
659 | PrfObj _ => error "from_pblobj' NOT with PrfObj")
660 val metID = get_obj g_metID pt p'
661 val {srls, scr, ...} = Specify.get_met metID
663 if last_elem p = 0 (*nothing written to pt yet*)
666 val ctxt = ContextC.initialise thy' (Model.vars_of itms)
667 val (is, ctxt, scr) = init_scrstate ctxt itms metID
668 in (srls, (is, ctxt), scr) end
669 else (srls, get_loc pt (p,p_), scr)
674 (*.get the stactics and problems of a script as tacs
675 instantiated with the current environment;
676 l is the location which generated the given formula.*)
677 (*WN.12.5.03: quick-and-dirty repair for listexpressions*)
678 fun is_spec_pos Pbl = true
679 | is_spec_pos Met = true
680 | is_spec_pos _ = false;
682 (* handle a leaf at the end of recursive descent:
683 a leaf is either a tactic or an 'expr' in "let v = expr"
684 where "expr" does not contain a tactic.
685 Handling a leaf comprises
686 (1) 'subst_stacexpr' substitute LTool.env and complete curried tactic
687 (2) rewrite the leaf by 'srls'
689 fun handle_leaf call thy srls E a v t =
690 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
691 case LTool.subst_stacexpr E a v t of
692 (a', LTool.STac stac) => (*script-tactic*)
694 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
697 then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> STac '" ^ Rule.term2str stac ^"'")
699 (a', LTool.STac stac'))
701 | (a', LTool.Expr lexpr) => (*leaf-expression*)
703 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
706 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> Expr '" ^ Rule.term2str lexpr'^"'")
708 (a', LTool.Expr lexpr')) (*lexpr' is the value of the Expr*)
711 (*. fetch _all_ tactics from script .*)
712 fun sel_rules _ (([],Res):pos') =
713 raise PTREE "no tactics applicable at the end of a calculation"
714 | sel_rules pt (p,p_) =
716 then [get_obj g_tac pt p]
719 val pp = par_pblobj pt p;
720 val thy' = get_obj g_domID pt pp;
721 val thy = Celem.assoc_thy thy';
722 val metID = get_obj g_metID pt pp;
723 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
724 val (sc, srls) = (case Specify.get_met metID' of
725 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
726 val (env, a, v) = (case get_istate pt (p, p_) of
727 Istate.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
728 in map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
729 (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
732 (* fetch tactics from script and filter _applicable_ tactics;
733 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
734 fun sel_appl_atomic_tacs _ (([], Res) : pos') =
735 raise PTREE "no tactics applicable at the end of a calculation"
736 | sel_appl_atomic_tacs pt (p, p_) =
738 then [get_obj g_tac pt p]
741 val pp = par_pblobj pt p
742 val thy' = get_obj g_domID pt pp
743 val thy = Celem.assoc_thy thy'
744 val metID = get_obj g_metID pt pp
746 if metID = Celem.e_metID
747 then (thd3 o snd3) (get_obj g_origin pt pp)
749 val (sc, srls, erls, ro) = (case Specify.get_met metID' of
750 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
751 | _ => error "sel_appl_atomic_tacs 1")
752 val (env, a, v) = (case get_istate pt (p, p_) of
753 Istate.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
754 val alltacs = (*we expect at least 1 stac in a script*)
755 map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
756 (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
758 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
760 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
761 in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;