1 (* Title: "Specify/refine.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";
10 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
11 (*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)
12 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
13 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
14 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
17 "-----------------------------------------------------------------------------------------------";
20 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
21 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
22 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
23 Test_Tool.show_ptyps();
24 val thy = @{theory "Isac_Knowledge"};
25 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
27 (*case 1: no refinement *)
28 val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");
29 val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");
30 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
32 (*case 2: refined to pbt without children *)
33 val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");
34 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
36 (*case 3: refined to pbt with children *)
37 val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");
38 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
40 (*case 4: refined to children (without child)*)
41 val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");
42 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
44 (*=================================================================
45 This test expects pbls at a certain position in the tree.
46 Since parallel evaluation (i.e. Theory_Data) this cannot be expected.
48 * provide an access function for a branch (not only leaves)
49 * sort the tree of pbls.
50 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
51 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
52 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
53 (* fragile test setup: expects ptyps as fixed *)
54 val level_1 = case nth 9 (get_ptyps ()) of
55 Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
56 val level_2 = case nth 4 level_1 of
57 Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
58 val pbla_branch = case level_2 of
59 [Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
61 (*case 1: no refinement *)
62 case refin [] ori1 (hd pbla_branch) of
63 SOME ["pbla"] => () | _ => error "refin case 1 broken";
65 (*case 2: refined to pbt without children *)
66 case refin [] ori2 (hd pbla_branch) of
67 SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";
69 (*case 3: refined to pbt with children *)
70 case refin [] ori3 (hd pbla_branch) of
71 SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";
73 (*case 4: refined to children (without child)*)
74 case refin [] ori4 (hd pbla_branch) of
75 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
77 (*case 5: start refinement somewhere in ptyps*)
78 val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;
79 case refin ["pbla"] ori4 ppp of
80 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
81 ==================================================================*)
84 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
85 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
86 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
87 (*case 1: no refinement *)
88 case Refine.refine_ori ori1 ["pbla", "refine", "test"] of
89 NONE => () | _ => error "Refine.refine_ori case 1 broken";
91 (*case 2: refined to pbt without children *)
92 case Refine.refine_ori ori2 ["pbla", "refine", "test"] of
93 SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 2 broken";
95 (*case 3: refined to pbt with children *)
96 case Refine.refine_ori ori3 ["pbla", "refine", "test"] of
97 SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 3 broken";
99 (*case 4: refined to children (without child)*)
100 case Refine.refine_ori ori4 ["pbla", "refine", "test"] of
101 SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 4 broken";
103 (*case 5: start refinement somewhere in ptyps*)
104 case Refine.refine_ori ori4 ["pbla2", "pbla", "refine", "test"] of
105 SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 5 broken";
108 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
109 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
110 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
111 val fmz1 = ["fixedValues [aaa=0]", "errorBound (ddd=0)"];
112 val fmz2 = ["fixedValues [aaa=0]", "relations aaa333"];
113 val fmz3 = ["fixedValues [aaa=0]", "valuesFor [aaa222]"];
114 val fmz4 = ["fixedValues [aaa=0]", "valuesFor [aaa222]",
115 "boundVariable aaa222yyy"];
117 (*case 1: no refinement *)
118 case Refine.refine fmz1 ["pbla", "refine", "test"] of
119 [M_Match.Matches (["pbla", "refine", "test"], _),
120 M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
121 M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
122 M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
123 | _ => error "--- Refine.refine test-pbtyps --- broken with case 1";
126 *** pass ["pbla", "pbla1"]
127 *** pass ["pbla", "pbla2"]
128 *** pass ["pbla", "pbla3"]
133 Given=[Correct "fixedValues [aaa = #0]",
134 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
138 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
139 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
143 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
144 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
148 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
149 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
152 (*case 2: refined to pbt without children *)
153 case Refine.refine fmz2 ["pbla", "refine", "test"] of
154 [M_Match.Matches (["pbla", "refine", "test"], _),
155 M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
156 M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
157 M_Match.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
158 | _ => error "--- Refine.refine test-pbtyps --- broken with case 2";
161 *** pass ["pbla", "pbla1"]
162 *** pass ["pbla", "pbla2"]
163 *** pass ["pbla", "pbla3"]
168 Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
169 Relate=[],Where=[],With=[]}),
173 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
174 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
178 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
179 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
183 Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
184 Relate=[],Where=[],With=[]})] : match list*)
186 (*case 3: refined to pbt with children *)
187 case Refine.refine fmz3 ["pbla", "refine", "test"] of
188 [M_Match.Matches (["pbla", "refine", "test"], _),
189 M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
190 M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
191 M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
192 M_Match.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
193 M_Match.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
194 M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
195 | _ => error "--- Refine.refine test-pbtyps --- broken with case 3";
198 *** pass ["pbla", "pbla1"]
199 *** pass ["pbla", "pbla2"]
200 *** pass ["pbla", "pbla2", "pbla2x"]
201 *** pass ["pbla", "pbla2", "pbla2y"]
202 *** pass ["pbla", "pbla2", "pbla2z"]
203 *** pass ["pbla", "pbla3"]
208 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
209 Relate=[],Where=[],With=[]}),
213 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
214 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
218 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
219 Relate=[],Where=[],With=[]}),
221 (["pbla2x", "pbla2", "pbla"],
223 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
224 Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
226 (["pbla2y", "pbla2", "pbla"],
228 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
229 Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
231 (["pbla2z", "pbla2", "pbla"],
233 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
234 Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
238 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
239 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
242 (*case 4: refined to children (without child)*)
243 case Refine.refine fmz4 ["pbla", "refine", "test"] of
244 [M_Match.Matches (["pbla", "refine", "test"], _),
245 M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
246 M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
247 M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
248 M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
249 | _ => error "--- Refine.refine test-pbtyps --- broken with case 4";
252 *** pass ["pbla", "pbla1"]
253 *** pass ["pbla", "pbla2"]
254 *** pass ["pbla", "pbla2", "pbla2x"]
255 *** pass ["pbla", "pbla2", "pbla2y"]
260 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
261 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
265 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
266 Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
267 Relate=[],Where=[],With=[]}),
271 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
272 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
274 (["pbla2x", "pbla2", "pbla"],
276 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
277 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
278 Relate=[],Where=[],With=[]}),
280 (["pbla2y", "pbla2", "pbla"],
282 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
283 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
286 (*case 5: start refinement somewhere in ptyps*)
287 case Refine.refine fmz4 ["pbla2", "pbla", "refine", "test"] of
288 [M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
289 M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
290 M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
291 | _ => error "--- Refine.refine test-pbtyps --- broken with case 5";
293 *** pass ["pbla", "pbla2"]
294 *** pass ["pbla", "pbla2", "pbla2x"]
295 *** pass ["pbla", "pbla2", "pbla2y"]
300 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
301 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
303 (["pbla2x", "pbla2", "pbla"],
305 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
306 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
307 Relate=[],Where=[],With=[]}),
309 (["pbla2y", "pbla2", "pbla"],
311 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
312 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
316 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
317 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
318 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
320 By child of 2d962612dd0a this test case revealed an undetected failure
321 of Specify.find_next_step -- for_problem: these propose Tactic.Refine_Problem,
322 but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"]..
323 encounters "case Refine.problem ... of NONE".
324 The failure might be caused by inappropriate problem-hierarchy.
327 val fmz = ["equality ((x+1)*(x+2)=x \<up> 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 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];
332 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
333 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
334 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
336 (*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
337 val nxt = (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
338 (*=== specify a not-matching problem --- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)
340 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
343 case f of Test_Out.PpcKF (Test_Out.Problem [],
344 {Find = [Incompl "solutions []"], With = [],
345 Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"],
346 Where = [False www(*! ! ! ! ! !*)],
347 Relate = [],...}) => www(*! ! !*)
348 | _ => error "--- Refine_Problem broken 1";
349 if www = "matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8)"
350 then () else error "--- Refine_Problem broken 2";
352 val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
353 (Problem ["LINEAR", "univariate", "equation", "test"], <<<<<===== diff.to above WN120313
354 {Find=[Incompl "solutions []"],
355 Given=[Correct "equality ((x + #1) * (x + #2) = x \<up> #2 + #8)",
356 Correct "solveFor x"],Relate=[],
357 Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
358 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
359 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
360 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],
364 (*/------------------- step into me Add_Find "solutions L" ---------------------------------\*)
365 (*[], Pbl*)val (p''''',_,f''''',nxt''''',_,pt''''') = (me nxt p c pt);
366 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
368 (*+*)val Add_Find "solutions L" = tac;
371 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
372 case Step.by_tactic tac (pt, p) of
373 ("ok", (_, _, ptp)) => ptp
374 | ("unsafe-ok", (_, _, ptp)) => ptp
375 | ("not-applicable",_) => (pt, p)
376 | ("end-of-calculation", (_, _, ptp)) => ptp
377 | ("failure", _) => raise ERROR "sys-raise ERROR"
378 | _ => raise ERROR "me: uncovered case Step.by_tactic"
380 val ("helpless", ([(*\<Or> should contain tac \<Or>*)], [], _)) = (*case*)
381 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
382 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
383 (*if*) Pos.on_calc_end ip (*else*);
384 val (_, probl_id, _) = Calc.references (pt, p);
385 val _ = (*case*) tacis (*of*);
386 (*if*) probl_id = Problem.id_empty (*else*);
388 switch_specify_solve p_ (pt, ip) (*return from Step.do_next*);
389 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
390 (*if*) Pos.on_specification ([], state_pos) (*then*);
392 val ("failure", ([], [], _)) =
393 specify_do_next (pt, input_pos);
394 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
395 val (_, (p_', tac)) =
396 Specify.find_next_step ptp;
397 (*/------------------- step into find_next_step --------------------------------------------\*)
398 (*+ store for continuation after find_next_step*)val (p_'_'''''_', tac'''''_') = (p_', tac);
400 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
401 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
402 spec = refs, ...} = Calc.specify_data (pt, pos);
403 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
404 (*if*) p_ = Pos.Pbl (*then*);
406 val ("dummy", (Pbl, Refine_Problem ["sqroot-test", "univariate", "equation", "test"])) =
407 for_problem oris (o_refs, refs) (pbl, met);
408 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
409 (oris, (o_refs, refs), (pbl, met));
410 val cpI = if pI = Problem.id_empty then pI' else pI;
411 val cmI = if mI = MethodC.id_empty then mI' else mI;
412 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
413 val {ppc = mpc, ...} = MethodC.from_store cmI
414 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0;
415 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
416 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
417 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
419 item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
420 (*if*) not preok (*then*);
422 (*+*)Pre_Conds.to_string xxxxx = "[\n" ^
423 "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
424 "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
425 "matches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
426 "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8))]";
427 (*TermC.matches \<up> \<up> \<up> \<up> \<up> ^ NONE, ok: why then NONE = Refine.problem below?*)
428 (*-------------------- stop step into find_next_step ----------------------------------------*)
429 (*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_')
430 (*\------------------- step into find_next_step --------------------------------------------/*)
432 (*-------------------- contiue step into specify_do_next ------------------------------------*)
433 val ist_ctxt = Ctree.get_loc pt (p, p_)
434 val Refine_Problem ["sqroot-test", "univariate", "equation", "test"] =
436 val ("failure", ([(*\<Or> should contain tac \<Or>*)], [], _)) =
437 Step_Specify.by_tactic_input tac (pt, (p, p_'));
438 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Refine_Problem pI), (ptp as (pt, pos as (p,_)))) =
439 (tac, (pt, (p, p_')));
440 val (dI, dI', probl, ctxt) = case get_obj I pt p of
441 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
442 (dI, dI', probl, ctxt)
443 val thy = if dI' = ThyC.id_empty then dI else dI'
445 val NONE = (*case*) (*------------------------------- vvv*)
446 Refine.problem (ThyC.get_theory thy) pI probl (*of*);
447 "~~~~~ fun problem , args:"; val (thy, pblID, itms) = ((ThyC.get_theory thy), pI, probl);
448 (* val SOME (Refine.Match_ (["sqroot-test", "univariate", "equation", "test"], _)) =*)
449 val SOME (Refine.Match_ (rfd as (pI', _))) = (*case*)
450 Refine.refined_ ((Store.apply (get_ptyps ())) (Refine.refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) (*of*);
451 (*if*) pblID = pI' (*then*);
452 NONE (*return from problem*);
453 (*-------------------- stop step into -------------------------------------------------------*)
454 val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt''''');
455 (*\------------------- step into me Add_Find "solutions L" ---------------------------------/*)
457 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
458 val nxt = (Refine_Problem ["univariate", "equation", "test"]);
459 (*=== refine problem ----- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*)
460 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
461 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 (*nxt = ("Specify_Theory", Specify_Theory "Test")*)
464 val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 (*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
466 val (p,_,f,nxt,_,pt) = me nxt p c pt;
467 (*nxt = ("Apply_Method", *)
468 val (p,_,f,nxt,_,pt) = me nxt p c pt;
469 (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
470 val (p,_,f,nxt,_,pt) = me nxt p c pt;
471 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
472 val (p,_,f,nxt,_,pt) = me nxt p c pt;
473 (*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
475 val (p,_,f,nxt,_,pt) = me nxt p c pt;
476 (*nxt = Model_Problem ["LINEAR", "univariate", "equation", "test"]*)
477 val (p,_,f,nxt,_,pt) = me nxt p c pt;
478 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
479 val (p,_,f,nxt,_,pt) = me nxt p c pt;
481 val (p,_,f,nxt,_,pt) = me nxt p c pt;
482 val (p,_,f,nxt,_,pt) = me nxt p c pt;
483 val (p,_,f,nxt,_,pt) = me nxt p c pt;
484 (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"])*)
485 val (p,_,f,nxt,_,pt) = me nxt p c pt;
486 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
487 val nxt = (Refine_Problem ["univariate", "equation", "test"]);
488 val (p,_,f,nxt,_,pt) = me nxt p c pt;
489 (*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
490 val (p,_,f,nxt,_,pt) = me nxt p c pt;
491 (*val nxt = ("Specify_Method",Specify_Method ("Test", "solve_linear"))*)
492 val (p,_,f,nxt,_,pt) = me nxt p c pt;
493 (*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)
494 val (p,_,f,nxt,_,pt) = me nxt p c pt;
495 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
496 val (p,_,f,nxt,_,pt) = me nxt p c pt;
497 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
498 val (p,_,f,nxt,_,pt) = me nxt p c pt;
499 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "eq*)
500 val (p,_,f,nxt,_,pt) = me nxt p c pt;
501 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
502 val (p,_,f,nxt,_,pt) = me nxt p c pt;
503 (*Check_Postcond ["normalise", "univariate", "equation", "test"])*)
504 val (p,_,f,nxt,_,pt) = me nxt p c pt;
505 val Test_Out.FormKF res = f;
508 then case nxt of End_Proof' => ()
509 | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
510 else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"