neuper@41985
|
1 |
(* Title: 100-init-rootpbl.sml
|
neuper@41985
|
2 |
Author: Walther Neuper 1105
|
neuper@41985
|
3 |
(c) copyright due to lincense terms.
|
neuper@41985
|
4 |
*)
|
neuper@41985
|
5 |
|
neuper@42011
|
6 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
neuper@42011
|
7 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
neuper@42011
|
8 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
Walther@60576
|
9 |
val (_(*example text*),
|
Walther@60576
|
10 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60576
|
11 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60576
|
12 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60576
|
13 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60576
|
14 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60576
|
15 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60576
|
16 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60576
|
17 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60576
|
18 |
refs as ("Diff_App",
|
Walther@60576
|
19 |
["univariate_calculus", "Optimisation"],
|
Walther@60576
|
20 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60588
|
21 |
= Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60556
|
22 |
|
Walther@60576
|
23 |
Test_Code.init_calc @{context} [(model, refs)];
|
Walther@60576
|
24 |
"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
|
Walther@60576
|
25 |
= (@{context}, [(model, refs)]);
|
Walther@60651
|
26 |
(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
|
Walther@60651
|
27 |
( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
|
neuper@42011
|
28 |
|
Walther@60652
|
29 |
(**)val return_initialise' =(**)
|
Walther@60652
|
30 |
Step_Specify.initialise' thy (model, refs);
|
Walther@60652
|
31 |
"~~~~~ fun initialise' , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
|
wneuper@59426
|
32 |
|
Walther@60652
|
33 |
Step_Specify.initialise thy (model, refs);
|
Walther@60576
|
34 |
"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
|
Walther@60651
|
35 |
(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
|
Walther@60651
|
36 |
val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
|
Walther@60576
|
37 |
val (pI, (pors, pctxt), mI) =
|
Walther@60651
|
38 |
if mI = ["no_met"]
|
Walther@60651
|
39 |
then raise error "else not covered by test"
|
Walther@60651
|
40 |
else
|
Walther@60651
|
41 |
let
|
Walther@60668
|
42 |
(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
|
Walther@60668
|
43 |
(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE init ctxt*)
|
Walther@60651
|
44 |
(*old*) in (pI, (pors, pctxt), mI) end;
|
Walther@60653
|
45 |
( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
|
Walther@60651
|
46 |
in (pI, (pors, pctxt), mI) end;
|
wneuper@59426
|
47 |
|
Walther@60651
|
48 |
(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
|
Walther@60651
|
49 |
(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
|
Walther@60652
|
50 |
(*-------------------- stop step into Step_Specify.initialise' ---------------------*)
|
Walther@60651
|
51 |
|
Walther@60652
|
52 |
val ((pt, p), tacis) = return_initialise'(* kept for continuation *);
|
Walther@60576
|
53 |
"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
|
Walther@60651
|
54 |
= ((pt, p), tacis);
|
Walther@60576
|
55 |
val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
|
wneuper@59426
|
56 |
|
Walther@60576
|
57 |
Test_Code.TESTg_form ctxt (pt,p);
|
Walther@60576
|
58 |
"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
|
Walther@60576
|
59 |
val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
|
Walther@60586
|
60 |
val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
|
Walther@60576
|
61 |
(*case*) form (*of*);
|
Walther@60576
|
62 |
val Pos.Pbl =
|
Walther@60576
|
63 |
(*case*) p_ (*of*);
|
Walther@60576
|
64 |
Test_Out.Problem [];
|
Walther@60576
|
65 |
Test_Out.MethodC [];
|
wneuper@59426
|
66 |
|
Walther@60576
|
67 |
(*val return =*)
|
Walther@60576
|
68 |
Test_Out.PpcKF (Test_Out.Problem [],
|
Walther@60586
|
69 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
|
Walther@60586
|
70 |
"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
|
neuper@41986
|
71 |
|
Walther@60576
|
72 |
(*//------------------ inserted hidden code ------------------------------------------------\\*)
|
Walther@60578
|
73 |
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
|
74 |
| item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
|
Walther@60576
|
75 |
| item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
|
Walther@60578
|
76 |
| item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60578
|
77 |
| item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60578
|
78 |
| 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
|
79 |
| item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
|
Walther@60576
|
80 |
fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
|
Walther@60576
|
81 |
case sel of
|
Walther@60576
|
82 |
"#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
|
Walther@60576
|
83 |
| "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
|
Walther@60576
|
84 |
| "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
|
Walther@60576
|
85 |
| "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
|
Walther@60576
|
86 |
| "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
|
Walther@60576
|
87 |
| _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
|
Walther@60576
|
88 |
fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
|
Walther@60576
|
89 |
{Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
|
Walther@60675
|
90 |
fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term ctxt term)
|
Walther@60675
|
91 |
| boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term ctxt term);
|
Walther@60576
|
92 |
(*\\------------------ inserted hidden code ------------------------------------------------//*)
|
Walther@60576
|
93 |
|
Walther@60586
|
94 |
fun coll model [] = model
|
Walther@60586
|
95 |
| coll model ((_, _, _, field, itm_)::itms) =
|
Walther@60586
|
96 |
coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
|
Walther@60576
|
97 |
val gfr = coll P_Model.empty itms;
|
Walther@60576
|
98 |
|
Walther@60576
|
99 |
(*val return =*)
|
Walther@60586
|
100 |
add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
|
Walther@60576
|
101 |
"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
|
Walther@60576
|
102 |
= (gfr, (map
|
Walther@60586
|
103 |
(boolterm2item ctxt) where_));
|
Walther@60576
|
104 |
"~~~~~ fun boolterm2item , args:"; val () = ();
|
Walther@60652
|
105 |
(*\\------------------ step into initialise' -------------------------------------//*)
|