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); print_depth 3;
50 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
51 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
52 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
54 "--------- maximum example with 'specify' ------------------------";
55 "--------- maximum example with 'specify' ------------------------";
56 "--------- maximum example with 'specify' ------------------------";
57 (*" Specify_Problem (match_itms_oris) ";*)
59 ["fixedValues [r=Arbfix]","maximum A",
60 "valuesFor [a,b::real]",
61 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
62 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
63 "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",
65 "boundVariable a","boundVariable b","boundVariable alpha",
66 "interval {x::real. 0 <= x & x <= 2*r}",
67 "interval {x::real. 0 <= x & x <= 2*r}",
68 "interval {x::real. 0 <= x & x <= pi}",
69 "errorBound (eps=(0::real))"];
71 ("DiffApp",["maximum_of","function"],
72 ["DiffApp","max_by_calculus"]);
75 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
76 val nxt = tac2tac_ pt p nxt;
77 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
78 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
80 val nxt = tac2tac_ pt p nxt;
81 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
84 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
85 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
87 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
88 Given=[Correct "fixedValues [r = Arbfix]"],
89 Relate=[Incompl "relations"], Where=[],With=[]})
90 then error "test-maximum.sml: model stepwise - different behaviour"
93 val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)");
94 (* WN1130630 THE maximum example WORKS IN isabisac09-2;
95 MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt.
96 Some tests have been broken much earlier,
97 see test/../calchead.sml "inhibit exn 010830". *)
98 (*========== inhibit exn WN1130630 maximum example broken =========================
99 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
100 ============ inhibit exn WN1130630 maximum example broken =======================*)
102 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
103 (*========== inhibit exn WN1130630 maximum example broken =========================
104 (* ERROR: Exception Bind raised *)
105 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
106 ============ inhibit exn WN1130630 maximum example broken =======================*)
108 val m = Specify_Problem ["maximum_of","function"];
109 val nxt = tac2tac_ pt p m;
110 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
111 (*========== inhibit exn WN1130630 maximum example broken =========================
112 if ppc<>(Problem ["maximum_of","function"],
113 {Find=[Incompl "maximum",Incompl "valuesFor"],
114 Given=[Correct "fixedValues [r = Arbfix]"],
115 Relate=[Incompl "relations []"], Where=[],With=[]})
116 then error "diffappl.sml: Specify_Problem different behaviour"
118 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
119 if ppc<>(Problem ["maximum_of","function"],
120 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
121 Given=[Correct "fixedValues [r = Arbfix]"],
122 Relate=[Missing "relations rs_"],Where=[],With=[]})
123 then error "diffappl.sml: Specify_Problem different behaviour"
125 ============ inhibit exn WN1130630 maximum example broken =======================*)
127 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
128 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
129 (*========== inhibit exn WN1130630 maximum example broken =========================
130 if ppc<>(Method ["DiffApp","max_by_calculus"],
131 {Find=[Incompl "maximum",Incompl "valuesFor"],
132 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
133 Missing "interval itv_",Missing "errorBound err_"],
134 Relate=[Incompl "relations []"],Where=[],With=[]})
135 then error "diffappl.sml: Specify_Method different behaviour"
137 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
138 if ppc<>(Method ["DiffApp","max_by_calculus"],
139 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
140 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
141 Missing "interval itv_",Missing "errorBound err_"],
142 Relate=[Missing "relations rs_"],Where=[],With=[]})
143 then error "diffappl.sml: Specify_Method different behaviour"
145 ============ inhibit exn WN1130630 maximum example broken =======================*)
147 "--------- maximum example with 'specify', fmz <> [] -------------";
148 "--------- maximum example with 'specify', fmz <> [] -------------";
149 "--------- maximum example with 'specify', fmz <> [] -------------";
151 ["fixedValues [r=Arbfix]","maximum A",
153 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
154 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
155 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
157 "boundVariable a","boundVariable b","boundVariable alpha",
158 "interval {x::real. 0 <= x & x <= 2*r}",
159 "interval {x::real. 0 <= x & x <= 2*r}",
160 "interval {x::real. 0 <= x & x <= pi}",
161 "errorBound (eps=(0::real))"];
163 ("DiffApp",["maximum_of","function"],
164 ["DiffApp","max_by_calculus"]);
166 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
167 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
169 val nxt = tac2tac_ pt p nxt;
170 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
171 val nxt = tac2tac_ pt p nxt;
172 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
173 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
175 val nxt = tac2tac_ pt p nxt;
176 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
177 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
179 val nxt = tac2tac_ pt p nxt;
180 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
181 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
183 val nxt = tac2tac_ pt p nxt;
184 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
185 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
187 val nxt = tac2tac_ pt p nxt;
188 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
189 (*val nxt = Add_Relation "relations [A = a * b]" *)
191 val nxt = tac2tac_ pt p nxt;
192 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
193 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
195 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
196 nxt_specif <> specify ?!
198 if nxt<>(Add_Relation
199 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
200 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
202 val nxt = tac2tac_ pt p nxt;
203 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
204 ------------------------------ FIXXXXME.meNEW !!! ---*)
206 (*val nxt = Specify_Theory "DiffApp" : tac*)
208 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
210 val nxt = tac2tac_ pt p nxt;
211 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
212 (*val nxt = Specify_Problem ["maximum_of","function"]*)
214 val nxt = tac2tac_ pt p nxt;
215 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
216 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
218 val nxt = tac2tac_ pt p nxt;
219 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
220 (*val nxt = Add_Given "boundVariable a" : tac*)
222 val nxt = tac2tac_ pt p nxt;
223 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
224 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
226 val nxt = tac2tac_ pt p nxt;
227 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
228 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
230 val nxt = tac2tac_ pt p nxt;
231 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
232 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
233 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
234 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
237 "--------- maximum example with 'specify', fmz = [] --------------";
238 "--------- maximum example with 'specify', fmz = [] --------------";
239 "--------- maximum example with 'specify', fmz = [] --------------";
241 val (dI',pI',mI') = empty_spec;
244 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
245 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
246 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
248 val nxt = tac2tac_ pt p nxt;
249 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
250 (*val nxt = Specify_Theory "e_domID" : tac*)
252 val nxt = Specify_Theory "DiffApp";
253 val nxt = tac2tac_ pt p nxt;
254 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
255 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
257 val nxt = Specify_Problem ["maximum_of","function"];
258 val nxt = tac2tac_ pt p nxt;
259 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
260 (*val nxt = Add_Given "fixedValues" : tac*)
262 val nxt = Add_Given "fixedValues [r=Arbfix]";
263 val nxt = tac2tac_ pt p nxt;
264 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
265 (*val nxt = Add_Find "maximum" : tac*)
267 val nxt = Add_Find "maximum A";
268 val nxt = tac2tac_ pt p nxt;
271 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
272 (*val nxt = Add_Find "valuesFor" : tac*)
274 val nxt = Add_Find "valuesFor [a]";
275 val nxt = tac2tac_ pt p nxt;
276 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
277 (*val nxt = Add_Relation "relations" ---
278 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
280 (*========== inhibit exn 010830 =======================================================*)
281 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
282 if nxt<>(Add_Relation "relations []")
283 then error "test specify, fmz <> []: nxt <> Add_Relation.."
284 else (); (*different with show_types !!!*)
286 (*========== inhibit exn 010830 =======================================================*)
288 val nxt = Add_Relation "relations [(A=a+b)]";
289 val nxt = tac2tac_ pt p nxt;
290 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
291 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
293 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
294 val nxt = tac2tac_ pt p nxt;
295 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
296 (*val nxt = Add_Given "boundVariable" : tac*)
298 val nxt = Add_Given "boundVariable alpha";
299 val nxt = tac2tac_ pt p nxt;
300 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
301 (*val nxt = Add_Given "interval" : tac*)
303 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
304 val nxt = tac2tac_ pt p nxt;
305 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
306 (*val nxt = Add_Given "errorBound" : tac*)
308 val nxt = Add_Given "errorBound (eps=999)";
309 val nxt = tac2tac_ pt p nxt;
310 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
311 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
313 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
314 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
315 then error "test specify, fmz <> []: nxt <> Add_Relation.."
318 (* 2.4.00 nach Transfer specify -> hard_gen
319 val nxt = Apply_Method ("DiffApp","max_by_calculus");
320 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
321 (*val nxt = Empty_Tac : tac*)
323 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
324 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
325 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
326 val Const ("Script.SubProblem",_) $
327 (Const ("Product_Type.Pair",_) $
329 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
330 (*...copied from stac2tac_*)
332 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
333 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
334 " REAL_LIST [c, c_2]]");
335 val ags = isalist2list ags';
336 val pI = ["LINEAR","system"];
337 val pats = (#ppc o get_pbt) pI;
338 "-a1-----------------------------------------------------";
339 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
340 val xxx = match_ags @{theory "EqSystem"} pats ags;
341 "-a2-----------------------------------------------------";
342 case match_ags @{theory "Isac"} pats ags of
343 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
344 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
345 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
346 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
348 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
350 "-b------------------------------------------------------";
351 val Const ("Script.SubProblem",_) $
352 (Const ("Product_Type.Pair",_) $
354 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
355 (*...copied from stac2tac_*)
357 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
358 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
359 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
360 val ags = isalist2list ags';
361 val pI = ["LINEAR","system"];
362 val pats = (#ppc o get_pbt) pI;
363 "-b1-----------------------------------------------------";
364 val xxx = match_ags @{theory "Isac"} pats ags;
365 "-b2-----------------------------------------------------";
366 case match_ags @{theory "EqSystem"} pats ags of
367 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
368 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
369 [_ $ Free ("c", _) $ _,
370 _ $ Free ("c_2", _) $ _]),
371 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
372 (* type of Find: [Free ("ss'''", "bool List.list")]*)
374 | _ => error "calchead.sml match_ags copy-named dropped --------";
376 "-c---ERROR case: stac is missing #Given equalities e_s--";
377 val stac as Const ("Script.SubProblem",_) $
378 (Const ("Product_Type.Pair",_) $
380 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
381 (*...copied from stac2tac_*)
383 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
384 " [REAL_LIST [c, c_2]]");
385 val ags = isalist2list ags';
386 val pI = ["LINEAR","system"];
387 val pats = (#ppc o get_pbt) pI;
388 (*============ inhibit exn AK110726 ==============================================
389 val xxx - match_ags (theory "EqSystem") pats ags;
390 ============ inhibit exn AK110726 ==============================================*)
391 "-c1-----------------------------------------------------";
392 "--------------------------step through code match_ags---";
393 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
394 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
395 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
396 val cy = filter is_copy_named pbt; (*=solution*)
397 (*============ inhibit exn AK110726 ==============================================
398 val oris' - matc thy pbt' ags [];
399 ============ inhibit exn AK110726 ==============================================*)
400 "-------------------------------step through code matc---";
401 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
402 (is_copy_named_idstr o free2str) t;
404 (*============ inhibit exn AK110726 ==============================================
405 val opt - mtc thy p a;
406 ============ inhibit exn AK110726 ==============================================*)
407 "--------------------------------step through code mtc---";
408 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
410 val ttt = (dsc $ var);
411 (*============ inhibit exn AK110726 ==============================================
412 cterm_of thy (dsc $ var);
413 ============ inhibit exn AK110726 ==============================================*)
415 "-------------------------------------step through end---";
416 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
417 val Const ("Script.SubProblem",_) $
418 (Const ("Product_Type.Pair",_) $
420 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
421 (*...copied from stac2tac_*)
423 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
424 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
425 " REAL_LIST [c, c_2]]");
426 val ags = isalist2list ags';
427 val pI = ["LINEAR","system"];
428 val pats = (#ppc o get_pbt) pI;
429 "-a1-----------------------------------------------------";
430 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
431 val xxx = match_ags @{theory "EqSystem"} pats ags;
432 "-a2-----------------------------------------------------";
433 case match_ags @{theory "Isac"} pats ags of
434 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
435 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
436 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
437 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
439 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
441 "-b------------------------------------------------------";
442 val Const ("Script.SubProblem",_) $
443 (Const ("Product_Type.Pair",_) $
445 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
446 (*...copied from stac2tac_*)
448 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
449 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
450 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
451 val ags = isalist2list ags';
452 val pI = ["LINEAR","system"];
453 val pats = (#ppc o get_pbt) pI;
454 "-b1-----------------------------------------------------";
455 val xxx = match_ags @{theory "Isac"} pats ags;
456 "-b2-----------------------------------------------------";
457 case match_ags @{theory "EqSystem"} pats ags of
458 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
459 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
460 [_ $ Free ("c", _) $ _,
461 _ $ Free ("c_2", _) $ _]),
462 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
463 (* type of Find: [Free ("ss'''", "bool List.list")]*)
465 | _ => error "calchead.sml match_ags copy-named dropped --------";
467 "-c---ERROR case: stac is missing #Given equalities e_s--";
468 val stac as Const ("Script.SubProblem",_) $
469 (Const ("Product_Type.Pair",_) $
471 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
472 (*...copied from stac2tac_*)
474 "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
475 " [REAL_LIST [c, c_2]]");
476 val ags = isalist2list ags';
477 val pI = ["LINEAR","system"];
478 val pats = (#ppc o get_pbt) pI;
479 (*============ inhibit exn AK110726 ==============================================
480 val xxx - match_ags (theory "EqSystem") pats ags;
481 -------------------------------------------------------------------*)
482 "-c1-----------------------------------------------------";
483 "--------------------------step through code match_ags---";
484 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
485 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
486 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
487 val cy = filter is_copy_named pbt; (*=solution*)
488 (*============ inhibit exn AK110726 ==============================================
489 val oris' - matc thy pbt' ags [];
490 -------------------------------------------------------------------*)
491 "-------------------------------step through code matc---";
492 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
493 (is_copy_named_idstr o free2str) t;
495 (*============ inhibit exn AK110726 ==============================================
496 val opt - mtc thy p a;
497 -------------------------------------------------------------------*)
498 "--------------------------------step through code mtc---";
499 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
501 val ttt = (dsc $ var);
502 (*============ inhibit exn AK110726 ==============================================
503 cterm_of thy (dsc $ var);
504 -------------------------------------------------------------------*)
505 "-------------------------------------step through end---";
507 case ((match_ags @{theory "EqSystem"} pats ags)
508 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
509 [] => match_ags_msg pI stac ags
510 | _ => error "calchead.sml match_ags 1st arg missing --------";
512 "-d------------------------------------------------------";
513 val stac as Const ("Script.SubProblem",_) $
514 (Const ("Product_Type.Pair",_) $
516 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
517 (*...copied from stac2tac_*)
519 "SubProblem (Test',[univariate,equation,test]," ^
520 " [no_met]) [BOOL (x+1=2), REAL x]");
521 val AGS = isalist2list ags';
522 val pI = ["univariate","equation","test"];
525 case ((match_ags @{theory "EqSystem"} pats ags)
526 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
527 [] => match_ags_msg pI stac ags
528 | _ => error "calchead.sml match_ags 1st arg missing --------";
530 "-d------------------------------------------------------";
531 val stac as Const ("Script.SubProblem",_) $
532 (Const ("Product_Type.Pair",_) $
534 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
535 (*...copied from stac2tac_*)
537 "SubProblem (Test',[univariate,equation,test]," ^
538 " [no_met]) [BOOL (x+1=2), REAL x]");
539 val AGS = isalist2list ags';
540 val pI = ["univariate","equation","test"];
541 val PATS = (#ppc o get_pbt) pI;
542 "-d1-----------------------------------------------------";
543 "--------------------------step through code match_ags---";
544 val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);
545 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
546 val pbt' = filter_out is_copy_named pbt;
547 val cy = filter is_copy_named pbt;
548 val oris' = matc thy pbt' ags [];
549 "-------------------------------step through code matc---";
550 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
551 (is_copy_named_idstr o free2str) t;
553 val opt = mtc thy p a;
554 "--------------------------------step through code mtc---";
555 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
556 val ttt = (dsc $ var);
557 cterm_of thy (dsc $ var);
558 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
560 "-d2-----------------------------------------------------";
562 "-------------------------------step through code matc---";
563 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
564 (is_copy_named_idstr o free2str) t;
566 val opt = mtc thy p a;
567 "--------------------------------step through code mtc---";
568 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
569 val ttt = (dsc $ var);
570 cterm_of thy (dsc $ var);
571 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
572 "-d3-----------------------------------------------------";
573 pbt = []; (*true, base case*)
574 "-----------------continue step through code match_ags---";
575 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
576 "--------------------------------step through cpy_nam----";
577 val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
578 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
579 "--------------------------------------------------------";
580 fun is_copy_named_generating_idstr str =
581 if is_copy_named_idstr str
582 then case (rev o Symbol.explode) str of
583 (*"_"::"_"::"_"::_ => false*)
584 "'"::"'"::"'"::_ => false
587 fun is_copy_named_generating (_, (_, t)) =
588 (is_copy_named_generating_idstr o free2str) t;
589 "--------------------------------------------------------";
590 is_copy_named_generating p (*true*);
591 fun sel (_,_,d,ts) = comp_ts (d, ts);
592 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
594 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
596 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
597 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
598 val vals = map sel oris;
599 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
601 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
602 (assoc (vars'~~vals, cy'));
603 (*SOME (Free ("x", "Real.real")) : term option*)
604 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
606 "-----------------continue step through code match_ags---";
607 val cy' = map (cpy_nam pbt' oris') cy;
608 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
609 "-------------------------------------step through end---";
611 case match_ags thy PATS AGS of
612 [(1, [1], "#Given", Const ("Descript.equality", _),
613 [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
614 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
615 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
616 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
618 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
620 "--------- regression test fun is_copy_named ------------";
621 "--------- regression test fun is_copy_named ------------";
622 "--------- regression test fun is_copy_named ------------";
623 val trm = (1, (2, @{term "v'i'"}));
624 if is_copy_named trm then () else error "regr. is_copy_named 1";
625 val trm = (1, (2, @{term "e_e"}));
626 if is_copy_named trm then error "regr. is_copy_named 2" else ();
627 val trm = (1, (2, @{term "L'''"}));
628 if is_copy_named trm then () else error "regr. is_copy_named 3";
630 (* out-comment 'structure CalcHead'...
631 val trm = (1, (2, @{term "v'i'"}));
632 if is_copy_named_generating trm then () else error "regr. is_copy_named";
633 val trm = (1, (2, @{term "L'''"}));
634 if is_copy_named_generating trm then error "regr. is_copy_named" else ();
637 "--------- regr.test fun cpy_nam ------------------------";
638 "--------- regr.test fun cpy_nam ------------------------";
639 "--------- regr.test fun cpy_nam ------------------------";
640 (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
641 (*the model-pattern, is_copy_named are filter_out*)
642 pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
643 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
644 (*the model specific for an example*)
645 oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
646 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
647 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
648 (*...all must be true*)
650 case cpy_nam pbt oris (hd cy) of
651 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
652 | _ => error "calchead.sml regr.test cpy_nam-1-";
654 (*new data: cpy_nam without changing the name*)
655 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
656 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
657 @{term "solution"}; type_of @{term "ss''' :: bool list"};
658 (*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)
659 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
660 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
661 (*the model specific for an example*)
662 val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
663 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
664 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
665 (*could be more than 1*)];
667 case cpy_nam pbt oris (hd cy) of
668 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
669 | _ => error "calchead.sml regr.test cpy_nam-2-";
671 "--------- check specify phase --------------------------";
672 "--------- check specify phase --------------------------";
673 "--------- check specify phase --------------------------";
674 (*val fmz = ["functionTerm (x^^^2 + 1)",*)
675 val fmz = ["functionTerm (x + 1)",
676 "integrateBy x","antiDerivative FF"];
678 ("Integrate",["integrate","function"],
679 ["diff","integration"]);
680 val p = e_pos'; val c = [];
682 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
683 (*> val it = "--- step 1 --" : string
687 (0, EdUndef, 0, Nundef,
689 {Find = [], With = [], Given = [], Where = [], Relate = []})))
691 val nxt = ("Model_Problem", Model_Problem) : string * tac
692 val p = ([], Pbl) : pos'
696 (["functionTerm (x^^^2 + 1)", "integrateBy x",
697 "antiDerivative FF"],
698 ("Integrate", ["integrate", "function"],
699 ["diff", "integration"])),
701 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
703 cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
704 probl = [], branch = TransitiveB,
707 Const ("Descript.functionTerm", "Real.real => Tools.una"),
709 "["Real.real, "Real.real] => "Real.real") $
710 (Const ("Atools.pow",
711 "["Real.real, "Real.real] => "Real.real") $
712 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
713 Free ("1", "Real.real")]),
715 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
716 [Free ("x", "Real.real")]),
718 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
719 [Free ("FF", "Real.real")])],
720 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
721 Const ("Integrate.Integrate",
722 "("Real.real, "Real.real) * => "Real.real") $
723 (Const ("Product_Type.Pair",
724 "["Real.real, "Real.real]
725 => ("Real.real, "Real.real) *") $
727 "["Real.real, "Real.real] => "Real.real") $
728 (Const ("Atools.pow",
729 "["Real.real, "Real.real] => "Real.real") $
730 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
731 Free ("1", "Real.real")) $
732 Free ("x", "Real.real"))),
733 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
735 "----- WN101007 worked until here (checked same as isac2002) ---";
736 if nxt = ("Model_Problem", Model_Problem) then ()
737 else error "clchead.sml: check specify phase step 1";
739 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
740 (*val it = "--- step 2 --" : string
741 val p = ([], Pbl) : pos'
745 (0, EdUndef, 0, Nundef,
747 {Find = [Incompl "Integrate.antiDerivative"],
749 Given = [Incompl "functionTerm", Incompl "integrateBy"],
751 Relate = []}))) : mout
752 val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
756 (["functionTerm (x^^^2 + 1)", "integrateBy x",
757 "antiDerivative FF"],
758 ("Integrate", ["integrate", "function"],
759 ["diff", "integration"])),
762 (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
764 cell = None, meth = [], spec =
765 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
766 [(0, [], false, "#Given",
767 Inc ((Const ("Descript.functionTerm",
768 "Real.real => Tools.una"),[]),
769 (Const ("empty", "'a"), []))),
770 (0, [], false, "#Given",
771 Inc ((Const ("Integrate.integrateBy",
772 "Real.real => Tools.una"),[]),
773 (Const ("empty", "'a"), []))),
774 (0, [], false, "#Find",
775 Inc ((Const ("Integrate.antiDerivative",
776 "Real.real => Tools.una"),[]),
777 (Const ("empty", "'a"), [])))],
778 branch = TransitiveB, origin =
780 Const ("Descript.functionTerm", "Real.real => Tools.una"),
782 "["Real.real, "Real.real] => "Real.real") $
783 (Const ("Atools.pow",
784 "["Real.real, "Real.real] => "Real.real") $
785 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
786 Free ("1", "Real.real")]),
788 Const ("Integrate.integrateBy", "Real.real => Tools.una"),
789 [Free ("x", "Real.real")]),
791 Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
792 [Free ("FF", "Real.real")])],
793 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
794 Const ("Integrate.Integrate",
795 "("Real.real, "Real.real) * => "Real.real") $
796 (Const ("Product_Type.Pair",
797 "["Real.real, "Real.real]
798 => ("Real.real, "Real.real) *") $
800 "["Real.real, "Real.real] => "Real.real") $
801 (Const ("Atools.pow",
802 "["Real.real, "Real.real] => "Real.real") $
803 Free ("x", "Real.real") $ Free ("2", "Real.real")) $
804 Free ("1", "Real.real")) $
805 Free ("x", "Real.real"))),
806 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
808 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
809 if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
810 else error "clchead.sml: check specify phase step 2";
812 val (p,_,f,nxt,_,pt) = me nxt p c pt;
813 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
814 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
815 else error "clchead.sml: check specify phase step 2";
817 "--------- check: fmz matches pbt -----------------------";
818 "--------- check: fmz matches pbt -----------------------";
819 "--------- check: fmz matches pbt -----------------------";
820 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
821 "the following fmz caused the above error";
822 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
823 val pI = ["plus_minus","polynom","vereinfachen"];
825 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
826 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
827 (*#############################^^^^^^^^^ defined by Isabelle*)
828 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
829 [Free ("N", _ (*"Real.real"*))])],
830 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
831 "#undef means: the element with description TERM in fmz did not match ";
832 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
833 "defined in Simplify.thy";
835 "So we try out how to create Simplify.Term:";
837 val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
838 " ^^^^^^^^^ see above";
842 val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
843 " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
847 val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
848 " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
849 " and unsed in pbl [plus_minus,polynom,vereinfachen]";
852 "----- so this is the correct fmz:";
853 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
854 val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
855 (*########################^^^^^^^^^ defined in Simplify.thy*)
856 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
858 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
860 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
861 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
862 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;