1 (* Title: Interpret/li-tool.sml
2 Author: Walther Neuper 2000
3 (c) due to copyright terms
5 Tools for Lucas_Interpreter
8 signature LUCAS_INTERPRETER_TOOL =
11 Associated of Tactic.T * term (*..result*) * Proof.context
12 | Ass_Weak of Tactic.T * term (*..result*) * Proof.context
14 val associate: Ctree.state -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
16 val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
17 val init_pstate: Proof.context -> I_Model.T_TEST -> MethodC.id ->
18 Istate.T * Proof.context * Program.T
19 val resume_prog: Pos.pos' -> Ctree.ctree ->
20 (Istate.T * Proof.context) * Program.T
22 val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
23 Program.leaf * term option
25 val implicit_take: Proof.context -> Program.T -> Env.T -> term option
26 val get_simplifier: Calc.T -> Rule_Set.T
27 val tac_from_prog: Ctree.state -> term -> Tactic.input
29 (*from isac_test for Minisubpbl*)
30 val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
32 val error_msg_2: Proof.context -> term -> I_Model.T -> string
33 val error_msg_2_TEST: Proof.context -> term -> I_Model.T_TEST -> string
34 val error_msg_1: string
35 val relate_args: Env.T -> term list -> term list -> Proof.context -> Program.term ->
36 MethodC.id -> term list -> term list -> (term * term) list
39 val trace_init: Proof.context -> string list -> unit
45 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
46 val LI_trace = Attrib.setup_config_bool \<^binding>\<open>LI_trace\<close> (K false);
49 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
55 (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
56 fun implicit_take _ (Rule.Prog prog) env =
57 Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
58 | implicit_take _ _ _ = raise ERROR "implicit_take: no match";
60 val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
61 fun error_msg_2 ctxt d itms =
62 ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
63 "itms:\n" ^ I_Model.to_string @{context} itms)
64 fun error_msg_2_TEST ctxt d itms =
65 ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
66 "itms:\n" ^ I_Model.to_string_TEST @{context} itms)
67 (* turn Model-items into arguments for a program *)
68 fun arguments_from_model ctxt mI itms =
70 val mvat = Pre_Conds.max_variant itms
71 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
72 val itms = filter (okv mvat) itms
73 fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate,
74 while changing I_Model.penvval_in triggers much more errors*)
75 val pats = (#model o MethodC.from_store ctxt) mI
76 val _ = if pats = [] then raise ERROR error_msg_1 else ()
77 in (flat o (map (itm2arg itms))) pats end;
80 convert a Prog_Tac to Tactic.input;
81 argument Ctree.state is specifically for "Prog_Tac.SubProblem" (requires Pos),
83 fun tac_from_prog (pt, pos) intac =
85 val pos = Pos.back_from_new pos
86 val ctxt = Ctree.get_ctxt pt pos
87 val thy = Proof_Context.theory_of ctxt
90 (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID $ _) =>
92 val tid = HOLogic.dest_string thmID
93 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
94 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =>
96 val tid = HOLogic.dest_string thmID
97 val sub' = Subst.program_to_input ctxt sub
98 in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
99 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =>
100 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
101 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =>
103 val sub' = Subst.program_to_input ctxt sub
104 in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
105 | (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =>
106 (Tactic.Calculate (HOLogic.dest_string op_))
107 | (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) =>
108 (Tactic.Take (UnparseC.term ctxt t))
109 | (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =>
110 Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
111 | (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
112 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =>
113 (Tactic.Check_elementwise (UnparseC.term ctxt pred))
114 | (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) => Tactic.Or_to_List
115 | (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =>
116 fst (Sub_Problem.tac_from_prog (pt, pos) ptac) (*might involve problem refinement etc*)
118 raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term ctxt t)
123 Tactic.T (* Subproblem' gets args instantiated in associate *)
124 * term (* resulting from application of Tactic.T *)
125 * Proof.context (* updated by assumptioons from Rewrite* *)
126 | Ass_Weak of Tactic.T * term * Proof.context
130 associate is the ONLY code within by_tactic, which handles Tactic.T individually;
131 thus it does ContextC.insert_assumptions in case of Rewrite*.
132 The argument Ctree.ctree is required only for Subproblem'.
134 fun trace_msg_3 ctxt tac =
135 if Config.get ctxt LI_trace then
136 tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
137 "@@@ tac_ = \"" ^ Tactic.string_of ctxt tac ^ "\"")
139 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
140 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
142 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ _ $ thmID_ $ f_) =>
143 if thmID = HOLogic.dest_string thmID_ then
145 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
146 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
148 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ rls_ $ f_) =>
149 if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
151 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
152 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
154 | _ => Not_Associated)
155 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
157 (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID_ $ f_) =>
158 if thmID = HOLogic.dest_string thmID_ then
160 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
161 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
163 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_) =>
164 if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
166 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
167 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
169 | _ => Not_Associated)
170 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
171 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_)) =
172 if Rule_Set.id rls = HOLogic.dest_string rls_ then
174 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
175 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
177 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
178 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_)) =
179 if Rule_Set.id rls = HOLogic.dest_string rls_ then
181 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
182 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
184 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
186 (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op__ $ f_) =>
187 if op_ = HOLogic.dest_string op__ then
188 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
190 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_) =>
191 if Rule_Set.contains (Rule.Eval (get_calc ctxt
192 op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
193 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
195 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls_ $ f_) =>
196 if Rule_Set.contains (Rule.Eval (get_calc ctxt
197 op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
198 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
200 | _ => Not_Associated)
201 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
202 (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>,_) $ consts' $ _)) =
203 if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
204 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _)) =
205 Associated (m, list, ctxt)
206 | associate _ ctxt (m as Tactic.Take' term, (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
207 Associated (m, term, ctxt)
208 | associate _ ctxt (m as Tactic.Substitute' (ro, asm_rls, subte, f, f'),
209 (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ _ $ t)) =
211 Associated (m, f', ctxt)
212 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
213 if foldl and_ (true, map TermC.contains_Var subte) then
215 val t' = subst_atomic (map HOLogic.dest_eq subte) t
217 if t = t' then raise ERROR "associate: Substitute' not applicable to val of Expr"
218 else Associated (Tactic.Substitute' (ro, asm_rls, subte, t, t'), t', ctxt)
221 (case Rewrite.rewrite_terms_ ctxt ro asm_rls subte t of
222 SOME (t', _) => Associated (Tactic.Substitute' (ro, asm_rls, subte, t, t'), t', ctxt)
223 | NONE => raise ERROR "associate: Substitute' not applicable to val of Expr")
224 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
225 (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
226 (case Sub_Problem.tac_from_prog pt stac of
227 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
228 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
229 | _ => raise ERROR ("associate: uncovered case"))
230 | associate _ ctxt (tac, _) =
231 (trace_msg_3 ctxt tac; Not_Associated);
233 (* in detail step find the next parent, which is either a PblObj xor a PrfObj *)
234 fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
235 | parent_node pt (pos as (p, _)) =
237 fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
239 if Ctree.is_pblobj (Ctree.get_obj I pt p)
240 then (true, p, Rule_Set.Empty, ContextC.empty)
243 val ctxt = Ctree.get_ctxt pt pos
245 case Ctree.get_obj Ctree.g_tac pt p of
246 Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls', ctxt)
247 | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls', ctxt)
248 | _ => par pt (Pos.lev_up p)
250 in par pt (Pos.lev_up p) end;
252 (* create the initial interpreter state
253 from the items of the guard and the formal arguments of the program.
254 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
255 (a) fmz is given by a math author
256 (b) fmz_ is transformed to O_Model.T as a prerequisite for efficient interactive modelling
257 (c) modelling creates an I_Model.T from O_Model.T + possible user input
258 (d) specifying a theory might add some items to I_Model.T and create a guard for the program
259 (e) fun relate_args creates an environment for evaluating the program.
260 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program:
261 * Since the arguments of the partial_function have no description (see Input_Descript.thy),
262 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
263 * pairing formal arguments with itm's follows the sequence
264 * Thus the resulting sequence-relation can be ambiguous.
265 * Ambiguities are done by rearranging fmz_ or the formal arguments.
266 * The latter is easier, albeit not optimal: a fmz_ can be used by different programs.
268 val errmsg = "ERROR: found no actual arguments for prog. of "
269 (** )local( ** ) open for tests*)
270 fun msg_miss ctxt sc metID caller f formals actuals =
271 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
272 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
273 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
275 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
276 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
277 fun msg_miss_type ctxt sc metID f formals actuals =
278 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
279 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
280 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
281 "\" doesn't mach any actual arg.\nwith:\n" ^
282 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
283 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
284 " with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
285 fun msg_ambiguous ctxt sc metID f aas formals actuals =
286 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
287 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
288 "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
289 "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
290 "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
292 "formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
293 "actuals: " ^ UnparseC.terms ctxt actuals
296 fun trace_init ctxt metID =
297 if Config.get ctxt LI_trace
298 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
300 fun assoc_by_type ctxt f aa prog met_id formals actuals =
301 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
302 [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
304 | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
307 The sequence of \<open>formals\<close> and \<open>actuals\<close> must be the same:
308 the sequence of \<open>formals\<close> is given by the program,
309 the sequence of \<open>actuals\<close> is given by the by theMethodC#model
311 In case of equal sequence the \<open>fun relate\<close> could be simpler ...
313 fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
314 raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
315 | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
316 | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
317 if type_of f = type_of a
319 relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
322 val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
324 relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals
327 fun init_pstate ctxt i_model met_id =
329 val (model_patt, program, prog, prog_rls, where_, where_rls) =
330 case MethodC.from_store ctxt met_id of
331 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
332 (model_patt, program, prog, prog_rls, where_, where_rls)
333 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
334 val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
336 val actuals = map snd env_model
337 val formals = Program.formal_args prog
338 val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
339 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
340 val ist = Istate.e_pstate
341 |> Istate.set_eval prog_rls
342 |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
344 (Istate.Pstate ist, ctxt, program)
346 (** )end( ** )local*)
348 (*DEL single call +tests, get the simplifier of the current method *)
349 fun get_simplifier (pt, pos as (p, _)) =
351 val p' = Ctree.par_pblobj pt p
352 val metID = Ctree.get_obj Ctree.g_metID pt p'
353 val ctxt = Ctree.get_ctxt pt pos
354 val {prog_rls, ...} = MethodC.from_store ctxt metID
357 (* resume program interpretation at the beginning of a step *)
358 fun resume_prog pos pt =
360 val (is_problem, p', rls', ctxt) = parent_node pt pos (*is Ctree.PrfObj in case of detail step*)
364 val metID = get_obj g_metID pt p'
365 val {prog_rls, ...} = MethodC.from_store ctxt metID
367 case get_loc pt pos of
368 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval prog_rls ist), ctxt)
369 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
371 ((is, ctxt), (#program o MethodC.from_store ctxt) metID)
375 Rule.Prog (Auto_Prog.gen (Proof_Context.theory_of ctxt) (get_last_formula (pt, pos)) rls'))
378 fun trace_msg_1 ctxt call t stac =
379 if Config.get ctxt LI_trace then
380 tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term ctxt t ^ "\" \<longrightarrow> Tac \"" ^
381 UnparseC.term ctxt stac ^ "\"")
383 fun trace_msg_2 ctxt call t lexpr' =
384 if Config.get ctxt LI_trace then
385 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term ctxt t ^ "' \<longrightarrow> Expr \"" ^
386 UnparseC.term ctxt lexpr' ^ "\"")
389 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
390 snd of return value are the formal arguments in case of currying.
392 fun check_leaf call ctxt prog_rls (E, (a, v)) t =
393 case Prog_Tac.eval_leaf E a v t of
394 (Program.Tac stac, a') =>
396 val stac' = Rewrite.eval_prog_expr ctxt prog_rls
397 (subst_atomic (Env.update_opt E (a, v)) stac)
399 (trace_msg_1 ctxt call t stac; (Program.Tac stac', a'))
401 | (Program.Expr lexpr, a') =>
403 val lexpr' = Rewrite.eval_prog_expr ctxt prog_rls
404 (subst_atomic (Env.update_opt E (a, v)) lexpr)
406 (trace_msg_2 ctxt call t lexpr'; (Program.Expr lexpr', a'))