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 "--------------------------------------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
25 "--------- get_interval after replace} other 2 ----------";
26 "--------- get_interval after replace} other 2 ----------";
27 "--------- get_interval after replace} other 2 ----------";
29 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
30 ("Test", ["sqroot-test","univariate","equation","test"],
31 ["Test","squ-equ-test-subpbl1"]))];
34 autoCalculate 1 CompleteCalc;
35 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
36 replaceFormula 1 "x = 1";
37 (*... returns calcChangedEvent with ...*)
38 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
39 val ((pt,_),_) = get_calc 1;
41 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
42 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
43 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
44 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
45 ([3, 2], Res)] then () else
46 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
48 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
50 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
51 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
52 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
57 "--------- maximum example with 'specify' ------------------------";
58 "--------- maximum example with 'specify' ------------------------";
59 "--------- maximum example with 'specify' ------------------------";
60 (*" Specify_Problem (match_itms_oris) ";*)
62 ["fixedValues [r=Arbfix]","maximum A",
64 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
65 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
66 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
68 "boundVariable a","boundVariable b","boundVariable alpha",
69 "interval {x::real. 0 <= x & x <= 2*r}",
70 "interval {x::real. 0 <= x & x <= 2*r}",
71 "interval {x::real. 0 <= x & x <= pi}",
72 "errorBound (eps=(0::real))"];
74 ("DiffApp",["maximum_of","function"],
75 ["DiffApp","max_by_calculus"]);
78 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
79 val nxt = tac2tac_ pt p nxt;
80 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
81 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
83 val nxt = tac2tac_ pt p nxt;
84 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
87 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
88 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
89 (*uncaught exception TYPE 6.5.03*)
90 (*========== inhibit exn AK110718 =======================================================
92 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
93 Given=[Correct "fixedValues [r = Arbfix]"],
94 Relate=[Incompl "relations []"], Where=[],With=[]})
95 then error "test-maximum.sml: model stepwise - different behaviour"
96 else (); (*different with show_types !!!*)
97 ========== inhibit exn AK110718 =======================================================*)
99 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
100 (*========== inhibit exn AK110718 =======================================================
101 (* ERROR: Exception Bind raised *)
102 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
103 ========== inhibit exn AK110718 =======================================================*)
105 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
106 (*========== inhibit exn AK110718 =======================================================
107 (* ERROR: Exception Bind raised *)
108 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
109 ========== inhibit exn AK110718 =======================================================*)
111 val m = Specify_Problem ["maximum_of","function"];
112 val nxt = tac2tac_ pt p m;
113 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
114 (*========== inhibit exn AK110718 =======================================================
115 if ppc<>(Problem ["maximum_of","function"],
116 {Find=[Incompl "maximum",Incompl "valuesFor"],
117 Given=[Correct "fixedValues [r = Arbfix]"],
118 Relate=[Incompl "relations []"], Where=[],With=[]})
119 then error "diffappl.sml: Specify_Problem different behaviour"
121 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
122 if ppc<>(Problem ["maximum_of","function"],
123 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
124 Given=[Correct "fixedValues [r = Arbfix]"],
125 Relate=[Missing "relations rs_"],Where=[],With=[]})
126 then error "diffappl.sml: Specify_Problem different behaviour"
128 ========== inhibit exn AK110718 =======================================================*)
130 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
131 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
132 (*========== inhibit exn AK110718 =======================================================
134 if ppc<>(Method ["DiffApp","max_by_calculus"],
135 {Find=[Incompl "maximum",Incompl "valuesFor"],
136 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
137 Missing "interval itv_",Missing "errorBound err_"],
138 Relate=[Incompl "relations []"],Where=[],With=[]})
139 then error "diffappl.sml: Specify_Method different behaviour"
141 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
142 if ppc<>(Method ["DiffApp","max_by_calculus"],
143 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
144 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
145 Missing "interval itv_",Missing "errorBound err_"],
146 Relate=[Missing "relations rs_"],Where=[],With=[]})
147 then error "diffappl.sml: Specify_Method different behaviour"
149 ========== inhibit exn AK110718 =======================================================*)
152 "--------- maximum example with 'specify', fmz <> [] -------------";
153 "--------- maximum example with 'specify', fmz <> [] -------------";
154 "--------- maximum example with 'specify', fmz <> [] -------------";
156 ["fixedValues [r=Arbfix]","maximum A",
158 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
159 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
160 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
162 "boundVariable a","boundVariable b","boundVariable alpha",
163 "interval {x::real. 0 <= x & x <= 2*r}",
164 "interval {x::real. 0 <= x & x <= 2*r}",
165 "interval {x::real. 0 <= x & x <= pi}",
166 "errorBound (eps=(0::real))"];
168 ("DiffApp",["maximum_of","function"],
169 ["DiffApp","max_by_calculus"]);
171 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
172 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
174 val nxt = tac2tac_ pt p nxt;
175 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
176 val nxt = tac2tac_ pt p nxt;
177 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
178 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
180 val nxt = tac2tac_ pt p nxt;
181 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
182 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
184 val nxt = tac2tac_ pt p nxt;
185 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
186 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
188 val nxt = tac2tac_ pt p nxt;
189 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
190 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
192 val nxt = tac2tac_ pt p nxt;
193 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
194 (*val nxt = Add_Relation "relations [A = a * b]" *)
196 val nxt = tac2tac_ pt p nxt;
197 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
198 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
200 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
201 nxt_specif <> specify ?!
203 if nxt<>(Add_Relation
204 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
205 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
207 val nxt = tac2tac_ pt p nxt;
208 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
209 ------------------------------ FIXXXXME.meNEW !!! ---*)
211 (*val nxt = Specify_Theory "DiffApp" : tac*)
213 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
215 val nxt = tac2tac_ pt p nxt;
216 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
217 (*val nxt = Specify_Problem ["maximum_of","function"]*)
219 val nxt = tac2tac_ pt p nxt;
220 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
221 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
223 val nxt = tac2tac_ pt p nxt;
224 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
225 (*val nxt = Add_Given "boundVariable a" : tac*)
227 val nxt = tac2tac_ pt p nxt;
228 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
229 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
231 val nxt = tac2tac_ pt p nxt;
232 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
233 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
235 val nxt = tac2tac_ pt p nxt;
236 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
237 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
238 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
239 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
242 "--------- maximum example with 'specify', fmz = [] --------------";
243 "--------- maximum example with 'specify', fmz = [] --------------";
244 "--------- maximum example with 'specify', fmz = [] --------------";
246 val (dI',pI',mI') = empty_spec;
249 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
250 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
251 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
253 val nxt = tac2tac_ pt p nxt;
254 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
255 (*val nxt = Specify_Theory "e_domID" : tac*)
257 val nxt = Specify_Theory "DiffApp";
258 val nxt = tac2tac_ pt p nxt;
259 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
260 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
262 val nxt = Specify_Problem ["maximum_of","function"];
263 val nxt = tac2tac_ pt p nxt;
264 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
265 (*val nxt = Add_Given "fixedValues" : tac*)
267 val nxt = Add_Given "fixedValues [r=Arbfix]";
268 val nxt = tac2tac_ pt p nxt;
269 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
270 (*val nxt = Add_Find "maximum" : tac*)
272 val nxt = Add_Find "maximum A";
273 val nxt = tac2tac_ pt p nxt;
276 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
277 (*val nxt = Add_Find "valuesFor" : tac*)
279 val nxt = Add_Find "valuesFor [a]";
280 val nxt = tac2tac_ pt p nxt;
281 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
282 (*val nxt = Add_Relation "relations" ---
283 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
285 (*========== inhibit exn 010830 =======================================================*)
286 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
287 if nxt<>(Add_Relation "relations []")
288 then error "test specify, fmz <> []: nxt <> Add_Relation.."
289 else (); (*different with show_types !!!*)
291 (*========== inhibit exn 010830 =======================================================*)
293 val nxt = Add_Relation "relations [(A=a+b)]";
294 val nxt = tac2tac_ pt p nxt;
295 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
296 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
298 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
299 val nxt = tac2tac_ pt p nxt;
300 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
301 (*val nxt = Add_Given "boundVariable" : tac*)
303 val nxt = Add_Given "boundVariable alpha";
304 val nxt = tac2tac_ pt p nxt;
305 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
306 (*val nxt = Add_Given "interval" : tac*)
308 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
309 val nxt = tac2tac_ pt p nxt;
310 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
311 (*val nxt = Add_Given "errorBound" : tac*)
313 val nxt = Add_Given "errorBound (eps=999)";
314 val nxt = tac2tac_ pt p nxt;
315 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
316 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
318 (*========== inhibit exn 010830 =======================================================
319 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
320 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
321 then error "test specify, fmz <> []: nxt <> Add_Relation.."
324 ========== inhibit exn 010830 =======================================================*)
326 (*========== inhibit exn 000402 =======================================================
327 (* 2.4.00 nach Transfer specify -> hard_gen
328 val nxt = Apply_Method ("DiffApp","max_by_calculus");
329 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
330 (*val nxt = Empty_Tac : tac*)
331 ========== inhibit exn 000402 =======================================================*)
334 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
336 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
337 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
338 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
339 val Const ("Script.SubProblem",_) $
340 (Const ("Product_Type.Pair",_) $
342 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
343 (*...copied from stac2tac_*)
345 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
346 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
347 " REAL_LIST [c, c_2]]");
348 val ags = isalist2list ags';
349 val pI = ["linear","system"];
350 val pats = (#ppc o get_pbt) pI;
351 "-a1-----------------------------------------------------";
352 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
353 val xxx = match_ags (theory "EqSystem") pats ags;
354 "-a2-----------------------------------------------------";
355 case match_ags (theory "Isac") pats ags of
356 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
357 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
358 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
359 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
361 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
364 "-b------------------------------------------------------";
365 val Const ("Script.SubProblem",_) $
366 (Const ("Product_Type.Pair",_) $
368 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
369 (*...copied from stac2tac_*)
371 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
372 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
373 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
374 val ags = isalist2list ags';
375 val pI = ["linear","system"];
376 val pats = (#ppc o get_pbt) pI;
377 "-b1-----------------------------------------------------";
378 val xxx = match_ags (theory "Isac") pats ags;
379 "-b2-----------------------------------------------------";
380 case match_ags (theory "EqSystem") pats ags of
381 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
382 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
383 [_ $ Free ("c", _) $ _,
384 _ $ Free ("c_2", _) $ _]),
385 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
386 (* type of Find: [Free ("ss'''", "bool List.list")]*)
388 | _ => error "calchead.sml match_ags copy-named dropped --------";
391 "-c---ERROR case: stac is missing #Given equalities e_s--";
392 val stac as Const ("Script.SubProblem",_) $
393 (Const ("Product_Type.Pair",_) $
395 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
396 (*...copied from stac2tac_*)
398 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
399 " [REAL_LIST [c, c_2]]");
400 val ags = isalist2list ags';
401 val pI = ["linear","system"];
402 val pats = (#ppc o get_pbt) pI;
403 (*---inhibit exn provided by this testcase--------------------------
404 val xxx - match_ags (theory "EqSystem") pats ags;
405 -------------------------------------------------------------------*)
406 "-c1-----------------------------------------------------";
407 "--------------------------step through code match_ags---";
408 val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
409 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
410 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
411 val cy = filter is_copy_named pbt; (*=solution*)
412 (*---inhibit exn provided by this testcase--------------------------
413 val oris' - matc thy pbt' ags [];
414 -------------------------------------------------------------------*)
415 "-------------------------------step through code matc---";
416 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
417 (is_copy_named_idstr o free2str) t;
419 (*---inhibit exn provided by this testcase--------------------------
420 val opt - mtc thy p a;
421 -------------------------------------------------------------------*)
422 "--------------------------------step through code mtc---";
423 val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
425 val ttt - (dsc $ var);
426 (*---inhibit exn provided by this testcase--------------------------
427 cterm_of thy (dsc $ var);
428 -------------------------------------------------------------------*)
429 "-------------------------------------step through end---";
431 case ((match_ags (theory "EqSystem") pats ags)
432 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
433 [] => match_ags_msg pI stac ags
434 | _ => error "calchead.sml match_ags 1st arg missing --------";
437 "-d------------------------------------------------------";
438 val stac as Const ("Script.SubProblem",_) $
439 (Const ("Product_Type.Pair",_) $
441 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
442 (*...copied from stac2tac_*)
444 "SubProblem (Test',[univariate,equation,test]," ^
445 " [no_met]) [BOOL (x+1=2), REAL x]");
446 val AGS = isalist2list ags';
447 val pI = ["univariate","equation","test"];
448 val PATS = (#ppc o get_pbt) pI;
449 "-d1-----------------------------------------------------";
450 "--------------------------step through code match_ags---";
451 val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
452 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
453 val pbt' = filter_out is_copy_named pbt;
454 val cy = filter is_copy_named pbt;
455 val oris' = matc thy pbt' ags [];
456 "-------------------------------step through code matc---";
457 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
458 (is_copy_named_idstr o free2str) t;
460 val opt = mtc thy p a;
461 "--------------------------------step through code mtc---";
462 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
463 val ttt = (dsc $ var);
464 cterm_of thy (dsc $ var);
465 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
467 "-d2-----------------------------------------------------";
469 "-------------------------------step through code matc---";
470 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
471 (is_copy_named_idstr o free2str) t;
473 val opt = mtc thy p a;
474 "--------------------------------step through code mtc---";
475 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
476 val ttt = (dsc $ var);
477 cterm_of thy (dsc $ var);
478 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
479 "-d3-----------------------------------------------------";
480 pbt = []; (*true, base case*)
481 "-----------------continue step through code match_ags---";
482 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
483 "--------------------------------step through cpy_nam----";
484 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
485 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
486 "--------------------------------------------------------";
487 fun is_copy_named_generating_idstr str =
488 if is_copy_named_idstr str
489 then case (rev o explode) str of
490 (*"_"::"_"::"_"::_ => false*)
491 "'"::"'"::"'"::_ => false
494 fun is_copy_named_generating (_, (_, t)) =
495 (is_copy_named_generating_idstr o free2str) t;
496 "--------------------------------------------------------";
497 is_copy_named_generating p (*true*);
498 fun sel (_,_,d,ts) = comp_ts (d, ts);
499 val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
501 val ext = (last_elem o drop_last o explode o free2str) t;
503 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
504 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
505 val vals = map sel oris;
506 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
508 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
509 (assoc (vars'~~vals, cy'));
510 (*SOME (Free ("x", "RealDef.real")) : term option*)
511 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
513 "-----------------continue step through code match_ags---";
514 val cy' = map (cpy_nam pbt' oris') cy;
515 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
516 "-------------------------------------step through end---";
518 case match_ags thy PATS AGS of
519 [(1, [1], "#Given", Const ("Descript.equality", _),
520 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
521 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
522 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
523 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
525 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
528 "--------- regression test fun is_copy_named ------------";
529 "--------- regression test fun is_copy_named ------------";
530 "--------- regression test fun is_copy_named ------------";
531 val trm = (1, (2, @{term "v'i'"}));
532 if is_copy_named trm then () else error "regr. is_copy_named 1";
533 val trm = (1, (2, @{term "e_e"}));
534 if is_copy_named trm then error "regr. is_copy_named 2" else ();
535 val trm = (1, (2, @{term "L'''"}));
536 if is_copy_named trm then () else error "regr. is_copy_named 3";
538 (* out-comment 'structure CalcHead'...
539 val trm = (1, (2, @{term "v'i'"}));
540 if is_copy_named_generating trm then () else error "regr. is_copy_named";
541 val trm = (1, (2, @{term "L'''"}));
542 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
545 "--------- regr.test fun cpy_nam ------------------------";
546 "--------- regr.test fun cpy_nam ------------------------";
547 "--------- regr.test fun cpy_nam ------------------------";
548 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
549 (*the model-pattern, is_copy_named are filter_out*)
550 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
551 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
552 (*the model specific for an example*)
553 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
554 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
555 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
556 (*...all must be true*)
558 case cpy_nam pbt oris (hd cy) of
559 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
560 | _ => error "calchead.sml regr.test cpy_nam-1-";
562 (*new data: cpy_nam without changing the name*)
563 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
564 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
565 @{term "solution"}; type_of @{term "ss''' :: bool list"};
566 (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
567 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
568 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
569 (*the model specific for an example*)
570 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
571 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
572 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
573 (*could be more than 1*)];
575 case cpy_nam pbt oris (hd cy) of
576 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
577 | _ => error "calchead.sml regr.test cpy_nam-2-";
579 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
582 "--------- check specify phase --------------------------";
583 "--------- check specify phase --------------------------";
584 "--------- check specify phase --------------------------";
585 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
586 val fmz = ["functionTerm (x + 1)",
587 "integrateBy x","antiDerivative FF"];
589 ("Integrate",["integrate","function"],
590 ["diff","integration"]);
591 val p = e_pos'; val c = [];
593 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
594 (*> val it = "--- step 1 --" : string
598 (0, EdUndef, 0, Nundef,
600 {Find = [], With = [], Given = [], Where = [], Relate = []})))
602 val nxt = ("Model_Problem", Model_Problem) : string * tac
603 val p = ([], Pbl) : pos'
607 (["functionTerm (x^^^2 + 1)", "integrateBy x",
608 "antiDerivative FF"],
609 ("Integrate", ["integrate", "function"],
610 ["diff", "integration"])),
612 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
614 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
615 probl = [], branch = TransitiveB,
618 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
620 "[RealDef.real, RealDef.real] => RealDef.real") $
621 (Const ("Atools.pow",
622 "[RealDef.real, RealDef.real] => RealDef.real") $
623 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
624 Free ("1", "RealDef.real")]),
626 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
627 [Free ("x", "RealDef.real")]),
629 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
630 [Free ("FF", "RealDef.real")])],
631 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
632 Const ("Integrate.Integrate",
633 "(RealDef.real, RealDef.real) * => RealDef.real") $
634 (Const ("Product_Type.Pair",
635 "[RealDef.real, RealDef.real]
636 => (RealDef.real, RealDef.real) *") $
638 "[RealDef.real, RealDef.real] => RealDef.real") $
639 (Const ("Atools.pow",
640 "[RealDef.real, RealDef.real] => RealDef.real") $
641 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
642 Free ("1", "RealDef.real")) $
643 Free ("x", "RealDef.real"))),
644 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
646 "----- WN101007 worked until here (checked same as isac2002) ---";
647 if nxt = ("Model_Problem", Model_Problem) then ()
648 else error "clchead.sml: check specify phase step 1";
650 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
651 (*val it = "--- step 2 --" : string
652 val p = ([], Pbl) : pos'
656 (0, EdUndef, 0, Nundef,
658 {Find = [Incompl "Integrate.antiDerivative"],
660 Given = [Incompl "functionTerm", Incompl "integrateBy"],
662 Relate = []}))) : mout
663 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
667 (["functionTerm (x^^^2 + 1)", "integrateBy x",
668 "antiDerivative FF"],
669 ("Integrate", ["integrate", "function"],
670 ["diff", "integration"])),
673 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
675 cell = None, meth = [], spec =
676 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
677 [(0, [], false, "#Given",
678 Inc ((Const ("Descript.functionTerm",
679 "RealDef.real => Tools.una"),[]),
680 (Const ("empty", "'a"), []))),
681 (0, [], false, "#Given",
682 Inc ((Const ("Integrate.integrateBy",
683 "RealDef.real => Tools.una"),[]),
684 (Const ("empty", "'a"), []))),
685 (0, [], false, "#Find",
686 Inc ((Const ("Integrate.antiDerivative",
687 "RealDef.real => Tools.una"),[]),
688 (Const ("empty", "'a"), [])))],
689 branch = TransitiveB, origin =
691 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
693 "[RealDef.real, RealDef.real] => RealDef.real") $
694 (Const ("Atools.pow",
695 "[RealDef.real, RealDef.real] => RealDef.real") $
696 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
697 Free ("1", "RealDef.real")]),
699 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
700 [Free ("x", "RealDef.real")]),
702 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
703 [Free ("FF", "RealDef.real")])],
704 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
705 Const ("Integrate.Integrate",
706 "(RealDef.real, RealDef.real) * => RealDef.real") $
707 (Const ("Product_Type.Pair",
708 "[RealDef.real, RealDef.real]
709 => (RealDef.real, RealDef.real) *") $
711 "[RealDef.real, RealDef.real] => RealDef.real") $
712 (Const ("Atools.pow",
713 "[RealDef.real, RealDef.real] => RealDef.real") $
714 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
715 Free ("1", "RealDef.real")) $
716 Free ("x", "RealDef.real"))),
717 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
719 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
720 if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
721 else error "clchead.sml: check specify phase step 2";
723 val (p,_,f,nxt,_,pt) = me nxt p c pt;
724 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
725 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
726 else error "clchead.sml: check specify phase step 2";