1 (* Title: "Minisubplb/400-start-meth-subpbl.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
5 ATTENTION: THE FILE IS TOO BIG FOR Java BUFFERS, so copy in pieces.
18 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
19 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
20 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
21 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
23 ("Test", ["sqroot-test", "univariate", "equation", "test"],
24 ["Test", "squ-equ-test-subpbl1"]);
25 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Find "solutions x_i" = nxt;
41 val return_Add_Find = me nxt p [] pt;
42 (*/------------------- step into me Add_Find ------------------------------------------------\*)
43 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
44 val ctxt = Ctree.get_ctxt pt p
45 val ("ok", (_, _, ptp as (pt, p))) =
46 (*case*) Step.by_tactic tac (pt, p) (*of*);
49 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
50 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
51 (p, ((pt, Pos.e_pos'), []));
52 (*if*) Pos.on_calc_end ip (*else*);
53 val (_, probl_id, _) = Calc.references (pt, p);
55 (*case*) tacis (*of*);
56 (*if*) probl_id = Problem.id_empty (*else*);
58 switch_specify_solve p_ (pt, ip);
59 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
60 (*if*) Pos.on_specification ([], state_pos) (*then*);
62 specify_do_next (pt, input_pos);
63 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
66 Specify.find_next_step ptp;
67 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
69 (*+isa* )val Refine_Problem ["LINEAR", "univariate", "equation", "test"] = tac;( **)
70 (*+isa2*)val Specify_Theory "Test" = tac;(**)
72 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
73 spec = refs, ...} = Calc.specify_data (pt, pos); (*I_Model.T------------------^^^*)
74 val ctxt = Ctree.get_ctxt pt pos;
75 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
76 (*if*) p_ = Pos.Pbl (*then*);
78 val return_for_problem as (_, (_, xxx)) =
79 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
80 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
81 (ctxt, oris, (o_refs, refs), (pbl, met));
82 val cpI = if pI = Problem.id_empty then pI' else pI;
83 val cmI = if mI = MethodC.id_empty then mI' else mI;
84 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
85 val {model = mpc, ...} = MethodC.from_store ctxt cmI
88 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
90 (*+*)val [(true, xxx)] = xxxxx;
91 (*+*)if (xxx |> UnparseC.term @{context}) =
92 "matches (x = 0) (- 1 + x = 0) \<or>\n" ^
93 "matches (?b * x = 0) (- 1 + x = 0) \<or>\n" ^
94 "matches (?a + x = 0) (- 1 + x = 0) \<or>\n" ^
95 "matches (?a + ?b * x = 0) (- 1 + x = 0)"
96 then () else error "pre-cond, to be evaluated, CHANGED";
98 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
99 (ctxt, where_rls, where_, (pbt, pbl)); (*..delete double above --- adhoc inserted n ---*)
101 val (env_model, (env_subst, env_eval)) =
102 make_environments model_patt i_model;
103 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
105 (*+*)(pbt |> Model_Pattern.to_string @{context}) = "[\"" ^
106 "(#Given, (equality, e_e))\", \"" ^
107 "(#Given, (solveFor, v_v))\", \"" ^
108 "(#Find, (solutions, v_v'i'))\"]";
109 (*+*)(( pbl) |> I_Model.to_string @{context}) = "[\n" ^
110 "(1, [1], true ,#Given, (Cor equality (- 1 + x = 0) ,(e_e, [- 1 + x = 0]), Position.T)), \n" ^
111 "(2, [1], true ,#Given, (Cor solveFor x ,(v_v, [x]), Position.T)), \n" ^
112 "(3, [1], true ,#Find, (Cor solutions x_i ,(v_v'i', [x_i]), Position.T))]";
115 map (fn (_, variants, _, _, _) => variants) i_model
118 val variants_separated = map (filter_variants' i_model) all_variants
119 val sums_corr = map (Model_Def.cnt_corrects) variants_separated
120 val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
121 val (_, max_variant) = hd (*..crude decision, up to improvement *)
122 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
124 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
125 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
126 val env_model = make_env_model equal_descr_pairs
127 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
129 val subst_eval_list =
130 make_envs_preconds equal_givens;
131 (*//------------------ step into make_envs_preconds ----------------------------------------\\*)
132 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
133 "~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (nth 1 equal_givens);
136 discern_feedback id feedb;
137 (*\\------------------ step into make_envs_preconds ----------------------------------------//*)
139 (*-------------------- continuing of_max_variant ---------------------------------------------*)
140 val (env_subst, env_eval) = split_list subst_eval_list
141 val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval))
142 (*\------------------- step into me Add_Find ------------------------------------------------/*)
143 val (p,_,f,nxt,_,pt) = return_Add_Find; (** )val Specify_Theory "Test" = nxt;( **)
145 (*isa* )val Empty_Tac = nxt;( **)
146 (*isa2*)val Specify_Theory "Test" = nxt;(**)
147 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (** )val Specify_Problem ["LINEAR", "univariate", "equation", "test"] = nxt;( **)
149 val return_Specify_Method
151 (*/------------------- step into me Specify_Problem -----------------------------------------\*)
152 (*\------------------- step into me Specify_Problem -----------------------------------------/*)
153 val (p,_,f,nxt,_,pt) = return_Specify_Method; val Specify_Method ["Test", "solve_linear"] = nxt;
155 val return_Specify_Method
157 (*/------------------- step into me Specify_Method ------------------------------------------\*)
158 (*\------------------- step into me Specify_Method ------------------------------------------/*)
159 val (p_return_Specify_Method,_,f,nxt,_,pt) = return_Specify_Method; val Apply_Method ["Test", "solve_linear"] = nxt;
161 val return_Apply_Method
162 = me nxt p_return_Specify_Method [] pt;
163 (*+*)val ([3], Pbl) = p;
164 (*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt not initialised by specify, PblObj{ctxt,...}" else ();
165 (*+*)if get_ctxt pt p_return_Specify_Method |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();
166 (*/------------------- step into me Apply_Method --------------------------------------------\*)
167 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p_return_Specify_Method, [], pt);
168 val ("ok", (_, _, (_, _))) = (*case*)
169 Step.by_tactic tac (pt, p) (*of*);
170 (*//------------------ step into by_tactic Apply_Method ------------------------------------\\*)
171 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
172 val Applicable.Yes tac' = (*case*) Step.check tac (pt, p) (*of*);
173 (*if*) Tactic.for_specify' tac'; (*else*)
175 Step_Solve.by_tactic tac' ptp;
176 "~~~~~ fun by_tactic , args:"; val (tac as Tactic.Apply_Method' _, ptp as (pt, p))
179 (*+*)val PblObj {ctxt, ...} = get_obj I pt [3];
180 (*+isa==isa2*)ContextC.get_assumptions ctxt = [];
181 (*+isa==isa2*)(Ctree.get_assumptions pt p |> map (UnparseC.term @{context})) = [];
183 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
184 "~~~~~ fun by_tactic , args:"; val (Tactic.Apply_Method' (mI, _, _, _), (_, ctxt), (pt, (pos as (p, _))))
185 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), (pt, p));
187 (*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
188 (*+*) = ["precond_rootmet x"]
189 (*+*)then () else error "assumptions 7 from Apply_Method'";
192 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
193 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
194 => (itms, oris, probl, o_spec, spec)
195 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj";
197 (*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
198 (*+*) = ["precond_rootmet x"]
199 (*+*)then () else error "assumptions 8";
201 val (_, pI', _) = References.select_input o_spec spec
202 val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
203 val prog_rls = LItool.get_simplifier (pt, pos)
205 val (is, env, ctxt, prog) = case
206 LItool.init_pstate ctxt itms mI of
207 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
208 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate";
210 (*+*)(ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
211 (*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"];
213 val ini = LItool.implicit_take ctxt prog env;
214 val pos = start_new_level pos
217 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
218 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
220 (*+*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
221 (*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]
222 (*+*)then () else error "assumptions 9";
224 val return = ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)));
225 "~~~~~ from LI.by_tactic to..to me return"; val ("ok", (_, _, ptp)) = return;
227 (*\\------------------ step into by_tactic Apply_Method ------------------------------------//*)
229 (*|------------------- continue me Applythod ------------------------------------------------|*)
231 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
232 (*//------------------ step into do_next ---------------------------------------------------\\*)
233 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
234 = (p, ((pt, Pos.e_pos'), []));
235 (*if*) Pos.on_calc_end ip (*else*);
236 val (_, probl_id, _) = Calc.references (pt, p);
238 (*case*) tacis (*of*);
239 (*if*) probl_id = Problem.id_empty (*else*);
241 switch_specify_solve p_ (pt, ip);
242 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
244 (*if*) Pos.on_specification ([], state_pos) (*else*);
246 LI.do_next (pt, input_pos);
247 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
248 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
249 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
250 val Next_Step (ist, ctxt, tac) =
251 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
253 val continue_do_next = (ist, ctxt, tac, ptp)(*keep for continuing LI.do_next*);
254 (*///----------------- step into find_next_step -------------------------------------------\\\*)
255 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) =
256 (sc, (pt, pos), ist, ctxt);
258 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
259 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
260 ((prog, (ptp, ctxt)), (Pstate ist));
261 (*if*) path = [] (*then*);
263 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
264 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) =
265 (cc, (trans_scan_dn ist), (Program.body_of prog));
267 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
268 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a)) =
269 (cc, (ist |> path_down [L, R]), e);
271 scan_dn cc (ist |> path_down_form ([L, R], a)) e;
272 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =
273 (cc, (ist |> path_down_form ([L, R], a)), e);
275 (*case*) scan_dn cc (ist |> path_down [L, R]) e1 (*of*);
276 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) =
277 (cc, (ist |> path_down [L, R]), e1);
278 (*if*) Tactical.contained_in t (*else*);
279 val (Program.Tac prog_tac, form_arg) =
280 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
282 check_tac cc ist (prog_tac, form_arg);
283 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
284 (cc, ist, (prog_tac, form_arg));
287 LItool.tac_from_prog (pt, p) prog_tac;
288 "~~~~~ fun tac_from_prog , args:"; val (_, _, (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _)) =
289 ((pt, p), (Proof_Context.theory_of ctxt), prog_tac);
291 Subst.program_to_input ctxt sub
292 (*-------------------- stop step into find_next_step -----------------------------------------*)
293 (*\\\----------------- step into find_next_step -------------------------------------------///*)
294 (*kept for continuing LI.do_next*)val (ist, ctxt, tac, ptp) = continue_do_next;
296 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
297 "~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos) (*fall through*)) =
298 (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
299 val pos = next_in_prog' pos
301 val (pos', c, _, pt) =
302 Solve_Step.add_general tac_ ic (pt, pos);
303 "~~~~~ fun add_general , args:"; val (tac, ic, cs) = (tac_, ic, (pt, pos));
304 (*if*) Tactic.for_specify' tac (*else*);
307 "~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))), (is, ctxt), (pt, (p, _))) =
310 Ctree.cappend_atomic pt p (is, ctxt) f
311 (Tactic.Rewrite_Set_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')) (f', asm) Ctree.Complete;
312 "~~~~~ fun cappend_atomic , args:"; val (pt, p, ic_res, f, r, f', s) =
313 (pt, p, (is, ctxt), f,
314 (Tactic.Rewrite_Set_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')), (f', asm), Ctree.Complete);
315 Subst.T_to_input ctxt subs';
317 "~~~~~ from fun switch_specify_solve \<longrightarrow>fun Step.do_next \<longrightarrow>fun me , return:"; val (_, ts)
318 = (LI.do_next (pt, input_pos));
319 (*-------------------- stop step into do_next ------------------------------------------------*)
320 (*\\------------------ step into do_next ---------------------------------------------------//*)
321 (*\------------------- step into me Apply_Method --------------------------------------------/*)
322 val (p_return_Apply_Method,_,f,nxt,_,pt) = return_Apply_Method;
323 val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = nxt;
325 val (p,_,f,nxt,_,pt) = me nxt p_return_Apply_Method [] pt; val Rewrite_Set "Test_simplify" = nxt;
327 (* final tests ... ---------------------------------------------------------------------------*)
328 val ([3, 1], Frm) = p_return_Apply_Method;
329 val "Rewrite_Set \"Test_simplify\"" = Tactic.input_to_string ctxt nxt;
331 (*p_frm BEFORE Apply_Method at Subproblem*)
332 val p_frm = ([3], Frm);
333 val ["precond_rootmet x"] = Ctree.get_assumptions pt p_frm |> map (UnparseC.term @{context});
335 (*assumptions<>[] before Apply_Method of Subproblem*)
336 val ([3], Met) = p_return_Specify_Method;
337 val [(*--- inserted by Apply_Method ---*)] = Ctree.get_assumptions pt p_return_Specify_Method;
339 (*FALSE: 2 assumptions recorded Apply_Method of Subproblem*)
340 val ([3, 1], Frm) = p_return_Apply_Method;
341 val ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"] =
342 Ctree.get_assumptions pt p_return_Apply_Method |> map (UnparseC.term @{context});
344 (*p_res AFTER Apply_Method at Subproblem*)
345 val p_res = ([3], Res);
346 val ["precond_rootmet x"] = Ctree.get_assumptions pt p_res |> map (UnparseC.term @{context});