322 but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"].. |
322 but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"].. |
323 encounters "case Refine.problem ... of NONE". |
323 encounters "case Refine.problem ... of NONE". |
324 The failure might be caused by inappropriate problem-hierarchy. |
324 The failure might be caused by inappropriate problem-hierarchy. |
325 *) |
325 *) |
326 val c = []; |
326 val c = []; |
327 val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))", "solveFor x", |
327 val fmz = ["equality ((x+1)*(x+2)=x \<up> 2+(8::real))", "solveFor x", |
328 "errorBound (eps=0)", "solutions L"]; |
328 "errorBound (eps=0)", "solutions L"]; |
329 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"], |
329 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"], |
330 ["Test", "squ-equ-test-subpbl1"]); |
330 ["Test", "squ-equ-test-subpbl1"]); |
331 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
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; |
332 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; |
333 (*[], 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"*) |
334 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*) |
335 |
335 |
336 (*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*) |
336 (*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*) |
337 val nxt = (Specify_Problem ["LINEAR", "univariate", "equation", "test"]); |
337 val nxt = (Specify_Problem ["LINEAR", "univariate", "equation", "test"]); |
338 (*=== specify a not-matching problem ---^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
338 (*=== specify a not-matching problem --- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*) |
339 |
339 |
340 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*) |
340 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*) |
341 |
341 |
342 val www = |
342 val www = |
343 case f of Test_Out.PpcKF (Test_Out.Problem [], |
343 case f of Test_Out.PpcKF (Test_Out.Problem [], |
344 {Find = [Incompl "solutions []"], With = [], |
344 {Find = [Incompl "solutions []"], With = [], |
345 Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"], |
345 Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"], |
346 Where = [False www(*! ! ! ! ! !*)], |
346 Where = [False www(*! ! ! ! ! !*)], |
347 Relate = [],...}) => www(*! ! !*) |
347 Relate = [],...}) => www(*! ! !*) |
348 | _ => error "--- Refine_Problem broken 1"; |
348 | _ => error "--- Refine_Problem broken 1"; |
349 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)" |
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"; |
350 then () else error "--- Refine_Problem broken 2"; |
351 (*ML> f; |
351 (*ML> f; |
352 val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef, |
352 val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef, |
353 (Problem ["LINEAR", "univariate", "equation", "test"], <<<<<===== diff.to above WN120313 |
353 (Problem ["LINEAR", "univariate", "equation", "test"], <<<<<===== diff.to above WN120313 |
354 {Find=[Incompl "solutions []"], |
354 {Find=[Incompl "solutions []"], |
355 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
355 Given=[Correct "equality ((x + #1) * (x + #2) = x \<up> #2 + #8)", |
356 Correct "solveFor x"],Relate=[], |
356 Correct "solveFor x"],Relate=[], |
357 Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) |
357 Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8) |
358 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #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 ^^^ #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 ^^^ #2 + #8)"], |
360 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"], |
361 With=[]}))) : mout |
361 With=[]}))) : mout |
362 *) |
362 *) |
363 |
363 |
364 (*/------------------- step into me Add_Find "solutions L" ---------------------------------\*) |
364 (*/------------------- step into me Add_Find "solutions L" ---------------------------------\*) |
365 (*[], Pbl*)val (p''''',_,f''''',nxt''''',_,pt''''') = (me nxt p c pt); |
365 (*[], Pbl*)val (p''''',_,f''''',nxt''''',_,pt''''') = (me nxt p c pt); |
418 val NONE = (*case*) |
418 val NONE = (*case*) |
419 item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt 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*); |
420 (*if*) not preok (*then*); |
421 |
421 |
422 (*+*)Pre_Conds.to_string xxxxx = "[\n" ^ |
422 (*+*)Pre_Conds.to_string xxxxx = "[\n" ^ |
423 "(false, matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\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 ^^^ 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 ^^^ 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 ^^^ 2 + 8))]"; |
426 "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8))]"; |
427 (*TermC.matches ^^^^^^^^^^^^^^^^ NONE, ok: why then NONE = Refine.problem below?*) |
427 (*TermC.matches \<up> \<up> \<up> \<up> \<up> ^ NONE, ok: why then NONE = Refine.problem below?*) |
428 (*-------------------- stop step into find_next_step ----------------------------------------*) |
428 (*-------------------- stop step into find_next_step ----------------------------------------*) |
429 (*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_') |
429 (*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_') |
430 (*\------------------- step into find_next_step --------------------------------------------/*) |
430 (*\------------------- step into find_next_step --------------------------------------------/*) |
431 |
431 |
432 (*-------------------- contiue step into specify_do_next ------------------------------------*) |
432 (*-------------------- contiue step into specify_do_next ------------------------------------*) |
454 val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); |
454 val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); |
455 (*\------------------- step into me Add_Find "solutions L" ---------------------------------/*) |
455 (*\------------------- step into me Add_Find "solutions L" ---------------------------------/*) |
456 |
456 |
457 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*) |
457 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*) |
458 val nxt = (Refine_Problem ["univariate", "equation", "test"]); |
458 val nxt = (Refine_Problem ["univariate", "equation", "test"]); |
459 (*=== refine problem -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
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; |
460 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; |
461 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*) |
461 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*) |
462 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
462 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
463 (*nxt = ("Specify_Theory", Specify_Theory "Test")*) |
463 (*nxt = ("Specify_Theory", Specify_Theory "Test")*) |
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; |