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

 \<close> ML \<open>

 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 (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]

 \<close> ML \<open>

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

 \<close> ML \<open>

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

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

     val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global

     val ((pt''', p'''), tacis''') = (* keep for continuation *)

 Step_Specify.nxt_specify_init_calc ctxt (model, refs);

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

 Step_Specify.initialise ctxt (model, refs);

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

 	    val thy = ThyC.get_theory_PIDE ctxt dI

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

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

 	      if mI = ["no_met"] 

 	      then raise error "else not covered by test"

 	      else

 	        let

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

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

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

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

 "~~~~~ 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, pre, _) =

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

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

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

 fun item_from_feedback (_: theory) (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term (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 _ (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term (Input_Descript.join (d, ts)))

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

   | item_from_feedback _ (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term 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 ppc [] = ppc

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

         coll (add_sel_ppc thy field ppc (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)) pre);

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

   = (gfr, (map 

           (boolterm2item ctxt) pre));

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

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