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 | Ass_Weak 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 init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
21 val get_simplifier : Ctree.state -> Rule.rls
22 (*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
23 Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Rule.program
24 (*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
25 Rule.rls(*..\<in> ist*) * (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 stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
31 val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
32 val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
33 val interpret_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
34 string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
35 Program.leaf * term option
37 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40 val is_spec_pos : Ctree.pos_ -> bool
41 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
42 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
46 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_tactic, see "and scr" *)
47 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
50 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* pstate steps = / ... case ass* pstate steps of /
61 Accept_Tac1 (pstate, steps) => ... ass* pstate 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. pstate *)
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) : Env.update, id))
89 handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
90 fun updateenv id vl (es : Env.update stack) =
91 (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
92 fun pushenv id vl (es : Env.update stack) =
93 (push (overwrite(top es, (id, vl))) es) : Env.update stack;
94 val popenv = pop : Env.update stack -> Env.update 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 fun init_form thy (Rule.Prog sc) env =
104 (case Prog_Tac.get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
105 | init_form _ _ _ = error "init_form: no match";
107 type dsc = typ; (* <-> nam..unknow in Descript.thy *)
109 (*.create the actual parameters (args) of script: their order
110 is given by the order in met.pat .*)
111 (*WN.5.5.03: ?: does this allow for different descriptions ???
112 ?: why not taken from formal args of script ???
113 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
114 val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
115 fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
116 "itms:\n" ^ Model.itms2str_ @{context} itms)
117 fun itms2args _ mI itms =
119 val mvat = Model.max_vt itms
120 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
121 val itms = filter (okv mvat) itms
122 fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
123 fun itm2arg itms (_,(d,_)) =
124 case find_first (test_dsc d) itms of
125 NONE => raise ERROR (errmsg2 d itms)
126 | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
127 (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
128 penv postponed; presently penv holds already Env.update for script*)
129 val pats = (#ppc o Specify.get_met) mI
130 val _ = if pats = [] then raise ERROR errmsg else ()
131 in (flat o (map (itm2arg itms))) pats end;
133 (* convert a script-tac 'stac' to 'tac' for users;
134 for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
135 if stac is an initac, then convert to a 'tac_' (as required in scan_dn2).
136 arg ctree for pushing the thy specified in rootpbl into subpbls *)
137 fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
139 val tid = HOLogic.dest_string thmID
140 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
141 | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
143 val tid = HOLogic.dest_string thmID
144 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
145 | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
146 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
147 | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
148 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
149 | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
150 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
151 | stac2tac_ _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
152 | stac2tac_ _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
153 (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
154 | stac2tac_ _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
155 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
156 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
157 | stac2tac_ _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
159 (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
160 | stac2tac_ pt _ (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
162 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
163 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
164 val ags = TermC.isalist2list ags';
169 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
170 (* Chead.match_ags : theory -> pat list -> term list -> ori list
171 ^^^ variables ^^^ values *)
172 handle ERROR "actual args do not match formal args"
173 => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
174 val pI' = Specify.refine_ori' pors pI;
175 in (pI', pors (* refinement over models with diff.prec only *),
176 (hd o #met o Specify.get_pbt) pI') end
177 else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
178 handle ERROR "actual args do not match formal args"
179 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
180 val (fmz_, vals) = Chead.oris2fmz_vals pors;
181 val {cas,ppc,thy,...} = Specify.get_pbt pI
182 val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
183 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
184 val ctxt = ContextC.initialise dI vals
187 NONE => Auto_Prog.pblterm dI pI
188 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
189 val f = Auto_Prog.subpbl (strip_thy dI) pI
190 in (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
192 | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
194 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
198 Tactic.T (* SubProblem gets args instantiated in associate *)
199 * term (* for itr_arg, result in ets *)
200 * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
201 | Ass_Weak of Tactic.T * term * Proof.context
204 (* check if tac_ is associated with stac.
205 Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
207 (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
208 (2) check if term t (the result has been calculated from) in tac_
209 has been changed (see "datatype tac_"); if yes, recalculate result
210 TODO.WN120106 recalculate impl.only for Substitute'
212 pt : ctree for pushing the thy specified in rootpbl into subpbls
213 d : unused (planned for data for comparison)
214 tac_ : from user (via applicable_in); to be compared with ...
215 stac : found in program
217 Ass : associated: e.g. thmID in stac = thmID in m
218 +++ arg in stac = arg in m
219 Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
220 NotAss : e.g. thmID in stac/=/thmID in m (not =)
222 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
223 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
225 (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
226 if thmID = HOLogic.dest_string thmID_
229 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
230 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
231 else ((*tracing"3### associate ..NotAss";*) NotAss)
232 | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
233 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
234 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
235 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
238 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
240 (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
241 if thmID = HOLogic.dest_string thmID_
244 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
245 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
247 | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
248 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
251 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
252 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
255 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
256 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
257 if Rule.id_rls rls = HOLogic.dest_string rls_
260 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
261 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
263 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
264 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
265 if Rule.id_rls rls = HOLogic.dest_string rls_
268 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
269 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
271 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
272 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
273 if Rule.id_rls rls = HOLogic.dest_string rls_
276 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
277 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
279 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
280 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
281 if Rule.id_rls rls = HOLogic.dest_string rls_
284 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
285 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
287 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
289 (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
290 if op_ = HOLogic.dest_string op__
293 then Ass (m, f', ctxt)
294 else Ass_Weak (m ,f', ctxt)
296 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
297 let val thy = Celem.assoc_thy "Isac_Knowledge";
299 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
300 (assoc_rls (HOLogic.dest_string rls_))
303 then Ass (m, f', ctxt)
304 else Ass_Weak (m ,f', ctxt)
307 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
308 let val thy = Celem.assoc_thy "Isac_Knowledge";
310 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
311 (assoc_rls (HOLogic.dest_string rls_))
314 then Ass (m, f', ctxt)
315 else Ass_Weak (m ,f', ctxt)
319 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
320 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
322 then Ass (m, consts_chkd, ctxt)
324 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
326 | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
327 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
328 (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
329 if f = t then Ass (m, f', ctxt)
330 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
331 if foldl and_ (true, map TermC.contains_Var subte)
333 let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
334 in if t = t' then error "associate: Substitute' not applicable to val of Expr"
335 else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
337 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
338 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
339 | NONE => error "associate: Substitute' not applicable to val of Expr")
341 (*compare "| stac2tac_ thy (Const ("Prog_Tac.SubProblem",_)" ..TODO: extract common code *)
342 | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
343 (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) =
345 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
346 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
347 val ags = TermC.isalist2list ags';
352 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
353 handle ERROR "actual args do not match formal args"
354 => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
355 val pI' = Specify.refine_ori' pors pI;
356 in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
358 else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
359 handle ERROR "actual args do not match formal args"
360 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
361 val (fmz_, vals) = Chead.oris2fmz_vals pors;
362 val {cas, ppc, thy, ...} = Specify.get_pbt pI
363 val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
364 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
365 val ctxt = ContextC.initialise dI vals
368 NONE => Auto_Prog.pblterm dI pI
369 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
370 val f = Auto_Prog.subpbl (strip_thy dI) pI
372 if domID = dI andalso pblID = pI
373 then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ContextC.e_ctxt(*TODO rm*), f), f, ctxt)
376 | associate _ _ (m, _) =
378 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
379 ^ "@@@ tac_ = " ^ Tactic.string_of m)
383 (* create the initial interpreter state
384 from the items of the guard and the formal arguments of the partial_function.
385 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
386 (a) fmz is given by a math author
387 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
388 (c) modelling creates an itm list from ori list + possible user input
389 (d) specifying a theory might add some items and create a guard for the partial_function
390 (e) fun relate_args creates an environment for evaluating the partial_function.
391 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
392 * Since the arguments of the partial_function have no description (see Descript.thy),
393 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
394 * pairing formal arguments with itm's follows the sequence
395 * Thus the resulting sequence-relation can be ambiguous.
396 * Ambiguities are done by rearranging fmz_ or the formal arguments.
397 * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
400 val errmsg = "ERROR: found no actual arguments for prog. of "
401 fun msg_miss sc metID caller f formals actuals =
402 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
403 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
404 "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
406 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
407 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
408 fun msg_miss_type sc metID f formals actuals =
409 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
410 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
411 "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
412 "\" doesn't mach an actual arg.\nwith:\n" ^
413 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
414 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
415 " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
416 fun msg_ambiguous sc metID f aas formals actuals =
417 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
418 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
419 "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
420 "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
421 "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
423 "formals: " ^ Rule.terms2str formals ^ "\n" ^
424 "actuals: " ^ Rule.terms2str actuals
425 fun trace_init metID =
427 then tracing("@@@ program " ^ strs2str metID)
429 fun trace_istate env =
431 then tracing("@@@ istate " ^ Env.env2str env)
434 fun init_pstate srls ctxt itms metID =
436 val itms = Specify.hack_until_review_Specify_2 metID itms
437 val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
438 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
439 val (scr, sc) = (case (#scr o Specify.get_met) metID of
440 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
441 | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
442 val formals = Program.formal_args sc
443 fun assoc_by_type f aa =
444 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
445 [] => error (msg_miss_type sc metID f formals actuals)
447 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
448 fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
449 | relate_args env [] _ = env (*may drop Find?*)
450 | relate_args env (f::ff) (aas as (a::aa)) =
451 if type_of f = type_of a
452 then relate_args (env @ [(f, a)]) ff aa
454 let val (f, a) = assoc_by_type f aas
455 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
456 val {pre, prls, ...} = Specify.get_met metID;
457 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
458 val ctxt = ctxt |> ContextC.insert_assumptions pres;
459 val ist = Istate.e_scrstate
460 |> Istate.set_eval srls
461 |> Istate.set_env_true (relate_args [] formals actuals)
463 (Istate.Pstate ist, ctxt, scr)
467 fun get_simplifier (pt, (p, _)) =
469 val p' = Ctree.par_pblobj pt p
470 val metID = Ctree.get_obj Ctree.g_metID pt p'
471 val {srls, ...} = Specify.get_met metID
474 (* decide, where to get program/istate from:
475 (* 1 *) from PblObj.Env.update: at begin of program if no init_form
476 (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
477 (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
478 fun from_pblobj_or_detail' _ (p, p_) pt =
479 if member op = [Pbl, Met] p_
480 then case get_obj g_env (*?DEPRECATED?*) pt p of
481 NONE => error "from_pblobj_or_detail': no istate"
482 | SOME (Istate.Pstate pst, ctxt) =>
484 val metID = get_obj g_metID pt p
485 val {srls, ...} = Specify.get_met metID
487 (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
489 | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
491 let val (pbl, p', rls') = par_pbl_det pt p
493 then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
495 val metID = get_obj g_metID pt p'
496 val {srls, ...} = Specify.get_met metID
498 case get_loc pt (p, p_) of
499 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
500 | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
501 in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
504 (*TODO.thy Auto_Prog.generate SHOULD REPLACE ALL HIS..*)
505 val prog = case rls' of
506 Rule.Rls {scr = Rule.Prog prog,...} => prog
507 | Rule.Seq {scr = Rule.Prog prog,...} => prog
508 | _ => raise ERROR ("from_pblobj_or_detail': not for rule-set \"" ^ Rule.id_rls rls' ^ "\"")
509 val t = get_last_formula (pt, (p, p_))
510 val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
511 in (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') end
514 fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
516 val p' = par_pblobj pt p
518 (case get_obj I pt p' of
519 PblObj {meth = itms, ...} => itms
520 | PrfObj _ => error "from_pblobj' NOT with PrfObj")
521 val metID = get_obj g_metID pt p'
522 val {srls, scr, ...} = Specify.get_met metID
524 if last_elem p = 0 (*nothing written to pt yet*)
527 val ctxt = ContextC.initialise thy' (Model.vars_of itms)
528 val (is, ctxt, scr) = init_pstate srls ctxt itms metID
529 in (srls(*..\<in> is*), (is, ctxt), scr) end
530 else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
533 (*.get the stactics and problems of a script as tacs
534 instantiated with the current environment;
535 l is the location which generated the given formula.*)
536 (*WN.12.5.03: quick-and-dirty repair for listexpressions*)
537 fun is_spec_pos Pbl = true
538 | is_spec_pos Met = true
539 | is_spec_pos _ = false;
541 (* handle a leaf at the end of recursive descent:
542 a leaf is either a tactic or an 'expr' in "let v = expr"
543 where "expr" does not contain a tactic.
544 Handling a leaf comprises
545 (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
546 (2) rewrite the leaf by 'srls'
548 fun interpret_leaf call ctxt srls (E, (a, v)) t =
549 case Prog_Tac.eval_leaf E a v t of
550 (Program.Tac stac, a') =>
552 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
553 (subst_atomic (Env.update_opt E (a,v)) stac)
556 then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
558 (Program.Tac stac', a'))
560 | (Program.Expr lexpr, a') =>
562 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
565 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
567 (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
570 (*. fetch _all_ tactics from script .*)
571 fun sel_rules _ (([],Res):pos') =
572 raise PTREE "no tactics applicable at the end of a calculation"
573 | sel_rules pt (p,p_) =
575 then [get_obj g_tac pt p]
578 val pp = par_pblobj pt p;
579 val thy' = get_obj g_domID pt pp;
580 val thy = Celem.assoc_thy thy';
581 val metID = get_obj g_metID pt pp;
582 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
583 val (sc, srls) = (case Specify.get_met metID' of
584 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
585 val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
586 val ctxt = get_ctxt pt (p, p_)
587 in map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
588 (interpret_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
591 (* fetch tactics from script and filter _applicable_ tactics;
592 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
593 fun sel_appl_atomic_tacs _ (([], Res) : pos') =
594 raise PTREE "no tactics applicable at the end of a calculation"
595 | sel_appl_atomic_tacs pt (p, p_) =
597 then [get_obj g_tac pt p]
600 val pp = par_pblobj pt p
601 val thy' = get_obj g_domID pt pp
602 val thy = Celem.assoc_thy thy'
603 val metID = get_obj g_metID pt pp
605 if metID = Celem.e_metID
606 then (thd3 o snd3) (get_obj g_origin pt pp)
608 val (sc, srls, erls, ro) = (case Specify.get_met metID' of
609 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
610 | _ => error "sel_appl_atomic_tacs 1")
611 val (env, (a, v)) = (case get_istate pt (p, p_) of
612 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
613 val ctxt = get_ctxt pt (p, p_)
614 val alltacs = (*we expect at least 1 stac in a script*)
615 map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
616 (interpret_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
618 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
620 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
621 in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;