1 (* Title: tests on calchead.sml
2 Author: Walther Neuper 051013,
3 (c) due to copyright terms
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
9 "--------------------------------------------------------";
10 "table of contents --------------------------------------";
11 "--------------------------------------------------------";
12 "--------- get_interval after replace} other 2 ----------";
13 "--------- maximum example with 'specify' ---------------";
14 "--------- maximum example with 'specify', fmz <> [] ----";
15 "--------- maximum example with 'specify', fmz = [] -----";
16 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
17 "--------- regression test fun is_copy_named ------------";
18 "--------- regr.test fun cpy_nam ------------------------";
19 "--------- check specify phase --------------------------";
20 "--------- check: fmz matches pbt -----------------------";
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 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
89 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
90 (*uncaught exception TYPE 6.5.03*)
91 (*========== inhibit exn AK110718 =======================================================
93 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
94 Given=[Correct "fixedValues [r = Arbfix]"],
95 Relate=[Incompl "relations []"], Where=[],With=[]})
96 then error "test-maximum.sml: model stepwise - different behaviour"
97 else (); (*different with show_types !!!*)
98 ========== inhibit exn AK110718 =======================================================*)
100 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
101 (*========== inhibit exn AK110718 =======================================================
102 (* ERROR: Exception Bind raised *)
103 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
104 ========== inhibit exn AK110718 =======================================================*)
106 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
107 (*========== inhibit exn AK110718 =======================================================
108 (* ERROR: Exception Bind raised *)
109 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
110 ========== inhibit exn AK110718 =======================================================*)
112 val m = Specify_Problem ["maximum_of","function"];
113 val nxt = tac2tac_ pt p m;
114 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
115 (*========== inhibit exn AK110718 =======================================================
116 if ppc<>(Problem ["maximum_of","function"],
117 {Find=[Incompl "maximum",Incompl "valuesFor"],
118 Given=[Correct "fixedValues [r = Arbfix]"],
119 Relate=[Incompl "relations []"], Where=[],With=[]})
120 then error "diffappl.sml: Specify_Problem different behaviour"
122 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
123 if ppc<>(Problem ["maximum_of","function"],
124 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
125 Given=[Correct "fixedValues [r = Arbfix]"],
126 Relate=[Missing "relations rs_"],Where=[],With=[]})
127 then error "diffappl.sml: Specify_Problem different behaviour"
129 ========== inhibit exn AK110718 =======================================================*)
131 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
132 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
133 (*========== inhibit exn AK110718 =======================================================
135 if ppc<>(Method ["DiffApp","max_by_calculus"],
136 {Find=[Incompl "maximum",Incompl "valuesFor"],
137 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
138 Missing "interval itv_",Missing "errorBound err_"],
139 Relate=[Incompl "relations []"],Where=[],With=[]})
140 then error "diffappl.sml: Specify_Method different behaviour"
142 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
143 if ppc<>(Method ["DiffApp","max_by_calculus"],
144 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
145 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
146 Missing "interval itv_",Missing "errorBound err_"],
147 Relate=[Missing "relations rs_"],Where=[],With=[]})
148 then error "diffappl.sml: Specify_Method different behaviour"
150 ========== inhibit exn AK110718 =======================================================*)
153 "--------- maximum example with 'specify', fmz <> [] -------------";
154 "--------- maximum example with 'specify', fmz <> [] -------------";
155 "--------- maximum example with 'specify', fmz <> [] -------------";
157 ["fixedValues [r=Arbfix]","maximum A",
159 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
160 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
161 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
163 "boundVariable a","boundVariable b","boundVariable alpha",
164 "interval {x::real. 0 <= x & x <= 2*r}",
165 "interval {x::real. 0 <= x & x <= 2*r}",
166 "interval {x::real. 0 <= x & x <= pi}",
167 "errorBound (eps=(0::real))"];
169 ("DiffApp",["maximum_of","function"],
170 ["DiffApp","max_by_calculus"]);
172 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
173 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
175 val nxt = tac2tac_ pt p nxt;
176 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
177 val nxt = tac2tac_ pt p nxt;
178 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
179 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
181 val nxt = tac2tac_ pt p nxt;
182 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
183 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
185 val nxt = tac2tac_ pt p nxt;
186 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
187 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
189 val nxt = tac2tac_ pt p nxt;
190 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
191 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
193 val nxt = tac2tac_ pt p nxt;
194 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
195 (*val nxt = Add_Relation "relations [A = a * b]" *)
197 val nxt = tac2tac_ pt p nxt;
198 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
199 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
201 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
202 nxt_specif <> specify ?!
204 if nxt<>(Add_Relation
205 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
206 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
208 val nxt = tac2tac_ pt p nxt;
209 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
210 ------------------------------ FIXXXXME.meNEW !!! ---*)
212 (*val nxt = Specify_Theory "DiffApp" : tac*)
214 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
216 val nxt = tac2tac_ pt p nxt;
217 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
218 (*val nxt = Specify_Problem ["maximum_of","function"]*)
220 val nxt = tac2tac_ pt p nxt;
221 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
222 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
224 val nxt = tac2tac_ pt p nxt;
225 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
226 (*val nxt = Add_Given "boundVariable a" : tac*)
228 val nxt = tac2tac_ pt p nxt;
229 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
230 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
232 val nxt = tac2tac_ pt p nxt;
233 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
234 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
236 val nxt = tac2tac_ pt p nxt;
237 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
238 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
239 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
240 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
243 "--------- maximum example with 'specify', fmz = [] --------------";
244 "--------- maximum example with 'specify', fmz = [] --------------";
245 "--------- maximum example with 'specify', fmz = [] --------------";
247 val (dI',pI',mI') = empty_spec;
250 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
251 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
252 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
254 val nxt = tac2tac_ pt p nxt;
255 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
256 (*val nxt = Specify_Theory "e_domID" : tac*)
258 val nxt = Specify_Theory "DiffApp";
259 val nxt = tac2tac_ pt p nxt;
260 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
261 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
263 val nxt = Specify_Problem ["maximum_of","function"];
264 val nxt = tac2tac_ pt p nxt;
265 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
266 (*val nxt = Add_Given "fixedValues" : tac*)
268 val nxt = Add_Given "fixedValues [r=Arbfix]";
269 val nxt = tac2tac_ pt p nxt;
270 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
271 (*val nxt = Add_Find "maximum" : tac*)
273 val nxt = Add_Find "maximum A";
274 val nxt = tac2tac_ pt p nxt;
277 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
278 (*val nxt = Add_Find "valuesFor" : tac*)
280 val nxt = Add_Find "valuesFor [a]";
281 val nxt = tac2tac_ pt p nxt;
282 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
283 (*val nxt = Add_Relation "relations" ---
284 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
286 (*========== inhibit exn 010830 =======================================================*)
287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
288 if nxt<>(Add_Relation "relations []")
289 then error "test specify, fmz <> []: nxt <> Add_Relation.."
290 else (); (*different with show_types !!!*)
292 (*========== inhibit exn 010830 =======================================================*)
294 val nxt = Add_Relation "relations [(A=a+b)]";
295 val nxt = tac2tac_ pt p nxt;
296 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
297 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
299 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
300 val nxt = tac2tac_ pt p nxt;
301 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
302 (*val nxt = Add_Given "boundVariable" : tac*)
304 val nxt = Add_Given "boundVariable alpha";
305 val nxt = tac2tac_ pt p nxt;
306 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
307 (*val nxt = Add_Given "interval" : tac*)
309 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
310 val nxt = tac2tac_ pt p nxt;
311 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
312 (*val nxt = Add_Given "errorBound" : tac*)
314 val nxt = Add_Given "errorBound (eps=999)";
315 val nxt = tac2tac_ pt p nxt;
316 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
317 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
319 (*========== inhibit exn 010830 =======================================================
320 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
321 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
322 then error "test specify, fmz <> []: nxt <> Add_Relation.."
325 ========== inhibit exn 010830 =======================================================*)
327 (*========== inhibit exn 000402 =======================================================
328 (* 2.4.00 nach Transfer specify -> hard_gen
329 val nxt = Apply_Method ("DiffApp","max_by_calculus");
330 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
331 (*val nxt = Empty_Tac : tac*)
332 ========== inhibit exn 000402 =======================================================*)
335 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
337 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
338 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
339 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
340 val Const ("Script.SubProblem",_) $
341 (Const ("Product_Type.Pair",_) $
343 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
344 (*...copied from stac2tac_*)
346 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
347 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
348 " REAL_LIST [c, c_2]]");
349 val ags = isalist2list ags';
350 val pI = ["linear","system"];
351 val pats = (#ppc o get_pbt) pI;
352 "-a1-----------------------------------------------------";
353 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
354 val xxx = match_ags (theory "EqSystem") pats ags;
355 "-a2-----------------------------------------------------";
356 case match_ags (theory "Isac") pats ags of
357 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
358 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
359 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
360 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
362 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
365 "-b------------------------------------------------------";
366 val Const ("Script.SubProblem",_) $
367 (Const ("Product_Type.Pair",_) $
369 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
370 (*...copied from stac2tac_*)
372 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
373 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
374 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
375 val ags = isalist2list ags';
376 val pI = ["linear","system"];
377 val pats = (#ppc o get_pbt) pI;
378 "-b1-----------------------------------------------------";
379 val xxx = match_ags (theory "Isac") pats ags;
380 "-b2-----------------------------------------------------";
381 case match_ags (theory "EqSystem") pats ags of
382 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
383 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
384 [_ $ Free ("c", _) $ _,
385 _ $ Free ("c_2", _) $ _]),
386 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
387 (* type of Find: [Free ("ss'''", "bool List.list")]*)
389 | _ => error "calchead.sml match_ags copy-named dropped --------";
392 "-c---ERROR case: stac is missing #Given equalities e_s--";
393 val stac as Const ("Script.SubProblem",_) $
394 (Const ("Product_Type.Pair",_) $
396 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
397 (*...copied from stac2tac_*)
399 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
400 " [REAL_LIST [c, c_2]]");
401 val ags = isalist2list ags';
402 val pI = ["linear","system"];
403 val pats = (#ppc o get_pbt) pI;
404 (*---inhibit exn provided by this testcase--------------------------
405 val xxx - match_ags (theory "EqSystem") pats ags;
406 -------------------------------------------------------------------*)
407 "-c1-----------------------------------------------------";
408 "--------------------------step through code match_ags---";
409 val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
410 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
411 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
412 val cy = filter is_copy_named pbt; (*=solution*)
413 (*---inhibit exn provided by this testcase--------------------------
414 val oris' - matc thy pbt' ags [];
415 -------------------------------------------------------------------*)
416 "-------------------------------step through code matc---";
417 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
418 (is_copy_named_idstr o free2str) t;
420 (*---inhibit exn provided by this testcase--------------------------
421 val opt - mtc thy p a;
422 -------------------------------------------------------------------*)
423 "--------------------------------step through code mtc---";
424 val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
426 val ttt - (dsc $ var);
427 (*---inhibit exn provided by this testcase--------------------------
428 cterm_of thy (dsc $ var);
429 -------------------------------------------------------------------*)
430 "-------------------------------------step through end---";
432 case ((match_ags (theory "EqSystem") pats ags)
433 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
434 [] => match_ags_msg pI stac ags
435 | _ => error "calchead.sml match_ags 1st arg missing --------";
438 "-d------------------------------------------------------";
439 val stac as Const ("Script.SubProblem",_) $
440 (Const ("Product_Type.Pair",_) $
442 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
443 (*...copied from stac2tac_*)
445 "SubProblem (Test',[univariate,equation,test]," ^
446 " [no_met]) [BOOL (x+1=2), REAL x]");
447 val AGS = isalist2list ags';
448 val pI = ["univariate","equation","test"];
449 val PATS = (#ppc o get_pbt) pI;
450 "-d1-----------------------------------------------------";
451 "--------------------------step through code match_ags---";
452 val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
453 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
454 val pbt' = filter_out is_copy_named pbt;
455 val cy = filter is_copy_named pbt;
456 val oris' = matc thy pbt' ags [];
457 "-------------------------------step through code matc---";
458 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
459 (is_copy_named_idstr o free2str) t;
461 val opt = mtc thy p a;
462 "--------------------------------step through code mtc---";
463 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
464 val ttt = (dsc $ var);
465 cterm_of thy (dsc $ var);
466 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
468 "-d2-----------------------------------------------------";
470 "-------------------------------step through code matc---";
471 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
472 (is_copy_named_idstr o free2str) t;
474 val opt = mtc thy p a;
475 "--------------------------------step through code mtc---";
476 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
477 val ttt = (dsc $ var);
478 cterm_of thy (dsc $ var);
479 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
480 "-d3-----------------------------------------------------";
481 pbt = []; (*true, base case*)
482 "-----------------continue step through code match_ags---";
483 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
484 "--------------------------------step through cpy_nam----";
485 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
486 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
487 "--------------------------------------------------------";
488 fun is_copy_named_generating_idstr str =
489 if is_copy_named_idstr str
490 then case (rev o explode) str of
491 (*"_"::"_"::"_"::_ => false*)
492 "'"::"'"::"'"::_ => false
495 fun is_copy_named_generating (_, (_, t)) =
496 (is_copy_named_generating_idstr o free2str) t;
497 "--------------------------------------------------------";
498 is_copy_named_generating p (*true*);
499 fun sel (_,_,d,ts) = comp_ts (d, ts);
500 val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
502 val ext = (last_elem o drop_last o explode o free2str) t;
504 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
505 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
506 val vals = map sel oris;
507 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
509 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
510 (assoc (vars'~~vals, cy'));
511 (*SOME (Free ("x", "RealDef.real")) : term option*)
512 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
514 "-----------------continue step through code match_ags---";
515 val cy' = map (cpy_nam pbt' oris') cy;
516 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
517 "-------------------------------------step through end---";
519 case match_ags thy PATS AGS of
520 [(1, [1], "#Given", Const ("Descript.equality", _),
521 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
522 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
523 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
524 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
526 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
529 "--------- regression test fun is_copy_named ------------";
530 "--------- regression test fun is_copy_named ------------";
531 "--------- regression test fun is_copy_named ------------";
532 val trm = (1, (2, @{term "v'i'"}));
533 if is_copy_named trm then () else error "regr. is_copy_named 1";
534 val trm = (1, (2, @{term "e_e"}));
535 if is_copy_named trm then error "regr. is_copy_named 2" else ();
536 val trm = (1, (2, @{term "L'''"}));
537 if is_copy_named trm then () else error "regr. is_copy_named 3";
539 (* out-comment 'structure CalcHead'...
540 val trm = (1, (2, @{term "v'i'"}));
541 if is_copy_named_generating trm then () else error "regr. is_copy_named";
542 val trm = (1, (2, @{term "L'''"}));
543 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
546 "--------- regr.test fun cpy_nam ------------------------";
547 "--------- regr.test fun cpy_nam ------------------------";
548 "--------- regr.test fun cpy_nam ------------------------";
549 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
550 (*the model-pattern, is_copy_named are filter_out*)
551 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
552 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
553 (*the model specific for an example*)
554 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
555 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
556 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
557 (*...all must be true*)
559 case cpy_nam pbt oris (hd cy) of
560 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
561 | _ => error "calchead.sml regr.test cpy_nam-1-";
563 (*new data: cpy_nam without changing the name*)
564 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
565 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
566 @{term "solution"}; type_of @{term "ss''' :: bool list"};
567 (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
568 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
569 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
570 (*the model specific for an example*)
571 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
572 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
573 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
574 (*could be more than 1*)];
576 case cpy_nam pbt oris (hd cy) of
577 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
578 | _ => error "calchead.sml regr.test cpy_nam-2-";
580 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
583 "--------- check specify phase --------------------------";
584 "--------- check specify phase --------------------------";
585 "--------- check specify phase --------------------------";
586 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
587 val fmz = ["functionTerm (x + 1)",
588 "integrateBy x","antiDerivative FF"];
590 ("Integrate",["integrate","function"],
591 ["diff","integration"]);
592 val p = e_pos'; val c = [];
594 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
595 (*> val it = "--- step 1 --" : string
599 (0, EdUndef, 0, Nundef,
601 {Find = [], With = [], Given = [], Where = [], Relate = []})))
603 val nxt = ("Model_Problem", Model_Problem) : string * tac
604 val p = ([], Pbl) : pos'
608 (["functionTerm (x^^^2 + 1)", "integrateBy x",
609 "antiDerivative FF"],
610 ("Integrate", ["integrate", "function"],
611 ["diff", "integration"])),
613 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
615 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
616 probl = [], branch = TransitiveB,
619 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
621 "[RealDef.real, RealDef.real] => RealDef.real") $
622 (Const ("Atools.pow",
623 "[RealDef.real, RealDef.real] => RealDef.real") $
624 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
625 Free ("1", "RealDef.real")]),
627 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
628 [Free ("x", "RealDef.real")]),
630 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
631 [Free ("FF", "RealDef.real")])],
632 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
633 Const ("Integrate.Integrate",
634 "(RealDef.real, RealDef.real) * => RealDef.real") $
635 (Const ("Product_Type.Pair",
636 "[RealDef.real, RealDef.real]
637 => (RealDef.real, RealDef.real) *") $
639 "[RealDef.real, RealDef.real] => RealDef.real") $
640 (Const ("Atools.pow",
641 "[RealDef.real, RealDef.real] => RealDef.real") $
642 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
643 Free ("1", "RealDef.real")) $
644 Free ("x", "RealDef.real"))),
645 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
647 "----- WN101007 worked until here (checked same as isac2002) ---";
648 if nxt = ("Model_Problem", Model_Problem) then ()
649 else error "clchead.sml: check specify phase step 1";
651 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
652 (*val it = "--- step 2 --" : string
653 val p = ([], Pbl) : pos'
657 (0, EdUndef, 0, Nundef,
659 {Find = [Incompl "Integrate.antiDerivative"],
661 Given = [Incompl "functionTerm", Incompl "integrateBy"],
663 Relate = []}))) : mout
664 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
668 (["functionTerm (x^^^2 + 1)", "integrateBy x",
669 "antiDerivative FF"],
670 ("Integrate", ["integrate", "function"],
671 ["diff", "integration"])),
674 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
676 cell = None, meth = [], spec =
677 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
678 [(0, [], false, "#Given",
679 Inc ((Const ("Descript.functionTerm",
680 "RealDef.real => Tools.una"),[]),
681 (Const ("empty", "'a"), []))),
682 (0, [], false, "#Given",
683 Inc ((Const ("Integrate.integrateBy",
684 "RealDef.real => Tools.una"),[]),
685 (Const ("empty", "'a"), []))),
686 (0, [], false, "#Find",
687 Inc ((Const ("Integrate.antiDerivative",
688 "RealDef.real => Tools.una"),[]),
689 (Const ("empty", "'a"), [])))],
690 branch = TransitiveB, origin =
692 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
694 "[RealDef.real, RealDef.real] => RealDef.real") $
695 (Const ("Atools.pow",
696 "[RealDef.real, RealDef.real] => RealDef.real") $
697 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
698 Free ("1", "RealDef.real")]),
700 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
701 [Free ("x", "RealDef.real")]),
703 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
704 [Free ("FF", "RealDef.real")])],
705 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
706 Const ("Integrate.Integrate",
707 "(RealDef.real, RealDef.real) * => RealDef.real") $
708 (Const ("Product_Type.Pair",
709 "[RealDef.real, RealDef.real]
710 => (RealDef.real, RealDef.real) *") $
712 "[RealDef.real, RealDef.real] => RealDef.real") $
713 (Const ("Atools.pow",
714 "[RealDef.real, RealDef.real] => RealDef.real") $
715 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
716 Free ("1", "RealDef.real")) $
717 Free ("x", "RealDef.real"))),
718 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
720 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
721 if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
722 else error "clchead.sml: check specify phase step 2";
724 val (p,_,f,nxt,_,pt) = me nxt p c pt;
725 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
726 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
727 else error "clchead.sml: check specify phase step 2";
729 "--------- check: fmz matches pbt -----------------------";
730 "--------- check: fmz matches pbt -----------------------";
731 "--------- check: fmz matches pbt -----------------------";
732 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
733 "the following fmz caused the above error";
734 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
735 val pI = ["plus_minus","polynom","vereinfachen"];
737 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
738 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
739 (*#############################^^^^^^^^^ defined by Isabelle*)
740 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
741 [Free ("N", _ (*"RealDef.real"*))])],
742 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
743 "#undef means: the element with description TERM in fmz did not match ";
744 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
745 "defined in Simplify.thy";
747 "So we try out how to create Simplify.Term:";
749 val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
750 " ^^^^^^^^^ see above";
754 val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
755 " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
759 val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
760 " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
761 " and unsed in pbl [plus_minus,polynom,vereinfachen]";
764 "----- so this is the correct fmz:";
765 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
766 val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
767 (*########################^^^^^^^^^ defined in Simplify.thy*)
768 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
770 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
772 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
773 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
774 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;