funpack: failed trial to generalise handling of meths which extend the model of a probl
1 (* Title: test/../script.sml
2 Author: Walther Neuper 050908
3 (c) copyright due to lincense terms.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "----------- fun sel_appl_atomic_tacs ----------------------------";
9 "----------- fun init_form, fun get_stac -------------------------";
10 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
11 "----------- Take as 1st stac in script --------------------------";
12 "----------- 'trace_script' from outside 'fun me '----------------";
13 "----------- fun sel_rules ---------------------------------------";
14 "----------- fun sel_appl_atomic_tacs ----------------------------";
15 "----------- fun de_esc_underscore -------------------------------";
16 "----------- fun go ----------------------------------------------";
17 "----------- fun formal_args -------------------------------------";
18 "----------- fun dsc_valT ----------------------------------------";
19 "----------- fun itms2args ---------------------------------------";
20 "----------- fun rep_tac_ ----------------------------------------";
21 "----------- fun init_scrstate -----------------------------------------------------------------";
22 "-----------------------------------------------------------------";
23 "-----------------------------------------------------------------";
24 "-----------------------------------------------------------------";
26 val thy = @{theory Isac};
28 "----------- fun sel_appl_atomic_tacs ----------------------------";
29 "----------- fun sel_appl_atomic_tacs ----------------------------";
30 "----------- fun sel_appl_atomic_tacs ----------------------------";
33 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
34 ("Test", ["sqroot-test","univariate","equation","test"],
35 ["Test","squ-equ-test-subpbl1"]))];
38 autoCalculate 1 CompleteCalcHead;
39 autoCalculate 1 (Step 1);
40 autoCalculate 1 (Step 1);
41 val ((pt, p), _) = get_calc 1; show_pt pt;
42 val appltacs = sel_appl_atomic_tacs pt p;
44 [Rewrite ("radd_commute", radd_commute),
45 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
46 => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
47 (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
48 else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
49 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
52 trace_script := false;
53 applyTactic 1 p (hd appltacs);
54 val ((pt, p), _) = get_calc 1; show_pt pt;
55 val appltacs = sel_appl_atomic_tacs pt p;
56 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
58 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
59 val ((pt, _), _) = get_calc cI;
64 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
65 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
66 val (mI,m) = mk_tac'_ tac;
67 applicable_in p pt m ; (*Appl*)
68 member op = specsteps mI; (*false*)
69 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
70 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
71 (*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
72 (mI,m); (*string * tac*)
74 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
75 (*val (msg, cs') = solve m (pt, pos);
76 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
79 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
80 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
82 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
83 val ctxt = get_ctxt pt po;
85 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
86 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
87 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
90 autoCalculate 1 CompleteCalc;
92 "----------- fun init_form, fun get_stac -------------------------";
93 "----------- fun init_form, fun get_stac -------------------------";
94 "----------- fun init_form, fun get_stac -------------------------";
95 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
96 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
97 ["Test","squ-equ-test-subpbl1"]);
98 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
99 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
106 "~~~~~ fun me, args:"; val (_,tac) = nxt;
107 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
108 val (mI,m) = mk_tac'_ tac;
109 val Appl m = applicable_in p pt m;
110 member op = specsteps mI; (*false*)
111 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
112 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
113 val {srls, ...} = get_met mI;
114 val PblObj {meth=itms, ...} = get_obj I pt p;
115 val thy' = get_obj g_domID pt p;
116 val thy = assoc_thy thy';
117 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
118 val ini = init_form thy sc env;
119 "----- fun init_form, args:"; val (Prog sc) = sc;
120 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
121 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
122 | _ => error "script: Const (?, ?) in script (as term) changed";;
125 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
126 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
127 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
128 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
130 ("Test", ["sqroot-test","univariate","equation","test"],
131 ["Test","squ-equ-test-subpbl1"]);
132 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
142 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
144 "~~~~~ fun me, args:"; val (_,tac) = nxt;
145 val (pt, p) = case locatetac tac (pt,p) of
146 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
147 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
148 val pIopt = get_pblID (pt,ip); (*SOME ["LINEAR", "univariate", "equation", "test"]*)
150 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
151 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
152 (*WAS stac2tac_ TODO: no match for SubProblem*)
153 val thy' = get_obj g_domID pt (par_pblobj pt p);
154 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
155 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
156 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
157 l; (*= [R, L, R, L, R, R]*)
158 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
159 "~~~~~ dont like to go into nstep_up...";
160 val t = str2term ("SubProblem" ^
161 "(''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''], [''Test'', ''solve_linear''])" ^
162 "[BOOL (-1 + x = 0), REAL x]");
163 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
166 | _ => error "script.sml x+1=2 start SubProblem from script";
169 "----------- Take as 1st stac in script --------------------------";
170 "----------- Take as 1st stac in script --------------------------";
171 "----------- Take as 1st stac in script --------------------------";
172 val p = e_pos'; val c = [];
173 val (p,_,f,nxt,_,pt) =
175 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
176 ("Integrate", ["integrate","function"], ["diff","integration"]))];
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
178 val (p,_,f,nxt,_,pt) = me nxt p c pt;
179 val (p,_,f,nxt,_,pt) = me nxt p c pt;
180 val (p,_,f,nxt,_,pt) = me nxt p c pt;
181 val (p,_,f,nxt,_,pt) = me nxt p c pt;
182 val (p,_,f,nxt,_,pt) = me nxt p c pt;
183 val (p,_,f,nxt,_,pt) = me nxt p c pt;
184 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
185 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
186 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
188 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
189 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
190 val (mI,m) = mk_tac'_ tac;
191 val Appl m = applicable_in p pt m;
192 member op = specsteps mI (*false*);
193 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
194 "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
196 val {srls, ...} = get_met mI;
197 val PblObj {meth=itms, ...} = get_obj I pt p;
198 val thy' = get_obj g_domID pt p;
199 val thy = assoc_thy thy';
200 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
201 val ini = init_form thy sc env;
204 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
205 val d = e_rls (*FIXME: get simplifier from domID*);
206 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
207 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
208 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
209 val thy = assoc_thy thy';
210 l = [] orelse ((*init.in solve..Apply_Method...*)
211 (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
212 "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
213 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
214 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
215 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
216 "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
217 (ya, ((E , l@[L,R], a,v,S,b),ss), e);
218 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
219 (* val ctxt = get_ctxt pt (p,p_)
220 exception PTREE "get_obj: pos = [0] does not exist" raised
221 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
224 "----------- 'trace_script' from outside 'fun me '----------------";
225 "----------- 'trace_script' from outside 'fun me '----------------";
226 "----------- 'trace_script' from outside 'fun me '----------------";
227 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
229 ("Test", ["sqroot-test","univariate","equation","test"],
230 ["Test","squ-equ-test-subpbl1"]);
231 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
232 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
233 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
234 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
235 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
236 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
237 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
238 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
239 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
241 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
242 val (p'''', pt'''') = (p, pt);
243 f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";
244 val (p, p_) = p(* = ([1], Frm)*);
245 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
246 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
247 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
250 term2str res = "??.empty"; (* scrstate before starting interpretation *)
251 (*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)
253 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
254 val (p'''', pt'''') = (p, pt);
255 f2str f = "x + 1 + -1 * 2 = 0";
256 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
257 val (p, p_) = p(* = ([1], Res)*);
258 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
259 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
260 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
261 loc_ = [R, L, R, L, L, R, R];
262 curry_arg = SOME (str2term "e_e::bool");
263 term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)
264 term2str (go loc_ sc) = "Rewrite_Set norm_equation False";
266 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
267 val (p'''', pt'''') = (p, pt);
268 f2str f = "-1 + x = 0";
269 case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => ()
270 | _ => error "CHANGED";
271 val (p, p_) = p(* = ([2], Res)*);
272 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
273 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
274 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
275 loc_ = [R, L, R, L, R, R];
276 curry_arg = SOME (str2term "e_e::bool");
277 term2str res = "-1 + x = 0"; (* scrstate after Test_simplify, before Subproblem *)
278 term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";
280 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
281 val (p'''', pt'''') = (p, pt); (*f2str f = exception Match; ...is a model, not a formula*)
282 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
283 val (p'''', pt'''') = (p, pt);
284 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
285 val (p'''', pt'''') = (p, pt);
286 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
287 val (p'''', pt'''') = (p, pt);
288 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
289 val (p'''', pt'''') = (p, pt);
290 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
291 val (p'''', pt'''') = (p, pt);
292 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
293 val (p'''', pt'''') = (p, pt);
294 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)
295 (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
297 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
298 val (p'''', pt'''') = (p, pt);
299 f2str f = "-1 + x = 0";
300 case snd nxt of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => () | _ => error "CHANGED";
301 val (p, p_) = p(* = ([3, 1], Frm)*);
302 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
303 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
304 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
307 term2str res = "??.empty"; (* scrstate before starting interpretation *)
308 (*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)
310 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
311 val (p'''', pt'''') = (p, pt);
312 f2str f = "x = 0 + -1 * -1";
313 case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
314 val (p, p_) = p(* = ([3, 1], Res)*);
315 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
316 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
317 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
318 loc_ = [R, L, R, L, R, L, R];
319 curry_arg = SOME (str2term "e_e::bool");
320 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
321 term2str (go loc_ sc) = "Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False";
323 "----------- fun sel_rules ---------------------------------------";
324 "----------- fun sel_rules ---------------------------------------";
325 "----------- fun sel_rules ---------------------------------------";
326 (* compare test/../interface.sml
327 "--------- getTactic, fetchApplicableTactics ------------";
330 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
331 ("Test", ["sqroot-test","univariate","equation","test"],
332 ["Test","squ-equ-test-subpbl1"]))];
335 autoCalculate 1 CompleteCalc;
336 val ((pt,_),_) = get_calc 1;
339 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
340 val tacs = sel_rules pt ([],Pbl);
341 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
342 | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
344 val tacs = sel_rules pt ([1],Res);
345 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
346 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
347 Check_elementwise "Assumptions"] => ()
348 | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
350 val tacs = sel_rules pt ([3],Pbl);
351 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
352 | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
354 val tacs = sel_rules pt ([3,1],Res);
355 case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
356 | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
358 val tacs = sel_rules pt ([3],Res);
359 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
360 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
361 Check_elementwise "Assumptions"] => ()
362 | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
364 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
365 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
366 | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
368 "----------- fun sel_appl_atomic_tacs ----------------------------";
369 "----------- fun sel_appl_atomic_tacs ----------------------------";
370 "----------- fun sel_appl_atomic_tacs ----------------------------";
372 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
373 ("Test", ["sqroot-test","univariate","equation","test"],
374 ["Test","squ-equ-test-subpbl1"]))];
377 autoCalculate 1 CompleteCalc;
379 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
380 fetchApplicableTactics 1 99999 ([],Pbl);
382 fetchApplicableTactics 1 99999 ([1],Res);
383 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
384 val ((pt, _), _) = get_calc cI;
386 case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
387 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
388 Check_elementwise "Assumptions"] => ()
389 | _ => error "fetchApplicableTactics ([1],Res) changed";
392 sel_appl_atomic_tacs pt p;
394 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
395 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
398 "~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);
399 is_spec_pos p_ = false;
400 val pp = par_pblobj pt p
401 val thy' = (get_obj g_domID pt pp):theory'
402 val thy = assoc_thy thy'
403 val metID = get_obj g_metID pt pp
406 then (thd3 o snd3) (get_obj g_origin pt pp)
408 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
409 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
410 val alltacs = (*we expect at least 1 stac in a script*)
411 map ((stac2tac pt thy) o rep_stacexpr o #2 o
412 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
415 Frm => get_obj g_form pt p
416 | Res => (fst o (get_obj g_result pt)) p;
417 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
418 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
420 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
421 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
424 "----------- fun de_esc_underscore -------------------------------";
425 "----------- fun de_esc_underscore -------------------------------";
426 "----------- fun de_esc_underscore -------------------------------";
428 > val str = "Rewrite_Set_Inst";
429 > val esc = esc_underscore str;
430 val it = "Rewrite'_Set'_Inst" : string
431 > val des = de_esc_underscore esc;
432 val des = de_esc_underscore esc;*)
434 "----------- fun go ----------------------------------------------";
435 "----------- fun go ----------------------------------------------";
436 "----------- fun go ----------------------------------------------";
438 > val t = (Thm.term_of o the o (parse thy)) "a+b";
439 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
440 > val plus_a = go [L] t;
442 > val plus = go [L,L] t;
443 > val a = go [L,R] t;
445 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";
446 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
447 > val pl_pl_a_b = go [L] t;
449 > val a = go [L,R,L,R] t;
450 > val b = go [L,R,R] t;
453 "----------- fun formal_args -------------------------------------";
454 "----------- fun formal_args -------------------------------------";
455 "----------- fun formal_args -------------------------------------";
458 [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
459 Free ("eqs_","bool List.list")] : term list
461 "----------- fun dsc_valT ----------------------------------------";
462 "----------- fun dsc_valT ----------------------------------------";
463 "----------- fun dsc_valT ----------------------------------------";
464 (*> val t = (Thm.term_of o the o (parse thy)) "equality";
466 val T = "bool => Tools.una" : typ
467 > val dsc = dsc_valT t;
468 val dsc = "una" : string
470 > val t = (Thm.term_of o the o (parse thy)) "fixedValues";
472 val T = "bool List.list => Tools.nam" : typ
473 > val dsc = dsc_valT t;
474 val dsc = "nam" : string*)
475 "----------- fun itms2args ---------------------------------------";
476 "----------- fun itms2args ---------------------------------------";
477 "----------- fun itms2args ---------------------------------------";
479 > val sc = ... Solve_root_equation ...
480 > val mI = ("Script","sqrt-equ-test");
481 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
482 > val ts = itms2args thy mI itms;
483 > map (term_to_string''' thy) ts;
484 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
486 "----------- fun rep_tac_ ----------------------------------------";
487 "----------- fun rep_tac_ ----------------------------------------";
488 "----------- fun rep_tac_ ----------------------------------------";
489 (***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
491 (a)----- als String zusammensetzen:
493 val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
495 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
497 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
498 > val tt = (Thm.term_of o the o (parse thy))
499 "(Rewrite_Inst[(''bdv'',x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
501 ML> tracing (term2str tt);
502 (Rewrite_Inst [(''bdv'',x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
503 #0 + d_d x (x ^^^ #2 + #3 * x)
505 (b)----- laut rep_tac_:
506 > val ttt=HOLogic.mk_eq (lhs,f');
510 (*Fehlersuche 1-2Monate vor 4.01:*)
511 > val tt = (Thm.term_of o the o (parse thy))
512 "Rewrite_Inst[(''bdv'',x)]square_equation_left True(x=#1+#2)";
515 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
516 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
517 > val subs = [((Thm.term_of o the o (parse thy)) "bdv",
518 (Thm.term_of o the o (parse thy)) "x")];
519 > val sT = (type_of o fst o hd) subs;
520 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
521 (map HOLogic.mk_prod subs);
522 > val sT' = type_of subs';
523 > val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
524 $ subs' $ Free (thmID,idT) $ @{term True} $ f;
527 > rep_tac_ (Rewrite_Inst'
528 ("Script","tless_true","eval_rls",false,subs,
529 ("square_equation_left",""),f,(f',[])));
531 (****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
532 > val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
533 "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
535 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
536 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
539 ("Script","tless_true","eval_rls",false,
540 ("square_equation_left",""),f,(f',[])));
541 > val SOME ct = parse thy
542 "Rewrite square_equation_left True (x=#1+#2)";
543 > rewrite_ Script.thy tless_true eval_rls true thm ct;
544 val it = SOME ("x = #3",[]) : (cterm * cterm list) option
546 (**************************************** | rep_tac_ (Rewrite_Set_Inst'
547 WN050824: type error ...
548 let val fT = type_of f;
549 val sT = (type_of o fst o hd) subs;
550 val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
551 (map HOLogic.mk_prod subs);
552 val sT' = type_of subs';
553 val b = if put then @{term True} else @{term False}
554 val lhs = Const ("Script.Rewrite'_Set'_Inst",
555 [sT',idT,fT,fT] ---> fT)
556 $ subs' $ Free (id_rls rls,idT) $ b $ f;
557 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
558 (* ... vals from Rewrite_Inst' ...
559 > rep_tac_ (Rewrite_Set_Inst'
560 ("Script",false,subs,
561 "isolate_bdv",f,(f',[])));
563 (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
565 (************************************** | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
567 val thy = assoc_thy thy';
568 val t = HOLogic.mk_eq (lhs,f');
570 --------------------------------------------------
571 val lll = (Thm.term_of o the o (parse thy))
572 "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
574 --------------------------------------------------
575 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
576 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
578 rep_tac_ (Rewrite_Set'
579 ("Script",false,"SqRoot_simplify",f,(f',[])));
580 val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
581 val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
583 (***************************************** | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
584 > val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
585 ... test-root-equ.sml: calculate ...
586 > val Appl m'=applicable_in p pt (Calculate "PLUS");
587 > val (lhs,_)=tac_2etac m';
589 val it = true : bool*)
591 "----------- fun init_scrstate -----------------------------------------------------------------";
592 "----------- fun init_scrstate -----------------------------------------------------------------";
593 "----------- fun init_scrstate -----------------------------------------------------------------";
594 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
595 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
596 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
597 "AbleitungBiegelinie dy"];
598 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
599 ["IntegrierenUndKonstanteBestimmen2"]);
600 val p = e_pos'; val c = [];
601 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
602 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
603 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
604 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
605 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
606 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
607 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
608 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
609 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
610 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
611 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
612 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)
613 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
615 val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
616 "~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
617 val (ScrState st, ctxt, Prog _) = init_scrstate thy itms metID;
619 "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(id_abl, dy)\",\"\n(b, y)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\"], [], NONE, \n??.empty, Safe, true)"
620 then () else error "init_scrstate changed for Biegelinie";
622 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
623 if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()
624 else error "modeling root-problem of Biegelinie 7.70 changed";