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 "--------- fun typeless ---------------------------------";
22 "--------- fun variants_in ------------------------------";
23 "--------- fun is_list_type -----------------------------";
24 "--------- fun has_list_type ----------------------------";
25 "--------- fun tag_form ---------------------------------";
26 "--------- fun foldr1, foldl1 ---------------------------";
27 "--------------------------------------------------------";
28 "--------------------------------------------------------";
29 "--------------------------------------------------------";
32 "--------- get_interval after replace} other 2 ----------";
33 "--------- get_interval after replace} other 2 ----------";
34 "--------- get_interval after replace} other 2 ----------";
36 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
37 ("Test", ["sqroot-test","univariate","equation","test"],
38 ["Test","squ-equ-test-subpbl1"]))];
41 autoCalculate 1 CompleteCalc;
42 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
43 replaceFormula 1 "x = 1";
44 (*... returns calcChangedEvent with ...*)
45 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
46 val ((pt,_),_) = get_calc 1;
48 default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
49 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
50 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
51 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
52 ([3, 2], Res)] then () else
53 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
55 default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
56 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
57 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
58 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
60 "--------- maximum example with 'specify' ------------------------";
61 "--------- maximum example with 'specify' ------------------------";
62 "--------- maximum example with 'specify' ------------------------";
63 (*" Specify_Problem (match_itms_oris) ";*)
65 ["fixedValues [r=Arbfix]","maximum A",
66 "valuesFor [a,b::real]",
67 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
68 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
69 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",
71 "boundVariable a","boundVariable b","boundVariable alpha",
72 "interval {x::real. 0 <= x & x <= 2*r}",
73 "interval {x::real. 0 <= x & x <= 2*r}",
74 "interval {x::real. 0 <= x & x <= pi}",
75 "errorBound (eps=(0::real))"];
77 ("DiffApp",["maximum_of","function"],
78 ["DiffApp","max_by_calculus"]);
81 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
82 val nxt = tac2tac_ pt p nxt;
83 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
84 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
86 val nxt = tac2tac_ pt p nxt;
87 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
90 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
91 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
93 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
94 Given=[Correct "fixedValues [r = Arbfix]"],
95 Relate=[Incompl "relations"], Where=[],With=[]})
96 then error "test-maximum.sml: model stepwise - different behaviour"
99 val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)");
100 (* WN1130630 THE maximum example WORKS IN isabisac09-2;
101 MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt.
102 Some tests have been broken much earlier,
103 see test/../calchead.sml "inhibit exn 010830". *)
104 (*========== inhibit exn WN1130630 maximum example broken =========================
105 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
106 ============ inhibit exn WN1130630 maximum example broken =======================*)
108 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
109 (*========== inhibit exn WN1130630 maximum example broken =========================
110 (* ERROR: Exception Bind raised *)
111 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
112 ============ inhibit exn WN1130630 maximum example broken =======================*)
114 val m = Specify_Problem ["maximum_of","function"];
115 val nxt = tac2tac_ pt p m;
116 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
117 (*========== inhibit exn WN1130630 maximum example broken =========================
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"
131 ============ inhibit exn WN1130630 maximum example broken =======================*)
133 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
134 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
135 (*========== inhibit exn WN1130630 maximum example broken =========================
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"
151 ============ inhibit exn WN1130630 maximum example broken =======================*)
153 "--------- maximum example with 'specify', fmz <> [] -------------";
154 "--------- maximum example with 'specify', fmz <> [] -------------";
155 "--------- maximum example with 'specify', fmz <> [] -------------";
157 ["fixedValues [r=Arbfix]","maximum A",
159 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
160 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
161 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
163 "boundVariable a","boundVariable b","boundVariable alpha",
164 "interval {x::real. 0 <= x & x <= 2*r}",
165 "interval {x::real. 0 <= x & x <= 2*r}",
166 "interval {x::real. 0 <= x & x <= pi}",
167 "errorBound (eps=(0::real))"];
169 ("DiffApp",["maximum_of","function"],
170 ["DiffApp","max_by_calculus"]);
172 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
173 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
175 val nxt = tac2tac_ pt p nxt;
176 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
177 val nxt = tac2tac_ pt p nxt;
178 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
179 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
181 val nxt = tac2tac_ pt p nxt;
182 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
183 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
185 val nxt = tac2tac_ pt p nxt;
186 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
187 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
189 val nxt = tac2tac_ pt p nxt;
190 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
191 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
193 val nxt = tac2tac_ pt p nxt;
194 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
195 (*val nxt = Add_Relation "relations [A = a * b]" *)
197 val nxt = tac2tac_ pt p nxt;
198 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
199 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
201 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
202 nxt_specif <> specify ?!
204 if nxt<>(Add_Relation
205 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
206 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
208 val nxt = tac2tac_ pt p nxt;
209 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
210 ------------------------------ FIXXXXME.meNEW !!! ---*)
212 (*val nxt = Specify_Theory "DiffApp" : tac*)
214 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
216 val nxt = tac2tac_ pt p nxt;
217 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
218 (*val nxt = Specify_Problem ["maximum_of","function"]*)
220 val nxt = tac2tac_ pt p nxt;
221 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
222 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
224 val nxt = tac2tac_ pt p nxt;
225 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
226 (*val nxt = Add_Given "boundVariable a" : tac*)
228 val nxt = tac2tac_ pt p nxt;
229 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
230 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
232 val nxt = tac2tac_ pt p nxt;
233 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
234 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
236 val nxt = tac2tac_ pt p nxt;
237 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
238 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
239 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
240 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
243 "--------- maximum example with 'specify', fmz = [] --------------";
244 "--------- maximum example with 'specify', fmz = [] --------------";
245 "--------- maximum example with 'specify', fmz = [] --------------";
247 val (dI',pI',mI') = empty_spec;
250 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
251 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
252 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
254 val nxt = tac2tac_ pt p nxt;
255 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
256 (*val nxt = Specify_Theory "e_domID" : tac*)
258 val nxt = Specify_Theory "DiffApp";
259 val nxt = tac2tac_ pt p nxt;
260 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
261 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
263 val nxt = Specify_Problem ["maximum_of","function"];
264 val nxt = tac2tac_ pt p nxt;
265 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
266 (*val nxt = Add_Given "fixedValues" : tac*)
268 val nxt = Add_Given "fixedValues [r=Arbfix]";
269 val nxt = tac2tac_ pt p nxt;
270 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
271 (*val nxt = Add_Find "maximum" : tac*)
273 val nxt = Add_Find "maximum A";
274 val nxt = tac2tac_ pt p nxt;
277 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
278 (*val nxt = Add_Find "valuesFor" : tac*)
280 val nxt = Add_Find "valuesFor [a]";
281 val nxt = tac2tac_ pt p nxt;
282 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
283 (*val nxt = Add_Relation "relations" ---
284 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
286 (*========== inhibit exn 010830 =======================================================*)
287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
288 if nxt<>(Add_Relation "relations []")
289 then error "test specify, fmz <> []: nxt <> Add_Relation.."
290 else (); (*different with show_types !!!*)
292 (*========== inhibit exn 010830 =======================================================*)
294 val nxt = Add_Relation "relations [(A=a+b)]";
295 val nxt = tac2tac_ pt p nxt;
296 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
297 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
299 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
300 val nxt = tac2tac_ pt p nxt;
301 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
302 (*val nxt = Add_Given "boundVariable" : tac*)
304 val nxt = Add_Given "boundVariable alpha";
305 val nxt = tac2tac_ pt p nxt;
306 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
307 (*val nxt = Add_Given "interval" : tac*)
309 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
310 val nxt = tac2tac_ pt p nxt;
311 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
312 (*val nxt = Add_Given "errorBound" : tac*)
314 val nxt = Add_Given "errorBound (eps=999)";
315 val nxt = tac2tac_ pt p nxt;
316 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
317 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
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 (* 2.4.00 nach Transfer specify -> hard_gen
325 val nxt = Apply_Method ("DiffApp","max_by_calculus");
326 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
327 (*val nxt = Empty_Tac : tac*)
329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
330 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
331 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
332 val Const ("Script.SubProblem",_) $
333 (Const ("Product_Type.Pair",_) $
335 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
336 (*...copied from stac2tac_*)
338 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
339 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
340 " REAL_LIST [c, c_2]]");
341 val ags = isalist2list ags';
342 val pI = ["LINEAR","system"];
343 val pats = (#ppc o get_pbt) pI;
344 "-a1-----------------------------------------------------";
345 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
346 val xxx = match_ags @{theory "EqSystem"} pats ags;
347 "-a2-----------------------------------------------------";
348 case match_ags @{theory "Isac"} pats ags of
349 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
350 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
351 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
352 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
354 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
356 "-b------------------------------------------------------";
357 val Const ("Script.SubProblem",_) $
358 (Const ("Product_Type.Pair",_) $
360 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
361 (*...copied from stac2tac_*)
363 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
364 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
365 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
366 val ags = isalist2list ags';
367 val pI = ["LINEAR","system"];
368 val pats = (#ppc o get_pbt) pI;
369 "-b1-----------------------------------------------------";
370 val xxx = match_ags @{theory "Isac"} pats ags;
371 "-b2-----------------------------------------------------";
372 case match_ags @{theory "EqSystem"} pats ags of
373 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
374 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
375 [_ $ Free ("c", _) $ _,
376 _ $ Free ("c_2", _) $ _]),
377 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
378 (* type of Find: [Free ("ss'''", "bool List.list")]*)
380 | _ => error "calchead.sml match_ags copy-named dropped --------";
382 "-c---ERROR case: stac is missing #Given equalities e_s--";
383 val stac as Const ("Script.SubProblem",_) $
384 (Const ("Product_Type.Pair",_) $
386 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
387 (*...copied from stac2tac_*)
389 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
390 " [REAL_LIST [c, c_2]]");
391 val ags = isalist2list ags';
392 val pI = ["LINEAR","system"];
393 val pats = (#ppc o get_pbt) pI;
394 (*============ inhibit exn AK110726 ==============================================
395 val xxx - match_ags (theory "EqSystem") pats ags;
396 ============ inhibit exn AK110726 ==============================================*)
397 "-c1-----------------------------------------------------";
398 "--------------------------step through code match_ags---";
399 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
400 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
401 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
402 val cy = filter is_copy_named pbt; (*=solution*)
403 (*============ inhibit exn AK110726 ==============================================
404 val oris' - matc thy pbt' ags [];
405 ============ inhibit exn AK110726 ==============================================*)
406 "-------------------------------step through code matc---";
407 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
408 (is_copy_named_idstr o free2str) t;
410 (*============ inhibit exn AK110726 ==============================================
411 val opt - mtc thy p a;
412 ============ inhibit exn AK110726 ==============================================*)
413 "--------------------------------step through code mtc---";
414 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
416 val ttt = (dsc $ var);
417 (*============ inhibit exn AK110726 ==============================================
418 Thm.global_cterm_of thy (dsc $ var);
419 ============ inhibit exn AK110726 ==============================================*)
421 "-------------------------------------step through end---";
422 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
423 val Const ("Script.SubProblem",_) $
424 (Const ("Product_Type.Pair",_) $
426 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
427 (*...copied from stac2tac_*)
429 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
430 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
431 " REAL_LIST [c, c_2]]");
432 val ags = isalist2list ags';
433 val pI = ["LINEAR","system"];
434 val pats = (#ppc o get_pbt) pI;
435 "-a1-----------------------------------------------------";
436 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
437 val xxx = match_ags @{theory "EqSystem"} pats ags;
438 "-a2-----------------------------------------------------";
439 case match_ags @{theory "Isac"} pats ags of
440 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
441 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
442 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
443 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
445 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
447 "-b------------------------------------------------------";
448 val Const ("Script.SubProblem",_) $
449 (Const ("Product_Type.Pair",_) $
451 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
452 (*...copied from stac2tac_*)
454 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
455 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
456 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
457 val ags = isalist2list ags';
458 val pI = ["LINEAR","system"];
459 val pats = (#ppc o get_pbt) pI;
460 "-b1-----------------------------------------------------";
461 val xxx = match_ags @{theory "Isac"} pats ags;
462 "-b2-----------------------------------------------------";
463 case match_ags @{theory "EqSystem"} pats ags of
464 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
465 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
466 [_ $ Free ("c", _) $ _,
467 _ $ Free ("c_2", _) $ _]),
468 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
469 (* type of Find: [Free ("ss'''", "bool List.list")]*)
471 | _ => error "calchead.sml match_ags copy-named dropped --------";
473 "-c---ERROR case: stac is missing #Given equalities e_s--";
474 val stac as Const ("Script.SubProblem",_) $
475 (Const ("Product_Type.Pair",_) $
477 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
478 (*...copied from stac2tac_*)
480 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
481 " [REAL_LIST [c, c_2]]");
482 val ags = isalist2list ags';
483 val pI = ["LINEAR","system"];
484 val pats = (#ppc o get_pbt) pI;
485 (*============ inhibit exn AK110726 ==============================================
486 val xxx - match_ags (theory "EqSystem") pats ags;
487 -------------------------------------------------------------------*)
488 "-c1-----------------------------------------------------";
489 "--------------------------step through code match_ags---";
490 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
491 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
492 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
493 val cy = filter is_copy_named pbt; (*=solution*)
494 (*============ inhibit exn AK110726 ==============================================
495 val oris' - matc thy pbt' ags [];
496 -------------------------------------------------------------------*)
497 "-------------------------------step through code matc---";
498 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
499 (is_copy_named_idstr o free2str) t;
501 (*============ inhibit exn AK110726 ==============================================
502 val opt - mtc thy p a;
503 -------------------------------------------------------------------*)
504 "--------------------------------step through code mtc---";
505 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
507 val ttt = (dsc $ var);
508 (*============ inhibit exn AK110726 ==============================================
509 Thm.global_cterm_of thy (dsc $ var);
510 -------------------------------------------------------------------*)
511 "-------------------------------------step through end---";
513 case ((match_ags @{theory "EqSystem"} pats ags)
514 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
515 [] => match_ags_msg pI stac ags
516 | _ => error "calchead.sml match_ags 1st arg missing --------";
518 "-d------------------------------------------------------";
519 val stac as Const ("Script.SubProblem",_) $
520 (Const ("Product_Type.Pair",_) $
522 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
523 (*...copied from stac2tac_*)
525 "SubProblem (Test',[univariate,equation,test]," ^
526 " [no_met]) [BOOL (x+1=2), REAL x]");
527 val AGS = isalist2list ags';
528 val pI = ["univariate","equation","test"];
531 case ((match_ags @{theory "EqSystem"} pats ags)
532 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
533 [] => match_ags_msg pI stac ags
534 | _ => error "calchead.sml match_ags 1st arg missing --------";
536 "-d------------------------------------------------------";
537 val stac as Const ("Script.SubProblem",_) $
538 (Const ("Product_Type.Pair",_) $
540 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
541 (*...copied from stac2tac_*)
543 "SubProblem (Test',[univariate,equation,test]," ^
544 " [no_met]) [BOOL (x+1=2), REAL x]");
545 val AGS = isalist2list ags';
546 val pI = ["univariate","equation","test"];
547 val PATS = (#ppc o get_pbt) pI;
548 "-d1-----------------------------------------------------";
549 "--------------------------step through code match_ags---";
550 val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);
551 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
552 val pbt' = filter_out is_copy_named pbt;
553 val cy = filter is_copy_named pbt;
554 val oris' = matc thy pbt' ags [];
555 "-------------------------------step through code matc---";
556 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
557 (is_copy_named_idstr o free2str) t;
559 val opt = mtc thy p a;
560 "--------------------------------step through code mtc---";
561 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
562 val ttt = (dsc $ var);
563 Thm.global_cterm_of thy (dsc $ var);
564 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
566 "-d2-----------------------------------------------------";
568 "-------------------------------step through code matc---";
569 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
570 (is_copy_named_idstr o free2str) t;
572 val opt = mtc thy p a;
573 "--------------------------------step through code mtc---";
574 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
575 val ttt = (dsc $ var);
576 Thm.global_cterm_of thy (dsc $ var);
577 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
578 "-d3-----------------------------------------------------";
579 pbt = []; (*true, base case*)
580 "-----------------continue step through code match_ags---";
581 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
582 "--------------------------------step through cpy_nam----";
583 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
584 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
585 "--------------------------------------------------------";
586 fun is_copy_named_generating_idstr str =
587 if is_copy_named_idstr str
588 then case (rev o Symbol.explode) str of
589 (*"_"::"_"::"_"::_ => false*)
590 "'"::"'"::"'"::_ => false
593 fun is_copy_named_generating (_, (_, t)) =
594 (is_copy_named_generating_idstr o free2str) t;
595 "--------------------------------------------------------";
596 is_copy_named_generating p (*true*);
597 fun sel (_,_,d,ts) = comp_ts (d, ts);
598 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
600 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
602 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
603 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
604 val vals = map sel oris;
605 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
607 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
608 (assoc (vars'~~vals, cy'));
609 (*SOME (Free ("x", "Real.real")) : term option*)
610 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
612 "-----------------continue step through code match_ags---";
613 val cy' = map (cpy_nam pbt' oris') cy;
614 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
615 "-------------------------------------step through end---";
617 case match_ags thy PATS AGS of
618 [(1, [1], "#Given", Const ("Descript.equality", _),
619 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
620 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
621 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
622 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
624 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
626 "--------- regression test fun is_copy_named ------------";
627 "--------- regression test fun is_copy_named ------------";
628 "--------- regression test fun is_copy_named ------------";
629 val trm = (1, (2, @{term "v'i'"}));
630 if is_copy_named trm then () else error "regr. is_copy_named 1";
631 val trm = (1, (2, @{term "e_e"}));
632 if is_copy_named trm then error "regr. is_copy_named 2" else ();
633 val trm = (1, (2, @{term "L'''"}));
634 if is_copy_named trm then () else error "regr. is_copy_named 3";
636 (* out-comment 'structure CalcHead'...
637 val trm = (1, (2, @{term "v'i'"}));
638 if is_copy_named_generating trm then () else error "regr. is_copy_named";
639 val trm = (1, (2, @{term "L'''"}));
640 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
643 "--------- regr.test fun cpy_nam ------------------------";
644 "--------- regr.test fun cpy_nam ------------------------";
645 "--------- regr.test fun cpy_nam ------------------------";
646 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
647 (*the model-pattern, is_copy_named are filter_out*)
648 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
649 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
650 (*the model specific for an example*)
651 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
652 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
653 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
654 (*...all must be true*)
656 case cpy_nam pbt oris (hd cy) of
657 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
658 | _ => error "calchead.sml regr.test cpy_nam-1-";
660 (*new data: cpy_nam without changing the name*)
661 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
662 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
663 @{term "solution"}; type_of @{term "ss''' :: bool list"};
664 (*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)
665 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
666 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
667 (*the model specific for an example*)
668 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
669 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
670 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
671 (*could be more than 1*)];
673 case cpy_nam pbt oris (hd cy) of
674 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
675 | _ => error "calchead.sml regr.test cpy_nam-2-";
677 "--------- check specify phase --------------------------";
678 "--------- check specify phase --------------------------";
679 "--------- check specify phase --------------------------";
680 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
681 val fmz = ["functionTerm (x + 1)",
682 "integrateBy x","antiDerivative FF"];
684 ("Integrate",["integrate","function"],
685 ["diff","integration"]);
686 val p = e_pos'; val c = [];
688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
689 (*> val it = "--- step 1 --" : string
693 (0, EdUndef, 0, Nundef,
695 {Find = [], With = [], Given = [], Where = [], Relate = []})))
697 val nxt = ("Model_Problem", Model_Problem) : string * tac
698 val p = ([], Pbl) : pos'
702 (["functionTerm (x^^^2 + 1)", "integrateBy x",
703 "antiDerivative FF"],
704 ("Integrate", ["integrate", "function"],
705 ["diff", "integration"])),
707 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
709 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
710 probl = [], branch = TransitiveB,
713 Const ("Descript.functionTerm", "Real.real => Tools.una"),
715 "["Real.real, "Real.real] => "Real.real") $
716 (Const ("Atools.pow",
717 "["Real.real, "Real.real] => "Real.real") $
718 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
719 Free ("1", "Real.real")]),
721 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
722 [Free ("x", "Real.real")]),
724 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
725 [Free ("FF", "Real.real")])],
726 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
727 Const ("Integrate.Integrate",
728 "("Real.real, "Real.real) * => "Real.real") $
729 (Const ("Product_Type.Pair",
730 "["Real.real, "Real.real]
731 => ("Real.real, "Real.real) *") $
733 "["Real.real, "Real.real] => "Real.real") $
734 (Const ("Atools.pow",
735 "["Real.real, "Real.real] => "Real.real") $
736 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
737 Free ("1", "Real.real")) $
738 Free ("x", "Real.real"))),
739 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
741 "----- WN101007 worked until here (checked same as isac2002) ---";
742 case nxt of ("Model_Problem", Model_Problem) => ()
743 | _ => error "clchead.sml: check specify phase step 1";
745 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
746 (*val it = "--- step 2 --" : string
747 val p = ([], Pbl) : pos'
751 (0, EdUndef, 0, Nundef,
753 {Find = [Incompl "Integrate.antiDerivative"],
755 Given = [Incompl "functionTerm", Incompl "integrateBy"],
757 Relate = []}))) : mout
758 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
762 (["functionTerm (x^^^2 + 1)", "integrateBy x",
763 "antiDerivative FF"],
764 ("Integrate", ["integrate", "function"],
765 ["diff", "integration"])),
768 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
770 cell = None, meth = [], spec =
771 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
772 [(0, [], false, "#Given",
773 Inc ((Const ("Descript.functionTerm",
774 "Real.real => Tools.una"),[]),
775 (Const ("empty", "'a"), []))),
776 (0, [], false, "#Given",
777 Inc ((Const ("Integrate.integrateBy",
778 "Real.real => Tools.una"),[]),
779 (Const ("empty", "'a"), []))),
780 (0, [], false, "#Find",
781 Inc ((Const ("Integrate.antiDerivative",
782 "Real.real => Tools.una"),[]),
783 (Const ("empty", "'a"), [])))],
784 branch = TransitiveB, origin =
786 Const ("Descript.functionTerm", "Real.real => Tools.una"),
788 "["Real.real, "Real.real] => "Real.real") $
789 (Const ("Atools.pow",
790 "["Real.real, "Real.real] => "Real.real") $
791 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
792 Free ("1", "Real.real")]),
794 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
795 [Free ("x", "Real.real")]),
797 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
798 [Free ("FF", "Real.real")])],
799 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
800 Const ("Integrate.Integrate",
801 "("Real.real, "Real.real) * => "Real.real") $
802 (Const ("Product_Type.Pair",
803 "["Real.real, "Real.real]
804 => ("Real.real, "Real.real) *") $
806 "["Real.real, "Real.real] => "Real.real") $
807 (Const ("Atools.pow",
808 "["Real.real, "Real.real] => "Real.real") $
809 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
810 Free ("1", "Real.real")) $
811 Free ("x", "Real.real"))),
812 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
814 "----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
815 case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()
816 | _ => error "clchead.sml: check specify phase step 2";
818 val (p,_,f,nxt,_,pt) = me nxt p c pt;
819 "----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
820 case nxt of ("Add_Given", Add_Given "integrateBy x") => ()
821 | _ => error "clchead.sml: check specify phase step 2";
823 "--------- check: fmz matches pbt -----------------------";
824 "--------- check: fmz matches pbt -----------------------";
825 "--------- check: fmz matches pbt -----------------------";
826 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
827 "the following fmz caused the above error";
828 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
829 val pI = ["plus_minus","polynom","vereinfachen"];
831 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
832 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
833 (*#############################^^^^^^^^^ defined by Isabelle*)
834 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
835 [Free ("N", _ (*"Real.real"*))])],
836 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
837 "#undef means: the element with description TERM in fmz did not match ";
838 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
839 "defined in Simplify.thy";
841 "So we try out how to create Simplify.Term:";
843 val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
844 " ^^^^^^^^^ see above";
848 val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
849 " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
853 val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
854 " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
855 " and unsed in pbl [plus_minus,polynom,vereinfachen]";
858 "----- so this is the correct fmz:";
859 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
860 val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
861 (*########################^^^^^^^^^ defined in Simplify.thy*)
862 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
864 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
866 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
867 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
868 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
870 "--------- fun typeless ---------------------------------";
871 "--------- fun typeless ---------------------------------";
872 "--------- fun typeless ---------------------------------";
874 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
875 > val (_,t1) = split_dsc_t hs (Thm.term_of ct);
876 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
877 > val (_,t2) = split_dsc_t hs (Thm.term_of ct);
878 > typeless t1 = typeless t2;
881 "--------- fun variants_in ------------------------------";
882 "--------- fun variants_in ------------------------------";
883 "--------- fun variants_in ------------------------------";
885 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
886 val it = ([3],[4,5,5,5,5,5]) : int list * int list
887 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
888 val it = [1,3,1,5] : int list
890 "--------- fun is_list_type -----------------------------";
891 "--------- fun is_list_type -----------------------------";
892 "--------- fun is_list_type -----------------------------";
893 (* fun destr (Type(str,sort)) = (str,sort);
894 > val (SOME ct) = parse thy "lll::real list";
895 > val ty = (#T o rep_cterm) ct;
899 val it = ("List.list",["RealDef.real"]) : string * typ list
900 > atomty ((#t o rep_cterm) ct);
902 *** Free ( lll, real list)
905 > val (SOME ct) = parse thy "[lll::real]";
906 > val ty = (#T o rep_cterm) ct;
910 val it = ("List.list",["'a"]) : string * typ list
911 > atomty ((#t o rep_cterm) ct);
913 *** Const ( List.list.Cons, [real, real list] => real list)
914 *** Free ( lll, real)
915 *** Const ( List.list.Nil, real list)
917 > val (SOME ct) = parse thy "lll";
918 > val ty = (#T o rep_cterm) ct;
920 val it = false : bool *)
921 "--------- fun has_list_type ----------------------------";
922 "--------- fun has_list_type ----------------------------";
923 "--------- fun has_list_type ----------------------------";
925 > val (SOME ct) = parse thy "lll::real list";
926 > has_list_type (Thm.term_of ct);
928 > val (SOME ct) = parse thy "[lll::real]";
929 > has_list_type (Thm.term_of ct);
930 val it = false : bool *)
931 "--------- fun tag_form ---------------------------------";
932 "--------- fun tag_form ---------------------------------";
933 "--------- fun tag_form ---------------------------------";
934 (* val formal = (the o (parse thy)) "[R::real]";
935 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
936 > tag_form thy (formal, given);
937 val it = "fixed_values [R]" : cterm
939 "--------- fun foldr1, foldl1 ---------------------------";
940 "--------- fun foldr1, foldl1 ---------------------------";
941 "--------- fun foldr1, foldl1 ---------------------------";
943 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
944 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
945 > val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
946 > Thm.global_cterm_of thy conj;
947 val it = "(a = b & c = d) & e = f" : cterm
950 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
951 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
952 > val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
953 > Thm.global_cterm_of thy conj;
954 val it = "a = b & c = d & e = f & g = h" : cterm