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 has_list_type ----------------------------";
24 "--------- fun tag_form ---------------------------------";
25 "--------- fun foldr1, foldl1 ---------------------------";
26 "--------------------------------------------------------";
27 "--------------------------------------------------------";
28 "--------------------------------------------------------";
31 "--------- get_interval after replace} other 2 ----------";
32 "--------- get_interval after replace} other 2 ----------";
33 "--------- get_interval after replace} other 2 ----------";
35 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
36 ("Test", ["sqroot-test","univariate","equation","test"],
37 ["Test","squ-equ-test-subpbl1"]))];
40 autoCalculate 1 CompleteCalc;
41 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
42 replaceFormula 1 "x = 1";
43 (*... returns calcChangedEvent with ...*)
44 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
45 val ((pt,_),_) = get_calc 1;
47 default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
48 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
49 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
50 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
51 ([3, 2], Res)] then () else
52 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
54 default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
55 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
56 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
57 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",
65 "valuesFor [a,b::real]",
66 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
67 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
68 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*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",["maximum_of","function"],
77 ["DiffApp","max_by_calculus"]);
80 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
81 val nxt = tac2tac_ pt p nxt;
82 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
83 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
85 val nxt = tac2tac_ pt p nxt;
86 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
89 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
90 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
92 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
93 Given=[Correct "fixedValues [r = Arbfix]"],
94 Relate=[Incompl "relations"], Where=[],With=[]})
95 then error "test-maximum.sml: model stepwise - different behaviour"
98 val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)");
99 (* WN1130630 THE maximum example WORKS IN isabisac09-2;
100 MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt.
101 Some tests have been broken much earlier,
102 see test/../calchead.sml "inhibit exn 010830". *)
103 (*========== inhibit exn WN1130630 maximum example broken =========================
104 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
105 ============ inhibit exn WN1130630 maximum example broken =======================*)
107 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
108 (*========== inhibit exn WN1130630 maximum example broken =========================
109 (* ERROR: Exception Bind raised *)
110 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
111 ============ inhibit exn WN1130630 maximum example broken =======================*)
113 val m = Specify_Problem ["maximum_of","function"];
114 val nxt = tac2tac_ pt p m;
115 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
116 (*========== inhibit exn WN1130630 maximum example broken =========================
117 if ppc<>(Problem ["maximum_of","function"],
118 {Find=[Incompl "maximum",Incompl "valuesFor"],
119 Given=[Correct "fixedValues [r = Arbfix]"],
120 Relate=[Incompl "relations []"], Where=[],With=[]})
121 then error "diffappl.sml: Specify_Problem different behaviour"
123 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
124 if ppc<>(Problem ["maximum_of","function"],
125 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
126 Given=[Correct "fixedValues [r = Arbfix]"],
127 Relate=[Missing "relations rs_"],Where=[],With=[]})
128 then error "diffappl.sml: Specify_Problem different behaviour"
130 ============ inhibit exn WN1130630 maximum example broken =======================*)
132 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
133 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
134 (*========== inhibit exn WN1130630 maximum example broken =========================
135 if ppc<>(Method ["DiffApp","max_by_calculus"],
136 {Find=[Incompl "maximum",Incompl "valuesFor"],
137 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
138 Missing "interval itv_",Missing "errorBound err_"],
139 Relate=[Incompl "relations []"],Where=[],With=[]})
140 then error "diffappl.sml: Specify_Method different behaviour"
142 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
143 if ppc<>(Method ["DiffApp","max_by_calculus"],
144 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
145 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
146 Missing "interval itv_",Missing "errorBound err_"],
147 Relate=[Missing "relations rs_"],Where=[],With=[]})
148 then error "diffappl.sml: Specify_Method different behaviour"
150 ============ inhibit exn WN1130630 maximum example broken =======================*)
152 "--------- maximum example with 'specify', fmz <> [] -------------";
153 "--------- maximum example with 'specify', fmz <> [] -------------";
154 "--------- maximum example with 'specify', fmz <> [] -------------";
156 ["fixedValues [r=Arbfix]","maximum A",
158 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
159 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
160 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
162 "boundVariable a","boundVariable b","boundVariable alpha",
163 "interval {x::real. 0 <= x & x <= 2*r}",
164 "interval {x::real. 0 <= x & x <= 2*r}",
165 "interval {x::real. 0 <= x & x <= pi}",
166 "errorBound (eps=(0::real))"];
168 ("DiffApp",["maximum_of","function"],
169 ["DiffApp","max_by_calculus"]);
171 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
172 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
174 val nxt = tac2tac_ pt p nxt;
175 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
176 val nxt = tac2tac_ pt p nxt;
177 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
178 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
180 val nxt = tac2tac_ pt p nxt;
181 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
182 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
184 val nxt = tac2tac_ pt p nxt;
185 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
186 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
188 val nxt = tac2tac_ pt p nxt;
189 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
190 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
192 val nxt = tac2tac_ pt p nxt;
193 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
194 (*val nxt = Add_Relation "relations [A = a * b]" *)
196 val nxt = tac2tac_ pt p nxt;
197 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
198 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
200 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
201 nxt_specif <> specify ?!
203 if nxt<>(Add_Relation
204 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
205 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
207 val nxt = tac2tac_ pt p nxt;
208 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
209 ------------------------------ FIXXXXME.meNEW !!! ---*)
211 (*val nxt = Specify_Theory "DiffApp" : tac*)
213 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
215 val nxt = tac2tac_ pt p nxt;
216 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
217 (*val nxt = Specify_Problem ["maximum_of","function"]*)
219 val nxt = tac2tac_ pt p nxt;
220 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
221 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
223 val nxt = tac2tac_ pt p nxt;
224 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
225 (*val nxt = Add_Given "boundVariable a" : tac*)
227 val nxt = tac2tac_ pt p nxt;
228 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
229 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
231 val nxt = tac2tac_ pt p nxt;
232 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
233 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
235 val nxt = tac2tac_ pt p nxt;
236 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
237 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
238 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
239 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
242 "--------- maximum example with 'specify', fmz = [] --------------";
243 "--------- maximum example with 'specify', fmz = [] --------------";
244 "--------- maximum example with 'specify', fmz = [] --------------";
246 val (dI',pI',mI') = empty_spec;
249 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
250 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
251 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
253 val nxt = tac2tac_ pt p nxt;
254 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
255 (*val nxt = Specify_Theory "e_domID" : tac*)
257 val nxt = Specify_Theory "DiffApp";
258 val nxt = tac2tac_ pt p nxt;
259 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
260 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
262 val nxt = Specify_Problem ["maximum_of","function"];
263 val nxt = tac2tac_ pt p nxt;
264 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
265 (*val nxt = Add_Given "fixedValues" : tac*)
267 val nxt = Add_Given "fixedValues [r=Arbfix]";
268 val nxt = tac2tac_ pt p nxt;
269 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
270 (*val nxt = Add_Find "maximum" : tac*)
272 val nxt = Add_Find "maximum A";
273 val nxt = tac2tac_ pt p nxt;
276 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
277 (*val nxt = Add_Find "valuesFor" : tac*)
279 val nxt = Add_Find "valuesFor [a]";
280 val nxt = tac2tac_ pt p nxt;
281 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
282 (*val nxt = Add_Relation "relations" ---
283 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
285 (*========== inhibit exn 010830 =======================================================*)
286 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
287 if nxt<>(Add_Relation "relations []")
288 then error "test specify, fmz <> []: nxt <> Add_Relation.."
289 else (); (*different with show_types !!!*)
291 (*========== inhibit exn 010830 =======================================================*)
293 val nxt = Add_Relation "relations [(A=a+b)]";
294 val nxt = tac2tac_ pt p nxt;
295 val(p,_, 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,_, 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,_, 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,_, 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,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
316 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
318 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
319 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
320 then error "test specify, fmz <> []: nxt <> Add_Relation.."
323 (* 2.4.00 nach Transfer specify -> hard_gen
324 val nxt = Apply_Method ("DiffApp","max_by_calculus");
325 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
326 (*val nxt = Empty_Tac : tac*)
328 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
330 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
331 val Const ("Script.SubProblem",_) $
332 (Const ("Product_Type.Pair",_) $
334 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
335 (*...copied from stac2tac_*)
337 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
338 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
339 " REAL_LIST [c, c_2]]");
340 val ags = isalist2list ags';
341 val pI = ["LINEAR","system"];
342 val pats = (#ppc o get_pbt) pI;
343 "-a1-----------------------------------------------------";
344 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
345 val xxx = match_ags @{theory "EqSystem"} pats ags;
346 "-a2-----------------------------------------------------";
347 case match_ags @{theory "Isac"} pats ags of
348 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
349 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
350 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
351 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
353 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
355 "-b------------------------------------------------------";
356 val Const ("Script.SubProblem",_) $
357 (Const ("Product_Type.Pair",_) $
359 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
360 (*...copied from stac2tac_*)
362 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
363 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
364 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
365 val ags = isalist2list ags';
366 val pI = ["LINEAR","system"];
367 val pats = (#ppc o get_pbt) pI;
368 "-b1-----------------------------------------------------";
369 val xxx = match_ags @{theory "Isac"} pats ags;
370 "-b2-----------------------------------------------------";
371 case match_ags @{theory "EqSystem"} pats ags of
372 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
373 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
374 [_ $ Free ("c", _) $ _,
375 _ $ Free ("c_2", _) $ _]),
376 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
377 (* type of Find: [Free ("ss'''", "bool List.list")]*)
379 | _ => error "calchead.sml match_ags copy-named dropped --------";
381 "-c---ERROR case: stac is missing #Given equalities e_s--";
382 val stac as Const ("Script.SubProblem",_) $
383 (Const ("Product_Type.Pair",_) $
385 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
386 (*...copied from stac2tac_*)
388 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
389 " [REAL_LIST [c, c_2]]");
390 val ags = isalist2list ags';
391 val pI = ["LINEAR","system"];
392 val pats = (#ppc o get_pbt) pI;
393 (*============ inhibit exn AK110726 ==============================================
394 val xxx - match_ags (theory "EqSystem") pats ags;
395 ============ inhibit exn AK110726 ==============================================*)
396 "-c1-----------------------------------------------------";
397 "--------------------------step through code match_ags---";
398 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
399 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
400 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
401 val cy = filter is_copy_named pbt; (*=solution*)
402 (*============ inhibit exn AK110726 ==============================================
403 val oris' - matc thy pbt' ags [];
404 ============ inhibit exn AK110726 ==============================================*)
405 "-------------------------------step through code matc---";
406 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
407 (is_copy_named_idstr o free2str) t;
409 (*============ inhibit exn AK110726 ==============================================
410 val opt - mtc thy p a;
411 ============ inhibit exn AK110726 ==============================================*)
412 "--------------------------------step through code mtc---";
413 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
415 val ttt = (dsc $ var);
416 (*============ inhibit exn AK110726 ==============================================
417 Thm.global_cterm_of thy (dsc $ var);
418 ============ inhibit exn AK110726 ==============================================*)
420 "-------------------------------------step through end---";
421 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
422 val Const ("Script.SubProblem",_) $
423 (Const ("Product_Type.Pair",_) $
425 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
426 (*...copied from stac2tac_*)
428 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
429 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
430 " REAL_LIST [c, c_2]]");
431 val ags = isalist2list ags';
432 val pI = ["LINEAR","system"];
433 val pats = (#ppc o get_pbt) pI;
434 "-a1-----------------------------------------------------";
435 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
436 val xxx = match_ags @{theory "EqSystem"} pats ags;
437 "-a2-----------------------------------------------------";
438 case match_ags @{theory "Isac"} pats ags of
439 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
440 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
441 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
442 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
444 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
446 "-b------------------------------------------------------";
447 val Const ("Script.SubProblem",_) $
448 (Const ("Product_Type.Pair",_) $
450 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
451 (*...copied from stac2tac_*)
453 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
454 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
455 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
456 val ags = isalist2list ags';
457 val pI = ["LINEAR","system"];
458 val pats = (#ppc o get_pbt) pI;
459 "-b1-----------------------------------------------------";
460 val xxx = match_ags @{theory "Isac"} pats ags;
461 "-b2-----------------------------------------------------";
462 case match_ags @{theory "EqSystem"} pats ags of
463 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
464 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
465 [_ $ Free ("c", _) $ _,
466 _ $ Free ("c_2", _) $ _]),
467 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
468 (* type of Find: [Free ("ss'''", "bool List.list")]*)
470 | _ => error "calchead.sml match_ags copy-named dropped --------";
472 "-c---ERROR case: stac is missing #Given equalities e_s--";
473 val stac as Const ("Script.SubProblem",_) $
474 (Const ("Product_Type.Pair",_) $
476 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
477 (*...copied from stac2tac_*)
479 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
480 " [REAL_LIST [c, c_2]]");
481 val ags = isalist2list ags';
482 val pI = ["LINEAR","system"];
483 val pats = (#ppc o get_pbt) pI;
484 (*============ inhibit exn AK110726 ==============================================
485 val xxx - match_ags (theory "EqSystem") pats ags;
486 -------------------------------------------------------------------*)
487 "-c1-----------------------------------------------------";
488 "--------------------------step through code match_ags---";
489 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
490 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
491 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
492 val cy = filter is_copy_named pbt; (*=solution*)
493 (*============ inhibit exn AK110726 ==============================================
494 val oris' - matc thy pbt' ags [];
495 -------------------------------------------------------------------*)
496 "-------------------------------step through code matc---";
497 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
498 (is_copy_named_idstr o free2str) t;
500 (*============ inhibit exn AK110726 ==============================================
501 val opt - mtc thy p a;
502 -------------------------------------------------------------------*)
503 "--------------------------------step through code mtc---";
504 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
506 val ttt = (dsc $ var);
507 (*============ inhibit exn AK110726 ==============================================
508 Thm.global_cterm_of thy (dsc $ var);
509 -------------------------------------------------------------------*)
510 "-------------------------------------step through end---";
512 case ((match_ags @{theory "EqSystem"} pats ags)
513 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
514 [] => match_ags_msg pI stac ags
515 | _ => error "calchead.sml match_ags 1st arg missing --------";
517 "-d------------------------------------------------------";
518 val stac as Const ("Script.SubProblem",_) $
519 (Const ("Product_Type.Pair",_) $
521 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
522 (*...copied from stac2tac_*)
524 "SubProblem (Test',[univariate,equation,test]," ^
525 " [no_met]) [BOOL (x+1=2), REAL x]");
526 val AGS = isalist2list ags';
527 val pI = ["univariate","equation","test"];
530 case ((match_ags @{theory "EqSystem"} pats ags)
531 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
532 [] => match_ags_msg pI stac ags
533 | _ => error "calchead.sml match_ags 1st arg missing --------";
535 "-d------------------------------------------------------";
536 val stac as Const ("Script.SubProblem",_) $
537 (Const ("Product_Type.Pair",_) $
539 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
540 (*...copied from stac2tac_*)
542 "SubProblem (Test',[univariate,equation,test]," ^
543 " [no_met]) [BOOL (x+1=2), REAL x]");
544 val AGS = isalist2list ags';
545 val pI = ["univariate","equation","test"];
546 val PATS = (#ppc o get_pbt) pI;
547 "-d1-----------------------------------------------------";
548 "--------------------------step through code match_ags---";
549 val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);
550 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
551 val pbt' = filter_out is_copy_named pbt;
552 val cy = filter is_copy_named pbt;
553 val oris' = matc thy pbt' ags [];
554 "-------------------------------step through code matc---";
555 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
556 (is_copy_named_idstr o free2str) t;
558 val opt = mtc thy p a;
559 "--------------------------------step through code mtc---";
560 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
561 val ttt = (dsc $ var);
562 Thm.global_cterm_of thy (dsc $ var);
563 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
565 "-d2-----------------------------------------------------";
567 "-------------------------------step through code matc---";
568 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
569 (is_copy_named_idstr o free2str) t;
571 val opt = mtc thy p a;
572 "--------------------------------step through code mtc---";
573 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
574 val ttt = (dsc $ var);
575 Thm.global_cterm_of thy (dsc $ var);
576 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
577 "-d3-----------------------------------------------------";
578 pbt = []; (*true, base case*)
579 "-----------------continue step through code match_ags---";
580 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
581 "--------------------------------step through cpy_nam----";
582 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
583 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
584 "--------------------------------------------------------";
585 fun is_copy_named_generating_idstr str =
586 if is_copy_named_idstr str
587 then case (rev o Symbol.explode) str of
588 (*"_"::"_"::"_"::_ => false*)
589 "'"::"'"::"'"::_ => false
592 fun is_copy_named_generating (_, (_, t)) =
593 (is_copy_named_generating_idstr o free2str) t;
594 "--------------------------------------------------------";
595 is_copy_named_generating p (*true*);
596 fun sel (_,_,d,ts) = comp_ts (d, ts);
597 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
599 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
601 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
602 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
603 val vals = map sel oris;
604 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
606 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
607 (assoc (vars'~~vals, cy'));
608 (*SOME (Free ("x", "Real.real")) : term option*)
609 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
611 "-----------------continue step through code match_ags---";
612 val cy' = map (cpy_nam pbt' oris') cy;
613 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
614 "-------------------------------------step through end---";
616 case match_ags thy PATS AGS of
617 [(1, [1], "#Given", Const ("Descript.equality", _),
618 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
619 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
620 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
621 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
623 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
625 "--------- regression test fun is_copy_named ------------";
626 "--------- regression test fun is_copy_named ------------";
627 "--------- regression test fun is_copy_named ------------";
628 val trm = (1, (2, @{term "v'i'"}));
629 if is_copy_named trm then () else error "regr. is_copy_named 1";
630 val trm = (1, (2, @{term "e_e"}));
631 if is_copy_named trm then error "regr. is_copy_named 2" else ();
632 val trm = (1, (2, @{term "L'''"}));
633 if is_copy_named trm then () else error "regr. is_copy_named 3";
635 (* out-comment 'structure CalcHead'...
636 val trm = (1, (2, @{term "v'i'"}));
637 if is_copy_named_generating trm then () else error "regr. is_copy_named";
638 val trm = (1, (2, @{term "L'''"}));
639 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
642 "--------- regr.test fun cpy_nam ------------------------";
643 "--------- regr.test fun cpy_nam ------------------------";
644 "--------- regr.test fun cpy_nam ------------------------";
645 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
646 (*the model-pattern, is_copy_named are filter_out*)
647 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
648 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
649 (*the model specific for an example*)
650 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
651 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
652 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
653 (*...all must be true*)
655 case cpy_nam pbt oris (hd cy) of
656 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
657 | _ => error "calchead.sml regr.test cpy_nam-1-";
659 (*new data: cpy_nam without changing the name*)
660 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
661 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
662 @{term "solution"}; type_of @{term "ss''' :: bool list"};
663 (*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)
664 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
665 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
666 (*the model specific for an example*)
667 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
668 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
669 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
670 (*could be more than 1*)];
672 case cpy_nam pbt oris (hd cy) of
673 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
674 | _ => error "calchead.sml regr.test cpy_nam-2-";
676 "--------- check specify phase --------------------------";
677 "--------- check specify phase --------------------------";
678 "--------- check specify phase --------------------------";
679 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
680 val fmz = ["functionTerm (x + 1)",
681 "integrateBy x","antiDerivative FF"];
683 ("Integrate",["integrate","function"],
684 ["diff","integration"]);
685 val p = e_pos'; val c = [];
687 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
688 (*> val it = "--- step 1 --" : string
692 (0, EdUndef, 0, Nundef,
694 {Find = [], With = [], Given = [], Where = [], Relate = []})))
696 val nxt = ("Model_Problem", Model_Problem) : string * tac
697 val p = ([], Pbl) : pos'
701 (["functionTerm (x^^^2 + 1)", "integrateBy x",
702 "antiDerivative FF"],
703 ("Integrate", ["integrate", "function"],
704 ["diff", "integration"])),
706 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
708 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
709 probl = [], branch = TransitiveB,
712 Const ("Descript.functionTerm", "Real.real => Tools.una"),
714 "["Real.real, "Real.real] => "Real.real") $
715 (Const ("Atools.pow",
716 "["Real.real, "Real.real] => "Real.real") $
717 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
718 Free ("1", "Real.real")]),
720 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
721 [Free ("x", "Real.real")]),
723 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
724 [Free ("FF", "Real.real")])],
725 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
726 Const ("Integrate.Integrate",
727 "("Real.real, "Real.real) * => "Real.real") $
728 (Const ("Product_Type.Pair",
729 "["Real.real, "Real.real]
730 => ("Real.real, "Real.real) *") $
732 "["Real.real, "Real.real] => "Real.real") $
733 (Const ("Atools.pow",
734 "["Real.real, "Real.real] => "Real.real") $
735 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
736 Free ("1", "Real.real")) $
737 Free ("x", "Real.real"))),
738 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
740 "----- WN101007 worked until here (checked same as isac2002) ---";
741 case nxt of ("Model_Problem", Model_Problem) => ()
742 | _ => error "clchead.sml: check specify phase step 1";
744 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
745 (*val it = "--- step 2 --" : string
746 val p = ([], Pbl) : pos'
750 (0, EdUndef, 0, Nundef,
752 {Find = [Incompl "Integrate.antiDerivative"],
754 Given = [Incompl "functionTerm", Incompl "integrateBy"],
756 Relate = []}))) : mout
757 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
761 (["functionTerm (x^^^2 + 1)", "integrateBy x",
762 "antiDerivative FF"],
763 ("Integrate", ["integrate", "function"],
764 ["diff", "integration"])),
767 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
769 cell = None, meth = [], spec =
770 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
771 [(0, [], false, "#Given",
772 Inc ((Const ("Descript.functionTerm",
773 "Real.real => Tools.una"),[]),
774 (Const ("empty", "'a"), []))),
775 (0, [], false, "#Given",
776 Inc ((Const ("Integrate.integrateBy",
777 "Real.real => Tools.una"),[]),
778 (Const ("empty", "'a"), []))),
779 (0, [], false, "#Find",
780 Inc ((Const ("Integrate.antiDerivative",
781 "Real.real => Tools.una"),[]),
782 (Const ("empty", "'a"), [])))],
783 branch = TransitiveB, origin =
785 Const ("Descript.functionTerm", "Real.real => Tools.una"),
787 "["Real.real, "Real.real] => "Real.real") $
788 (Const ("Atools.pow",
789 "["Real.real, "Real.real] => "Real.real") $
790 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
791 Free ("1", "Real.real")]),
793 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
794 [Free ("x", "Real.real")]),
796 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
797 [Free ("FF", "Real.real")])],
798 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
799 Const ("Integrate.Integrate",
800 "("Real.real, "Real.real) * => "Real.real") $
801 (Const ("Product_Type.Pair",
802 "["Real.real, "Real.real]
803 => ("Real.real, "Real.real) *") $
805 "["Real.real, "Real.real] => "Real.real") $
806 (Const ("Atools.pow",
807 "["Real.real, "Real.real] => "Real.real") $
808 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
809 Free ("1", "Real.real")) $
810 Free ("x", "Real.real"))),
811 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
813 "----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
814 case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()
815 | _ => error "clchead.sml: check specify phase step 2";
817 val (p,_,f,nxt,_,pt) = me nxt p c pt;
818 "----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
819 case nxt of ("Add_Given", Add_Given "integrateBy x") => ()
820 | _ => error "clchead.sml: check specify phase step 2";
822 "--------- check: fmz matches pbt -----------------------";
823 "--------- check: fmz matches pbt -----------------------";
824 "--------- check: fmz matches pbt -----------------------";
825 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
826 "the following fmz caused the above error";
827 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
828 val pI = ["plus_minus","polynom","vereinfachen"];
830 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
831 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
832 (*#############################^^^^^^^^^ defined by Isabelle*)
833 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
834 [Free ("N", _ (*"Real.real"*))])],
835 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
836 "#undef means: the element with description TERM in fmz did not match ";
837 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
838 "defined in Simplify.thy";
840 "So we try out how to create Simplify.Term:";
842 val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
843 " ^^^^^^^^^ see above";
847 val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
848 " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
852 val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
853 " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
854 " and unsed in pbl [plus_minus,polynom,vereinfachen]";
857 "----- so this is the correct fmz:";
858 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
859 val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
860 (*########################^^^^^^^^^ defined in Simplify.thy*)
861 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
863 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
865 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
866 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
867 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
869 "--------- fun typeless ---------------------------------";
870 "--------- fun typeless ---------------------------------";
871 "--------- fun typeless ---------------------------------";
873 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
874 > val (_,t1) = split_dsc_t hs (Thm.term_of ct);
875 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
876 > val (_,t2) = split_dsc_t hs (Thm.term_of ct);
877 > typeless t1 = typeless t2;
880 "--------- fun variants_in ------------------------------";
881 "--------- fun variants_in ------------------------------";
882 "--------- fun variants_in ------------------------------";
884 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
885 val it = ([3],[4,5,5,5,5,5]) : int list * int list
886 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
887 val it = [1,3,1,5] : int list
889 "--------- fun tag_form ---------------------------------";
890 "--------- fun tag_form ---------------------------------";
891 "--------- fun tag_form ---------------------------------";
892 (* val formal = (the o (parse thy)) "[R::real]";
893 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
894 > tag_form thy (formal, given);
895 val it = "fixed_values [R]" : cterm
897 "--------- fun foldr1, foldl1 ---------------------------";
898 "--------- fun foldr1, foldl1 ---------------------------";
899 "--------- fun foldr1, foldl1 ---------------------------";
901 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
902 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
903 > val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
904 > Thm.global_cterm_of thy conj;
905 val it = "(a = b & c = d) & e = f" : cterm
908 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
909 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
910 > val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
911 > Thm.global_cterm_of thy conj;
912 val it = "a = b & c = d & e = f & g = h" : cterm