Walther@60578
|
1 |
(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
|
Walther@60578
|
2 |
Author: Walther Neuper 1105
|
Walther@60578
|
3 |
(c) copyright due to lincense terms.
|
Walther@60578
|
4 |
|
Walther@60659
|
5 |
Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
|
Walther@60578
|
6 |
in order not to get lost while working in Test_Some etc,
|
Walther@60578
|
7 |
re-introduce ML (*--- step into XXXXX ---*) and Co.
|
Walther@60578
|
8 |
and use Sidekick for orientation.
|
Walther@60659
|
9 |
Nesting is indicated by /--- //-- ///- at the left margin of the comments.
|
Walther@60578
|
10 |
*)
|
Walther@60578
|
11 |
|
Walther@60578
|
12 |
open Test_Code
|
Walther@60578
|
13 |
open Pos
|
Walther@60578
|
14 |
open Ctree
|
Walther@60578
|
15 |
open Tactic
|
Walther@60578
|
16 |
|
Walther@60578
|
17 |
val (_(*example text*),
|
Walther@60578
|
18 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60578
|
19 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60578
|
20 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60578
|
21 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60578
|
22 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60578
|
23 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60578
|
24 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60578
|
25 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60578
|
26 |
refs as ("Diff_App",
|
Walther@60578
|
27 |
["univariate_calculus", "Optimisation"],
|
Walther@60578
|
28 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60588
|
29 |
= Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60578
|
30 |
|
Walther@60578
|
31 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
|
Walther@60578
|
32 |
val c = [];
|
Walther@60578
|
33 |
|
Walther@60659
|
34 |
(*+*)val PblObj {ctxt, ...} = get_obj I pt [];
|
Walther@60659
|
35 |
(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
|
Walther@60659
|
36 |
(*val Free ("r", TFree ("'a", [])) = Syntax.read_term ctxt "r" ..ERROR until cs.b7a2ad3b3d45*)
|
Walther@60659
|
37 |
(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
|
Walther@60578
|
38 |
|
Walther@60659
|
39 |
val return_me_Model_Problem =
|
Walther@60659
|
40 |
me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
|
Walther@60659
|
41 |
(*/------------------- step into me Model_Problem ------------------------------------------\\*)
|
Walther@60578
|
42 |
"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
|
Walther@60578
|
43 |
val (pt, p) =
|
Walther@60578
|
44 |
(*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
|
Walther@60578
|
45 |
case Step.by_tactic tac (pt,p) of
|
Walther@60578
|
46 |
("ok", (_, _, ptp)) => ptp;
|
Walther@60578
|
47 |
|
Walther@60659
|
48 |
(*val ("ok", (ts as (_, _, _) :: _, _, _)) = (*case*)*)
|
Walther@60659
|
49 |
val return_do_next = (*case*)
|
Walther@60578
|
50 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60659
|
51 |
val ts = return_do_next |> #2 |> #1 |> hd (* keep for continuing me Model_Problem *)
|
Walther@60659
|
52 |
val continue_Model_Problem = (ts, (pt, p)) (* keep for continuing me Model_Problem *);
|
Walther@60578
|
53 |
(*//------------------ step into do_next ---------------------------------------------------\\*)
|
Walther@60578
|
54 |
"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
|
Walther@60578
|
55 |
(p, ((pt, e_pos'),[]));
|
Walther@60578
|
56 |
val pIopt = get_pblID (pt,ip);
|
Walther@60578
|
57 |
(*if*) ip = ([],Res); (* = false*)
|
Walther@60578
|
58 |
val _ = (*case*) tacis (*of*);
|
Walther@60578
|
59 |
val SOME _ = (*case*) pIopt (*of*);
|
Walther@60578
|
60 |
|
Walther@60578
|
61 |
val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
|
Walther@60578
|
62 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60578
|
63 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60578
|
64 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60578
|
65 |
|
Walther@60578
|
66 |
val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
|
Walther@60578
|
67 |
Step.specify_do_next (pt, input_pos);
|
Walther@60659
|
68 |
(*///----------------- step into specify_do_next -------------------------------------------\\*)
|
Walther@60578
|
69 |
"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
Walther@60578
|
70 |
|
Walther@60659
|
71 |
(* val (_, (p_', tac)) =*)
|
Walther@60659
|
72 |
val return_find_next_step = (*keep for continuing specify_do_next*)
|
Walther@60578
|
73 |
Specify.find_next_step ptp;
|
Walther@60659
|
74 |
(*////---------------- step into find_next_step --------------------------------------------\\*)
|
Walther@60578
|
75 |
"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
|
Walther@60578
|
76 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60578
|
77 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60578
|
78 |
val ctxt = Ctree.get_ctxt pt pos;
|
Walther@60578
|
79 |
(*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60578
|
80 |
(*if*) p_ = Pos.Pbl (*then*);
|
Walther@60578
|
81 |
|
Walther@60578
|
82 |
Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
|
Walther@60578
|
83 |
"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
|
Walther@60578
|
84 |
= (ctxt, oris, (o_refs, refs), (pbl, met));
|
Walther@60578
|
85 |
val cdI = if dI = ThyC.id_empty then dI' else dI;
|
Walther@60578
|
86 |
val cpI = if pI = Problem.id_empty then pI' else pI;
|
Walther@60578
|
87 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60585
|
88 |
val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
|
Walther@60586
|
89 |
val {model = mpc, ...} = MethodC.from_store ctxt cmI
|
Walther@60590
|
90 |
val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
|
Walther@60578
|
91 |
(*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
|
Walther@60578
|
92 |
(*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
|
Walther@60578
|
93 |
(*case*) find_first (I_Model.is_error o #5) pbl (*of*);
|
Walther@60578
|
94 |
|
Walther@60578
|
95 |
(*case*)
|
Walther@60578
|
96 |
Specify.item_to_add (ThyC.get_theory_PIDE ctxt
|
Walther@60578
|
97 |
(if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
|
Walther@60578
|
98 |
"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
|
Walther@60578
|
99 |
= ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
|
Walther@60578
|
100 |
fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
|
Walther@60578
|
101 |
fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
|
Walther@60578
|
102 |
fun test_id ids r = member op= ids (#1 (r : O_Model.single))
|
Walther@60578
|
103 |
fun test_subset itm (_, _, _, d, ts) =
|
Walther@60578
|
104 |
(I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
|
Walther@60578
|
105 |
fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
|
Walther@60578
|
106 |
| false_and_not_Sup (_, _, false, _, _) = true
|
Walther@60578
|
107 |
| false_and_not_Sup _ = false
|
Walther@60578
|
108 |
val v = if itms = [] then 1 else I_Model.max_variant itms
|
Walther@60578
|
109 |
val vors = if v = 0 then oris else filter (testr_vt v) oris
|
Walther@60578
|
110 |
val vits =
|
Walther@60578
|
111 |
if v = 0
|
Walther@60578
|
112 |
then itms (* because of dsc without dat *)
|
Walther@60578
|
113 |
else filter (testi_vt v) itms; (* itms..vat *)
|
Walther@60578
|
114 |
val icl = filter false_and_not_Sup vits; (* incomplete *)
|
Walther@60578
|
115 |
(*if*) icl = [] (*else*);
|
Walther@60578
|
116 |
val SOME ori =
|
Walther@60578
|
117 |
(*case*) find_first (test_subset (hd icl)) vors (*of*);
|
Walther@60659
|
118 |
(*\\\\---------------- step into find_next_step --------------------------------------------//*)
|
Walther@60659
|
119 |
(*|||----------------- continuing specify_do_next --------------------------------------------*)
|
Walther@60659
|
120 |
val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
|
Walther@60659
|
121 |
|
Walther@60659
|
122 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60659
|
123 |
(*+*)val Add_Given "Constants [r = 7]" = tac
|
Walther@60659
|
124 |
val _ =
|
Walther@60659
|
125 |
(*case*) tac (*of*);
|
Walther@60659
|
126 |
|
Walther@60659
|
127 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60659
|
128 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
|
Walther@60659
|
129 |
(tac, (pt, (p, p_')));
|
Walther@60659
|
130 |
|
Walther@60659
|
131 |
Specify.by_Add_ "#Given" ct ptp;
|
Walther@60659
|
132 |
"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
|
Walther@60659
|
133 |
("#Given", ct, ptp);
|
Walther@60659
|
134 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
|
Walther@60659
|
135 |
val (i_model, m_patt) =
|
Walther@60659
|
136 |
if p_ = Pos.Met then
|
Walther@60659
|
137 |
(met,
|
Walther@60659
|
138 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
Walther@60659
|
139 |
else
|
Walther@60659
|
140 |
(pbl,
|
Walther@60659
|
141 |
(if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
|
Walther@60659
|
142 |
(*case*)
|
Walther@60659
|
143 |
I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
|
Walther@60659
|
144 |
"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
|
Walther@60659
|
145 |
(ctxt, m_field, oris, i_model, m_patt, ct);
|
Walther@60659
|
146 |
(*new*) val (t as (descriptor $ _)) = Syntax.read_term ctxt str
|
Walther@60659
|
147 |
|
Walther@60675
|
148 |
(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
|
Walther@60659
|
149 |
|
Walther@60659
|
150 |
(*new*)val SOME m_field' =
|
Walther@60659
|
151 |
(*new*) (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
|
Walther@60659
|
152 |
(*new*) (*if*) m_field <> m_field' (*else*);
|
Walther@60659
|
153 |
|
Walther@60659
|
154 |
(*+*)val "#Given" = m_field; val "#Given" = m_field'
|
Walther@60659
|
155 |
|
Walther@60659
|
156 |
(*new*)val (msg, _, _) =
|
Walther@60659
|
157 |
(*new*) (*case*) O_Model.contains ctxt m_field o_model t (*of*);
|
Walther@60659
|
158 |
|
Walther@60659
|
159 |
(*+*)val (_, _, _, _, vals) = hd o_model;
|
Walther@60675
|
160 |
(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
|
Walther@60659
|
161 |
(*+*) if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
|
Walther@60659
|
162 |
(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
|
Walther@60659
|
163 |
(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
|
Walther@60659
|
164 |
(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
|
Walther@60659
|
165 |
(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
|
Walther@60659
|
166 |
(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
|
Walther@60659
|
167 |
(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
|
Walther@60659
|
168 |
(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
|
Walther@60659
|
169 |
(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
|
Walther@60659
|
170 |
(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
|
Walther@60659
|
171 |
(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
|
Walther@60659
|
172 |
(*+*) = O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
|
Walther@60578
|
173 |
(*\\------------------ step into into do_next ----------------------------------------------//*)
|
Walther@60578
|
174 |
|
Walther@60659
|
175 |
(*|------------------- continue with me Model_Problem ----------------------------------------*)
|
Walther@60659
|
176 |
val (ts, (pt, p)) = continue_Model_Problem;
|
Walther@60659
|
177 |
val ("ok", (ts as (_, _, _) :: _, _, _)) = return_do_next
|
Walther@60659
|
178 |
|
Walther@60578
|
179 |
val tacis as (_::_) =
|
Walther@60578
|
180 |
(*case*) ts (*of*);
|
Walther@60578
|
181 |
val (tac, _, _) = last_elem tacis
|
Walther@60578
|
182 |
|
Walther@60578
|
183 |
val return = (p, [] : NEW,
|
Walther@60578
|
184 |
TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
|
Walther@60578
|
185 |
"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
|
Walther@60578
|
186 |
val (form, _, _) = ME_Misc.pt_extract ctxt ptp
|
Walther@60586
|
187 |
val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
|
Walther@60578
|
188 |
(*case*) form (*of*);
|
Walther@60578
|
189 |
|
Walther@60578
|
190 |
(*+*)val Pos.Pbl = p_;
|
Walther@60578
|
191 |
Test_Out.PpcKF ( (Test_Out.Problem [],
|
Walther@60586
|
192 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
|
Walther@60578
|
193 |
|
Walther@60586
|
194 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
|
Walther@60586
|
195 |
"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
|
Walther@60586
|
196 |
fun coll model [] = model
|
Walther@60586
|
197 |
| coll model ((_, _, _, field, itm_) :: itms) =
|
Walther@60586
|
198 |
coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
|
Walther@60578
|
199 |
|
Walther@60578
|
200 |
val gfr = coll P_Model.empty itms;
|
Walther@60586
|
201 |
"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
|
Walther@60578
|
202 |
= (P_Model.empty, itms);
|
Walther@60578
|
203 |
|
Walther@60578
|
204 |
(*+*)val 4 = length itms;
|
Walther@60578
|
205 |
(*+*)val itm = nth 1 itms;
|
Walther@60578
|
206 |
|
Walther@60578
|
207 |
coll P_Model.empty [itm];
|
Walther@60586
|
208 |
"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
|
Walther@60578
|
209 |
= (P_Model.empty, [itm]);
|
Walther@60578
|
210 |
|
Walther@60586
|
211 |
(add_sel_ppc thy field model (item_from_feedback thy itm_));
|
Walther@60578
|
212 |
"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
|
Walther@60586
|
213 |
= (thy, field, model, (item_from_feedback thy itm_));
|
Walther@60578
|
214 |
|
Walther@60578
|
215 |
P_Model.item_from_feedback thy itm_;
|
Walther@60578
|
216 |
"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
|
Walther@60578
|
217 |
P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
|
Walther@60659
|
218 |
(*\------------------- step into into me Model_Problem -------------------------------------//*)
|
Walther@60659
|
219 |
val (p, _, f, nxt, _, pt) = return_me_Model_Problem
|
Walther@60578
|
220 |
|
Walther@60659
|
221 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Maximum A" = nxt;
|
Walther@60578
|
222 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
|
Walther@60578
|
223 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
|
Walther@60578
|
224 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
|
Walther@60578
|
225 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
|
Walther@60578
|
226 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;
|
Walther@60659
|
227 |
val return_me_Specify_Theory
|
Walther@60659
|
228 |
= me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
|
Walther@60578
|
229 |
|
Walther@60659
|
230 |
(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
|
Walther@60578
|
231 |
"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
|
Walther@60578
|
232 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60578
|
233 |
val (pt, p) =
|
Walther@60578
|
234 |
case Step.by_tactic tac (pt, p) of
|
Walther@60578
|
235 |
("ok", (_, _, ptp)) => ptp
|
Walther@60578
|
236 |
|
Walther@60578
|
237 |
val ("ok", (ts as (_, _, _) :: _, _, _)) =
|
Walther@60578
|
238 |
(*case*)
|
Walther@60578
|
239 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60578
|
240 |
(*//------------------ step into do_next ---------------------------------------------------\\*)
|
Walther@60578
|
241 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
Walther@60578
|
242 |
= (p, ((pt, Pos.e_pos'), [])) (*of*);
|
Walther@60578
|
243 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60578
|
244 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60578
|
245 |
val _ =
|
Walther@60578
|
246 |
(*case*) tacis (*of*);
|
Walther@60578
|
247 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60578
|
248 |
|
Walther@60578
|
249 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60578
|
250 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60578
|
251 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60578
|
252 |
|
Walther@60578
|
253 |
Step.specify_do_next (pt, input_pos);
|
Walther@60578
|
254 |
"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
|
Walther@60578
|
255 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60578
|
256 |
val ist_ctxt = Ctree.get_loc pt (p, p_);
|
Walther@60578
|
257 |
(*case*) tac (*of*);
|
Walther@60578
|
258 |
|
Walther@60578
|
259 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60578
|
260 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Problem pI), (pt, pos as (p, _)))
|
Walther@60578
|
261 |
= (tac, (pt, (p, p_')));
|
Walther@60578
|
262 |
val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
|
Walther@60578
|
263 |
PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
|
Walther@60578
|
264 |
(oris, dI, dI', pI', probl, ctxt)
|
Walther@60578
|
265 |
val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
|
Walther@60585
|
266 |
val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
|
Walther@60659
|
267 |
(*\\------------------ step into do_next ---------------------------------------------------//*)
|
Walther@60659
|
268 |
(*\------------------- step into me Specify_Theory -----------------------------------------//*)
|
Walther@60659
|
269 |
val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
|
Walther@60578
|
270 |
|
Walther@60659
|
271 |
val return_me_Specify_Problem (* keep for continuing me *)
|
Walther@60659
|
272 |
= me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
|
Walther@60659
|
273 |
(*/------------------- step into me Specify_Problem ----------------------------------------\\*)
|
Walther@60659
|
274 |
"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
|
Walther@60578
|
275 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60578
|
276 |
|
Walther@60659
|
277 |
(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
|
Walther@60659
|
278 |
(**) val return_by_tactic =(**) (*case*)
|
Walther@60578
|
279 |
Step.by_tactic tac (pt, p) (*of*);
|
Walther@60659
|
280 |
(*//------------------ step into by_tactic -------------------------------------------------\\*)
|
Walther@60578
|
281 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
Walther@60578
|
282 |
|
Walther@60578
|
283 |
(*case*)
|
Walther@60578
|
284 |
Step.check tac (pt, p) (*of*);
|
Walther@60578
|
285 |
"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
|
Walther@60578
|
286 |
(*if*) Tactic.for_specify tac (*then*);
|
Walther@60578
|
287 |
|
Walther@60578
|
288 |
Specify_Step.check tac (ctree, pos);
|
Walther@60578
|
289 |
"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
|
Walther@60578
|
290 |
= (tac, (ctree, pos));
|
Walther@60578
|
291 |
val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
|
Walther@60578
|
292 |
Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
|
Walther@60578
|
293 |
=> (oris, dI, pI, dI', pI', itms)
|
Walther@60578
|
294 |
val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
|
Walther@60659
|
295 |
(*\\------------------ step into by_tactic -------------------------------------------------//*)
|
Walther@60659
|
296 |
val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
|
Walther@60578
|
297 |
|
Walther@60578
|
298 |
(*case*)
|
Walther@60578
|
299 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60578
|
300 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
|
Walther@60578
|
301 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60578
|
302 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60578
|
303 |
val _ =
|
Walther@60578
|
304 |
(*case*) tacis (*of*);
|
Walther@60578
|
305 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60578
|
306 |
|
Walther@60578
|
307 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60578
|
308 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60578
|
309 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60578
|
310 |
|
Walther@60578
|
311 |
Step.specify_do_next (pt, input_pos);
|
Walther@60578
|
312 |
"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
|
Walther@60578
|
313 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60578
|
314 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60578
|
315 |
val _ =
|
Walther@60578
|
316 |
(*case*) tac (*of*);
|
Walther@60578
|
317 |
|
Walther@60578
|
318 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60578
|
319 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
|
Walther@60578
|
320 |
= (tac, (pt, (p, p_')));
|
Walther@60578
|
321 |
|
Walther@60578
|
322 |
val (o_model, ctxt, i_model) =
|
Walther@60578
|
323 |
Specify_Step.complete_for id (pt, pos);
|
Walther@60578
|
324 |
"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
|
Walther@60578
|
325 |
val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
|
Walther@60578
|
326 |
...} = Calc.specify_data (ctree, pos);
|
Walther@60578
|
327 |
val ctxt = Ctree.get_ctxt ctree pos
|
Walther@60578
|
328 |
val (dI, _, _) = References.select_input o_refs refs;
|
Walther@60586
|
329 |
val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
Walther@60578
|
330 |
val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
|
Walther@60578
|
331 |
val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
|
Walther@60578
|
332 |
val thy = ThyC.get_theory_PIDE ctxt dI
|
Walther@60590
|
333 |
val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
|
Walther@60659
|
334 |
(*\------------------- step into me Specify_Problem ----------------------------------------//*)
|
Walther@60659
|
335 |
val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
|
Walther@60578
|
336 |
|
Walther@60659
|
337 |
val return_me_Add_Given_FunctionVariable
|
Walther@60659
|
338 |
= me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
|
Walther@60659
|
339 |
(*/------------------- step into me Specify_Method -----------------------------------------\\*)
|
Walther@60659
|
340 |
"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
|
Walther@60578
|
341 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60578
|
342 |
val (pt, p) =
|
Walther@60578
|
343 |
(*Step.by_tactic is here for testing by me; do_next would suffice in me*)
|
Walther@60578
|
344 |
case Step.by_tactic tac (pt, p) of
|
Walther@60578
|
345 |
("ok", (_, _, ptp)) => ptp;
|
Walther@60578
|
346 |
|
Walther@60578
|
347 |
(*case*)
|
Walther@60578
|
348 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60578
|
349 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
|
Walther@60578
|
350 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60578
|
351 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60578
|
352 |
val _ =
|
Walther@60578
|
353 |
(*case*) tacis (*of*);
|
Walther@60578
|
354 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60578
|
355 |
|
Walther@60578
|
356 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60578
|
357 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60578
|
358 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60578
|
359 |
|
Walther@60578
|
360 |
Step.specify_do_next (pt, input_pos);
|
Walther@60578
|
361 |
"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
|
Walther@60578
|
362 |
|
Walther@60578
|
363 |
val (_, (p_', tac)) =
|
Walther@60578
|
364 |
Specify.find_next_step ptp;
|
Walther@60578
|
365 |
"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
|
Walther@60578
|
366 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60578
|
367 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60578
|
368 |
val ctxt = Ctree.get_ctxt pt pos;
|
Walther@60578
|
369 |
(*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60578
|
370 |
(*if*) p_ = Pos.Pbl (*else*);
|
Walther@60578
|
371 |
|
Walther@60578
|
372 |
Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
|
Walther@60578
|
373 |
"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
|
Walther@60578
|
374 |
= (ctxt, oris, (o_refs, refs), (pbl, met));
|
Walther@60578
|
375 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60586
|
376 |
val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
|
Walther@60590
|
377 |
val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
|
Walther@60578
|
378 |
val NONE =
|
Walther@60578
|
379 |
(*case*) find_first (I_Model.is_error o #5) met (*of*);
|
Walther@60578
|
380 |
|
Walther@60578
|
381 |
(*case*)
|
Walther@60578
|
382 |
Specify.item_to_add (ThyC.get_theory_PIDE ctxt
|
Walther@60578
|
383 |
(if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
|
Walther@60578
|
384 |
"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
|
Walther@60578
|
385 |
= ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
|
Walther@60659
|
386 |
(*\------------------- step into me Specify_Method -----------------------------------------//*)
|
Walther@60659
|
387 |
val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
|
Walther@60578
|
388 |
|
Walther@60659
|
389 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
|
Walther@60578
|
390 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
|
Walther@60578
|
391 |
(*
|
Walther@60578
|
392 |
nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,
|
Walther@60659
|
393 |
but the ***Program*** is not yet perfectly implemented.
|
Walther@60578
|
394 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
Walther@60578
|
395 |
*)
|