ML \<open>

 \<close> ML \<open>

 (* 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 (_(*example text*), 

   (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 

      "Extremum (A = 2 * u * v - u \<up> 2)" :: 

      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

      "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: 

      "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 

      "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

      "ErrorBound (\<epsilon> = (0::real))" :: []), 

    refs as ("Diff_App", 

      ["univariate_calculus", "Optimisation"],

      ["Optimisation", "by_univariate_calculus"])))

   = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

  Test_Code.init_calc @{context} [(model, refs)];

 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])

   = (@{context}, [(model, refs)]);

 (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global

 ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt  (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)

 (**)val return_nxt_specify_init_calc_PIDE =(**)

 Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);

 "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));

 Step_Specify.initialise_PIDE thy (model, refs);

 "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));

 (*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)

 	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)

 	    val (pI, (pors, pctxt), mI) = 

         if mI = ["no_met"] 

         then raise error "else not covered by test"

         else

           let

 (*old* )     val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)

 (*old*)     val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)

 (*old*)   in (pI, (pors, pctxt), mI) end;

 ( *new*)     val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;

           in (pI, (pors, pctxt), mI) end;

 (*/------------------- check result of O_Model.init_PIDE ------------------------------------\*)

 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";

 (*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";

 (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)

 val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);

 "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)

   = ((pt, p), tacis);

 	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;

  Test_Code.TESTg_form ctxt (pt,p);

 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));

     val (form, _, _) =  ME_Misc.pt_extract ctxt ptp;

 val Ctree.ModSpec (_, p_, _, gfr, where_, _) =

     (*case*) form (*of*);

 val Pos.Pbl =

       (*case*) p_ (*of*);

     Test_Out.Problem [];

     Test_Out.MethodC [];

 (*val return =*)

   Test_Out.PpcKF (Test_Out.Problem [], 

    P_Model.from (Proof_Context.theory_of ctxt) gfr where_);

 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);

 (*//------------------ inserted hidden code ------------------------------------------------\\*)

 fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))

   | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c

   | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c

   | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

   | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))

   | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy  pid)

   | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"

 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =

   case sel of

     "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}

   | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}

   | "#Find"  => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}

   | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}

   | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)

   | _  => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")

 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =

   {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}

 fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)

   | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);

 (*\\------------------ inserted hidden code ------------------------------------------------//*)

     fun coll model [] = model

       | coll model ((_, _, _, field, itm_)::itms) =

         coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;

     val gfr = coll P_Model.empty itms;

 (*val return =*)

            add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);

 "~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)

   = (gfr, (map 

           (boolterm2item ctxt) where_));

 "~~~~~ fun boolterm2item , args:"; val () = ();

 (*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>