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 "--------------------------------------------------------";
24 (*========== inhibit exn =======================================================
25 "--------- get_interval after replace} other 2 ----------";
26 "--------- get_interval after replace} other 2 ----------";
27 "--------- get_interval after replace} other 2 ----------";
30 [(["equality (x+1=2)", "solveFor x","solutions L"],
32 ["sqroot-test","univariate","equation","test"],
33 ["Test","squ-equ-test-subpbl1"]))];
36 autoCalculate 1 CompleteCalc;
37 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
38 replaceFormula 1 "x = 1";
39 (*... returns calcChangedEvent with ...*)
40 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
41 val ((pt,_),_) = get_calc 1;
43 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
44 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
45 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
46 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
47 ([3, 2], Res)] then () else
48 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
50 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
52 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
53 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
54 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
59 "--------- maximum example with 'specify' ------------------------";
60 "--------- maximum example with 'specify' ------------------------";
61 "--------- maximum example with 'specify' ------------------------";
62 (*" Specify_Problem (match_itms_oris) ";*)
64 ["fixedValues [r=Arbfix]","maximum A",
66 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
67 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
68 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
70 "boundVariable a","boundVariable b","boundVariable alpha",
71 "interval {x::real. 0 <= x & x <= 2*r}",
72 "interval {x::real. 0 <= x & x <= 2*r}",
73 "interval {x::real. 0 <= x & x <= pi}",
74 "errorBound (eps=(0::real))"];
76 ("DiffApp.thy",["maximum_of","function"],
77 ["DiffApp","max_by_calculus"]);
80 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
81 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
83 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
84 val nxt = tac2tac_ pt p nxt;
85 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
86 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
88 val nxt = tac2tac_ pt p nxt;
89 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
93 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
94 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
95 (*uncaught exception TYPE 6.5.03*)
98 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
99 Given=[Correct "fixedValues [r = Arbfix]"],
100 Relate=[Incompl "relations []"], Where=[],With=[]})
101 then error "test-maximum.sml: model stepwise - different behaviour"
102 else (); (*different with show_types !!!*)
105 (*-----appl_add should not create Error', but accept as Sup,Syn
106 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
107 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
109 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
110 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
113 val m = Specify_Problem ["maximum_of","function"];
114 val nxt = tac2tac_ pt p m;
115 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
118 if ppc<>(Problem ["maximum_of","function"],
119 {Find=[Incompl "maximum",Incompl "valuesFor"],
120 Given=[Correct "fixedValues [r = Arbfix]"],
121 Relate=[Incompl "relations []"], Where=[],With=[]})
122 then error "diffappl.sml: Specify_Problem different behaviour"
124 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
125 if ppc<>(Problem ["maximum_of","function"],
126 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
127 Given=[Correct "fixedValues [r = Arbfix]"],
128 Relate=[Missing "relations rs_"],Where=[],With=[]})
129 then error "diffappl.sml: Specify_Problem different behaviour"
132 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
133 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
136 if ppc<>(Method ["DiffApp","max_by_calculus"],
137 {Find=[Incompl "maximum",Incompl "valuesFor"],
138 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
139 Missing "interval itv_",Missing "errorBound err_"],
140 Relate=[Incompl "relations []"],Where=[],With=[]})
141 then error "diffappl.sml: Specify_Method different behaviour"
143 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
144 if ppc<>(Method ["DiffApp","max_by_calculus"],
145 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
146 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
147 Missing "interval itv_",Missing "errorBound err_"],
148 Relate=[Missing "relations rs_"],Where=[],With=[]})
149 then error "diffappl.sml: Specify_Method different behaviour"
154 "--------- maximum example with 'specify', fmz <> [] -------------";
155 "--------- maximum example with 'specify', fmz <> [] -------------";
156 "--------- maximum example with 'specify', fmz <> [] -------------";
158 ["fixedValues [r=Arbfix]","maximum A",
160 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
161 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
162 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
164 "boundVariable a","boundVariable b","boundVariable alpha",
165 "interval {x::real. 0 <= x & x <= 2*r}",
166 "interval {x::real. 0 <= x & x <= 2*r}",
167 "interval {x::real. 0 <= x & x <= pi}",
168 "errorBound (eps=(0::real))"];
170 ("DiffApp.thy",["maximum_of","function"],
171 ["DiffApp","max_by_calculus"]);
173 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
174 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
176 val nxt = tac2tac_ pt p nxt;
177 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
178 val nxt = tac2tac_ pt p nxt;
179 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
180 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : 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 "maximum (A::bool)" : 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 [(a::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_Find "valuesFor [(b::real)]" : tac*)
194 val nxt = tac2tac_ pt p nxt;
195 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
196 (*val nxt = Add_Relation "relations [A = a * b]" *)
198 val nxt = tac2tac_ pt p nxt;
199 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
200 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
202 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
203 nxt_specif <> specify ?!
205 if nxt<>(Add_Relation
206 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
207 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
209 val nxt = tac2tac_ pt p nxt;
210 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
211 ------------------------------ FIXXXXME.meNEW !!! ---*)
213 (*val nxt = Specify_Theory "DiffApp.thy" : tac*)
215 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
217 val nxt = tac2tac_ pt p nxt;
218 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
219 (*val nxt = Specify_Problem ["maximum_of","function"]*)
221 val nxt = tac2tac_ pt p nxt;
222 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
223 (*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
225 val nxt = tac2tac_ pt p nxt;
226 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
227 (*val nxt = Add_Given "boundVariable a" : tac*)
229 val nxt = tac2tac_ pt p nxt;
230 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
231 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
233 val nxt = tac2tac_ pt p nxt;
234 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
235 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
237 val nxt = tac2tac_ pt p nxt;
238 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
239 (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
240 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
241 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
244 "--------- maximum example with 'specify', fmz = [] --------------";
245 "--------- maximum example with 'specify', fmz = [] --------------";
246 "--------- maximum example with 'specify', fmz = [] --------------";
248 val (dI',pI',mI') = empty_spec;
251 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
252 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
253 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
255 val nxt = tac2tac_ pt p nxt;
256 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
257 (*val nxt = Specify_Theory "e_domID" : tac*)
259 val nxt = Specify_Theory "DiffApp.thy";
260 val nxt = tac2tac_ pt p nxt;
261 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
262 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
264 val nxt = Specify_Problem ["maximum_of","function"];
265 val nxt = tac2tac_ pt p nxt;
266 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
267 (*val nxt = Add_Given "fixedValues" : tac*)
269 val nxt = Add_Given "fixedValues [r=Arbfix]";
270 val nxt = tac2tac_ pt p nxt;
271 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
272 (*val nxt = Add_Find "maximum" : tac*)
274 val nxt = Add_Find "maximum A";
275 val nxt = tac2tac_ pt p nxt;
278 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
279 (*val nxt = Add_Find "valuesFor" : tac*)
281 val nxt = Add_Find "valuesFor [a]";
282 val nxt = tac2tac_ pt p nxt;
283 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
284 (*val nxt = Add_Relation "relations" ---
285 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
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 !!!*)
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") *)
317 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
318 if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
319 then error "test specify, fmz <> []: nxt <> Add_Relation.."
323 (* 2.4.00 nach Transfer specify -> hard_gen
324 val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
325 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
326 (*val nxt = Empty_Tac : tac*)
328 ============ inhibit exn =====================================================*)
330 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
332 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
333 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
334 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
335 val Const ("Script.SubProblem",_) $
338 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
339 (*...copied from stac2tac_*)
341 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
342 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
343 " REAL_LIST [c, c_2]]");
344 val ags = isalist2list ags';
345 val pI = ["linear","system"];
346 val pats = (#ppc o get_pbt) pI;
347 "-a1-----------------------------------------------------";
348 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
349 val xxx = match_ags (theory "EqSystem") pats ags;
350 "-a2-----------------------------------------------------";
351 case match_ags (theory "Isac") pats ags of
352 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
353 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
354 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
355 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
357 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
360 "-b------------------------------------------------------";
361 val Const ("Script.SubProblem",_) $
364 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
365 (*...copied from stac2tac_*)
367 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
368 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
369 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
370 val ags = isalist2list ags';
371 val pI = ["linear","system"];
372 val pats = (#ppc o get_pbt) pI;
373 "-b1-----------------------------------------------------";
374 val xxx = match_ags (theory "Isac") pats ags;
375 "-b2-----------------------------------------------------";
376 case match_ags (theory "EqSystem") pats ags of
377 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
378 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
379 [_ $ Free ("c", _) $ _,
380 _ $ Free ("c_2", _) $ _]),
381 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
382 (* type of Find: [Free ("ss'''", "bool List.list")]*)
384 | _ => error "calchead.sml match_ags copy-named dropped --------";
387 "-c---ERROR case: stac is missing #Given equalities e_s--";
388 val stac as Const ("Script.SubProblem",_) $
391 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
392 (*...copied from stac2tac_*)
394 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
395 " [REAL_LIST [c, c_2]]");
396 val ags = isalist2list ags';
397 val pI = ["linear","system"];
398 val pats = (#ppc o get_pbt) pI;
399 (*---inhibit exn provided by this testcase--------------------------
400 val xxx - match_ags (theory "EqSystem") pats ags;
401 -------------------------------------------------------------------*)
402 "-c1-----------------------------------------------------";
403 "--------------------------step through code match_ags---";
404 val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
405 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
406 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
407 val cy = filter is_copy_named pbt; (*=solution*)
408 (*---inhibit exn provided by this testcase--------------------------
409 val oris' - matc thy pbt' ags [];
410 -------------------------------------------------------------------*)
411 "-------------------------------step through code matc---";
412 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
413 (is_copy_named_idstr o free2str) t;
415 (*---inhibit exn provided by this testcase--------------------------
416 val opt - mtc thy p a;
417 -------------------------------------------------------------------*)
418 "--------------------------------step through code mtc---";
419 val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
421 val ttt - (dsc $ var);
422 (*---inhibit exn provided by this testcase--------------------------
423 cterm_of thy (dsc $ var);
424 -------------------------------------------------------------------*)
425 "-------------------------------------step through end---";
427 case ((match_ags (theory "EqSystem") pats ags)
428 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
429 [] => match_ags_msg pI stac ags
430 | _ => error "calchead.sml match_ags 1st arg missing --------";
433 "-d------------------------------------------------------";
434 val stac as Const ("Script.SubProblem",_) $
437 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
438 (*...copied from stac2tac_*)
440 "SubProblem (Test',[univariate,equation,test]," ^
441 " [no_met]) [BOOL (x+1=2), REAL x]");
442 val AGS = isalist2list ags';
443 val pI = ["univariate","equation","test"];
444 val PATS = (#ppc o get_pbt) pI;
445 "-d1-----------------------------------------------------";
446 "--------------------------step through code match_ags---";
447 val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
448 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
449 val pbt' = filter_out is_copy_named pbt;
450 val cy = filter is_copy_named pbt;
451 val oris' = matc thy pbt' ags [];
452 "-------------------------------step through code matc---";
453 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
454 (is_copy_named_idstr o free2str) t;
456 val opt = mtc thy p a;
457 "--------------------------------step through code mtc---";
458 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
459 val ttt = (dsc $ var);
460 cterm_of thy (dsc $ var);
461 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
463 "-d2-----------------------------------------------------";
465 "-------------------------------step through code matc---";
466 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
467 (is_copy_named_idstr o free2str) t;
469 val opt = mtc thy p a;
470 "--------------------------------step through code mtc---";
471 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
472 val ttt = (dsc $ var);
473 cterm_of thy (dsc $ var);
474 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
475 "-d3-----------------------------------------------------";
476 pbt = []; (*true, base case*)
477 "-----------------continue step through code match_ags---";
478 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
479 "--------------------------------step through cpy_nam----";
480 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
481 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
482 "--------------------------------------------------------";
483 fun is_copy_named_generating_idstr str =
484 if is_copy_named_idstr str
485 then case (rev o explode) str of
486 (*"_"::"_"::"_"::_ => false*)
487 "'"::"'"::"'"::_ => false
490 fun is_copy_named_generating (_, (_, t)) =
491 (is_copy_named_generating_idstr o free2str) t;
492 "--------------------------------------------------------";
493 is_copy_named_generating p (*true*);
494 fun sel (_,_,d,ts) = comp_ts (d, ts);
495 val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
497 val ext = (last_elem o drop_last o explode o free2str) t;
499 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
500 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
501 val vals = map sel oris;
502 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
504 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
505 (assoc (vars'~~vals, cy'));
506 (*SOME (Free ("x", "RealDef.real")) : term option*)
507 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
509 "-----------------continue step through code match_ags---";
510 val cy' = map (cpy_nam pbt' oris') cy;
511 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
512 "-------------------------------------step through end---";
514 case match_ags thy PATS AGS of
515 [(1, [1], "#Given", Const ("Descript.equality", _),
516 [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $
517 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
518 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
519 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
521 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
524 "--------- regression test fun is_copy_named ------------";
525 "--------- regression test fun is_copy_named ------------";
526 "--------- regression test fun is_copy_named ------------";
527 val trm = (1, (2, @{term "v'i'"}));
528 if is_copy_named trm then () else error "regr. is_copy_named 1";
529 val trm = (1, (2, @{term "e_e"}));
530 if is_copy_named trm then error "regr. is_copy_named 2" else ();
531 val trm = (1, (2, @{term "L'''"}));
532 if is_copy_named trm then () else error "regr. is_copy_named 3";
534 (* out-comment 'structure CalcHead'...
535 val trm = (1, (2, @{term "v'i'"}));
536 if is_copy_named_generating trm then () else error "regr. is_copy_named";
537 val trm = (1, (2, @{term "L'''"}));
538 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
541 "--------- regr.test fun cpy_nam ------------------------";
542 "--------- regr.test fun cpy_nam ------------------------";
543 "--------- regr.test fun cpy_nam ------------------------";
544 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
545 (*the model-pattern, is_copy_named are filter_out*)
546 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
547 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
548 (*the model specific for an example*)
549 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
550 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
551 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
552 (*...all must be true*)
554 case cpy_nam pbt oris (hd cy) of
555 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
556 | _ => error "calchead.sml regr.test cpy_nam-1-";
558 (*new data: cpy_nam without changing the name*)
559 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
560 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
561 @{term "solution"}; type_of @{term "ss''' :: bool list"};
562 (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
563 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
564 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
565 (*the model specific for an example*)
566 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
567 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
568 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
569 (*could be more than 1*)];
571 case cpy_nam pbt oris (hd cy) of
572 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
573 | _ => error "calchead.sml regr.test cpy_nam-2-";
575 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
578 "--------- check specify phase --------------------------";
579 "--------- check specify phase --------------------------";
580 "--------- check specify phase --------------------------";
581 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
582 val fmz = ["functionTerm (x + 1)",
583 "integrateBy x","antiDerivative FF"];
585 ("Integrate",["integrate","function"],
586 ["diff","integration"]);
587 val p = e_pos'; val c = [];
589 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
590 (*> val it = "--- step 1 --" : string
594 (0, EdUndef, 0, Nundef,
596 {Find = [], With = [], Given = [], Where = [], Relate = []})))
598 val nxt = ("Model_Problem", Model_Problem) : string * tac
599 val p = ([], Pbl) : pos'
603 (["functionTerm (x^^^2 + 1)", "integrateBy x",
604 "antiDerivative FF"],
605 ("Integrate.thy", ["integrate", "function"],
606 ["diff", "integration"])),
608 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
610 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
611 probl = [], branch = TransitiveB,
614 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
616 "[RealDef.real, RealDef.real] => RealDef.real") $
617 (Const ("Atools.pow",
618 "[RealDef.real, RealDef.real] => RealDef.real") $
619 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
620 Free ("1", "RealDef.real")]),
622 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
623 [Free ("x", "RealDef.real")]),
625 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
626 [Free ("FF", "RealDef.real")])],
627 ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
628 Const ("Integrate.Integrate",
629 "(RealDef.real, RealDef.real) * => RealDef.real") $
631 "[RealDef.real, RealDef.real]
632 => (RealDef.real, RealDef.real) *") $
634 "[RealDef.real, RealDef.real] => RealDef.real") $
635 (Const ("Atools.pow",
636 "[RealDef.real, RealDef.real] => RealDef.real") $
637 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
638 Free ("1", "RealDef.real")) $
639 Free ("x", "RealDef.real"))),
640 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
642 "----- WN101007 worked until here (checked same as isac2002) ---";
644 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
645 (*val it = "--- step 2 --" : string
646 val p = ([], Pbl) : pos'
650 (0, EdUndef, 0, Nundef,
652 {Find = [Incompl "Integrate.antiDerivative"],
654 Given = [Incompl "functionTerm", Incompl "integrateBy"],
656 Relate = []}))) : mout
657 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
661 (["functionTerm (x^^^2 + 1)", "integrateBy x",
662 "antiDerivative FF"],
663 ("Integrate.thy", ["integrate", "function"],
664 ["diff", "integration"])),
667 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
669 cell = None, meth = [], spec =
670 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
671 [(0, [], false, "#Given",
672 Inc ((Const ("Descript.functionTerm",
673 "RealDef.real => Tools.una"),[]),
674 (Const ("empty", "'a"), []))),
675 (0, [], false, "#Given",
676 Inc ((Const ("Integrate.integrateBy",
677 "RealDef.real => Tools.una"),[]),
678 (Const ("empty", "'a"), []))),
679 (0, [], false, "#Find",
680 Inc ((Const ("Integrate.antiDerivative",
681 "RealDef.real => Tools.una"),[]),
682 (Const ("empty", "'a"), [])))],
683 branch = TransitiveB, origin =
685 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
687 "[RealDef.real, RealDef.real] => RealDef.real") $
688 (Const ("Atools.pow",
689 "[RealDef.real, RealDef.real] => RealDef.real") $
690 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
691 Free ("1", "RealDef.real")]),
693 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
694 [Free ("x", "RealDef.real")]),
696 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
697 [Free ("FF", "RealDef.real")])],
698 ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
699 Const ("Integrate.Integrate",
700 "(RealDef.real, RealDef.real) * => RealDef.real") $
702 "[RealDef.real, RealDef.real]
703 => (RealDef.real, RealDef.real) *") $
705 "[RealDef.real, RealDef.real] => RealDef.real") $
706 (Const ("Atools.pow",
707 "[RealDef.real, RealDef.real] => RealDef.real") $
708 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
709 Free ("1", "RealDef.real")) $
710 Free ("x", "RealDef.real"))),
711 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
713 "----- WN101007 ptree checked same as isac2002, diff. in nxt ---";
716 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
717 nxt_specif_additem "#Given" ;
721 val (p,_,f,nxt,_,pt) = me nxt p c pt;
722 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)