1 (* Title: "Minisubpbl/250-Rewrite_Set-from-method.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
7 "----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
8 "----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
21 (*[1], Frm*)val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
23 (*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
24 1 relevant for original decomposition *)
25 (*[1], Res*)val (p'''_',_,f,nxt'''_',_,pt'''_') = me nxt'''' p'''' [] pt'''';(*nxt = Rewrite_Set "Test_simplify"*)
27 if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2" andalso fst nxt'''' = "Rewrite_Set"
28 then () else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
30 (* val (p,_,f,nxt,_,pt) = ERROR WAS: nxt = ("Empty_Tac",..*) me nxt p [] pt;
31 (* ERROR WAS: assy: call by ([3], Pbl) *)
32 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
34 (*ERROR WAS: assy: call by ([3], Pbl)*)
35 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
36 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
37 val (mI, m) = Solve.mk_tac'_ tac;
38 val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
39 member op = Solve.specsteps mI (* = false*);
41 loc_solve_ (mI,m) ptp ; (* assy: call by ([3], Pbl)*)
42 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = ((mI,m), ptp);
43 Solve.solve m (pt, pos); (* assy: call by ([3], Pbl)*)
44 (* step somewhere within a calculation *)
45 "~~~~~ fun solve, args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
46 Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
47 val thy' = get_obj g_domID pt (par_pblobj pt p);
48 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
50 locate_input_tactic sc (pt, po) (fst is) (snd is) m; (* assy: call by ([3], Pbl)*)
51 "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
52 = (sc, (pt, po), (fst is), (snd is), m);
53 val srls = get_simplifier cstate;
55 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
56 "~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))
57 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
58 (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
60 (*val Assoc (scrstate, steps) = in isabisacREP*)
61 (*ERROR assy: call by ([3], Pbl) in isabisac*)
62 assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],a,v,S,b), m) (Program.body_of sc);
64 (* checked all arguments of assy for equality: isabisac -- isabisacREP *)
65 "~~~~~ fun assy [1], args:"; val (ya, ((E,l,a,v,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
66 = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,S,b), m), (Program.body_of sc));
68 (*val Assoc (scrstate, steps) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac) e;
69 "~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss),
70 (Const ("Tactical.Seq"(*1*),_) $e1 $ e2 $ a)) =
71 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), tac), e);
73 (*val Assoc (scrstate, steps) = in isabisacREP*)
74 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
75 (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*);
76 "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
77 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
79 term2str e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
80 term2str e1 = "Try (Rewrite_Set norm_equation)" (*in isabisacREP*);
81 termopt2str a = "(SOME e_e)" (*in isabisac + isabisacREP*);
83 (*val Assoc (scrstate, steps) = in isabisacREP*)
84 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
85 assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e ;
86 (*======= end of scanning tacticals, a leaf =======*)
87 "~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) =
88 (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
89 val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*);
91 (*val Ass (m,v') = in isabisacREP*)
92 (*val NotAss = in isabisac*)
93 (*case*) associate pt ctxt (m, stac) (*of*);
94 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
95 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
97 if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
99 "~~~~~ continue me[1] after locatetac";
100 val (pt, p) = ptp''''';
101 (* isabisac17: val ("helpless", _) = (*case*) step p ((pt, Ctree.e_pos'),[]) (*of*)*)
102 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
103 val pIopt = get_pblID (pt,ip);
104 (*if*) ip = ([], Ctree.Res) = false;
105 val _ = (*case*) tacis (*of*);
106 (*if*) ip = p = false;
107 (*if*) member op = [Pbl, Met] p_ = false;
109 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
110 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
111 val thy' = get_obj g_domID pt (par_pblobj pt p);
112 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
114 (* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
116 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)),
117 (Pstate (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
118 (*if*) l = [] = false;
120 (* isabisac17: nstep_up thy ptp sc E l Skip_ a v ERROR go: no [L,L,R] *)
121 (* isabisac15: val Appy (tac_, scrstate) = nstep_up thy ptp sc E l Skip_ a v *)
122 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
123 (thy, ptp, sc, E, l, Skip_, a, v);
125 val up = drop_last l;
127 if up = [R, L, R, L, L, R] then () else error "250-Rewrite_Set: nstep_up CHANGED";
128 (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*)
129 (*isabisac17: (go up sc) ERROR go: no [L,L,R]*)
131 val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls) = (go up sc)
132 val (Const ("Tactical.Try"(*2*), _) $ _) = ttt;
133 if term2str ttt = "Try (Rewrite_Set ''norm_equation'')"
134 then () else error "250-Rewrite_Set: (go up sc) CHANGED";
136 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*2*), _) $ _), a, v) =
137 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v );
139 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
141 (* nxt'''_' = Rewrite_Set "Test_simplify"
142 //--2 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
143 2 relevant for exception TERM raised (line 297 of "term.ML"): dest_Free -1 + x = 0 *)
144 (**)val (p,_,f,nxt,_,pt) = me nxt'''_' p'''_' [] pt'''_';(**)
145 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
147 (*locatetac is here for testing by me; step would suffice in me*)
148 case locatetac tac (pt, p) of
149 ("ok", (_, _, ptp)) => ptp
150 | ("unsafe-ok", (_, _, ptp)) => ptp
151 | ("not-applicable",_) => (pt, p)
152 | ("end-of-calculation", (_, _, ptp)) => ptp
153 | ("failure", _) => error "sys-error"
154 | _ => error "me: uncovered case"
156 (*case*) step p ((pt, Ctree.e_pos'), []) (*of*);
157 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis))
158 = (p, ((pt, Ctree.e_pos'), []));
159 val pIopt = get_pblID (pt,ip);
160 (*if*) ip = ([], Ctree.Res) (*else*);
161 val _ = (*case*) tacis (*of*);
162 val SOME _ = (*case*) pIopt (*of*);
163 (*if*) member op = [Ctree.Pbl, Ctree.Met] p_
164 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
166 do_solve_step (pt, ip);
167 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
168 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
169 val thy' = get_obj g_domID pt (par_pblobj pt p);
170 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
172 (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
173 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))
174 = ((thy', srls), (pt, pos), sc, is);
176 (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);
177 "~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (E, l, a, v, _, _)))
178 = (thy, ptp, sc, (Istate.Pstate (E,l,a,v,s,false)));
179 (*if*) l = [] (*else*);
181 nstep_up thy ptp sc E l Skip_ a v;
182 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
183 = (thy, ptp, sc, E, l, Skip_, a, v);
184 (*if*) 1 < length l (*then*);
185 val up = drop_last l;
187 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
188 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*1*),_) $ _ ), a, v)
189 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
191 nstep_up thy ptp scr E l Skip_ a v;
192 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
193 = (thy, ptp, scr, E, l, Skip_, a, v);
194 (*if*) 1 < length l (*then*);
195 val up = drop_last l;
197 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
198 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Tactical.Seq"(*2*), _) $ _ $ _), a, v)
199 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
201 nstep_up thy ptp scr E l ay a v;
202 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
203 = (thy, ptp, scr, E, l, ay, a, v);
204 (*if*) 1 < length l (*then*);
205 val up = drop_last l;
207 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
208 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _), a, v)
209 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
211 nstep_up thy ptp scr E l ay a v;
212 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
213 = (thy, ptp, scr, E, l, ay, a, v);
214 (*if*) 1 < length l (*then*);
215 val up = drop_last l;
217 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
218 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("HOL.Let", _) $ _), a, v)
219 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
220 (*if*) ay = Napp_ (*else*);
224 Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
225 | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))
226 val i = TermC.mk_Free (i, T)
227 val E = Env.upd_env E (i, v);
229 (*case*) appy thy ptp E (up @ [Celem.R, Celem.D]) body a v (*of*);
230 "~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v)
231 = (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v);
233 (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*);
234 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v)
235 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
236 val (a', STac stac) = (*case*) Lucin.handle_leaf "next " th sr (E, (a, v)) t (*of*);
238 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac;
239 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
240 = (pt, (Celem.assoc_thy th), stac);
241 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
242 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
243 val ags = TermC.isalist2list ags';
244 (*if*) mI = ["no_met"] (*else*);
246 (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
247 handle ERROR "actual args do not match formal args"
248 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)
249 val (fmz_, vals) = Chead.oris2fmz_vals pors;
250 val {cas,ppc,thy,...} = Specify.get_pbt pI
251 val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
252 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
253 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);
254 (*\\--2 end step into relevant call ----------------------------------------------------------//*)
256 if p = ([2], Res) andalso f2str f = "-1 + x = 0" then
258 ("Subproblem", Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
259 | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
260 else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
262 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)