1 (* Title: tests for Interpret/ptyps.sml
2 Author: Walther Neuper 010916
3 (c) due to copyright terms
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "-ptyps.thy: store test-pbtyps by 'setup' ------------------------";
10 "----------- testdata for refin, refine_ori ----------------------";
11 (*"----------- refin test-pbtyps -------requires 'setup'------------";*)
12 "----------- refine_ori test-pbtyps --requires 'setup'------------";
13 "----------- refine test-pbtyps ------requires 'setup'------------";
14 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
15 "----------- fun coll_guhs ---------------------------------------";
16 "----------- fun guh2kestoreID -----------------------------------";
17 "----------- fun mark --------------------------------------------";
18 "----------- fun coll --------------------------------------------";
19 "----------- fun coll_variants -----------------------------------";
20 "----------- fun add_id ------------------------------------------";
21 "----------- fun filter_vat --------------------------------------";
22 "----------- fun match_pbl ---------------------------------------";
23 "----------- fun match_oris --------------------------------------";
24 "-------- fun get_fun_ids ----------------------------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
27 "-----------------------------------------------------------------";
29 "----------- testdata for refin, refine_ori ----------------------";
30 "----------- testdata for refin, refine_ori ----------------------";
31 "----------- testdata for refin, refine_ori ----------------------";
33 val thy = @{theory "Isac"};
34 val ctxt = Proof_Context.init_global @{theory "Isac"};
36 (*case 1: no refinement *)
37 val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
38 val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
39 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
41 (*case 2: refined to pbt without children *)
42 val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
43 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
45 (*case 3: refined to pbt with children *)
46 val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
47 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
49 (*case 4: refined to children (without child)*)
50 val (d3,ts3) = split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
51 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
53 (*=================================================================
54 This test expects pbls at a certain position in the tree.
55 Since parallel evaluation (i.e. Theory_Data) this cannot be expected.
57 * provide an access function for a branch (not only leaves)
58 * sort the tree of pbls.
59 "----------- refin test-pbtyps -----------------------------------";
60 "----------- refin test-pbtyps -----------------------------------";
61 "----------- refin test-pbtyps -----------------------------------";
62 (* fragile test setup: expects ptyps as fixed *)
63 val level_1 = case nth 9 (get_ptyps ()) of
64 Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
65 val level_2 = case nth 4 level_1 of
66 Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
67 val pbla_branch = case level_2 of
68 [Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
70 (*case 1: no refinement *)
71 case refin [] ori1 (hd pbla_branch) of
72 SOME ["pbla"] => () | _ => error "refin case 1 broken";
74 (*case 2: refined to pbt without children *)
75 case refin [] ori2 (hd pbla_branch) of
76 SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";
78 (*case 3: refined to pbt with children *)
79 case refin [] ori3 (hd pbla_branch) of
80 SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";
82 (*case 4: refined to children (without child)*)
83 case refin [] ori4 (hd pbla_branch) of
84 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
86 (*case 5: start refinement somewhere in ptyps*)
87 val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = pbla_branch;
88 case refin ["pbla"] ori4 ppp of
89 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
90 ==================================================================*)
92 "----------- refine_ori test-pbtyps ------------------------------";
93 "----------- refine_ori test-pbtyps ------------------------------";
94 "----------- refine_ori test-pbtyps ------------------------------";
95 (*case 1: no refinement *)
96 case refine_ori ori1 ["pbla", "refine", "test"] of
97 NONE => () | _ => error "refine_ori case 1 broken";
99 (*case 2: refined to pbt without children *)
100 case refine_ori ori2 ["pbla", "refine", "test"] of
101 SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "refine_ori case 2 broken";
103 (*case 3: refined to pbt with children *)
104 case refine_ori ori3 ["pbla", "refine", "test"] of
105 SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "refine_ori case 3 broken";
107 (*case 4: refined to children (without child)*)
108 case refine_ori ori4 ["pbla", "refine", "test"] of
109 SOME ["pbla2y","pbla2","pbla", "refine", "test"] => () | _ => error "refine_ori case 4 broken";
111 (*case 5: start refinement somewhere in ptyps*)
112 case refine_ori ori4 ["pbla2","pbla", "refine", "test"] of
113 SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "refine_ori case 5 broken";
115 "----------- refine test-pbtyps ----------------------------------";
116 "----------- refine test-pbtyps ----------------------------------";
117 "----------- refine test-pbtyps ----------------------------------";
118 val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];
119 val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];
120 val fmz3 = ["fixedValues [aaa=0]","valuesFor [aaa222]"];
121 val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
122 "boundVariable aaa222yyy"];
124 (*case 1: no refinement *)
125 case refine fmz1 ["pbla", "refine", "test"] of
126 [Matches (["pbla", "refine", "test"], _),
127 NoMatch (["pbla1", "pbla", "refine", "test"], _),
128 NoMatch (["pbla2", "pbla", "refine", "test"], _),
129 NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
130 | _ => error "--- refine test-pbtyps --- broken with case 1";
133 *** pass ["pbla","pbla1"]
134 *** pass ["pbla","pbla2"]
135 *** pass ["pbla","pbla3"]
140 Given=[Correct "fixedValues [aaa = #0]",
141 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
145 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
146 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
150 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
151 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
155 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
156 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
159 (*case 2: refined to pbt without children *)
160 case refine fmz2 ["pbla", "refine", "test"] of
161 [Matches (["pbla", "refine", "test"], _),
162 NoMatch (["pbla1", "pbla", "refine", "test"], _),
163 NoMatch (["pbla2", "pbla", "refine", "test"], _),
164 Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
165 | _ => error "--- refine test-pbtyps --- broken with case 2";
168 *** pass ["pbla","pbla1"]
169 *** pass ["pbla","pbla2"]
170 *** pass ["pbla","pbla3"]
175 Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
176 Relate=[],Where=[],With=[]}),
180 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
181 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
185 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
186 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
190 Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
191 Relate=[],Where=[],With=[]})] : match list*)
193 (*case 3: refined to pbt with children *)
194 case refine fmz3 ["pbla", "refine", "test"] of
195 [Matches (["pbla", "refine", "test"], _),
196 NoMatch (["pbla1", "pbla", "refine", "test"], _),
197 Matches (["pbla2", "pbla", "refine", "test"], _),
198 NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
199 NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
200 NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
201 NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
202 | _ => error "--- refine test-pbtyps --- broken with case 3";
205 *** pass ["pbla","pbla1"]
206 *** pass ["pbla","pbla2"]
207 *** pass ["pbla","pbla2","pbla2x"]
208 *** pass ["pbla","pbla2","pbla2y"]
209 *** pass ["pbla","pbla2","pbla2z"]
210 *** pass ["pbla","pbla3"]
215 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
216 Relate=[],Where=[],With=[]}),
220 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
221 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
225 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
226 Relate=[],Where=[],With=[]}),
228 (["pbla2x","pbla2","pbla"],
230 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
231 Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
233 (["pbla2y","pbla2","pbla"],
235 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
236 Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
238 (["pbla2z","pbla2","pbla"],
240 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
241 Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
245 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
246 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
249 (*case 4: refined to children (without child)*)
250 case refine fmz4 ["pbla", "refine", "test"] of
251 [Matches (["pbla", "refine", "test"], _),
252 NoMatch (["pbla1", "pbla", "refine", "test"], _),
253 Matches (["pbla2", "pbla", "refine", "test"], _),
254 NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
255 Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
256 | _ => error "--- refine test-pbtyps --- broken with case 4";
259 *** pass ["pbla","pbla1"]
260 *** pass ["pbla","pbla2"]
261 *** pass ["pbla","pbla2","pbla2x"]
262 *** pass ["pbla","pbla2","pbla2y"]
267 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
268 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
272 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
273 Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
274 Relate=[],Where=[],With=[]}),
278 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
279 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
281 (["pbla2x","pbla2","pbla"],
283 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
284 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
285 Relate=[],Where=[],With=[]}),
287 (["pbla2y","pbla2","pbla"],
289 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
290 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
293 (*case 5: start refinement somewhere in ptyps*)
294 case refine fmz4 ["pbla2","pbla", "refine", "test"] of
295 [Matches (["pbla2", "pbla", "refine", "test"], _),
296 NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
297 Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
298 | _ => error "--- refine test-pbtyps --- broken with case 5";
300 *** pass ["pbla","pbla2"]
301 *** pass ["pbla","pbla2","pbla2x"]
302 *** pass ["pbla","pbla2","pbla2y"]
307 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
308 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
310 (["pbla2x","pbla2","pbla"],
312 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
313 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
314 Relate=[],Where=[],With=[]}),
316 (["pbla2y","pbla2","pbla"],
318 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
319 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
322 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
323 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
324 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
325 (*WN120313: attention: the 'nxt' in the comments are not correct!*)
327 val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))","solveFor x",
328 "errorBound (eps=0)","solutions L"];
329 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
330 ["Test","squ-equ-test-subpbl1"]);
331 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
332 val (p,_,f,nxt,_,pt) = me nxt p c pt;
333 val (p,_,f,nxt,_,pt) = me nxt p c pt;
334 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Add_Find", Add_Find "solutions L")*)
336 val nxt = ("Specify_Problem", Specify_Problem ["LINEAR","univariate","equation","test"]);
337 (*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
338 val (p,_,f,nxt,_,pt) = me nxt p c pt;
340 case f of PpcKF (Problem [],
341 {Find = [Incompl "solutions []"], With = [],
342 Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
344 Relate = [],...}) => www
345 | _ => error "--- Refine_Problem broken 1";
346 if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
347 then () else error "--- Refine_Problem broken 2";
349 val it = Form' (PpcKF (0,EdUndef,0,Nundef,
350 (Problem ["LINEAR","univariate","equation","test"], <<<<<===== diff.to above WN120313
351 {Find=[Incompl "solutions []"],
352 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
353 Correct "solveFor x"],Relate=[],
354 Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
355 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
356 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
357 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
359 val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)
361 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e*);
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 (*val nxt = ("Empty_Tac",Empty_Tac)
364 ... Refine_Problem ["LINEAR"..] fails internally 040312: works!?!*)
366 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
367 (*=== refine problem -----------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
368 val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
370 val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 (*nxt = ("Specify_Theory", Specify_Theory "Test")*)
372 val (p,_,f,nxt,_,pt) = me nxt p c pt;
373 (*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
374 val (p,_,f,nxt,_,pt) = me nxt p c pt;
375 (*nxt = ("Apply_Method", *)
376 val (p,_,f,nxt,_,pt) = me nxt p c pt;
377 (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
378 val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
380 val (p,_,f,nxt,_,pt) = me nxt p c pt;
381 (*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
383 val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 (*nxt = Model_Problem ["LINEAR","univariate","equation","test"]*)
385 val (p,_,f,nxt,_,pt) = me nxt p c pt;
386 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 val (p,_,f,nxt,_,pt) = me nxt p c pt;
390 val (p,_,f,nxt,_,pt) = me nxt p c pt;
391 val (p,_,f,nxt,_,pt) = me nxt p c pt;
392 (*nxt = Specify_Problem ["LINEAR","univariate","equation","test"])*)
393 val (p,_,f,nxt,_,pt) = me nxt p c pt;
394 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
395 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
396 val (p,_,f,nxt,_,pt) = me nxt p c pt;
397 (*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
398 val (p,_,f,nxt,_,pt) = me nxt p c pt;
399 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
400 val (p,_,f,nxt,_,pt) = me nxt p c pt;
401 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
403 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
404 val (p,_,f,nxt,_,pt) = me nxt p c pt;
405 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
406 val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
408 val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
410 val (p,_,f,nxt,_,pt) = me nxt p c pt;
411 (*Check_Postcond ["normalise","univariate","equation","test"])*)
412 val (p,_,f,nxt,_,pt) = me nxt p c pt;
416 then case nxt of ("End_Proof'", End_Proof') => ()
417 | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
418 else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
420 "----------- fun coll_guhs ---------------------------------------";
421 "----------- fun coll_guhs ---------------------------------------";
422 "----------- fun coll_guhs ---------------------------------------";
424 (#guh : pbt -> guh) e_pbt;
426 fun XXXnode coll (Ptyp (_,[n],ns)) =
427 [(#guh : pbt -> guh) n]
428 and XXXnodes coll [] = coll
429 | XXXnodes coll (n::ns : pbt ptyp list) = (XXXnode coll n) @
431 (*^^^ this works, but not this ...
432 fun node coll (Ptyp (_,[n],ns)) =
433 [(#guh : 'a -> guh) n]
434 and nodes coll [] = coll
435 | nodes coll (n::ns : 'a ptyp list) = (node coll n) @ (nodes coll ns);
438 Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)
439 Found near #guh : 'a -> guh
441 i.e. there is no common fun for pbls and mets ?!?*)
443 coll_pblguhs (get_ptyps ());
444 sort string_ord (coll_pblguhs (get_ptyps ()));
448 "----------- fun guh2kestoreID -----------------------------------";
449 "----------- fun guh2kestoreID -----------------------------------";
450 "----------- fun guh2kestoreID -----------------------------------";
451 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
452 (* ERROR: Exception Bind raised *)
453 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
454 Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
457 nodes [] guh1 (get_ptyps ());
458 nodes [] guh2 (get_ptyps ());
460 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
462 Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
463 (Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
465 Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
467 _ ) = (get_ptyps ());
469 nodes [] guh3 (get_ptyps ());
470 nodes [] guh21 (get_ptyps ());
473 "----------- fun mark --------------------------------------------";
474 "----------- fun mark --------------------------------------------";
475 "----------- fun mark --------------------------------------------";
477 > val xs = [1,1,1,2,4,4,5];
479 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
482 "----------- fun coll --------------------------------------------";
483 "----------- fun coll --------------------------------------------";
484 "----------- fun coll --------------------------------------------";
486 > val xs = [1,1,1,2,4,4,4];
488 val it = [1,2,4] : int list
490 "----------- fun coll_variants -----------------------------------";
491 "----------- fun coll_variants -----------------------------------";
492 "----------- fun coll_variants -----------------------------------";
493 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
494 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
495 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
496 "----------- fun add_id ------------------------------------------";
497 "----------- fun add_id ------------------------------------------";
498 "----------- fun add_id ------------------------------------------";
500 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
502 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
504 "----------- fun filter_vat --------------------------------------";
505 "----------- fun filter_vat --------------------------------------";
506 "----------- fun filter_vat --------------------------------------";
507 (*> map (filter_vat oris) [1,2,3];
509 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
510 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
511 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
512 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
513 (6,[1],"#undef",Const (#,#),[Free #]),
514 (9,[1,2],"#undef",Const (#,#),[# $ #]),
515 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
516 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
517 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
518 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
519 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
520 (7,[2],"#undef",Const (#,#),[Free #]),
521 (9,[1,2],"#undef",Const (#,#),[# $ #]),
522 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
523 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
524 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
525 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
526 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
527 (8,[3],"#undef",Const (#,#),[Free #]),
528 (10,[3],"#undef",Const (#,#),[# $ #]),
529 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
530 "----------- fun match_pbl ---------------------------------------";
531 "----------- fun match_pbl ---------------------------------------";
532 "----------- fun match_pbl ---------------------------------------";
534 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
535 "solveFor x","errorBound (eps=0)","solutions L"];
536 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
537 get_pbt ["univariate","equation"];
540 "----------- fun match_oris --------------------------------------";
541 "----------- fun match_oris --------------------------------------";
542 "----------- fun match_oris --------------------------------------";
543 (* val (pblRD,ori)=("xxx",oris);
544 val py = get_pbt ["equation"];
545 val py = get_pbt ["univariate","equation"];
546 val py = get_pbt ["linear","univariate","equation"];
547 val py = get_pbt ["root\"","univariate","equation"];
548 match_oris (#prls py) ori (#ppc py, #where_ py);
551 "-------- fun get_fun_ids ----------------------------------------------------";
552 "-------- fun get_fun_ids ----------------------------------------------------";
553 "-------- fun get_fun_ids ----------------------------------------------------";
554 val met_fun_ids = get_fun_ids @{theory Biegelinie};
555 if map fst (get_fun_ids @{theory Biegelinie}) =
556 ["Biegelinie.function_to_equality", "Biegelinie.biegelinie", "Biegelinie.belastung_zu_biegelinie",
557 "Biegelinie.setzte_randbedingungen"] then () else error "get_fun_ids changed"