(* 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_initialise' =(**)

Step_Specify.initialise' thy (model, refs);

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

Step_Specify.initialise 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 thy fmz;

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

(*+*)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.initialise' ---------------------*)

val ((pt, p), tacis) = return_initialise'(* 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 initialise' -------------------------------------//*)