test/Tools/isac/Minisubpbl/100-init-rootpbl.sml
branchdecompose-isar
changeset 42011 6a9ba30ab6bc
parent 41986 64efbbbed4b4
child 42012 e0144cf528e1
     1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 07:24:18 2011 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 08:12:51 2011 +0200
     1.3 @@ -3,10 +3,29 @@
     1.4     (c) copyright due to lincense terms.
     1.5  *)
     1.6  
     1.7 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     1.8 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     1.9 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
    1.10  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.11  val (dI',pI',mI') =
    1.12    ("Test", ["sqroot-test","univariate","equation","test"],
    1.13     ["Test","squ-equ-test-subpbl1"]);
    1.14 +*}
    1.15 +ML {*
    1.16 +"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
    1.17 +"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
    1.18 +val thy = assoc_thy dI
    1.19 +;mI = ["no_met"]; (*false*)
    1.20 +val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
    1.21 +val {cas, ppc, thy=thy',...} = get_pbt pI
    1.22 +val dI = theory2theory' (maxthy thy thy');
    1.23 +val hdl =
    1.24 +  case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
    1.25 +val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.26 +				  (pors, (dI, pI, mI), hdl)
    1.27 +val pt = update_ctxt pt [] pctxt
    1.28 +;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
    1.29 +
    1.30  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.31  case nxt of ("Model_Problem", _) => ()
    1.32  | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";