1 (* Title: "Minisubpbl/300-init-subpbl.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
10 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
11 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
12 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
13 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
15 ("Test", ["sqroot-test", "univariate", "equation", "test"],
16 ["Test", "squ-equ-test-subpbl1"]);
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
25 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "norm_equation" = nxt;
26 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "Test_simplify" = nxt;
28 (*[2], Res*)val return_Rewrite_Set_Test_simplify = me nxt p [] pt;
29 (*/------------------- step into me_Rewrite_Set_Test_simplify ------------------------------\\*)
30 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
31 val ctxt = Ctree.get_ctxt pt p
32 val ("ok", (_, _, ptp as (pt, p))) =
33 (*case*) Step.by_tactic tac (pt, p) (*of*);
36 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
37 (*//------------------ step into do_next ---------------------------------------------------\\*)
38 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
39 (p, ((pt, Pos.e_pos'), []));
40 (*if*) Pos.on_calc_end ip (*else*);
41 val (_, probl_id, _) = Calc.references (pt, p);
43 (*case*) tacis (*of*);
44 (*if*) probl_id = Problem.id_empty (*else*);
46 switch_specify_solve p_ (pt, ip);
47 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
48 (*if*) Pos.on_specification ([], state_pos) (*else*);
50 LI.do_next (pt, input_pos);
51 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
52 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
53 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
56 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
57 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) =
58 (sc, (pt, pos), ist, ctxt);
59 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
60 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
61 ((prog, (ptp, ctxt)), (Pstate ist));
62 (*if*) path = [] (*else*);
64 go_scan_up (prog, cc) (trans_scan_up ist);
65 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
66 ((prog, cc), (trans_scan_up ist));
67 (*if*) path = [R] (*root of the program body*) (*else*);
69 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
70 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _)) =
71 (pcc, (ist |> path_up), (go_up ctxt path sc));
74 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
76 (*if*) path = [R] (*root of the program body*) (*else*);
78 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
79 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _)) =
80 (pcc, (ist |> path_up), (go_up ctxt path sc));
83 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
85 (*if*) path = [R] (*root of the program body*) (*else*);
87 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
88 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _)) =
89 (pcc, (ist |> path_up), (go_up ctxt path sc));
92 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
94 (*if*) path = [R] (*root of the program body*) (*else*);
96 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
97 "~~~~~ and scan_up , args:"; val (pcc as (sc, cc as (_, ctxt)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _)) =
98 (pcc, (ist |> path_up), (go_up ctxt path sc));
99 val (i, body) = check_Let_up ctxt ist sc;
101 (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
102 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) =
103 (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
105 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
106 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) =
107 (cc, (ist |> path_down [L, R]), e);
108 (*+*)val "SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]" =
109 (*+*) UnparseC.term @{context} e;
110 (*if*) Tactical.contained_in t (*else*);
111 val (Program.Tac prog_tac, form_arg) =
112 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
114 check_tac cc ist (prog_tac, form_arg);
115 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
116 (cc, ist, (prog_tac, form_arg));
119 LItool.tac_from_prog (pt, p) prog_tac;
120 "~~~~~ fun tac_from_prog , args:"; val ((pt, p), _, (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
121 ((pt, p), (Proof_Context.theory_of ctxt), prog_tac);
124 (Sub_Problem.tac_from_prog (pt, p) ptac);
125 "~~~~~ fun tac_from_prog , args:"; val ((pt, p), (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags')) =
127 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
128 val thy = Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
129 val init_ctxt = Proof_Context.init_global thy
130 val ags = TermC.isalist2list ags';
135 val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
136 handle ERROR "actual args do not match formal args"
137 => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
138 val pI' = Refine.by_o_model' init_ctxt pors pI;
139 in (pI', pors (* refinement over models with diff.prec only *),
140 (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
141 else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
142 handle ERROR "actual args do not match formal args"
143 => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
144 val (fmz_, vals) = O_Model.values' init_ctxt pors;
145 val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
146 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
147 val dI = Context.theory_name
148 (Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
149 val ctxt = ContextC.init_for_prog init_ctxt vals
150 (*-------------------- stop step into do_next ------------------------------------------------*)
151 (*\\------------------ step into do_next ---------------------------------------------------//*)
152 (*\------------------- step into me_Rewrite_Set_Test_simplify ------------------------------//*)
153 (*[2], Res*)val (p,_,f,nxt,_,pt) = return_Rewrite_Set_Test_simplify;
154 val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
155 (*[3], Pbl*)val return_me_Model_Problem_sub = me nxt p [] pt;
156 (*/------------------- step into me_Model_Problem_sub -------------------------------------\\*)
157 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
159 (*ERROR: Specify_Step.check Model_Problem: uncovered case Ctree.get_obj*)
160 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
161 Step.by_tactic tac (pt, p) (*of*);
162 (*//------------------ step into by_tactic Subproblem --------------------------------------\\*)
163 (*+*)get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
165 "~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt, p));
166 val Applicable.Yes m = Step.check tac (pt, p);
167 (*if*) Tactic.for_specify' m; (*false*)
170 Step_Solve.by_tactic m (pt, p);
171 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
172 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
173 val thy' = get_obj g_domID pt (par_pblobj pt p);
174 val (is, sc) = resume_prog (p,p_) pt;
176 val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =
177 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
178 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog prog, cstate, istate, ctxt, tac)
179 = (sc, (pt, po), (fst is), (snd is), m);
181 (** )val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = ( *case*)
182 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
183 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Pstate (ist as {path, ...})))
184 = ((prog, (cstate, ctxt, tac)), istate);
185 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
187 go_scan_up1 (prog, cctt) ist;
188 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, act_arg, ...}))
189 = ((prog, cctt), ist);
190 (*if*) 1 < length path (*true*);
192 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
193 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
194 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
196 go_scan_up1 pcct ist;
197 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
199 (*if*) 1 < length path (*true*);
201 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
202 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
203 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
205 go_scan_up1 pcct ist (*2*: comes from e2*);
206 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
208 (*if*) 1 < length path (*true*);
210 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
211 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ _ $ _ $ _))
212 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
214 go_scan_up1 pcct ist (*all has been done in (*2*) below*);
215 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
217 (*if*) 1 < length path (*true*);
219 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
220 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, ctxt, _))), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
221 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
222 val (i, body) = check_Let_up ctxt ist prog;
224 (*case*) scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);
225 "~~~~~ fun scan_dn1 , args:"; val (cct, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
226 = (cct, (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef), body);
228 (*case*) scan_dn1 cct (ist |> path_down [L, R]) e (*of*);
229 (*======= end of scanning tacticals, a leaf =======*)
230 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
231 = (cct, (ist |> path_down [L, R]), e);
233 val (Program.Tac _, NONE) = (*case*)
234 check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
235 "~~~~~ fun check_leaf , args:"; val (call, thy, prog_rls, (E, (a, v)), t)
236 = ("locate", ctxt, eval, (get_subst ist), t);
238 val (Program.Tac stac, a) = (*case*) Prog_Tac.eval_leaf E a v t (*of*);
239 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>SubProblem\<close>, _) $ _ $ _)))
242 (Program.Tac (subst_atomic E t), NONE); (*return value*)
243 "~~~~~ from fun eval_leaf \<longrightarrow> fun check_leaf return val:"; val ((Program.Tac stac, a'))
244 = ((Program.Tac (subst_atomic E t), NONE : term option));
246 Rewrite.eval_prog_expr ctxt prog_rls
247 (subst_atomic (Env.update_opt E (a,v)) stac);
249 (Program.Tac stac', a'); (*return from check_leaf*)
250 "~~~~~ from fun check_leaf \<longrightarrow> fun scan_dn1 return val:"; val (Program.Tac prog_tac, form_arg)
251 = (Program.Tac stac', a' : term option);
253 (Program.Tac prog_tac, form_arg) (*return from check_leaf*);
255 check_tac1 cct ist (prog_tac, form_arg) (*return from scan_dn1*);
256 "~~~~~ from fun scan_dn1\<longrightarrow>fun scan_up1 HOL.Let(*1*), return:"; val (Accept_Tac1 iss)
257 = (check_tac1 cct ist (prog_tac, form_arg));
259 (*+*)val (pstate, ctxt, tac) = iss;
260 (*+*)if ContextC.is_empty ctxt then error "ERROR: scan_dn1 should NOT return ContextC.empty" else ();
261 "~~~~~ from fun scan_up1 HOL.Let(*1*), --------------------------------- NO return:"; val () = ();
263 (*+*)if ContextC.is_empty ctxt''''' then error "locate_input_tactic should NOT return ContextC.empty" else ();
265 "~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac))
266 = (Safe_Step (Pstate ist''''', ctxt''''', tac'_'''''));
267 val p' = next_in_prog po
269 val (p'', _, _,pt') =
270 Step.add tac (istate, ctxt) (pt, (p', p_));
271 "~~~~~ fun add , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
272 (l as (_, ctxt)), (pos as (p, p_)), pt)
273 = (@{theory}(*ThyC.get_theory @{context} "Isac_Knowledge"*), tac, (istate, ctxt), (p', p_), pt);
274 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
275 (oris, (domID, pblID, metID), hdl, ctxt_specify);
277 (*+*)if ContextC.is_empty ctxt_specify then error "ERROR: Step.add should NOT get input ContextC.empty" else ();
278 (*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "Step.add MUST store ctxt"
280 (*\\------------------ step into by_tactic Subproblem -------------------------------------//*)
281 (*\------------------- step into me_Model_Problem_sub --------------------------------------//*)
282 val (p,_,f,nxt,_,pt) = return_me_Model_Problem_sub; val Model_Problem = nxt;
284 (* final test ... ----------------------------------------------------------------------------*)
285 if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty)
286 then () else error "Minisubpbl/300-init-subpbl.sml changed";
288 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "equality (- 1 + x = 0)" = nxt