1 (* tests on calchead.sml
4 (c) due to copyright terms
6 use"../smltest/ME/calchead.sml";
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "--------- get_interval after replace} other 2 -------------------";
14 "--------- maximum example with 'specify' ------------------------";
15 "--------- maximum example with 'specify', fmz <> [] -------------";
16 "--------- maximum example with 'specify', fmz = [] --------------";
17 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
20 "-----------------------------------------------------------------";
23 "--------- get_interval after replace} other 2 -------------------";
24 "--------- get_interval after replace} other 2 -------------------";
25 "--------- get_interval after replace} other 2 -------------------";
28 [(["equality (x+1=2)", "solveFor x","solutions L"],
30 ["sqroot-test","univariate","equation","test"],
31 ["Test","squ-equ-test-subpbl1"]))];
34 autoCalculate 1 CompleteCalc;
35 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
36 replaceFormula 1 "x = 1";
37 (*... returns calcChangedEvent with ...*)
38 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
39 val ((pt,_),_) = get_calc 1;
41 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
42 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
43 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
44 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
45 ([3, 2], Res)] then () else
46 raise error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
48 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
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 raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
57 "--------- maximum example with 'specify' ------------------------";
58 "--------- maximum example with 'specify' ------------------------";
59 "--------- maximum example with 'specify' ------------------------";
60 (*" Specify_Problem (match_itms_oris) ";*)
62 ["fixedValues [r=Arbfix]","maximum A",
64 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
65 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
66 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
68 "boundVariable a","boundVariable b","boundVariable alpha",
69 "interval {x::real. 0 <= x & x <= 2*r}",
70 "interval {x::real. 0 <= x & x <= 2*r}",
71 "interval {x::real. 0 <= x & x <= pi}",
72 "errorBound (eps=(0::real))"];
74 ("DiffApp.thy",["maximum_of","function"],
75 ["DiffApp","max_by_calculus"]);
78 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
79 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
81 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
82 val nxt = tac2tac_ pt p nxt;
83 val(p,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
91 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
92 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
93 (*uncaught exception TYPE 6.5.03*)
96 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
97 Given=[Correct "fixedValues [r = Arbfix]"],
98 Relate=[Incompl "relations []"], Where=[],With=[]})
99 then raise error "test-maximum.sml: model stepwise - different behaviour"
100 else (); (*different with show_types !!!*)
103 (*-----appl_add should not create Error', but accept as Sup,Syn
104 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
105 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
107 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
108 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
111 val m = Specify_Problem ["maximum_of","function"];
112 val nxt = tac2tac_ pt p m;
113 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
116 if ppc<>(Problem ["maximum_of","function"],
117 {Find=[Incompl "maximum",Incompl "valuesFor"],
118 Given=[Correct "fixedValues [r = Arbfix]"],
119 Relate=[Incompl "relations []"], Where=[],With=[]})
120 then raise error "diffappl.sml: Specify_Problem different behaviour"
122 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
123 if ppc<>(Problem ["maximum_of","function"],
124 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
125 Given=[Correct "fixedValues [r = Arbfix]"],
126 Relate=[Missing "relations rs_"],Where=[],With=[]})
127 then raise error "diffappl.sml: Specify_Problem different behaviour"
130 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
131 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
134 if ppc<>(Method ["DiffApp","max_by_calculus"],
135 {Find=[Incompl "maximum",Incompl "valuesFor"],
136 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",
137 Missing "interval itv_",Missing "errorBound err_"],
138 Relate=[Incompl "relations []"],Where=[],With=[]})
139 then raise error "diffappl.sml: Specify_Method different behaviour"
141 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly
142 if ppc<>(Method ["DiffApp","max_by_calculus"],
143 {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
144 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",
145 Missing "interval itv_",Missing "errorBound err_"],
146 Relate=[Missing "relations rs_"],Where=[],With=[]})
147 then raise error "diffappl.sml: Specify_Method different behaviour"
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.thy",["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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
176 val nxt = tac2tac_ pt p nxt;
177 val(p,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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 raise 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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
209 ------------------------------ FIXXXXME.meNEW !!! ---*)
211 (*val nxt = Specify_Theory "DiffApp.thy" : 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,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
221 (*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
223 val nxt = tac2tac_ pt p nxt;
224 val(p,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
237 (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
238 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
239 then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
253 val nxt = tac2tac_ pt p nxt;
254 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
255 (*val nxt = Specify_Theory "e_domID" : tac*)
257 val nxt = Specify_Theory "DiffApp.thy";
258 val nxt = tac2tac_ pt p nxt;
259 val(p,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
282 (*val nxt = Add_Relation "relations" ---
283 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
285 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
286 if nxt<>(Add_Relation "relations []")
287 then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
288 else (); (*different with show_types !!!*)
291 val nxt = Add_Relation "relations [(A=a+b)]";
292 val nxt = tac2tac_ pt p nxt;
293 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
294 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
296 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
297 val nxt = tac2tac_ pt p nxt;
298 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
299 (*val nxt = Add_Given "boundVariable" : tac*)
301 val nxt = Add_Given "boundVariable alpha";
302 val nxt = tac2tac_ pt p nxt;
303 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
304 (*val nxt = Add_Given "interval" : tac*)
306 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
307 val nxt = tac2tac_ pt p nxt;
308 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
309 (*val nxt = Add_Given "errorBound" : tac*)
311 val nxt = Add_Given "errorBound (eps=999)";
312 val nxt = tac2tac_ pt p nxt;
313 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
314 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
315 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
316 if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
317 then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
321 (* 2.4.00 nach Transfer specify -> hard_gen
322 val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
323 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
324 (*val nxt = Empty_Tac : tac*)
327 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
328 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
330 val Const ("Script.SubProblem",_) $
333 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
334 (*...copied from stac2tac_*)
336 "SubProblem (EqSystem_, [linear, system], [no_met])\
337 \ [bool_list_ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
338 \ real_list_ [c, c_2]]";
339 val ags = isalist2list ags';
340 val pI = ["linear","system"];
341 val pats = (#ppc o get_pbt) pI;
342 case match_ags Isac.thy 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 | _ => raise error "calchead.sml match_ags 2 args OK -----------------";
351 val Const ("Script.SubProblem",_) $
354 (Const ("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 case match_ags Isac.thy pats ags of
364 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
365 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
366 [_ $ Free ("c", _) $ _,
367 _ $ Free ("c_2", _) $ _]),
368 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
369 (* type of Find: [Free ("ss___", "bool List.list")]*)
371 | _ => raise error "calchead.sml match_ags copy-named dropped --------";
374 val stac as Const ("Script.SubProblem",_) $
377 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
378 (*...copied from stac2tac_*)
380 "SubProblem (EqSystem_, [linear, system], [no_met])\
381 \ [real_list_ [c, c_2]]";
382 val ags = isalist2list ags';
383 val pI = ["linear","system"];
384 val pats = (#ppc o get_pbt) pI;
385 case ((match_ags Isac.thy pats ags)
386 handle TYPE _ => []) of
387 [] => match_ags_msg pI stac ags
388 | _ => raise error "calchead.sml match_ags 1st arg missing --------";
391 use"../smltest/ME/calchead.sml";
394 val stac as Const ("Script.SubProblem",_) $
397 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
398 (*...copied from stac2tac_*)
400 "SubProblem (Test_,[univariate,equation,test],\
401 \ [no_met]) [bool_ (x+1=2), real_ x]";
402 val ags = isalist2list ags';
403 val pI = ["univariate","equation","test"];
404 val pats = (#ppc o get_pbt) pI;
405 case match_ags Isac.thy pats ags of
407 Const ("Descript.equality", _),
408 [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),
409 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
410 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
411 (* type of Find: [Free ("x_i", "bool List.list")]*)
413 | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";