separate struct. UnparseC, shift code to ThmC
1 (* Title: "Minisubpbl/200-start-method-NEXT_STEP.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
7 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
8 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
16 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
17 (*[], Pbl*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
19 (*/--------- step into Specify_Theory --------------------------------------------------------\*)
20 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));
21 val pIopt = Ctree.get_pblID (pt, ip);
22 (*if*) ip = ([], Pos.Res) (*else*);
23 val _ = (*case*) tacis (*of*);
24 val SOME _ = (*case*) pIopt (*of*);
26 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
27 switch_specify_solve p_ (pt, ip);
28 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
29 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
31 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
32 specify_do_next (pt, input_pos);
33 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
35 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
37 SpecifyNEW.find_next_step ptp;
38 "~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = ptp;
39 val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
40 case Ctree.get_obj I pt p of
41 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
42 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
43 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
44 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
45 val cpI = if pI = Celem.e_pblID then pI' else pI;
46 val cmI = if mI = Celem.e_metID then mI' else mI;
47 val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
49 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
51 (*+*) Rule_Set.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =
52 (*+*) ("dummy_ord", fn), rules = [], scr = EmptyScr, srls = Rule_Set.Empty}:
53 (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
54 (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
55 (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x' *)
56 ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
57 (*\--------- step into Specify_Theory --------------------------------------------------------/*)
59 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
60 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
61 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
62 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
63 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
64 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(* Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
65 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
66 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
67 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
68 (*[3], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
69 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
70 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
72 val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;
74 if p = ([3, 1], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term2str) = "x = 0 + -1 * -1"
75 then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()
76 | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"
77 else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"