1 (* Title: interpreter for scripts
2 Author: Walther Neuper 2000
3 (c) due to copyright terms
6 signature LUCAS_INTERPRETER_TOOL =
9 Ass of Tactic.T * term * Proof.context
10 | Ass_Weak of Tactic.T * term * Proof.context
12 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
14 val init_form : 'a -> Program.T -> (term * term) list -> term option
15 val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID ->
16 Istate.T * Proof.context * Program.T
18 val get_simplifier : Calc.T -> Rule.rls
19 (*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*)
20 val resume_prog : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
21 (Istate.T * Proof.context) * Program.T
23 val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input
24 val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
25 Program.leaf * term option
26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
30 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
33 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
34 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
37 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
43 (* determine the first tactic in case of a program with one argument (like simplification)
44 and without an initial Tactic.Take *)
45 fun init_form thy (Rule.Prog prog) env =
46 (case Prog_Tac.get_first thy prog of
48 | SOME prog_tac => SOME (subst_atomic env prog_tac))
49 | init_form _ _ _ = error "init_form: no match";
51 type dsc = typ; (* <-> nam..unknow in Descript.thy *)
53 (*.create the actual parameters (args) of script: their order
54 is given by the order in met.pat .*)
55 (*WN.5.5.03: ?: does this allow for different descriptions ???
56 ?: why not taken from formal args of script ???
57 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
58 val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
59 fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
60 "itms:\n" ^ Model.itms2str_ @{context} itms)
61 fun itms2args _ mI itms =
63 val mvat = Model.max_vt itms
64 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
65 val itms = filter (okv mvat) itms
66 fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
67 fun itm2arg itms (_,(d,_)) =
68 case find_first (test_dsc d) itms of
69 NONE => raise ERROR (errmsg2 d itms)
70 | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
71 (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
72 penv postponed; presently penv holds already Env.update for script*)
73 val pats = (#ppc o Specify.get_met) mI
74 val _ = if pats = [] then raise ERROR errmsg else ()
75 in (flat o (map (itm2arg itms))) pats end;
77 (* convert a Prog_Tac to Tactic.input *)
78 fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
80 val tid = HOLogic.dest_string thmID
81 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid)) end
82 | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
84 val tid = HOLogic.dest_string thmID
85 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid))) end
86 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
87 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
88 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
89 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls))
90 | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
91 (Tactic.Calculate (HOLogic.dest_string op_))
92 | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t))
93 | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
94 (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub))
95 | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
96 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
97 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred))
98 | tac_from_prog _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = Tactic.Or_to_List
99 | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
100 fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
101 | tac_from_prog _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
105 Tactic.T (* SubProblem gets args instantiated in associate *)
106 * term (* for itr_arg, result in ets *)
107 * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
108 | Ass_Weak of Tactic.T * term * Proof.context
111 (* check if tac_ is associated with stac.
112 Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
114 (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
115 (2) check if term t (the result has been calculated from) in tac_
116 has been changed (see "datatype tac_"); if yes, recalculate result
117 TODO.WN120106 recalculate impl.only for Substitute'
119 pt : ctree for pushing the thy specified in rootpbl into subpbls
120 d : unused (planned for data for comparison)
121 tac_ : from user (via applicable_in); to be compared with ...
122 stac : found in program
124 Ass : associated: e.g. thmID in stac = thmID in m
125 +++ arg in stac = arg in m
126 Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
127 NotAss : e.g. thmID in stac/=/thmID in m (not =)
129 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
130 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
132 (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
133 if thmID = HOLogic.dest_string thmID_
136 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
137 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
138 else ((*tracing"3### associate ..NotAss";*) NotAss)
139 | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
140 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
141 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
142 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
145 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
147 (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
148 if thmID = HOLogic.dest_string thmID_
151 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
152 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
154 | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
155 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
158 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
159 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
162 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
163 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
164 if Rule.id_rls rls = HOLogic.dest_string rls_
167 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
168 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
170 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
171 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
172 if Rule.id_rls rls = HOLogic.dest_string rls_
175 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
176 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
178 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
179 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
180 if Rule.id_rls rls = HOLogic.dest_string rls_
183 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
184 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
186 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
187 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
188 if Rule.id_rls rls = HOLogic.dest_string rls_
191 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
192 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
194 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
196 (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
197 if op_ = HOLogic.dest_string op__
200 then Ass (m, f', ctxt)
201 else Ass_Weak (m ,f', ctxt)
203 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
204 let val thy = Celem.assoc_thy "Isac_Knowledge";
206 if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
207 (assoc_rls (HOLogic.dest_string rls_))
210 then Ass (m, f', ctxt)
211 else Ass_Weak (m ,f', ctxt)
214 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
215 let val thy = Celem.assoc_thy "Isac_Knowledge";
217 if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
218 (assoc_rls (HOLogic.dest_string rls_))
221 then Ass (m, f', ctxt)
222 else Ass_Weak (m ,f', ctxt)
226 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
227 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
229 then Ass (m, consts_chkd, ctxt)
231 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
233 | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
234 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
235 (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
236 if f = t then Ass (m, f', ctxt)
237 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
238 if foldl and_ (true, map TermC.contains_Var subte)
240 let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
241 in if t = t' then error "associate: Substitute' not applicable to val of Expr"
242 else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
244 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
245 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
246 | NONE => error "associate: Substitute' not applicable to val of Expr")
247 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
248 (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
249 (case Sub_Problem.tac_from_prog pt stac of
250 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
251 if domID = dI andalso pblID = pI
252 then Ass (tac, f, ctxt)
254 | _ => raise ERROR ("associate: uncovered case"))
255 | associate _ _ (m, _) =
257 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
258 ^ "@@@ tac_ = " ^ Tactic.string_of m)
262 (* create the initial interpreter state
263 from the items of the guard and the formal arguments of the partial_function.
264 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
265 (a) fmz is given by a math author
266 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
267 (c) modelling creates an itm list from ori list + possible user input
268 (d) specifying a theory might add some items and create a guard for the partial_function
269 (e) fun relate_args creates an environment for evaluating the partial_function.
270 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
271 * Since the arguments of the partial_function have no description (see Descript.thy),
272 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
273 * pairing formal arguments with itm's follows the sequence
274 * Thus the resulting sequence-relation can be ambiguous.
275 * Ambiguities are done by rearranging fmz_ or the formal arguments.
276 * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
279 val errmsg = "ERROR: found no actual arguments for prog. of "
280 fun msg_miss sc metID caller f formals actuals =
281 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
282 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
283 "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
285 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
286 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
287 fun msg_miss_type sc metID f formals actuals =
288 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
289 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
290 "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
291 "\" doesn't mach an actual arg.\nwith:\n" ^
292 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
293 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
294 " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
295 fun msg_ambiguous sc metID f aas formals actuals =
296 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
297 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
298 "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
299 "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
300 "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
302 "formals: " ^ Rule.terms2str formals ^ "\n" ^
303 "actuals: " ^ Rule.terms2str actuals
304 fun trace_init metID =
306 then tracing("@@@ program " ^ strs2str metID)
309 fun init_pstate srls ctxt itms metID =
311 val itms = Specify.hack_until_review_Specify_2 metID itms
312 val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
313 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
314 val (scr, sc) = (case (#scr o Specify.get_met) metID of
315 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
316 | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
317 val formals = Program.formal_args sc
318 fun assoc_by_type f aa =
319 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
320 [] => error (msg_miss_type sc metID f formals actuals)
322 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
323 fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
324 | relate_args env [] _ = env (*may drop Find?*)
325 | relate_args env (f::ff) (aas as (a::aa)) =
326 if type_of f = type_of a
327 then relate_args (env @ [(f, a)]) ff aa
329 let val (f, a) = assoc_by_type f aas
330 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
331 val {pre, prls, ...} = Specify.get_met metID;
332 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
333 val ctxt = ctxt |> ContextC.insert_assumptions pres;
334 val ist = Istate.e_pstate
335 |> Istate.set_eval srls
336 |> Istate.set_env_true (relate_args [] formals actuals)
338 (Istate.Pstate ist, ctxt, scr)
342 fun get_simplifier (pt, (p, _)) =
344 val p' = Ctree.par_pblobj pt p
345 val metID = Ctree.get_obj Ctree.g_metID pt p'
346 val {srls, ...} = Specify.get_met metID
349 fun resume_prog thy (p, p_) pt =
351 val (is_problem, p', rls') = parent_node pt p
356 val metID = get_obj g_metID pt p'
357 val {srls, ...} = Specify.get_met metID
359 case get_loc pt (p, p_) of
360 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
361 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
362 in ((is, ctxt), (#scr o Specify.get_met) metID) end
365 Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
368 (* handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
369 TODO: what is a' ??? *)
370 fun check_leaf call ctxt srls (E, (a, v)) t =
371 case Prog_Tac.eval_leaf E a v t of
372 (Program.Tac stac, a') =>
374 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
375 (subst_atomic (Env.update_opt E (a, v)) stac)
378 then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
380 (Program.Tac stac', a'))
382 | (Program.Expr lexpr, a') =>
384 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
385 (subst_atomic (Env.update_opt E (a, v)) lexpr)
388 then tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
390 (Program.Expr lexpr', a'))