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_OLD ctxt where_rls where_
85 (pbt, I_Model.OLD_to_TEST itms');
86 "~~~~~ fun check_OLD , 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) = case get_obj I pt p of (*STILL asms=[]*)
152 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
153 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
154 val {model, ...} = MethodC.from_store ctxt mI;
155 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
157 val (is, env, ctxt, prog) = case
158 LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
159 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
160 val return_init_pstate = (is, env, ctxt, prog)
161 (*#------------------- un-hide local of init_pstate -----------------------------------------\*)
162 fun msg_miss ctxt sc metID caller f formals actuals =
163 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
164 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
165 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
167 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
168 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
169 fun msg_miss_type ctxt sc metID f formals actuals =
170 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
171 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
172 "formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
173 "\" doesn't mach any actual arg.\nwith:\n" ^
174 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
175 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
176 " with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
177 fun msg_ambiguous ctxt sc metID f aas formals actuals =
178 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
179 "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
180 "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
181 "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
182 "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
184 "formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
185 "actuals: " ^ UnparseC.terms ctxt actuals
186 fun trace_init ctxt metID =
187 if Config.get ctxt LI_trace
188 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
191 fun assoc_by_type ctxt f aa prog met_id formals actuals =
192 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
193 [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
195 | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
197 fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics
198 Env.T -> (* [] for building return Env.T *)
199 term list -> (* changed during building return Env.T *)
200 term list -> (* changed during building return Env.T *)
201 Proof.context -> (* *)
202 term -> (* program code *)
203 MethodC.id -> (* for error msg *)
204 term list -> (* original value, unchanged *)
205 term list -> (* original value, unchanged *)
206 Env.T (* return Env.T *)
208 fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
209 raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
210 | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
211 | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
212 if type_of f = type_of a
213 then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
215 let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
216 in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
218 (*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->
219 term list -> term list -> Env.T;
220 (*#------------------- un-hide local of init_pstate -----------------------------------------/*)
222 (*//------------------ step into init_pstate NEW -------------------------------------------\\*)
223 val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
224 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
225 (ctxt, I_Model.OLD_to_TEST i_model, met_id);
226 val (model_patt, program, prog, prog_rls, where_, where_rls) =
227 case MethodC.from_store ctxt met_id of
228 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
229 (model_patt, program, prog, prog_rls, where_, where_rls)
230 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
232 val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
233 val actuals = map snd env_model
234 (*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
236 val formals = Program.formal_args prog
237 (*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
239 (*+*)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})" =
240 (prog |> UnparseC.term @{context})
242 val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
244 (*||------------------ continue init_pstate NEW --------------------------------------------\\*)
245 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
246 val ist = Istate.e_pstate
247 |> Istate.set_eval prog_rls
248 |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);
249 (*+*) (relate_args [] formals actuals ctxt prog met_id formals actuals);
250 (*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =
251 (relate_args [] formals actuals ctxt prog met_id formals actuals)
252 |> Subst.to_string @{context}
254 val return_init_pstate_steps = (* = return_init_pstate*)
255 (Istate.Pstate ist, ctxt, program)
256 (*\\------------------ step into init_pstate NEW -------------------------------------------//*)
257 val (is, env, ctxt, prog) = return_init_pstate;
259 (*|------------------- continuing Specify_Method ---------------------------------------------*)
260 (*\------------------- step into Specify_Method --------------------------------------------//*)
261 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
263 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac
265 (*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);
266 (*/------------------- step into Apply_Method ----------------------------------------------\\*)
267 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
268 (p ,((pt, e_pos'), []));
269 (*if*) Pos.on_calc_end ip (*else*);
270 val (_, probl_id, _) = Calc.references (pt, p);
272 (*case*) tacis (*of*);
273 (*if*) probl_id = Problem.id_empty (*else*);
275 Step.switch_specify_solve p_ (pt, ip);
276 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
278 (*if*) Pos.on_specification ([], state_pos) (*else*);
280 LI.do_next (pt, input_pos);
281 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
282 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
283 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
285 val return_LI_find_next_step = (*case*)
286 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
287 (*//------------------ step into LI.find_next_step -----------------------------------------\\*)
288 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
289 (sc, (pt, pos), ist, ctxt);
290 (*.. this showed that we have ContextC.empty*)
291 (*\\------------------ step into LI.find_next_step -----------------------------------------//*)
292 val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
294 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
295 "~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
296 = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
297 val pos = next_in_prog' pos
299 val (pos', c, _, pt) =
300 Solve_Step.add_general tac_ ic (pt, pos);
301 "~~~~~ fun add_general , args:"; val (tac, ic, cs)
302 = (tac_, ic, (pt, pos));
303 (*if*) Tactic.for_specify' tac (*else*);
305 Solve_Step.add tac ic cs;
306 "~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
308 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
309 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
310 val pt = Ctree.update_branch pt p Ctree.TransitiveB
313 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
314 (*\------------------- step into Apply_Method ----------------------------------------------//*)
315 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set
317 (* final test ... ----------------------------------------------------------------------------*)
318 (*+*)val ([2], Res) = p;
319 Test_Tool.show_pt_tac pt; (*[
320 ([], Frm), solve (x + 1 = 2, x)
321 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
322 ([1], Frm), x + 1 = 2
323 . . . . . . . . . . Rewrite_Set "norm_equation",
324 ([1], Res), x + 1 + - 1 * 2 = 0
325 . . . . . . . . . . Rewrite_Set "Test_simplify",
326 ([2], Res), - 1 + x = 0
327 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT