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 init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> Method.id ->
17 Istate.T * Proof.context * Program.T
18 val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
19 (Istate.T * Proof.context) * Program.T
21 val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
22 Program.leaf * term option
24 val implicit_take: Program.T -> (term * term) list -> term option
25 val get_simplifier: Calc.T -> Rule_Set.T
26 val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
28 val trace_on: bool Unsynchronized.ref
30 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
33 val arguments_from_model : Method.id -> I_Model.T -> term list
34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
38 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
44 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
45 val trace_on = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *)
47 (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
48 fun implicit_take (Rule.Prog prog) env =
49 (case Prog_Tac.get_first_argument prog of
51 | SOME prog_tac => SOME (subst_atomic env prog_tac))
52 | implicit_take _ _ = raise ERROR "implicit_take: no match";
55 val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
56 fun error_msg_2 d itms = ("arguments_from_model: '" ^ UnparseC.term d ^ "' not in itms:\n" ^
57 "itms:\n" ^ I_Model.to_string @{context} itms)
58 (* turn model-items into arguments for a program *)
59 fun arguments_from_model mI itms =
61 val mvat = I_Model.max_vt itms
62 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
63 val itms = filter (okv mvat) itms
64 fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.d_in itm_)
65 fun itm2arg itms (_,(d,_)) =
66 case find_first (test_dsc d) itms of
67 NONE => raise ERROR (error_msg_2 d itms)
68 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
69 val pats = (#ppc o Specify.get_met) mI
70 val _ = if pats = [] then raise ERROR error_msg_1 else ()
71 in (flat o (map (itm2arg itms))) pats end;
73 (* convert a Prog_Tac to Tactic.input; specific for "Prog_Tac.SubProblem" *)
74 fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
76 val tid = HOLogic.dest_string thmID
77 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
78 | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
80 val tid = HOLogic.dest_string thmID
81 in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
82 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
83 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
84 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
85 (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
86 | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
87 (Tactic.Calculate (HOLogic.dest_string op_))
88 | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (UnparseC.term t))
89 | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
90 (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
91 | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
92 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
93 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
94 | tac_from_prog _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = Tactic.Or_to_List
95 | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
96 fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
97 | tac_from_prog _ thy t = raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term_in_thy thy t);
101 Tactic.T (* Subproblem' gets args instantiated in associate *)
102 * term (* resulting from application of Tactic.T *)
103 * Proof.context (* updated by assumptioons from Rewrite* *)
104 | Ass_Weak of Tactic.T * term * Proof.context
108 associate is the ONLY code within by_tactic, which handles Tactic.T individually;
109 thus it does ContextC.insert_assumptions in case of Rewrite*.
110 The argument Ctree.ctree is required only for Subproblem'.
112 fun trace_msg_3 tac =
114 tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
115 "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
117 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
118 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
120 (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
121 if thmID = HOLogic.dest_string thmID_ then
123 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
124 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
126 | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
127 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
129 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
130 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
132 | _ => Not_Associated)
133 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
135 (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
136 if thmID = HOLogic.dest_string thmID_ then
138 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
139 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
141 | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
142 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
144 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
145 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
147 | _ => Not_Associated)
148 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
149 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
150 if Rule_Set.id rls = HOLogic.dest_string rls_ then
152 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
153 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
155 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
156 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
157 if Rule_Set.id rls = HOLogic.dest_string rls_ then
159 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
160 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
162 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
164 (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
165 if op_ = HOLogic.dest_string op__ then
166 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
168 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
169 if Rule_Set.contains (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
170 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
171 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
173 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
174 if Rule_Set.contains (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
175 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
176 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
178 | _ => Not_Associated)
179 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
180 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
181 if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
182 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
183 Associated (m, list, ctxt)
184 | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) =
185 Associated (m, term, ctxt)
186 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
187 (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
189 Associated (m, f', ctxt)
190 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
191 if foldl and_ (true, map TermC.contains_Var subte) then
193 val t' = subst_atomic (map HOLogic.dest_eq subte) t
195 if t = t' then raise ERROR "associate: Substitute' not applicable to val of Expr"
196 else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
199 (case Rewrite.rewrite_terms_ (ThyC.Isac ()) ro erls subte t of
200 SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
201 | NONE => raise ERROR "associate: Substitute' not applicable to val of Expr")
202 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
203 (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
204 (case Sub_Problem.tac_from_prog pt stac of
205 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
206 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
207 | _ => raise ERROR ("associate: uncovered case"))
208 | associate _ _ (tac, _) =
209 (trace_msg_3 tac; Not_Associated);
211 (* create the initial interpreter state
212 from the items of the guard and the formal arguments of the program.
213 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
214 (a) fmz is given by a math author
215 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
216 (c) modelling creates an itm list from ori list + possible user input
217 (d) specifying a theory might add some items and create a guard for the program
218 (e) fun relate_args creates an environment for evaluating the program.
219 Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program:
220 * Since the arguments of the partial_function have no description (see Descript.thy),
221 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
222 * pairing formal arguments with itm's follows the sequence
223 * Thus the resulting sequence-relation can be ambiguous.
224 * Ambiguities are done by rearranging fmz_ or the formal arguments.
225 * The latter is easier, albeit not optimal: a fmz_ can be used by different programs.
228 val errmsg = "ERROR: found no actual arguments for prog. of "
229 fun msg_miss sc metID caller f formals actuals =
230 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
231 "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
232 "formal arg \"" ^ UnparseC.term f ^ "\" doesn't mach an actual arg.\n" ^
234 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
235 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals
236 fun msg_miss_type sc metID f formals actuals =
237 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
238 "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
239 "formal arg \"" ^ UnparseC.term f ^ "\" of type \"" ^ UnparseC.typ (type_of f) ^
240 "\" doesn't mach an actual arg.\nwith:\n" ^
241 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
242 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals ^ "\n" ^
243 " with types: " ^ (strs2str o (map (UnparseC.typ o type_of))) actuals
244 fun msg_ambiguous sc metID f aas formals actuals =
245 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
246 "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
247 "formal arg. \"" ^ UnparseC.term f ^ "\" type-matches with several..." ^
248 "actual args. \"" ^ UnparseC.terms aas ^ "\"\n" ^
249 "selected \"" ^ UnparseC.term (hd aas) ^ "\"\n" ^
251 "formals: " ^ UnparseC.terms formals ^ "\n" ^
252 "actuals: " ^ UnparseC.terms actuals
253 fun trace_init metID =
255 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
258 fun init_pstate srls ctxt itms metID =
260 val itms = Specify.hack_until_review_Specify_2 metID itms
261 val actuals = arguments_from_model metID itms
262 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
263 val (scr, sc) = (case (#scr o Specify.get_met) metID of
264 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
265 | _ => raise ERROR ("init_pstate with " ^ Method.id_to_string metID))
266 val formals = Program.formal_args sc
267 fun assoc_by_type f aa =
268 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
269 [] => raise ERROR (msg_miss_type sc metID f formals actuals)
271 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
272 fun relate_args _ (f::_) [] = raise ERROR (msg_miss sc metID "relate_args" f formals actuals)
273 | relate_args env [] _ = env (*may drop Find?*)
274 | relate_args env (f::ff) (aas as (a::aa)) =
275 if type_of f = type_of a
276 then relate_args (env @ [(f, a)]) ff aa
278 let val (f, a) = assoc_by_type f aas
279 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
280 val {pre, prls, ...} = Specify.get_met metID;
281 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
282 val ctxt = ctxt |> ContextC.insert_assumptions pres;
283 val ist = Istate.e_pstate
284 |> Istate.set_eval srls
285 |> Istate.set_env_true (relate_args [] formals actuals)
287 (Istate.Pstate ist, ctxt, scr)
291 (* get the simplifier of the current method *)
292 fun get_simplifier (pt, (p, _)) =
294 val p' = Ctree.par_pblobj pt p
295 val metID = Ctree.get_obj Ctree.g_metID pt p'
296 val {srls, ...} = Specify.get_met metID
299 (* resume program interpretation at the beginning of a step *)
300 fun resume_prog thy (p, p_) pt =
302 val (is_problem, p', rls') = parent_node pt p
306 val metID = get_obj g_metID pt p'
307 val {srls, ...} = Specify.get_met metID
309 case get_loc pt (p, p_) of
310 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
311 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
313 ((is, ctxt), (#scr o Specify.get_met) metID)
317 Rule.Prog (Auto_Prog.gen (ThyC.get_theory thy) (get_last_formula (pt, (p, p_))) rls'))
321 fun trace_msg_1 call t stac =
323 tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
325 fun trace_msg_2 call t lexpr' =
327 tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"")
330 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
331 snd of return value is the formal arguments in case of currying.
333 fun check_leaf call ctxt srls (E, (a, v)) t =
334 case Prog_Tac.eval_leaf E a v t of
335 (Program.Tac stac, a') =>
337 val stac' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
338 (subst_atomic (Env.update_opt E (a, v)) stac)
340 (trace_msg_1 call t stac; (Program.Tac stac', a'))
342 | (Program.Expr lexpr, a') =>
344 val lexpr' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
345 (subst_atomic (Env.update_opt E (a, v)) lexpr)
347 (trace_msg_2 call t lexpr'; (Program.Expr lexpr', a'))