1 (* Title: 100-init-rootpbl.sml |
1 (* Title: 100-init-rootpbl.sml |
2 Author: Walther Neuper 1105 |
2 Author: Walther Neuper 1105 |
3 (c) copyright due to lincense terms. |
3 (c) copyright due to lincense terms. |
4 *) |
4 *) |
5 |
5 |
|
6 "----------- Minisubplb/100-init-rootpbl.sml ---------------------"; |
|
7 "----------- Minisubplb/100-init-rootpbl.sml ---------------------"; |
|
8 "----------- Minisubplb/100-init-rootpbl.sml ---------------------"; |
6 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
7 val (dI',pI',mI') = |
10 val (dI',pI',mI') = |
8 ("Test", ["sqroot-test","univariate","equation","test"], |
11 ("Test", ["sqroot-test","univariate","equation","test"], |
9 ["Test","squ-equ-test-subpbl1"]); |
12 ["Test","squ-equ-test-subpbl1"]); |
|
13 *} |
|
14 ML {* |
|
15 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))]; |
|
16 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp); |
|
17 val thy = assoc_thy dI |
|
18 ;mI = ["no_met"]; (*false*) |
|
19 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI) |
|
20 val {cas, ppc, thy=thy',...} = get_pbt pI |
|
21 val dI = theory2theory' (maxthy thy thy'); |
|
22 val hdl = |
|
23 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t; |
|
24 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) |
|
25 (pors, (dI, pI, mI), hdl) |
|
26 val pt = update_ctxt pt [] pctxt |
|
27 ;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate; |
|
28 |
10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
29 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
11 case nxt of ("Model_Problem", _) => () |
30 case nxt of ("Model_Problem", _) => () |
12 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"; |
31 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"; |
13 |
32 |