neuper@41985: (* Title:  100-init-rootpbl.sml
neuper@41985:    Author: Walther Neuper 1105
neuper@41985:    (c) copyright due to lincense terms.
neuper@41985: *)
neuper@41985: 
neuper@42011: "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
neuper@42011: "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
neuper@42011: "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
Walther@60576: val (_(*example text*), 
Walther@60576:   (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 
Walther@60576:      "Extremum (A = 2 * u * v - u \<up> 2)" :: 
Walther@60576:      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60576:      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60576:      "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: 
Walther@60576:      "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 
Walther@60576:      "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
Walther@60576:      "ErrorBound (\<epsilon> = (0::real))" :: []), 
Walther@60576:    refs as ("Diff_App", 
Walther@60576:      ["univariate_calculus", "Optimisation"],
Walther@60576:      ["Optimisation", "by_univariate_calculus"])))
Walther@60588:   = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
Walther@60556: 
Walther@60576:  Test_Code.init_calc @{context} [(model, refs)];
Walther@60576: "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
Walther@60576:   = (@{context}, [(model, refs)]);
Walther@60651: (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
Walther@60651: ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt  (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
neuper@42011: 
Walther@60651: (**)val return_nxt_specify_init_calc_PIDE =(**)
Walther@60651: Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
Walther@60576: "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
wneuper@59426: 
Walther@60651: Step_Specify.initialise_PIDE thy (model, refs);
Walther@60576: "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
Walther@60651: (*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
Walther@60651: 	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
Walther@60576: 	    val (pI, (pors, pctxt), mI) = 
Walther@60651:         if mI = ["no_met"] 
Walther@60651:         then raise error "else not covered by test"
Walther@60651:         else
Walther@60651:           let
Walther@60651: (*old* )     val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
Walther@60651: (*old*)     val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
Walther@60651: (*old*)   in (pI, (pors, pctxt), mI) end;
Walther@60651: ( *new*)     val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
Walther@60651:           in (pI, (pors, pctxt), mI) end;
wneuper@59426: 
Walther@60651: (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
Walther@60651: (*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
Walther@60576: (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
Walther@60651: 
Walther@60651: val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
Walther@60576: "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
Walther@60651:   = ((pt, p), tacis);
Walther@60576: 	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
wneuper@59426: 
Walther@60576:  Test_Code.TESTg_form ctxt (pt,p);
Walther@60576: "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
Walther@60576:     val (form, _, _) =  ME_Misc.pt_extract ctxt ptp;
Walther@60586: val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
Walther@60576:     (*case*) form (*of*);
Walther@60576: val Pos.Pbl =
Walther@60576:       (*case*) p_ (*of*);
Walther@60576:     Test_Out.Problem [];
Walther@60576:     Test_Out.MethodC [];
wneuper@59426: 
Walther@60576: (*val return =*)
Walther@60576:   Test_Out.PpcKF (Test_Out.Problem [], 
Walther@60586:    P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
Walther@60586: "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
neuper@41986: 
Walther@60576: (*//------------------ inserted hidden code ------------------------------------------------\\*)
Walther@60578: fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
Walther@60576:   | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
Walther@60576:   | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
Walther@60578:   | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))
Walther@60578:   | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy  (Input_Descript.join (d, ts)))
Walther@60578:   | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy  pid)
Walther@60576:   | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
Walther@60576: fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
Walther@60576:   case sel of
Walther@60576:     "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
Walther@60576:   | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
Walther@60576:   | "#Find"  => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
Walther@60576:   | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
Walther@60576:   | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
Walther@60576:   | _  => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
Walther@60576: fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
Walther@60576:   {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
Walther@60576: fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)
Walther@60576:   | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);
Walther@60576: (*\\------------------ inserted hidden code ------------------------------------------------//*)
Walther@60576: 
Walther@60586:     fun coll model [] = model
Walther@60586:       | coll model ((_, _, _, field, itm_)::itms) =
Walther@60586:         coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
Walther@60576:     val gfr = coll P_Model.empty itms;
Walther@60576: 
Walther@60576: (*val return =*)
Walther@60586:            add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
Walther@60576: "~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
Walther@60576:   = (gfr, (map 
Walther@60586:           (boolterm2item ctxt) where_));
Walther@60576: "~~~~~ fun boolterm2item , args:"; val () = ();
Walther@60576: (*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)