1 (* Title: "Minisubpbl/200-start-method-NEXT_STEP.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
18 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
19 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
20 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
21 tracing "--- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
22 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
24 ("Test", ["sqroot-test", "univariate", "equation", "test"],
25 ["Test", "squ-equ-test-subpbl1"]);
26 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
27 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
28 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac
29 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac
31 (*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
32 (*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)
33 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
34 (p, ((pt, e_pos'), []));
35 (*if*) Pos.on_calc_end ip (*else*);
36 val (_, probl_id, _) = Calc.references (pt, p);
38 (*case*) tacis (*of*);
39 (*if*) probl_id = Problem.id_empty (*else*);
41 Step.switch_specify_solve p_ (pt, ip);
42 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
43 (*if*) Pos.on_specification ([], state_pos) (*then*);
45 Step.specify_do_next (pt, input_pos);
46 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
47 val (_, (p_', tac)) = Specify.find_next_step ptp
48 val ist_ctxt = Ctree.get_loc pt (p, p_)
52 Step_Specify.by_tactic_input tac (pt, (p, p_'));
53 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =
54 (tac, (pt, (p, p_')));
56 val (o_model, ctxt, i_model) =
57 Specify_Step.complete_for id (pt, pos);
58 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
59 val {origin = (o_model, _, _), probl = i_prob, ctxt,
60 ...} = Calc.specify_data (ctree, pos);
61 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
62 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
63 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
65 val (_, (i_model, _)) =
66 M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
67 "~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
68 (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
69 (*0*)val mv = Pre_Conds.max_variant pbl;
71 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
72 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
73 SOME _ => false | NONE => true;
74 (*1*)val mis = (filter (notmem pbl)) pbt;
76 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
77 fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
78 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
79 val news = (flat o (map (oris2itms oris))) mis;
80 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
81 val newitms = filter mem_vat news;
82 (*4*)val itms' = pbl @ newitms;
84 val (pb, where_') = Pre_Conds.check ctxt where_rls where_
85 (pbt, I_Model.OLD_to_TEST itms');
86 "~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
87 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms'));
88 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
89 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
90 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
91 val full_subst = if env_eval = [] then pres_subst_other
92 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
94 (*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
95 (*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
96 (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst
98 (*+*)val ctxt = Config.put rewrite_trace true ctxt;
100 Pre_Conds.eval ctxt where_rls) full_subst;
101 (* (*declare [[rewrite_trace = true]]*)
102 @## rls: prls_met_test_squ_sub on: precond_rootmet x
103 @### try calc: "Test.precond_rootmet"
104 @#### eval asms: "(precond_rootmet x) = True"
106 @### try calc: "Test.precond_rootmet"
107 @### try calc: "Test.precond_rootmet"
109 (*+*)val ctxt = Config.put rewrite_trace false ctxt;
111 "~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =
112 ("aaa", "bbb", tTEST, ctxt);
113 SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
114 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
116 (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";
117 "~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");
118 thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
121 "~~~~~ fun cut_longid , args:"; val (dn) = (n2);
122 (*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)
123 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;
125 (*[1], Frm*)val return_Step_do_next_Specify_Method = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
126 (*/------------------- step into Specify_Method --------------------------------------------\\*)
127 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
128 (p, ((pt, e_pos'), []));
129 (*if*) Pos.on_calc_end ip (*else*);
130 val (_, probl_id, _) = Calc.references (pt, p);
132 (*case*) tacis (*of*);
133 (*if*) probl_id = Problem.id_empty (*else*);
135 switch_specify_solve p_ (pt, ip);
136 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
137 (*if*) Pos.on_specification ([], state_pos) (*then*);
139 specify_do_next (pt, input_pos);
140 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
141 val (_, (p_', tac)) = Specify.find_next_step ptp
142 val ist_ctxt = Ctree.get_loc pt (p, p_)
143 (*+*)val Tactic.Apply_Method mI =
146 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
147 ist_ctxt (pt, (p, p_'));
148 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
149 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
150 ist_ctxt, (pt, (p, p_')));
151 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
152 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
153 => (itms, oris, probl, o_spec, spec)
154 | _ => raise ERROR ""
155 val (_, pI', _) = References.select_input o_spec spec
156 val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
157 val {model = met_patt, ...} = MethodC.from_store ctxt mI;
158 val (_, itms) = I_Model.s_make_complete oris
159 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
161 val (is, env, ctxt, prog) = case
162 LItool.init_pstate ctxt itms mI of
163 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
164 val return_init_pstate = (is, env, ctxt, prog)
165 (*#------------------- un-hide local of init_pstate -----------------------------------------\*)
166 fun msg_miss ctxt sc metID caller f formals actuals =
167 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
168 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
169 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
171 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
172 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
173 fun msg_miss_type ctxt sc metID f formals actuals =
174 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
175 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
176 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
177 "\" doesn't mach any actual arg.\nwith:\n" ^
178 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
179 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
180 " with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
181 fun msg_ambiguous ctxt sc metID f aas formals actuals =
182 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
183 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
184 "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
185 "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
186 "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
188 "formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
189 "actuals: " ^ UnparseC.terms ctxt actuals
190 fun trace_init ctxt metID =
191 if Config.get ctxt LI_trace
192 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
195 fun assoc_by_type ctxt f aa prog met_id formals actuals =
196 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
197 [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
199 | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
201 fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics
202 Env.T -> (* [] for building return Env.T *)
203 term list -> (* changed during building return Env.T *)
204 term list -> (* changed during building return Env.T *)
205 Proof.context -> (* *)
206 term -> (* program code *)
207 MethodC.id -> (* for error msg *)
208 term list -> (* original value, unchanged *)
209 term list -> (* original value, unchanged *)
210 Env.T (* return Env.T *)
212 fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
213 raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
214 | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
215 | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
216 if type_of f = type_of a
217 then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
219 let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
220 in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
222 (*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->
223 term list -> term list -> Env.T;
224 (*#------------------- un-hide local of init_pstate -----------------------------------------/*)
226 (*//------------------ step into init_pstate NEW -------------------------------------------\\*)
227 val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
228 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
229 (ctxt, i_model, met_id);
230 val (model_patt, program, prog, prog_rls, where_, where_rls) =
231 case MethodC.from_store ctxt met_id of
232 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
233 (model_patt, program, prog, prog_rls, where_, where_rls)
234 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
236 val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
237 val actuals = map snd env_model
238 (*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
240 val formals = Program.formal_args prog
241 (*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
243 (*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n (Try (Rewrite_Set ''norm_equation'') #>\n Try (Rewrite_Set ''Test_simplify''))\n e_e;\n L_La =\n SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
244 (prog |> UnparseC.term @{context})
246 val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
248 (*||------------------ continue init_pstate NEW --------------------------------------------\\*)
249 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
250 val ist = Istate.e_pstate
251 |> Istate.set_eval prog_rls
252 |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);
253 (*+*) (relate_args [] formals actuals ctxt prog met_id formals actuals);
254 (*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =
255 (relate_args [] formals actuals ctxt prog met_id formals actuals)
256 |> Subst.to_string @{context}
258 val return_init_pstate_steps = (* = return_init_pstate*)
259 (Istate.Pstate ist, ctxt, program)
260 (*\\------------------ step into init_pstate NEW -------------------------------------------//*)
261 val (is, env, ctxt, prog) = return_init_pstate;
263 (*|------------------- continuing Specify_Method ---------------------------------------------*)
264 (*\------------------- step into Specify_Method --------------------------------------------//*)
265 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
267 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac
269 (*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);
270 (*/------------------- step into Apply_Method ----------------------------------------------\\*)
271 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
272 (p ,((pt, e_pos'), []));
273 (*if*) Pos.on_calc_end ip (*else*);
274 val (_, probl_id, _) = Calc.references (pt, p);
276 (*case*) tacis (*of*);
277 (*if*) probl_id = Problem.id_empty (*else*);
279 Step.switch_specify_solve p_ (pt, ip);
280 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
282 (*if*) Pos.on_specification ([], state_pos) (*else*);
284 LI.do_next (pt, input_pos);
285 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
286 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
287 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
289 val return_LI_find_next_step = (*case*)
290 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
291 (*//------------------ step into LI.find_next_step -----------------------------------------\\*)
292 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
293 (sc, (pt, pos), ist, ctxt);
294 (*.. this showed that we have ContextC.empty*)
295 (*\\------------------ step into LI.find_next_step -----------------------------------------//*)
296 val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
298 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
299 "~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
300 = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
301 val pos = next_in_prog' pos
303 val (pos', c, _, pt) =
304 Solve_Step.add_general tac_ ic (pt, pos);
305 "~~~~~ fun add_general , args:"; val (tac, ic, cs)
306 = (tac_, ic, (pt, pos));
307 (*if*) Tactic.for_specify' tac (*else*);
309 Solve_Step.add tac ic cs;
310 "~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
312 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
313 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
314 val pt = Ctree.update_branch pt p Ctree.TransitiveB
317 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
318 (*\------------------- step into Apply_Method ----------------------------------------------//*)
319 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set
321 (* final test ... ----------------------------------------------------------------------------*)
322 (*+*)val ([2], Res) = p;
323 Test_Tool.show_pt_tac pt; (*[
324 ([], Frm), solve (x + 1 = 2, x)
325 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
326 ([1], Frm), x + 1 = 2
327 . . . . . . . . . . Rewrite_Set "norm_equation",
328 ([1], Res), x + 1 + - 1 * 2 = 0
329 . . . . . . . . . . Rewrite_Set "Test_simplify",
330 ([2], Res), - 1 + x = 0
331 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT