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.ctree -> 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: Rule_Set.T -> Proof.context -> I_Model.T -> 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: Program.T -> Env.T -> term option
26 val get_simplifier: Calc.T -> Rule_Set.T
27 val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
30 val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
35 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
41 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
42 val LI_trace = Attrib.setup_config_bool \<^binding>\<open>LI_trace\<close> (K false);
44 (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
45 fun implicit_take (Rule.Prog prog) env =
46 Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
47 | implicit_take _ _ = raise ERROR "implicit_take: no match";
50 val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
51 fun error_msg_2 d itms = ("arguments_from_model: '" ^ UnparseC.term d ^ "' not in itms:\n" ^
52 "itms:\n" ^ I_Model.to_string @{context} itms)
53 (* turn Model-items into arguments for a program *)
54 fun arguments_from_model ctxt mI itms =
56 val mvat = I_Model.max_variant itms
57 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
58 val itms = filter (okv mvat) itms
59 fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.descriptor itm_)
60 fun itm2arg itms (_, (d, _)) =
61 case find_first (test_dsc d) itms of
62 NONE => raise ERROR (error_msg_2 d itms)
63 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
64 val pats = (#ppc o MethodC.from_store ctxt) mI
65 val _ = if pats = [] then raise ERROR error_msg_1 else ()
66 in (flat o (map (itm2arg itms))) pats end;
68 (* convert a Prog_Tac to Tactic.input; specific for "Prog_Tac.SubProblem" *)
69 fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID $ _) =
71 val tid = HOLogic.dest_string thmID
72 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
73 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
75 val tid = HOLogic.dest_string thmID
76 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
77 in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
78 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
79 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
80 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
82 val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
83 in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
84 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
85 (Tactic.Calculate (HOLogic.dest_string op_))
86 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t))
87 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
88 Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
89 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
90 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =
91 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
92 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) = Tactic.Or_to_List
93 | tac_from_prog pt _ (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =
94 fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
95 | tac_from_prog _ thy t = raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term_in_thy thy t);
99 Tactic.T (* Subproblem' gets args instantiated in associate *)
100 * term (* resulting from application of Tactic.T *)
101 * Proof.context (* updated by assumptioons from Rewrite* *)
102 | Ass_Weak of Tactic.T * term * Proof.context
106 associate is the ONLY code within by_tactic, which handles Tactic.T individually;
107 thus it does ContextC.insert_assumptions in case of Rewrite*.
108 The argument Ctree.ctree is required only for Subproblem'.
110 fun trace_msg_3 ctxt tac =
111 if Config.get ctxt LI_trace then
112 tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
113 "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
115 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
116 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
118 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ _ $ thmID_ $ f_) =>
119 if thmID = HOLogic.dest_string thmID_ then
121 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
122 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
124 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ rls_ $ f_) =>
125 if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
127 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
128 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
130 | _ => Not_Associated)
131 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
133 (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID_ $ f_) =>
134 if thmID = HOLogic.dest_string thmID_ then
136 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
137 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
139 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_) =>
140 if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
142 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
143 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
145 | _ => Not_Associated)
146 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
147 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_)) =
148 if Rule_Set.id rls = HOLogic.dest_string rls_ then
150 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
151 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
153 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
154 (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_)) =
155 if Rule_Set.id rls = HOLogic.dest_string rls_ then
157 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
158 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
160 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
162 (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op__ $ f_) =>
163 if op_ = HOLogic.dest_string op__ then
164 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
166 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_) =>
167 if Rule_Set.contains (Rule.Eval (get_calc ctxt
168 op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
169 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
171 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls_ $ f_) =>
172 if Rule_Set.contains (Rule.Eval (get_calc ctxt
173 op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
174 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
176 | _ => Not_Associated)
177 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
178 (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>,_) $ consts' $ _)) =
179 if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
180 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _)) =
181 Associated (m, list, ctxt)
182 | associate _ ctxt (m as Tactic.Take' term, (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
183 Associated (m, term, ctxt)
184 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
185 (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ _ $ t)) =
187 Associated (m, f', ctxt)
188 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
189 if foldl and_ (true, map TermC.contains_Var subte) then
191 val t' = subst_atomic (map HOLogic.dest_eq subte) t
193 if t = t' then raise ERROR "associate: Substitute' not applicable to val of Expr"
194 else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
197 (case Rewrite.rewrite_terms_ (Proof_Context.init_global (ThyC.Isac ())) ro erls subte t of
198 SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
199 | NONE => raise ERROR "associate: Substitute' not applicable to val of Expr")
200 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
201 (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
202 (case Sub_Problem.tac_from_prog pt stac of
203 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
204 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
205 | _ => raise ERROR ("associate: uncovered case"))
206 | associate _ ctxt (tac, _) =
207 (trace_msg_3 ctxt tac; Not_Associated);
209 (* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*)
210 fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
211 | parent_node pt (pos as (p, _)) =
213 fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
215 if Ctree.is_pblobj (Ctree.get_obj I pt p)
216 then (true, p, Rule_Set.Empty, ContextC.empty)
219 val ctxt = Ctree.get_ctxt pt pos
221 case Ctree.get_obj Ctree.g_tac pt p of
222 Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls', ctxt)
223 | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls', ctxt)
224 | _ => par pt (Pos.lev_up p)
226 in par pt (Pos.lev_up p) end;
228 (* create the initial interpreter state
229 from the items of the guard and the formal arguments of the program.
230 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
231 (a) fmz is given by a math author
232 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
233 (c) modelling creates an itm list from ori list + possible user input
234 (d) specifying a theory might add some items and create a guard for the program
235 (e) fun relate_args creates an environment for evaluating the program.
236 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program:
237 * Since the arguments of the partial_function have no description (see Input_Descript.thy),
238 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
239 * pairing formal arguments with itm's follows the sequence
240 * Thus the resulting sequence-relation can be ambiguous.
241 * Ambiguities are done by rearranging fmz_ or the formal arguments.
242 * The latter is easier, albeit not optimal: a fmz_ can be used by different programs.
245 val errmsg = "ERROR: found no actual arguments for prog. of "
246 fun msg_miss sc metID caller f formals actuals =
247 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
248 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
249 "formal arg \"" ^ UnparseC.term f ^ "\" doesn't mach an actual arg.\n" ^
251 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
252 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals
253 fun msg_miss_type sc metID f formals actuals =
254 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
255 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
256 "formal arg \"" ^ UnparseC.term f ^ "\" of type \"" ^ UnparseC.typ (type_of f) ^
257 "\" doesn't mach an actual arg.\nwith:\n" ^
258 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
259 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals ^ "\n" ^
260 " with types: " ^ (strs2str o (map (UnparseC.typ o type_of))) actuals
261 fun msg_ambiguous sc metID f aas formals actuals =
262 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
263 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
264 "formal arg. \"" ^ UnparseC.term f ^ "\" type-matches with several..." ^
265 "actual args. \"" ^ UnparseC.terms aas ^ "\"\n" ^
266 "selected \"" ^ UnparseC.term (hd aas) ^ "\"\n" ^
268 "formals: " ^ UnparseC.terms formals ^ "\n" ^
269 "actuals: " ^ UnparseC.terms actuals
270 fun trace_init ctxt metID =
271 if Config.get ctxt LI_trace
272 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
275 fun init_pstate (srls: Rule_Def.rule_set) (ctxt: Proof.context) (itms) (metID) =
277 val actuals = arguments_from_model ctxt metID itms
278 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
279 val (scr, sc) = (case (#scr o MethodC.from_store ctxt) metID of
280 scr as Rule.Prog sc => (trace_init ctxt metID; (scr, sc))
281 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
282 val formals = Program.formal_args sc
283 fun assoc_by_type f aa =
284 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
285 [] => raise ERROR (msg_miss_type sc metID f formals actuals)
287 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
288 fun relate_args _ (f::_) [] = raise ERROR (msg_miss sc metID "relate_args" f formals actuals)
289 | relate_args env [] _ = env (*may drop Find?*)
290 | relate_args env (f::ff) (aas as (a::aa)) =
291 if type_of f = type_of a
292 then relate_args (env @ [(f, a)]) ff aa
294 let val (f, a) = assoc_by_type f aas
295 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
296 val {pre, prls, ...} = MethodC.from_store ctxt metID;
297 val pres = Pre_Conds.check prls pre itms 0 |> snd |> map snd;
298 val ctxt = ctxt |> ContextC.insert_assumptions pres;
299 val ist = Istate.e_pstate
300 |> Istate.set_eval srls
301 |> Istate.set_env_true (relate_args [] formals actuals)
303 (Istate.Pstate ist, ctxt, scr)
307 (* get the simplifier of the current method *)
308 fun get_simplifier (pt, pos as (p, _)) =
310 val p' = Ctree.par_pblobj pt p
311 val metID = Ctree.get_obj Ctree.g_metID pt p'
312 val ctxt = Ctree.get_ctxt pt pos
313 val {srls, ...} = MethodC.from_store ctxt metID
316 (* resume program interpretation at the beginning of a step *)
317 fun resume_prog pos pt =
319 val (is_problem, p', rls', ctxt) = parent_node pt pos (*is Ctree.PrfObj in case of detail step*)
323 val metID = get_obj g_metID pt p'
324 val {srls, ...} = MethodC.from_store ctxt metID
326 case get_loc pt pos of
327 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
328 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
330 ((is, ctxt), (#scr o MethodC.from_store ctxt) metID)
334 Rule.Prog (Auto_Prog.gen (Proof_Context.theory_of ctxt) (get_last_formula (pt, pos)) rls'))
337 fun trace_msg_1 ctxt call t stac =
338 if Config.get ctxt LI_trace then
339 tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
341 fun trace_msg_2 ctxt call t lexpr' =
342 if Config.get ctxt LI_trace then
343 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"")
346 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
347 snd of return value are the formal arguments in case of currying.
349 fun check_leaf call ctxt srls (E, (a, v)) t =
350 case Prog_Tac.eval_leaf E a v t of
351 (Program.Tac stac, a') =>
353 val stac' = Rewrite.eval_prog_expr ctxt srls
354 (subst_atomic (Env.update_opt E (a, v)) stac)
356 (trace_msg_1 ctxt call t stac; (Program.Tac stac', a'))
358 | (Program.Expr lexpr, a') =>
360 val lexpr' = Rewrite.eval_prog_expr ctxt srls
361 (subst_atomic (Env.update_opt E (a, v)) lexpr)
363 (trace_msg_2 ctxt call t lexpr'; (Program.Expr lexpr', a'))