(* 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;

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

 (*///----------------------------------------- save for final check ------------------------\\\*)

 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))];

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

     val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)

 (*ADD check*) 

 val PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} = get_obj I pt (fst p);

 (* ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt

    IN Minimsubpbl/150-add-given.sml IS CAUSED HEREBY:*)

 case oris of

   ((1, [1], "#Given", Const ("Descript.equality", _),

     [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()

 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"

 | _ => error ""

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

 	    val thy = Celem.assoc_thy dI;

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

 val xxx = Specify.get_pbt pI

 val yyy = #ppc xxx

 val (oris, ctxt) = Specify.prep_ori fmz thy yyy

 ;

 case oris of

   ((1, [1], "#Given", Const ("Descript.equality", _),

     [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()

 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"

 | _ => error ""

 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);

       val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;

 (*ADD check*) 

 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of

   SOME (Const ("Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $

     (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $

       Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => ()

 | SOME (Free ("equality", _) $

     (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $

       Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => error ""

 | _ => error "something is wrong with initialising Minisubpnl";

 val [(fmz, (dI',pI',mI'))] = [(fmz''''', spec''''')];

 (*\\\----------------------------------------- saved for final check -----------------------///*)

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

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

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