(* Title:  100-init-rootpbl.sml

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/100-init-rootpbl.sml ---------------------";

"----------- Minisubplb/100-init-rootpbl.sml ---------------------";

"----------- Minisubplb/100-init-rootpbl.sml ---------------------";

val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

val (dI',pI',mI') =

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]);

"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];

"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);

val thy = assoc_thy dI

;mI = ["no_met"]; (*false*)

val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)

val {cas, ppc, thy=thy',...} = get_pbt pI

val dI = theory2theory' (maxthy thy thy');

val hdl =

  case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t

            | _ => error "Minisubplb/100-init-rootpbl.sml no headline"

val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))

				  (pors, (dI, pI, mI), hdl)

val pt = update_ctxt pt [] pctxt

;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

case nxt of ("Model_Problem", _) => ()

| _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";