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";
55 "--------- maximum example with 'specify' ------------------------";
56 "--------- maximum example with 'specify' ------------------------";
57 "--------- maximum example with 'specify' ------------------------";
58 (*" Specify_Problem (match_itms_oris) ";*)
60 ["fixedValues [r=Arbfix]","maximum A",
61 "valuesFor [a,b::real]",
62 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
63 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
64 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",
66 "boundVariable a","boundVariable b","boundVariable alpha",
67 "interval {x::real. 0 <= x & x <= 2*r}",
68 "interval {x::real. 0 <= x & x <= 2*r}",
69 "interval {x::real. 0 <= x & x <= pi}",
70 "errorBound (eps=(0::real))"];
72 ("DiffApp",["maximum_of","function"],
73 ["DiffApp","max_by_calculus"]);
76 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
77 val nxt = tac2tac_ pt p nxt;
78 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
79 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
81 val nxt = tac2tac_ pt p nxt;
82 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
85 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
86 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
88 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
89 Given=[Correct "fixedValues [r = Arbfix]"],
90 Relate=[Incompl "relations"], Where=[],With=[]})
91 then error "test-maximum.sml: model stepwise - different behaviour"
94 val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)");
95 (* WN1130630 THE maximum example WORKS IN isabisac09-2;
96 MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt.
97 Some tests have been broken much earlier,
98 see test/../calchead.sml "inhibit exn 010830". *)
99 (*========== inhibit exn WN1130630 maximum example broken =========================
100 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
101 ============ inhibit exn WN1130630 maximum example broken =======================*)
103 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
104 (*========== inhibit exn WN1130630 maximum example broken =========================
105 (* ERROR: Exception Bind raised *)
106 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
107 ============ inhibit exn WN1130630 maximum example broken =======================*)
109 val m = Specify_Problem ["maximum_of","function"];
110 val nxt = tac2tac_ pt p m;
111 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
112 (*========== inhibit exn WN1130630 maximum example broken =========================
113 if ppc<>(Problem ["maximum_of","function"],
114 {Find=[Incompl "maximum",Incompl "valuesFor"],
115 Given=[Correct "fixedValues [r = Arbfix]"],
116 Relate=[Incompl "relations []"], Where=[],With=[]})
117 then error "diffappl.sml: Specify_Problem different behaviour"
119 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
120 if ppc<>(Problem ["maximum_of","function"],
121 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
122 Given=[Correct "fixedValues [r = Arbfix]"],
123 Relate=[Missing "relations rs_"],Where=[],With=[]})
124 then error "diffappl.sml: Specify_Problem different behaviour"
126 ============ inhibit exn WN1130630 maximum example broken =======================*)
128 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
129 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
130 (*========== inhibit exn WN1130630 maximum example broken =========================
131 if ppc<>(Method ["DiffApp","max_by_calculus"],
132 {Find=[Incompl "maximum",Incompl "valuesFor"],
133 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
134 Missing "interval itv_",Missing "errorBound err_"],
135 Relate=[Incompl "relations []"],Where=[],With=[]})
136 then error "diffappl.sml: Specify_Method different behaviour"
138 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
139 if ppc<>(Method ["DiffApp","max_by_calculus"],
140 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
141 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
142 Missing "interval itv_",Missing "errorBound err_"],
143 Relate=[Missing "relations rs_"],Where=[],With=[]})
144 then error "diffappl.sml: Specify_Method different behaviour"
146 ============ inhibit exn WN1130630 maximum example broken =======================*)
148 "--------- maximum example with 'specify', fmz <> [] -------------";
149 "--------- maximum example with 'specify', fmz <> [] -------------";
150 "--------- maximum example with 'specify', fmz <> [] -------------";
152 ["fixedValues [r=Arbfix]","maximum A",
154 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
155 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
156 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
158 "boundVariable a","boundVariable b","boundVariable alpha",
159 "interval {x::real. 0 <= x & x <= 2*r}",
160 "interval {x::real. 0 <= x & x <= 2*r}",
161 "interval {x::real. 0 <= x & x <= pi}",
162 "errorBound (eps=(0::real))"];
164 ("DiffApp",["maximum_of","function"],
165 ["DiffApp","max_by_calculus"]);
167 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
168 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
170 val nxt = tac2tac_ pt p nxt;
171 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
172 val nxt = tac2tac_ pt p nxt;
173 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
174 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
176 val nxt = tac2tac_ pt p nxt;
177 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
178 (*val nxt = Add_Find "maximum (A::bool)" : 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 "valuesFor [(a::real)]" : 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 [(b::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_Relation "relations [A = a * b]" *)
192 val nxt = tac2tac_ pt p nxt;
193 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
194 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
196 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
197 nxt_specif <> specify ?!
199 if nxt<>(Add_Relation
200 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
201 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
203 val nxt = tac2tac_ pt p nxt;
204 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
205 ------------------------------ FIXXXXME.meNEW !!! ---*)
207 (*val nxt = Specify_Theory "DiffApp" : tac*)
209 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
211 val nxt = tac2tac_ pt p nxt;
212 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
213 (*val nxt = Specify_Problem ["maximum_of","function"]*)
215 val nxt = tac2tac_ pt p nxt;
216 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
217 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
219 val nxt = tac2tac_ pt p nxt;
220 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
221 (*val nxt = Add_Given "boundVariable a" : tac*)
223 val nxt = tac2tac_ pt p nxt;
224 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
225 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
227 val nxt = tac2tac_ pt p nxt;
228 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
229 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
231 val nxt = tac2tac_ pt p nxt;
232 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
233 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
234 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
235 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
238 "--------- maximum example with 'specify', fmz = [] --------------";
239 "--------- maximum example with 'specify', fmz = [] --------------";
240 "--------- maximum example with 'specify', fmz = [] --------------";
242 val (dI',pI',mI') = empty_spec;
245 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
246 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
247 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
249 val nxt = tac2tac_ pt p nxt;
250 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
251 (*val nxt = Specify_Theory "e_domID" : tac*)
253 val nxt = Specify_Theory "DiffApp";
254 val nxt = tac2tac_ pt p nxt;
255 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
256 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
258 val nxt = Specify_Problem ["maximum_of","function"];
259 val nxt = tac2tac_ pt p nxt;
260 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
261 (*val nxt = Add_Given "fixedValues" : tac*)
263 val nxt = Add_Given "fixedValues [r=Arbfix]";
264 val nxt = tac2tac_ pt p nxt;
265 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
266 (*val nxt = Add_Find "maximum" : tac*)
268 val nxt = Add_Find "maximum A";
269 val nxt = tac2tac_ pt p nxt;
272 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
273 (*val nxt = Add_Find "valuesFor" : tac*)
275 val nxt = Add_Find "valuesFor [a]";
276 val nxt = tac2tac_ pt p nxt;
277 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
278 (*val nxt = Add_Relation "relations" ---
279 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
281 (*========== inhibit exn 010830 =======================================================*)
282 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
283 if nxt<>(Add_Relation "relations []")
284 then error "test specify, fmz <> []: nxt <> Add_Relation.."
285 else (); (*different with show_types !!!*)
287 (*========== inhibit exn 010830 =======================================================*)
289 val nxt = Add_Relation "relations [(A=a+b)]";
290 val nxt = tac2tac_ pt p nxt;
291 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
292 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
294 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
295 val nxt = tac2tac_ pt p nxt;
296 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
297 (*val nxt = Add_Given "boundVariable" : tac*)
299 val nxt = Add_Given "boundVariable alpha";
300 val nxt = tac2tac_ pt p nxt;
301 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
302 (*val nxt = Add_Given "interval" : tac*)
304 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
305 val nxt = tac2tac_ pt p nxt;
306 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
307 (*val nxt = Add_Given "errorBound" : tac*)
309 val nxt = Add_Given "errorBound (eps=999)";
310 val nxt = tac2tac_ pt p nxt;
311 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
312 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
314 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
315 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
316 then error "test specify, fmz <> []: nxt <> Add_Relation.."
319 (* 2.4.00 nach Transfer specify -> hard_gen
320 val nxt = Apply_Method ("DiffApp","max_by_calculus");
321 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
322 (*val nxt = Empty_Tac : tac*)
324 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
325 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
326 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
327 val Const ("Script.SubProblem",_) $
328 (Const ("Product_Type.Pair",_) $
330 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
331 (*...copied from stac2tac_*)
333 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
334 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
335 " REAL_LIST [c, c_2]]");
336 val ags = isalist2list ags';
337 val pI = ["linear","system"];
338 val pats = (#ppc o get_pbt) pI;
339 "-a1-----------------------------------------------------";
340 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
341 val xxx = match_ags @{theory "EqSystem"} pats ags;
342 "-a2-----------------------------------------------------";
343 case match_ags @{theory "Isac"} pats ags of
344 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
345 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
346 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
347 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
349 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
351 "-b------------------------------------------------------";
352 val Const ("Script.SubProblem",_) $
353 (Const ("Product_Type.Pair",_) $
355 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
356 (*...copied from stac2tac_*)
358 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
359 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
360 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
361 val ags = isalist2list ags';
362 val pI = ["linear","system"];
363 val pats = (#ppc o get_pbt) pI;
364 "-b1-----------------------------------------------------";
365 val xxx = match_ags @{theory "Isac"} pats ags;
366 "-b2-----------------------------------------------------";
367 case match_ags @{theory "EqSystem"} pats ags of
368 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
369 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
370 [_ $ Free ("c", _) $ _,
371 _ $ Free ("c_2", _) $ _]),
372 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
373 (* type of Find: [Free ("ss'''", "bool List.list")]*)
375 | _ => error "calchead.sml match_ags copy-named dropped --------";
377 "-c---ERROR case: stac is missing #Given equalities e_s--";
378 val stac as Const ("Script.SubProblem",_) $
379 (Const ("Product_Type.Pair",_) $
381 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
382 (*...copied from stac2tac_*)
384 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
385 " [REAL_LIST [c, c_2]]");
386 val ags = isalist2list ags';
387 val pI = ["linear","system"];
388 val pats = (#ppc o get_pbt) pI;
389 (*---inhibit exn provided by this testcase--------------------------
390 val xxx - match_ags (theory "EqSystem") pats ags;
391 -------------------------------------------------------------------*)
392 "-c1-----------------------------------------------------";
393 "--------------------------step through code match_ags---";
394 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
395 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
396 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
397 val cy = filter is_copy_named pbt; (*=solution*)
398 (*---inhibit exn provided by this testcase--------------------------
399 val oris' - matc thy pbt' ags [];
400 -------------------------------------------------------------------*)
401 "-------------------------------step through code matc---";
402 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
403 (is_copy_named_idstr o free2str) t;
405 (*---inhibit exn provided by this testcase--------------------------
406 val opt - mtc thy p a;
407 -------------------------------------------------------------------*)
408 "--------------------------------step through code mtc---";
409 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
411 val ttt = (dsc $ var);
412 (*---inhibit exn provided by this testcase--------------------------
413 cterm_of thy (dsc $ var);
414 -------------------------------------------------------------------*)
416 "-------------------------------------step through end---";
417 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
418 val Const ("Script.SubProblem",_) $
419 (Const ("Product_Type.Pair",_) $
421 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
422 (*...copied from stac2tac_*)
424 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
425 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
426 " REAL_LIST [c, c_2]]");
427 val ags = isalist2list ags';
428 val pI = ["linear","system"];
429 val pats = (#ppc o get_pbt) pI;
430 "-a1-----------------------------------------------------";
431 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
432 val xxx = match_ags @{theory "EqSystem"} pats ags;
433 "-a2-----------------------------------------------------";
434 case match_ags @{theory "Isac"} pats ags of
435 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
436 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
437 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
438 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
440 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
442 "-b------------------------------------------------------";
443 val Const ("Script.SubProblem",_) $
444 (Const ("Product_Type.Pair",_) $
446 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
447 (*...copied from stac2tac_*)
449 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
450 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
451 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
452 val ags = isalist2list ags';
453 val pI = ["linear","system"];
454 val pats = (#ppc o get_pbt) pI;
455 "-b1-----------------------------------------------------";
456 val xxx = match_ags @{theory "Isac"} pats ags;
457 "-b2-----------------------------------------------------";
458 case match_ags @{theory "EqSystem"} pats ags of
459 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
460 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
461 [_ $ Free ("c", _) $ _,
462 _ $ Free ("c_2", _) $ _]),
463 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
464 (* type of Find: [Free ("ss'''", "bool List.list")]*)
466 | _ => error "calchead.sml match_ags copy-named dropped --------";
468 "-c---ERROR case: stac is missing #Given equalities e_s--";
469 val stac as Const ("Script.SubProblem",_) $
470 (Const ("Product_Type.Pair",_) $
472 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
473 (*...copied from stac2tac_*)
475 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
476 " [REAL_LIST [c, c_2]]");
477 val ags = isalist2list ags';
478 val pI = ["linear","system"];
479 val pats = (#ppc o get_pbt) pI;
480 (*---inhibit exn provided by this testcase--------------------------
481 val xxx - match_ags (theory "EqSystem") pats ags;
482 -------------------------------------------------------------------*)
483 "-c1-----------------------------------------------------";
484 "--------------------------step through code match_ags---";
485 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
486 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
487 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
488 val cy = filter is_copy_named pbt; (*=solution*)
489 (*---inhibit exn provided by this testcase--------------------------
490 val oris' - matc thy pbt' ags [];
491 -------------------------------------------------------------------*)
492 "-------------------------------step through code matc---";
493 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
494 (is_copy_named_idstr o free2str) t;
496 (*---inhibit exn provided by this testcase--------------------------
497 val opt - mtc thy p a;
498 -------------------------------------------------------------------*)
499 "--------------------------------step through code mtc---";
500 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
502 val ttt = (dsc $ var);
503 (*---inhibit exn provided by this testcase--------------------------
504 cterm_of thy (dsc $ var);
505 -------------------------------------------------------------------*)
506 "-------------------------------------step through end---";
508 case ((match_ags @{theory "EqSystem"} pats ags)
509 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
510 [] => match_ags_msg pI stac ags
511 | _ => error "calchead.sml match_ags 1st arg missing --------";
513 "-d------------------------------------------------------";
514 val stac as Const ("Script.SubProblem",_) $
515 (Const ("Product_Type.Pair",_) $
517 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
518 (*...copied from stac2tac_*)
520 "SubProblem (Test',[univariate,equation,test]," ^
521 " [no_met]) [BOOL (x+1=2), REAL x]");
522 val AGS = isalist2list ags';
523 val pI = ["univariate","equation","test"];
526 case ((match_ags @{theory "EqSystem"} pats ags)
527 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
528 [] => match_ags_msg pI stac ags
529 | _ => error "calchead.sml match_ags 1st arg missing --------";
531 "-d------------------------------------------------------";
532 val stac as Const ("Script.SubProblem",_) $
533 (Const ("Product_Type.Pair",_) $
535 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
536 (*...copied from stac2tac_*)
538 "SubProblem (Test',[univariate,equation,test]," ^
539 " [no_met]) [BOOL (x+1=2), REAL x]");
540 val AGS = isalist2list ags';
541 val pI = ["univariate","equation","test"];
542 val PATS = (#ppc o get_pbt) pI;
543 "-d1-----------------------------------------------------";
544 "--------------------------step through code match_ags---";
545 val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);
546 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
547 val pbt' = filter_out is_copy_named pbt;
548 val cy = filter is_copy_named pbt;
549 val oris' = matc thy pbt' ags [];
550 "-------------------------------step through code matc---";
551 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
552 (is_copy_named_idstr o free2str) t;
554 val opt = mtc thy p a;
555 "--------------------------------step through code mtc---";
556 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
557 val ttt = (dsc $ var);
558 cterm_of thy (dsc $ var);
559 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
561 "-d2-----------------------------------------------------";
563 "-------------------------------step through code matc---";
564 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
565 (is_copy_named_idstr o free2str) t;
567 val opt = mtc thy p a;
568 "--------------------------------step through code mtc---";
569 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
570 val ttt = (dsc $ var);
571 cterm_of thy (dsc $ var);
572 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
573 "-d3-----------------------------------------------------";
574 pbt = []; (*true, base case*)
575 "-----------------continue step through code match_ags---";
576 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
577 "--------------------------------step through cpy_nam----";
578 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
579 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
580 "--------------------------------------------------------";
581 fun is_copy_named_generating_idstr str =
582 if is_copy_named_idstr str
583 then case (rev o Symbol.explode) str of
584 (*"_"::"_"::"_"::_ => false*)
585 "'"::"'"::"'"::_ => false
588 fun is_copy_named_generating (_, (_, t)) =
589 (is_copy_named_generating_idstr o free2str) t;
590 "--------------------------------------------------------";
591 is_copy_named_generating p (*true*);
592 fun sel (_,_,d,ts) = comp_ts (d, ts);
593 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
595 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
597 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
598 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
599 val vals = map sel oris;
600 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
602 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
603 (assoc (vars'~~vals, cy'));
604 (*SOME (Free ("x", "RealDef.real")) : term option*)
605 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
607 "-----------------continue step through code match_ags---";
608 val cy' = map (cpy_nam pbt' oris') cy;
609 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
610 "-------------------------------------step through end---";
612 case match_ags thy PATS AGS of
613 [(1, [1], "#Given", Const ("Descript.equality", _),
614 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
615 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
616 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
617 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
619 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
621 "--------- regression test fun is_copy_named ------------";
622 "--------- regression test fun is_copy_named ------------";
623 "--------- regression test fun is_copy_named ------------";
624 val trm = (1, (2, @{term "v'i'"}));
625 if is_copy_named trm then () else error "regr. is_copy_named 1";
626 val trm = (1, (2, @{term "e_e"}));
627 if is_copy_named trm then error "regr. is_copy_named 2" else ();
628 val trm = (1, (2, @{term "L'''"}));
629 if is_copy_named trm then () else error "regr. is_copy_named 3";
631 (* out-comment 'structure CalcHead'...
632 val trm = (1, (2, @{term "v'i'"}));
633 if is_copy_named_generating trm then () else error "regr. is_copy_named";
634 val trm = (1, (2, @{term "L'''"}));
635 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
638 "--------- regr.test fun cpy_nam ------------------------";
639 "--------- regr.test fun cpy_nam ------------------------";
640 "--------- regr.test fun cpy_nam ------------------------";
641 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
642 (*the model-pattern, is_copy_named are filter_out*)
643 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
644 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
645 (*the model specific for an example*)
646 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
647 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
648 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
649 (*...all must be true*)
651 case cpy_nam pbt oris (hd cy) of
652 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
653 | _ => error "calchead.sml regr.test cpy_nam-1-";
655 (*new data: cpy_nam without changing the name*)
656 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
657 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
658 @{term "solution"}; type_of @{term "ss''' :: bool list"};
659 (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
660 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
661 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
662 (*the model specific for an example*)
663 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
664 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
665 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
666 (*could be more than 1*)];
668 case cpy_nam pbt oris (hd cy) of
669 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
670 | _ => error "calchead.sml regr.test cpy_nam-2-";
672 "--------- check specify phase --------------------------";
673 "--------- check specify phase --------------------------";
674 "--------- check specify phase --------------------------";
675 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
676 val fmz = ["functionTerm (x + 1)",
677 "integrateBy x","antiDerivative FF"];
679 ("Integrate",["integrate","function"],
680 ["diff","integration"]);
681 val p = e_pos'; val c = [];
683 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
684 (*> val it = "--- step 1 --" : string
688 (0, EdUndef, 0, Nundef,
690 {Find = [], With = [], Given = [], Where = [], Relate = []})))
692 val nxt = ("Model_Problem", Model_Problem) : string * tac
693 val p = ([], Pbl) : pos'
697 (["functionTerm (x^^^2 + 1)", "integrateBy x",
698 "antiDerivative FF"],
699 ("Integrate", ["integrate", "function"],
700 ["diff", "integration"])),
702 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
704 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
705 probl = [], branch = TransitiveB,
708 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
710 "[RealDef.real, RealDef.real] => RealDef.real") $
711 (Const ("Atools.pow",
712 "[RealDef.real, RealDef.real] => RealDef.real") $
713 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
714 Free ("1", "RealDef.real")]),
716 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
717 [Free ("x", "RealDef.real")]),
719 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
720 [Free ("FF", "RealDef.real")])],
721 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
722 Const ("Integrate.Integrate",
723 "(RealDef.real, RealDef.real) * => RealDef.real") $
724 (Const ("Product_Type.Pair",
725 "[RealDef.real, RealDef.real]
726 => (RealDef.real, RealDef.real) *") $
728 "[RealDef.real, RealDef.real] => RealDef.real") $
729 (Const ("Atools.pow",
730 "[RealDef.real, RealDef.real] => RealDef.real") $
731 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
732 Free ("1", "RealDef.real")) $
733 Free ("x", "RealDef.real"))),
734 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
736 "----- WN101007 worked until here (checked same as isac2002) ---";
737 if nxt = ("Model_Problem", Model_Problem) then ()
738 else error "clchead.sml: check specify phase step 1";
740 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
741 (*val it = "--- step 2 --" : string
742 val p = ([], Pbl) : pos'
746 (0, EdUndef, 0, Nundef,
748 {Find = [Incompl "Integrate.antiDerivative"],
750 Given = [Incompl "functionTerm", Incompl "integrateBy"],
752 Relate = []}))) : mout
753 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
757 (["functionTerm (x^^^2 + 1)", "integrateBy x",
758 "antiDerivative FF"],
759 ("Integrate", ["integrate", "function"],
760 ["diff", "integration"])),
763 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
765 cell = None, meth = [], spec =
766 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
767 [(0, [], false, "#Given",
768 Inc ((Const ("Descript.functionTerm",
769 "RealDef.real => Tools.una"),[]),
770 (Const ("empty", "'a"), []))),
771 (0, [], false, "#Given",
772 Inc ((Const ("Integrate.integrateBy",
773 "RealDef.real => Tools.una"),[]),
774 (Const ("empty", "'a"), []))),
775 (0, [], false, "#Find",
776 Inc ((Const ("Integrate.antiDerivative",
777 "RealDef.real => Tools.una"),[]),
778 (Const ("empty", "'a"), [])))],
779 branch = TransitiveB, origin =
781 Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
783 "[RealDef.real, RealDef.real] => RealDef.real") $
784 (Const ("Atools.pow",
785 "[RealDef.real, RealDef.real] => RealDef.real") $
786 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
787 Free ("1", "RealDef.real")]),
789 Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
790 [Free ("x", "RealDef.real")]),
792 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
793 [Free ("FF", "RealDef.real")])],
794 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
795 Const ("Integrate.Integrate",
796 "(RealDef.real, RealDef.real) * => RealDef.real") $
797 (Const ("Product_Type.Pair",
798 "[RealDef.real, RealDef.real]
799 => (RealDef.real, RealDef.real) *") $
801 "[RealDef.real, RealDef.real] => RealDef.real") $
802 (Const ("Atools.pow",
803 "[RealDef.real, RealDef.real] => RealDef.real") $
804 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
805 Free ("1", "RealDef.real")) $
806 Free ("x", "RealDef.real"))),
807 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
809 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
810 if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
811 else error "clchead.sml: check specify phase step 2";
813 val (p,_,f,nxt,_,pt) = me nxt p c pt;
814 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
815 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
816 else error "clchead.sml: check specify phase step 2";
818 "--------- check: fmz matches pbt -----------------------";
819 "--------- check: fmz matches pbt -----------------------";
820 "--------- check: fmz matches pbt -----------------------";
821 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
822 "the following fmz caused the above error";
823 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
824 val pI = ["plus_minus","polynom","vereinfachen"];
826 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
827 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
828 (*#############################^^^^^^^^^ defined by Isabelle*)
829 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
830 [Free ("N", _ (*"RealDef.real"*))])],
831 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
832 "#undef means: the element with description TERM in fmz did not match ";
833 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
834 "defined in Simplify.thy";
836 "So we try out how to create Simplify.Term:";
838 val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
839 " ^^^^^^^^^ see above";
843 val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
844 " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
848 val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
849 " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
850 " and unsed in pbl [plus_minus,polynom,vereinfachen]";
853 "----- so this is the correct fmz:";
854 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
855 val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
856 (*########################^^^^^^^^^ defined in Simplify.thy*)
857 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
859 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
861 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
862 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
863 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;