test/Tools/isac/Minisubpbl/100-init-rootpbl.sml
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279 255c853ea2f0
parent 42013 e9ef067fcf2a
child 59426 c7b52bf9c8ae
permissions -rw-r--r--
renamed Ctree.ptree --> Ctree.ctree
     1 (* Title:  100-init-rootpbl.sml
     2    Author: Walther Neuper 1105
     3    (c) copyright due to lincense terms.
     4 *)
     5 
     6 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     7 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     8 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    10 val (dI',pI',mI') =
    11   ("Test", ["sqroot-test","univariate","equation","test"],
    12    ["Test","squ-equ-test-subpbl1"]);
    13 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
    14 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
    15 val thy = assoc_thy dI
    16 ;mI = ["no_met"]; (*false*)
    17 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
    18 val {cas, ppc, thy=thy',...} = get_pbt pI
    19 val dI = theory2theory' (maxthy thy thy');
    20 val hdl =
    21   case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
    22             | _ => error "Minisubplb/100-init-rootpbl.sml no headline"
    23 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    24 				  (pors, (dI, pI, mI), hdl)
    25 val pt = update_ctxt pt [] pctxt
    26 ;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
    27 
    28 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    29 case nxt of ("Model_Problem", _) => ()
    30 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
    31