2 (* Title: tests on calchead.sml
3 Author: Walther Neuper 051013,
4 (c) due to copyright terms
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "--------- get_interval after replace} other 2 ----------";
14 "--------- maximum example with 'specify' ---------------";
15 "--------- maximum example with 'specify', fmz <> [] ----";
16 "--------- maximum example with 'specify', fmz = [] -----";
17 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
18 "--------- regression test fun is_copy_named ------------";
19 "--------- regr.test fun cpy_nam ------------------------";
20 "--------- check specify phase --------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
23 "--------------------------------------------------------";
26 "--------- get_interval after replace} other 2 ----------";
27 "--------- get_interval after replace} other 2 ----------";
28 "--------- get_interval after replace} other 2 ----------";
30 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
31 ("Test", ["sqroot-test","univariate","equation","test"],
32 ["Test","squ-equ-test-subpbl1"]))];
35 autoCalculate 1 CompleteCalc;
36 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
37 replaceFormula 1 "x = 1";
38 (*... returns calcChangedEvent with ...*)
39 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
40 val ((pt,_),_) = get_calc 1;
42 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
43 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
44 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
45 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
46 ([3, 2], Res)] then () else
47 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
49 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
51 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
52 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
53 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
58 "--------- maximum example with 'specify' ------------------------";
59 "--------- maximum example with 'specify' ------------------------";
60 "--------- maximum example with 'specify' ------------------------";
61 (*" Specify_Problem (match_itms_oris) ";*)
63 ["fixedValues [r=Arbfix]","maximum A",
65 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
66 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
67 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
69 "boundVariable a","boundVariable b","boundVariable alpha",
70 "interval {x::real. 0 <= x & x <= 2*r}",
71 "interval {x::real. 0 <= x & x <= 2*r}",
72 "interval {x::real. 0 <= x & x <= pi}",
73 "errorBound (eps=(0::real))"];
75 ("DiffApp",["maximum_of","function"],
76 ["DiffApp","max_by_calculus"]);
79 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
80 val nxt = tac2tac_ pt p nxt;
81 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
82 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
84 val nxt = tac2tac_ pt p nxt;
85 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
88 (*========== inhibit exn AK110718 =======================================================
89 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
90 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
91 (*uncaught exception TYPE 6.5.03*)
94 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
95 Given=[Correct "fixedValues [r = Arbfix]"],
96 Relate=[Incompl "relations []"], Where=[],With=[]})
97 then error "test-maximum.sml: model stepwise - different behaviour"
98 else (); (*different with show_types !!!*)
99 ========== inhibit exn AK110718 =======================================================*)
101 (*========== inhibit exn AK110718 =======================================================
102 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
103 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
105 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
106 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
107 ========== inhibit exn AK110718 =======================================================*)
109 val m = Specify_Problem ["maximum_of","function"];
110 val nxt = tac2tac_ pt p m;
111 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
113 (*========== inhibit exn AK110718 =======================================================
114 if ppc<>(Problem ["maximum_of","function"],
115 {Find=[Incompl "maximum",Incompl "valuesFor"],
116 Given=[Correct "fixedValues [r = Arbfix]"],
117 Relate=[Incompl "relations []"], Where=[],With=[]})
118 then error "diffappl.sml: Specify_Problem different behaviour"
120 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
121 if ppc<>(Problem ["maximum_of","function"],
122 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
123 Given=[Correct "fixedValues [r = Arbfix]"],
124 Relate=[Missing "relations rs_"],Where=[],With=[]})
125 then error "diffappl.sml: Specify_Problem different behaviour"
128 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
129 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
132 if ppc<>(Method ["DiffApp","max_by_calculus"],
133 {Find=[Incompl "maximum",Incompl "valuesFor"],
134 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
135 Missing "interval itv_",Missing "errorBound err_"],
136 Relate=[Incompl "relations []"],Where=[],With=[]})
137 then error "diffappl.sml: Specify_Method different behaviour"
139 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
140 if ppc<>(Method ["DiffApp","max_by_calculus"],
141 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
142 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
143 Missing "interval itv_",Missing "errorBound err_"],
144 Relate=[Missing "relations rs_"],Where=[],With=[]})
145 then error "diffappl.sml: Specify_Method different behaviour"
147 ========== inhibit exn AK110718 =======================================================*)
150 "--------- maximum example with 'specify', fmz <> [] -------------";
151 "--------- maximum example with 'specify', fmz <> [] -------------";
152 "--------- maximum example with 'specify', fmz <> [] -------------";
154 ["fixedValues [r=Arbfix]","maximum A",
156 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
157 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
158 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
160 "boundVariable a","boundVariable b","boundVariable alpha",
161 "interval {x::real. 0 <= x & x <= 2*r}",
162 "interval {x::real. 0 <= x & x <= 2*r}",
163 "interval {x::real. 0 <= x & x <= pi}",
164 "errorBound (eps=(0::real))"];
166 ("DiffApp",["maximum_of","function"],
167 ["DiffApp","max_by_calculus"]);
169 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
170 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
172 val nxt = tac2tac_ pt p nxt;
173 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
174 val nxt = tac2tac_ pt p nxt;
175 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
176 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
178 val nxt = tac2tac_ pt p nxt;
179 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
180 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
182 val nxt = tac2tac_ pt p nxt;
183 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
184 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
186 val nxt = tac2tac_ pt p nxt;
187 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
188 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
190 val nxt = tac2tac_ pt p nxt;
191 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
192 (*val nxt = Add_Relation "relations [A = a * b]" *)
194 val nxt = tac2tac_ pt p nxt;
195 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
196 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
198 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
199 nxt_specif <> specify ?!
201 if nxt<>(Add_Relation
202 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
203 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
205 val nxt = tac2tac_ pt p nxt;
206 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
207 ------------------------------ FIXXXXME.meNEW !!! ---*)
209 (*val nxt = Specify_Theory "DiffApp" : tac*)
211 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
213 val nxt = tac2tac_ pt p nxt;
214 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
215 (*val nxt = Specify_Problem ["maximum_of","function"]*)
217 val nxt = tac2tac_ pt p nxt;
218 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
219 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
221 val nxt = tac2tac_ pt p nxt;
222 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
223 (*val nxt = Add_Given "boundVariable a" : tac*)
225 val nxt = tac2tac_ pt p nxt;
226 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
227 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
229 val nxt = tac2tac_ pt p nxt;
230 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
231 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
233 val nxt = tac2tac_ pt p nxt;
234 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
235 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
236 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
237 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
240 "--------- maximum example with 'specify', fmz = [] --------------";
241 "--------- maximum example with 'specify', fmz = [] --------------";
242 "--------- maximum example with 'specify', fmz = [] --------------";
244 val (dI',pI',mI') = empty_spec;
247 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
248 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
249 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
251 val nxt = tac2tac_ pt p nxt;
252 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
253 (*val nxt = Specify_Theory "e_domID" : tac*)
255 val nxt = Specify_Theory "DiffApp";
256 val nxt = tac2tac_ pt p nxt;
257 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
258 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
260 val nxt = Specify_Problem ["maximum_of","function"];
261 val nxt = tac2tac_ pt p nxt;
262 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
263 (*val nxt = Add_Given "fixedValues" : tac*)
265 val nxt = Add_Given "fixedValues [r=Arbfix]";
266 val nxt = tac2tac_ pt p nxt;
267 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
268 (*val nxt = Add_Find "maximum" : tac*)
270 val nxt = Add_Find "maximum A";
271 val nxt = tac2tac_ pt p nxt;
274 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
275 (*val nxt = Add_Find "valuesFor" : tac*)
277 val nxt = Add_Find "valuesFor [a]";
278 val nxt = tac2tac_ pt p nxt;
279 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
280 (*val nxt = Add_Relation "relations" ---
281 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
283 (*========== inhibit exn 010830 =======================================================
284 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
285 if nxt<>(Add_Relation "relations []")
286 then error "test specify, fmz <> []: nxt <> Add_Relation.."
287 else (); (*different with show_types !!!*)
289 ========== inhibit exn 010830 =======================================================*)
291 val nxt = Add_Relation "relations [(A=a+b)]";
292 val nxt = tac2tac_ pt p nxt;
293 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
294 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
296 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
297 val nxt = tac2tac_ pt p nxt;
298 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
299 (*val nxt = Add_Given "boundVariable" : tac*)
301 val nxt = Add_Given "boundVariable alpha";
302 val nxt = tac2tac_ pt p nxt;
303 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
304 (*val nxt = Add_Given "interval" : tac*)
306 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
307 val nxt = tac2tac_ pt p nxt;
308 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
309 (*val nxt = Add_Given "errorBound" : tac*)
311 val nxt = Add_Given "errorBound (eps=999)";
312 val nxt = tac2tac_ pt p nxt;
313 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
314 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
316 (*========== inhibit exn 010830 =======================================================
317 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
318 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
319 then error "test specify, fmz <> []: nxt <> Add_Relation.."
322 ========== inhibit exn 010830 =======================================================*)
324 (*========== inhibit exn 000402 =======================================================
325 (* 2.4.00 nach Transfer specify -> hard_gen
326 val nxt = Apply_Method ("DiffApp","max_by_calculus");
327 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
328 (*val nxt = Empty_Tac : tac*)
329 ========== inhibit exn 000402 =======================================================*)
332 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
334 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
335 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
336 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
337 val Const ("Script.SubProblem",_) $
338 (Const ("Product_Type.Pair",_) $
340 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
341 (*...copied from stac2tac_*)
343 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
344 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
345 " REAL_LIST [c, c_2]]");
346 val ags = isalist2list ags';
347 val pI = ["linear","system"];
348 val pats = (#ppc o get_pbt) pI;
349 "-a1-----------------------------------------------------";
350 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
351 val xxx = match_ags (theory "EqSystem") pats ags;
352 "-a2-----------------------------------------------------";
353 case match_ags (theory "Isac") pats ags of
354 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
355 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
356 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
357 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
359 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
362 "-b------------------------------------------------------";
363 val Const ("Script.SubProblem",_) $
364 (Const ("Product_Type.Pair",_) $
366 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
367 (*...copied from stac2tac_*)
369 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
370 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
371 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
372 val ags = isalist2list ags';
373 val pI = ["linear","system"];
374 val pats = (#ppc o get_pbt) pI;
375 "-b1-----------------------------------------------------";
376 val xxx = match_ags (theory "Isac") pats ags;
377 "-b2-----------------------------------------------------";
378 case match_ags (theory "EqSystem") pats ags of
379 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
380 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
381 [_ $ Free ("c", _) $ _,
382 _ $ Free ("c_2", _) $ _]),
383 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
384 (* type of Find: [Free ("ss'''", "bool List.list")]*)
386 | _ => error "calchead.sml match_ags copy-named dropped --------";
389 "-c---ERROR case: stac is missing #Given equalities e_s--";
390 val stac as Const ("Script.SubProblem",_) $
391 (Const ("Product_Type.Pair",_) $
393 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
394 (*...copied from stac2tac_*)
396 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
397 " [REAL_LIST [c, c_2]]");
398 val ags = isalist2list ags';
399 val pI = ["linear","system"];
400 val pats = (#ppc o get_pbt) pI;
401 (*---inhibit exn provided by this testcase--------------------------
402 val xxx - match_ags (theory "EqSystem") pats ags;
403 -------------------------------------------------------------------*)
404 "-c1-----------------------------------------------------";
405 "--------------------------step through code match_ags---";
406 val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
407 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
408 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
409 val cy = filter is_copy_named pbt; (*=solution*)
410 (*---inhibit exn provided by this testcase--------------------------
411 val oris' - matc thy pbt' ags [];
412 -------------------------------------------------------------------*)
413 "-------------------------------step through code matc---";
414 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
415 (is_copy_named_idstr o free2str) t;
417 (*---inhibit exn provided by this testcase--------------------------
418 val opt - mtc thy p a;
419 -------------------------------------------------------------------*)
420 "--------------------------------step through code mtc---";
421 val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
423 val ttt - (dsc $ var);
424 (*---inhibit exn provided by this testcase--------------------------
425 cterm_of thy (dsc $ var);
426 -------------------------------------------------------------------*)
427 "-------------------------------------step through end---";
429 case ((match_ags (theory "EqSystem") pats ags)
430 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
431 [] => match_ags_msg pI stac ags
432 | _ => error "calchead.sml match_ags 1st arg missing --------";
435 "-d------------------------------------------------------";
436 val stac as Const ("Script.SubProblem",_) $
437 (Const ("Product_Type.Pair",_) $
439 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
440 (*...copied from stac2tac_*)
442 "SubProblem (Test',[univariate,equation,test]," ^
443 " [no_met]) [BOOL (x+1=2), REAL x]");
444 val AGS = isalist2list ags';
445 val pI = ["univariate","equation","test"];
446 val PATS = (#ppc o get_pbt) pI;
447 "-d1-----------------------------------------------------";
448 "--------------------------step through code match_ags---";
449 val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
450 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
451 val pbt' = filter_out is_copy_named pbt;
452 val cy = filter is_copy_named pbt;
453 val oris' = matc thy pbt' ags [];
454 "-------------------------------step through code matc---";
455 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
456 (is_copy_named_idstr o free2str) t;
458 val opt = mtc thy p a;
459 "--------------------------------step through code mtc---";
460 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
461 val ttt = (dsc $ var);
462 cterm_of thy (dsc $ var);
463 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
465 "-d2-----------------------------------------------------";
467 "-------------------------------step through code matc---";
468 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
469 (is_copy_named_idstr o free2str) t;
471 val opt = mtc thy p a;
472 "--------------------------------step through code mtc---";
473 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
474 val ttt = (dsc $ var);
475 cterm_of thy (dsc $ var);
476 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
477 "-d3-----------------------------------------------------";
478 pbt = []; (*true, base case*)
479 "-----------------continue step through code match_ags---";
480 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
481 "--------------------------------step through cpy_nam----";
482 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
483 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
484 "--------------------------------------------------------";
485 fun is_copy_named_generating_idstr str =
486 if is_copy_named_idstr str
487 then case (rev o explode) str of
488 (*"_"::"_"::"_"::_ => false*)
489 "'"::"'"::"'"::_ => false
492 fun is_copy_named_generating (_, (_, t)) =
493 (is_copy_named_generating_idstr o free2str) t;
494 "--------------------------------------------------------";
495 is_copy_named_generating p (*true*);
496 fun sel (_,_,d,ts) = comp_ts (d, ts);
497 val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
499 val ext = (last_elem o drop_last o explode o free2str) t;
501 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
502 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
503 val vals = map sel oris;
504 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
506 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
507 (assoc (vars'~~vals, cy'));
508 (*SOME (Free ("x", "RealDef.real")) : term option*)
509 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
511 "-----------------continue step through code match_ags---";
512 val cy' = map (cpy_nam pbt' oris') cy;
513 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
514 "-------------------------------------step through end---";
516 case match_ags thy PATS AGS of
517 [(1, [1], "#Given", Const ("Descript.equality", _),
518 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
519 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
520 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
521 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
523 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
526 "--------- regression test fun is_copy_named ------------";
527 "--------- regression test fun is_copy_named ------------";
528 "--------- regression test fun is_copy_named ------------";
529 val trm = (1, (2, @{term "v'i'"}));
530 if is_copy_named trm then () else error "regr. is_copy_named 1";
531 val trm = (1, (2, @{term "e_e"}));
532 if is_copy_named trm then error "regr. is_copy_named 2" else ();
533 val trm = (1, (2, @{term "L'''"}));
534 if is_copy_named trm then () else error "regr. is_copy_named 3";
536 (* out-comment 'structure CalcHead'...
537 val trm = (1, (2, @{term "v'i'"}));
538 if is_copy_named_generating trm then () else error "regr. is_copy_named";
539 val trm = (1, (2, @{term "L'''"}));
540 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
543 "--------- regr.test fun cpy_nam ------------------------";
544 "--------- regr.test fun cpy_nam ------------------------";
545 "--------- regr.test fun cpy_nam ------------------------";
546 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
547 (*the model-pattern, is_copy_named are filter_out*)
548 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
549 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
550 (*the model specific for an example*)
551 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
552 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
553 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
554 (*...all must be true*)
556 case cpy_nam pbt oris (hd cy) of
557 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
558 | _ => error "calchead.sml regr.test cpy_nam-1-";
560 (*new data: cpy_nam without changing the name*)
561 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
562 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
563 @{term "solution"}; type_of @{term "ss''' :: bool list"};
564 (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
565 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
566 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
567 (*the model specific for an example*)
568 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
569 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
570 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
571 (*could be more than 1*)];
573 case cpy_nam pbt oris (hd cy) of
574 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
575 | _ => error "calchead.sml regr.test cpy_nam-2-";
577 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
580 "--------- check specify phase --------------------------";
581 "--------- check specify phase --------------------------";
582 "--------- check specify phase --------------------------";
583 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
584 val fmz = ["functionTerm (x + 1)",
585 "integrateBy x","antiDerivative FF"];
587 ("Integrate",["integrate","function"],
588 ["diff","integration"]);
589 val p = e_pos'; val c = [];
591 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
592 (*> val it = "--- step 1 --" : string
596 (0, EdUndef, 0, Nundef,
598 {Find = [], With = [], Given = [], Where = [], Relate = []})))
600 val nxt = ("Model_Problem", Model_Problem) : string * tac
601 val p = ([], Pbl) : pos'
605 (["functionTerm (x^^^2 + 1)", "integrateBy x",
606 "antiDerivative FF"],
607 ("Integrate", ["integrate", "function"],
608 ["diff", "integration"])),
610 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
612 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
613 probl = [], branch = TransitiveB,
616 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
618 "[RealDef.real, RealDef.real] => RealDef.real") $
619 (Const ("Atools.pow",
620 "[RealDef.real, RealDef.real] => RealDef.real") $
621 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
622 Free ("1", "RealDef.real")]),
624 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
625 [Free ("x", "RealDef.real")]),
627 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
628 [Free ("FF", "RealDef.real")])],
629 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
630 Const ("Integrate.Integrate",
631 "(RealDef.real, RealDef.real) * => RealDef.real") $
632 (Const ("Product_Type.Pair",
633 "[RealDef.real, RealDef.real]
634 => (RealDef.real, RealDef.real) *") $
636 "[RealDef.real, RealDef.real] => RealDef.real") $
637 (Const ("Atools.pow",
638 "[RealDef.real, RealDef.real] => RealDef.real") $
639 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
640 Free ("1", "RealDef.real")) $
641 Free ("x", "RealDef.real"))),
642 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
644 "----- WN101007 worked until here (checked same as isac2002) ---";
645 if nxt = ("Model_Problem", Model_Problem) then ()
646 else error "clchead.sml: check specify phase step 1";
648 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
649 (*val it = "--- step 2 --" : string
650 val p = ([], Pbl) : pos'
654 (0, EdUndef, 0, Nundef,
656 {Find = [Incompl "Integrate.antiDerivative"],
658 Given = [Incompl "functionTerm", Incompl "integrateBy"],
660 Relate = []}))) : mout
661 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
665 (["functionTerm (x^^^2 + 1)", "integrateBy x",
666 "antiDerivative FF"],
667 ("Integrate", ["integrate", "function"],
668 ["diff", "integration"])),
671 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
673 cell = None, meth = [], spec =
674 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
675 [(0, [], false, "#Given",
676 Inc ((Const ("Descript.functionTerm",
677 "RealDef.real => Tools.una"),[]),
678 (Const ("empty", "'a"), []))),
679 (0, [], false, "#Given",
680 Inc ((Const ("Integrate.integrateBy",
681 "RealDef.real => Tools.una"),[]),
682 (Const ("empty", "'a"), []))),
683 (0, [], false, "#Find",
684 Inc ((Const ("Integrate.antiDerivative",
685 "RealDef.real => Tools.una"),[]),
686 (Const ("empty", "'a"), [])))],
687 branch = TransitiveB, origin =
689 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
691 "[RealDef.real, RealDef.real] => RealDef.real") $
692 (Const ("Atools.pow",
693 "[RealDef.real, RealDef.real] => RealDef.real") $
694 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
695 Free ("1", "RealDef.real")]),
697 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
698 [Free ("x", "RealDef.real")]),
700 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
701 [Free ("FF", "RealDef.real")])],
702 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
703 Const ("Integrate.Integrate",
704 "(RealDef.real, RealDef.real) * => RealDef.real") $
705 (Const ("Product_Type.Pair",
706 "[RealDef.real, RealDef.real]
707 => (RealDef.real, RealDef.real) *") $
709 "[RealDef.real, RealDef.real] => RealDef.real") $
710 (Const ("Atools.pow",
711 "[RealDef.real, RealDef.real] => RealDef.real") $
712 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
713 Free ("1", "RealDef.real")) $
714 Free ("x", "RealDef.real"))),
715 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
717 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
718 if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
719 else error "clchead.sml: check specify phase step 2";
721 val (p,_,f,nxt,_,pt) = me nxt p c pt;
722 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
723 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
724 else error "clchead.sml: check specify phase step 2";
726 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
727 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)