1 (* Title: 100-init-rootpbl.sml
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
7 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
8 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
9 val (_(*example text*),
10 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
11 "Extremum (A = 2 * u * v - u \<up> 2)" ::
12 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
13 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
14 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
15 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
16 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
17 "ErrorBound (\<epsilon> = (0::real))" :: []),
19 ["univariate_calculus", "Optimisation"],
20 ["Optimisation", "by_univariate_calculus"])))
21 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
23 Test_Code.init_calc @{context} [(model, refs)];
24 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
25 = (@{context}, [(model, refs)]);
26 (*old* )val ctxt = thy_id |> ThyC.get_theory ctxt |> Proof_Context.init_global
27 ( *new*)val thy = thy_id |> ThyC.get_theory ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
29 (**)val return_initialise' =(**)
30 Step_Specify.initialise' thy (model, refs);
31 "~~~~~ fun initialise' , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
33 Step_Specify.initialise thy (model, refs);
34 "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
35 (*old* )val thy = ThyC.get_theory ctxt dI( *old*)
36 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
37 val (pI, (pors, pctxt), mI) =
39 then raise error "else not covered by test"
42 (*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
43 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE init ctxt*)
44 (*old*) in (pI, (pors, pctxt), mI) end;
45 ( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
46 in (pI, (pors, pctxt), mI) end;
48 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
49 (*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
50 (*-------------------- stop step into Step_Specify.initialise' ---------------------*)
52 val ((pt, p), tacis) = return_initialise'(* kept for continuation *);
53 "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
55 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
57 Test_Code.TESTg_form ctxt (pt,p);
58 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
59 val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
60 val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
68 Test_Out.PpcKF (Test_Out.Problem [],
69 P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
70 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
72 (*//------------------ inserted hidden code ------------------------------------------------\\*)
73 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
75 "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
76 | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
77 | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
78 | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
79 | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
80 | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
81 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
82 {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
83 fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term ctxt term)
84 | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term ctxt term);
85 fun coll model [] = model
86 | coll model ((_, _, _, field, (feedb, _)) :: itms) =
87 coll (add_sel_ppc thy field model (item_from_feedback thy feedb)) itms;
88 (*\\------------------ inserted hidden code ------------------------------------------------//*)
90 val gfr = coll P_Model.empty itms;
93 add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
94 "~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
96 (boolterm2item ctxt) where_));
97 "~~~~~ fun boolterm2item , args:"; val () = ();
98 (*\\------------------ step into initialise' -------------------------------------//*)