1 (* Title: "Specify/i-model.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- survey on handling of input terms -------------------------------------------------";
10 "----------- investigate fun add_single in I_Model ---------------------------------------------";
11 "----------- build I_Model.init_POS -----------------------------------------------------------";
12 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
13 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
14 "----------- build I_Model.s_make_complete -----------------------------------------------------";
15 "----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
16 "----------- fun item_to_add: Maximum-exammple -------------------------------------------------";
17 "----------- fun item_to_add: Biegelinie-example -----------------------------------------------";
18 "-----------------------------------------------------------------------------------------------";
19 "-----------------------------------------------------------------------------------------------";
20 "-----------------------------------------------------------------------------------------------";
29 val ctxt = Proof_Context.init_global @{theory Biegelinie};
31 "----------- survey on handling of input terms -------------------------------------------------";
32 "----------- survey on handling of input terms -------------------------------------------------";
33 "----------- survey on handling of input terms -------------------------------------------------";
34 (*//------------------ survey on handling of input terms in specify-phase ------------------\\*)
35 (* * ---------- handling of lists -----------------------------------------------------*)
36 (* ** ---------- current situation ---------------------------------------------------*)
37 (** )(*---- from tests -------------------------------------------vvvvvvv *);
38 val o_single as (3, [1, 2, 3], "#Find", descr, [t1, t2]) = (nth 3 o_model)
39 val "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"])"
40 = O_Model.single_to_string ctxt o_single
41 val "[u]" = UnparseC.term ctxt t1
42 val "[v]" = UnparseC.term ctxt t2
44 val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}
45 val true = (*if*)Model_Def.is_list_descr descr(*else*);
47 val values = vals_term |> TermC.isalist2list |> map TermC.single_to_list
48 val feedb = Cor_POS (descr, values)
50 val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt
52 (*get values out of feedback:*)
53 val [Free ("u", _), Free ("v", _)] = (values |> map TermC.isalist2list |> flat): term list
55 (* ** ---------- wanted situation ----------------------------------------------------*)
56 val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}
57 val true = (*if*)Model_Def.is_list_descr descr(*else*);
59 val values = [vals_term]
60 val feedb = Cor_POS (descr, values)
62 val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
64 (*get values out of feedback:*)
65 val "[u, v]" = values |> map (UnparseC.term ctxt) |> hd
67 (* * ---------- handling of NON-lists -------------------------------------------------*)
68 (* ** ---------- current situation ---------------------------------------------------*)
69 (** )(*---- from tests -------------------------------------------vvvvvvv *);
70 val o_single as (2, [1, 2, 3], "#Find", Const ("Input_Descript.Maximum", _), [Free ("A", _)])
73 val t as (descr $ vals_term) = @{term "Maximum A"}
74 val false = (*if*)Model_Def.is_list_descr descr(*then*);
76 val values = [vals_term]
77 val feedb = Cor_POS (descr, values)
79 val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
81 (*get values out of feedback:*)
82 val "A" = values |> map (UnparseC.term ctxt) |> hd
84 (* ** ---------- wanted situation ----------------------------------------------------*)
85 val t as (descr $ vals_term) = @{term "Maximum A"}
86 val false = (*if*)Model_Def.is_list_descr descr(*then*);
88 val values = [vals_term]
89 val feedb = Cor_POS (descr, values)
91 val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
93 (*get values out of feedback:*)
94 val "A" = values |> map (UnparseC.term ctxt) |> hd;
95 (*\\------------------ survey on handling of input terms in specify-phase ------------------//*)
98 "----------- investigate fun add_single in I_Model -------------------------------------------";
99 "----------- investigate fun add_single in I_Model -------------------------------------------";
100 "----------- investigate fun add_single in I_Model -------------------------------------------";
101 val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
102 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
103 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
104 "AbleitungBiegelinie dy"];
105 val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
106 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
107 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
108 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)
110 (*[], Pbl*)val return_me_Add_Given =
111 me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
112 (*/------------------- step into me Add_Given ----------------------------------------------\\*)
113 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
115 val ("ok", (_, _, ptp)) = (*case*)
116 Step.by_tactic tac (pt, p) (*of*);
117 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
119 val Applicable.Yes tac' = (*case*)
120 Step.check tac (pt, p) (*of*);
121 (*if*) Tactic.for_specify' tac' (*then*);
123 Step_Specify.by_tactic tac' ptp;
124 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
126 val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)
127 Specify.by_Add_ "#Given" ct (pt, p);
128 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
129 ("#Given", ct, (pt, p));
130 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
131 val (i_model, m_patt) =
134 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
137 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
139 (*+*)if O_Model.to_string @{context} oris = "[\n" ^
140 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
141 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
142 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
143 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
144 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
145 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
146 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
147 (*+*)then () else error "INITIAL O_Model CHANGED";
148 (*+*)val "[\n(1, [1], true ,#Given, (Cor_POS Traegerlaenge L , pen2str, Position.T)), \n(2, [1], false ,#Given, (Inc_POS Streckenlast __, Position.T)), \n(3, [1], false ,#Find, (Inc_POS Biegelinie __, Position.T)), \n(4, [1], false ,#Relate, (Inc_POS Randbedingungen [] [__=__, __=__], Position.T))]"
149 = pbl |> I_Model.to_string_POS ctxt
151 val return_check_single = (*case*)
152 I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*);
153 (*//------------------ step into check_single ----------------------------------------------\\*)
154 "~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
155 = (ctxt, m_field, oris, (I_Model.TEST_to_OLD i_model), m_patt, ct);
156 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
157 handle ERROR msg => error (msg (*^ Position.here pp*))
160 (*case*) Model_Pattern.get_field descriptor m_patt;
162 (*if*) m_field <> m_field' (*else*);
163 val ("", ori', all) =(**)
164 (*case*) O_Model.contains ctxt m_field o_model t (*of*);
166 (*+*)O_Model.single_to_string @{context} ori';
167 (*+*)val [Free ("q_0", _)] = all;
169 (**)val ("", itm) =(**)
170 (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
172 (*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
173 (*\\------------------ step into check_single ----------------------------------------------//*)
174 val I_Model.Add i_single = return_check_single
176 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
178 val return_by_Add_ = ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
180 (*-------------------- stop into me Add_Given ------------------------------------------------*)
181 (*\------------------- step into me Add_Given ----------------------------------------------//*)
182 val (p,_,f,nxt,_,pt) = return_me_Add_Given;
184 (*ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real* )
185 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
187 (* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )
188 if p = ([], Pbl) then
189 case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _
190 => error "investigate fun add_single CHANGED 1"
191 else error "investigate fun add_single CHANGED 2"
192 ( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)
193 if p = ([], Pbl) then
194 case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _
195 => error "investigate fun add_single CHANGED 1"
196 else error "investigate fun add_single CHANGED 2"
197 ( *ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real*)
200 "----------- build I_Model.init_POS -----------------------------------------------------------";
201 "----------- build I_Model.init_POS -----------------------------------------------------------";
202 "----------- build I_Model.init_POS -----------------------------------------------------------";
203 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
205 (* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
206 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
208 val model_input = (*type Position.T is hidden, thus redefinition*)
209 [("#Given", [("Constants [r = 7]", Position.none)]),
210 ("#Where", [("0 < r", Position.none)]),
212 [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
214 [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
215 ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
216 : (Model_Pattern.m_field * (string * Position.T) list) list
217 val example_id = "Diff_App-No.123a";
218 (*----------------------------------------- init state -----------------------------------------*)
219 set_data CTbasic_POS.EmptyPtree @{theory Calculation};
220 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
222 val CTbasic_POS.EmptyPtree =
223 (*case*) the_data @{theory Calculation} (*of*);
226 "~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);
227 val example_id' = References_Def.explode_id example_id
228 val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
229 Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
230 val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id
231 val (o_model, ctxt) = O_Model.init thy model model_patt
233 (*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
234 (*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
238 I_Model.init_POS ctxt o_model model_patt;
239 "~~~~~ fun init_POS , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
241 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_POS Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
242 = I_Model.to_string_POS @{context} empty_i_model;
245 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
246 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
247 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
248 fun check str = if str = "true" then true else false
249 fun complete str = if str = "true" then true else false
251 val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]
253 val result_all_variants =
254 map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;
255 (*----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
257 val [NONE, NONE, NONE] = result_all_variants: int list option list
259 (*+*)val true = forall is_none result_all_variants
261 val variants_complete =
262 if forall is_none result_all_variants
264 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
266 val NONE = variants_complete: int list option
269 (*more significant result ..*)
270 val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list
272 in case the result is null, no I_Model is_complete,
273 in case the result contains more than 1 variant, this might determine the decision for MethodC.
275 val variants_complete =
276 if forall is_none result_all_variants
278 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
280 val SOME [11, 13] = variants_complete: int list option;
282 (*/----- reactivate with CS "remove sep_variants_envs"-----\* )
283 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
284 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
285 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
286 (*see Outer_Syntax: val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
289 (*//------------------ test data setup -----------------------------------------------------\\*)
291 *****************************************************************************************
292 ***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****
293 ***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists) *****
294 *****************************************************************************************
295 The ERROR occurred somewhere since introducing structure or since transition to PIDE.
296 *****************************************************************************************
297 We complete the two single_POS "1" and "5" below and replace them in empty_input;
298 we add "6" as variant of "5" to the empty input.
299 later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).
300 The test intermediatly pairs (feedback_POS, Position.T) in I_Model.T_POS
301 and leaves the rest as is.
303 I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,
304 I_Model.is_complete_POS NO instantiation (done in Template.show):
305 it serves to maintain the OLD test/*
307 val thy = @{theory Calculation}
311 CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
312 | _(*state (*FOR TEST*)*) => (**)the_data thy(**)
314 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
315 CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
317 probl: Model_Def.i_model_POS
318 (*[(1, [1, 2, 3], false, "#Given", (Inp_POS (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
319 (2, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
320 (3, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
321 (4, [1, 2, 3], false, "#Relate", (Inp_POS (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
322 (5, [1, 2], false, "#Relate", (Inp_POS (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
324 val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)
325 (1, [1,2,3], true, "#Given",
326 (Cor_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
327 (@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::
328 nth 2 probl :: nth 3 probl :: nth 4 probl ::
329 (5, [1,2], true, "#Relate",
330 (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
331 (@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::
332 (6, [3], true, "#Relate",
333 (Cor_POS ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),
334 (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
337 val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
338 Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")
340 val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $
341 Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD
342 (*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition
343 AND as "id" in Subst.T [("fixes", [0 < x])] *);
344 (model_patt |> Model_Pattern.to_string ctxt) =
345 "[\"(#Given, (Constants, fixes))\", " ^
346 "\"(#Find, (Maximum, maxx))\", " ^
347 "\"(#Find, (AdditionalValues, vals))\", " ^
348 "\"(#Relate, (Extremum, extr))\", " ^
349 "\"(#Relate, (SideConditions, sideconds))\"]";
350 val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})
351 (*\\------------------ test data setup -----------------------------------------------------//*)
353 (*/------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------\*)
354 (*\------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------/*)
355 ( *\----- reactivate with CS "remove sep_variants_envs"-----/*)
358 "----------- build I_Model.s_make_complete -----------------------------------------------------";
359 "----------- build I_Model.s_make_complete -----------------------------------------------------";
360 "----------- build I_Model.s_make_complete -----------------------------------------------------";
361 val (_(*example text*),
362 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
363 "Extremum (A = 2 * u * v - u \<up> 2)" ::
364 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
365 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
366 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
367 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
368 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
369 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
370 "ErrorBound (\<epsilon> = (0::real))" :: []),
372 ["univariate_calculus", "Optimisation"],
373 ["Optimisation", "by_univariate_calculus"])))
374 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
377 val (p,_,f,nxt,_,pt) =
378 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
379 val (p,_,f,nxt,_,pt) = me nxt p c pt;
381 (*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
382 val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
383 PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
384 => (o_model, (pbl_imod, met_imod), (pI, mI))
385 | _ => raise ERROR ""
387 val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
388 (1, [1, 2, 3], true, "#undef", (Cor_POS (@{term Constants},
389 [@{term "[r = (7::real)]"}]), Position.none)),
390 (1, [1, 2], true, "#undef", (Cor_POS (@{term SideConditions},
391 [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
393 val met_imod = [ (*1 item for creating code*)
394 (8, [2], true, "#undef", (Cor_POS (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
396 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
397 (*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
398 (*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
399 (*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
400 (*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
401 (*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
402 (*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
403 (*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
404 (*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
405 (*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
406 (*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
407 (*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
408 (*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
409 then () else error "setup test data for I_Model.s_make_complete CHANGED";
410 (*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
412 val return_s_make_complete =
413 s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
414 (*/------------------- step into s_make_complete -------------------------------------------\\*)
415 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
416 (o_model, (pbl_imod, met_imod), (pI, mI));
417 val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
418 val {model = met_patt, ...} = MethodC.from_store ctxt mI;
419 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
420 val i_from_pbl = map (fn (_, (descr, _)) =>
421 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
423 (*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
424 "~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
425 (@{term Constants}, pbl_max_vnts, pbl_imod);
426 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false
427 | SOME descr' => if descr = descr' then true else false) i_model
429 (*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_POS
431 val return_get_descr_vnt_1 =
432 case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
433 [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))
434 | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
435 (*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
437 (*|------------------- continue s_make_complete ----------------------------------------------*)
438 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
439 if is_empty_single_POS i_single
441 case get_descr_vnt' feedb pbl_max_vnts o_model of
442 (*-----------^^^^^^^^^^^^^^-----------------------------*)
443 [] => raise ERROR (msg pbl_max_vnts feedb)
444 | o_singles => map transfer_terms o_singles
445 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
447 (*+*)val [2, 1] = vnts;
448 (*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\n" ^
449 "(1, [1, 2, 3], true ,#undef, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
450 "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
451 "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
452 "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
453 "(1, [1, 2], true ,#undef, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
454 then () else error "pbl_from_o_model CHANGED 1"
456 (*//------------------ step into map ((fn i_single -----------------------------------------\\*)
457 "~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
458 (*if*) is_empty_single_POS i_single (*else*);
459 get_descr_vnt' feedb pbl_max_vnts o_model;
461 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
462 if is_empty_single_POS i_single
464 case get_descr_vnt' feedb pbl_max_vnts o_model of
465 (*---------- ^^^^^^^^^^^^^^ ----------------------------*)
466 [] => raise ERROR (msg pbl_max_vnts feedb)
467 | o_singles => map transfer_terms o_singles
468 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
469 (*\\------------------ step into map ((fn i_single -----------------------------------------//*)
471 (*|------------------- continue s_make_complete ----------------------------------------------*)
472 val i_from_met = map (fn (_, (descr, _)) =>
473 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
475 (*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^
476 "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
477 "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
478 "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
479 "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T)), \n" ^
480 "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^
481 (*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
482 "(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n" ^
483 "(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n" ^
484 "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"
485 (*+*)then () else error "s_make_complete: from_met CHANGED";
487 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
488 (*+*)val [2] = met_max_vnts
490 val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
491 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
492 if is_empty_single_POS i_single
494 case get_descr_vnt' feedb [met_max_vnt] o_model of
495 [] => raise ERROR (msg [met_max_vnt] feedb)
496 | o_singles => map transfer_terms o_singles
497 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
499 (*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
500 "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
501 "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
502 "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
503 "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
504 "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^
505 "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
506 "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
507 "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
508 (*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
510 val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
511 (*\------------------- step into s_make_complete -------------------------------------------//*)
513 if return_s_make_complete = return_s_make_complete_step
514 then () else error "s_make_complete: stewise construction <> value of fun"
517 "----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
518 "----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
519 "----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
520 val (_(*example text*),
521 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
522 "Extremum (A = 2 * u * v - u \<up> 2)" ::
523 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
524 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
525 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
526 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
527 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
528 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
529 "ErrorBound (\<epsilon> = (0::real))" :: []),
531 ["univariate_calculus", "Optimisation"],
532 ["Optimisation", "by_univariate_calculus"])))
533 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
536 val (p,_,f,nxt,_,pt) =
537 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;
540 (*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
541 val (o_model, (pI, mI)) = case get_obj I pt (fst p) of
542 PblObj {origin = (o_model, (_, pI, mI), _), ...}
543 => (o_model, (pI, mI))
544 | _ => raise ERROR ""
549 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
550 (*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
551 (*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
552 (*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
553 (*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
554 (*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
555 (*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
556 (*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
557 (*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
558 (*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
559 (*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
560 (*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
561 (*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
562 then () else error "setup test data for I_Model.s_make_complete CHANGED";
563 (*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
565 val return_s_make_complete =
566 s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
567 (*/------------------- step into s_make_complete -------------------------------------------\\*)
568 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
569 (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
570 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
572 val i_from_pbl = map (fn (_, (descr, _)) =>
573 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
574 (*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
575 "~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
576 (@{term Constants}, pbl_max_vnts, pbl_imod);
577 val equal_descr(*for (*+*)filter (fn (_, vnts',..*): I_Model.T_POS =
578 filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false
579 | SOME descr' => if descr = descr' then true else false) i_model
581 (*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) (equal_descr: I_Model.T_POS)
584 val return_get_descr_vnt_1 =
585 case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
586 [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))
587 | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
588 (*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
590 (*+*)if return_get_descr_vnt_1 = nth 1 i_from_pbl
591 (*+*)then () else error "return_get_descr_vnt_1 <> nth 1 i_from_pbl";
592 (*+*)if (i_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
593 "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
594 "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
595 "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T)), \n" ^
596 "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
597 "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T))]"
598 (*+*)then () else error "I_Model.s_make_complete > i_from_pbl CHANGED";
600 (*|------------------- continue s_make_complete ----------------------------------------------*)
601 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
602 if is_empty_single_POS i_single
604 case get_descr_vnt' feedb pbl_max_vnts o_model of
605 (*-----------^^^^^^^^^^^^^^-----------------------------*)
606 [] => raise ERROR (msg pbl_max_vnts feedb)
607 | o_singles => map transfer_terms o_singles
608 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
610 (*+*)val [1, 2, 3] = vnts;
611 (*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\n" ^
612 "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
613 "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
614 "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
615 "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
616 "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
617 "(6, [3], true ,#Relate, (Cor_POS SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"
618 then () else error "pbl_from_o_model CHANGED 2"
620 (*//------------------ step into map ((fn i_single -----------------------------------------\\*)
621 "~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =
623 (*if*) is_empty_single_POS i_single (*then*);
624 (*case*) get_descr_vnt' feedb pbl_max_vnts o_model;
626 (*+*)val (0, [], false, "i_model_empty", (Sup_POS (Const ("Input_Descript.Constants", _), []), _))
628 (*+*)val true = is_empty_single_POS i_single
630 val return_get_descr_vnt'= (*case*)
631 get_descr_vnt' feedb pbl_max_vnts o_model (*of*);
632 (*\\------------------ step into map ((fn i_single -----------------------------------------//*)
634 (*|------------------- continue s_make_complete ----------------------------------------------*)
635 val i_from_met = map (fn (_, (descr, _)) =>
636 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
638 (*+*)val [1, 2, 3] = pbl_max_vnts (*..? ? GOON*);
639 (*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^
640 "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
641 "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
642 "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
643 "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T)), \n" ^
644 "(0, [], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n" ^
645 "(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n" ^
646 "(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n" ^
647 "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"
648 (*+*)then () else error "s_make_complete: i_from_met CHANGED";
650 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
651 (*+*)val [1, 2, 3]: variant list = met_max_vnts
653 val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
654 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
655 if is_empty_single_POS i_single
657 case get_descr_vnt' feedb [max_vnt] o_model of
658 [] => raise ERROR (msg [max_vnt] feedb)
659 | o_singles => map transfer_terms o_singles
660 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
662 (*+*)val 1 = max_vnt;
663 (*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
664 "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
665 "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
666 "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
667 "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
668 "(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n" ^
669 "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
670 "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
671 "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
672 (*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
674 val return_s_make_complete_step as (pbl_imod_step, met_imod_step)=
675 (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
677 (*\------------------- step into s_make_complete -------------------------------------------//*)
678 if return_s_make_complete = return_s_make_complete_step
679 then () else error "s_make_complete: stewise construction <> value of fun"
681 (* final test ... ----------------------------------------------------------------------------*)
682 val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
683 = pbl_imod_step |> I_Model.to_string_POS @{context}
684 val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
685 = met_imod_step |> I_Model.to_string_POS @{context};
689 (*** fun item_to_add: Maximum-example ====================================================== ***);
690 "----------- fun item_to_add: Maximum-example --------------------------------------------------";
691 "----------- fun item_to_add: Maximum-example --------------------------------------------------";
692 (*//------------------ setup test data for item_to_add Maximum-exammple --------------------\\*)
695 (1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n
696 (2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n
697 (3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n
698 (4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n
699 (5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n
700 (7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n
701 (10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n
702 (12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
703 = o_model |> O_Model.to_string ctxt
705 val true = o_model_test = o_model
707 val ctxt = @{context}
710 (1, [1, 2, 3], "#Given", @{term Constants}, [@{term "[r = (7::real)]"}]),
711 (2, [1, 2, 3], "#Find", @{term Maximum}, [@{term "A::real"} ]),
712 (3, [1, 2, 3], "#Find", @{term AdditionalValues}, [@{term "[u::real]"}, @{term "[v::real]"}]),
713 (4, [1, 2, 3], "#Relate", @{term Extremum}, [@{term "A = 2 * u * v - u \<up> 2"}]),
714 (5, [1, 2], "#Relate", @{term SideConditions}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
715 (7, [1], "#undef", @{term FunctionVariable}, [@{term "a::real"}]),
716 (10,[1, 2], "#undef", @{term Domain}, [@{term "{0<..<(r::real)}"}]),
717 (12,[1, 2, 3], "#undef", @{term ErrorBound}, [@{term "\<epsilon> = (0::real)"}]),
718 (0, [1], "#Find", @{term solutions}, [@{term "L::real list"}])
720 (*\\------------------ setup test data for item_to_add Maximum-exammple --------------------//*)
722 (** fun item_to_add: Constants [r = (7::real)] ============================================== **);
723 val i_single : I_Model.single_POS =
724 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Constants}, []) , Position.none)))
725 val SOME ("#Given", "Constants [r = 7]") = item_to_add ctxt o_model_test [i_single];
727 (** fun item_to_add: Maximum A ============================================================== **);
728 val i_single : I_Model.single_POS =
729 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Maximum}, []) , Position.none)))
730 val SOME ("#Find", "Maximum A") = item_to_add ctxt o_model_test [i_single];
732 (** fun item_to_add: AdditionalValues [u] =================================================== **);
733 val i_single : I_Model.single_POS =
734 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, []) , Position.none)))
735 val SOME ("#Find", "AdditionalValues [u]") = item_to_add ctxt o_model_test [i_single];
737 (** fun item_to_add: AdditionalValues [u, v] ================================================ **);
738 val i_single : I_Model.single_POS =
739 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[u::real]"}]) , Position.none)))
740 (**)val SOME ("#Find", "AdditionalValues [u, v]") = item_to_add ctxt o_model_test [i_single];
742 (** fun item_to_add: AdditionalValues [v, u] ================================================ **);
743 (*/------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------\\*)
744 val i_single : I_Model.single_POS =
745 (*present [v, u] (reverse order), because second element has been input first ------vvvvvvvvvv*)
746 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[v::real]"}]) , Position.none)))
748 (**)val return_item_to_add as SOME ("#Find", "AdditionalValues [v, u]") = (**)
749 (** )val calling_code as SOME ("#Find", "AdditionalValues [v, u]") =( **)
750 item_to_add ctxt o_model_test [i_single];
751 (*//------------------ step into item_to_add -----------------------------------------------\\*)
752 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, o_model_test, [i_single]);
753 val max_vnt as 1 = last_elem (*this decides, for which variant initially help is given*)
754 (Model_Def.max_variants o_model i_model)
755 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
756 val i_to_select = i_model
757 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
760 (*+*)val "[\n(3, [1, 2, 3], false ,from o_model, (Inc_POS AdditionalValues [v] , pen2str, Position.T))]"
761 = i_to_select |> I_Model.to_string_POS ctxt
762 (*+*)val [(_, _, _, _, (Inc_POS (_, [Const ("List.list.Cons", _) $ Free ("v", _) $ _]), _))]
766 (*if*) i_to_select = []
768 (** )val return_item_to_add =( **)
769 (**)val return_fill_from_o as
770 SOME (_, _, _, _, (Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx), _)) =(**)
771 (*I_Model.*)fill_from_o o_vnts (hd i_to_select) (*of*);
772 (*///----------------- step into fill_from_o -----------------------------------------------\\*)
773 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =
774 (o_vnts, (hd i_to_select));
775 val (m_field, all_value) =
776 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
777 SOME (_, _, m_field, _, ts) => (m_field, ts)
778 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
779 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
780 (*+*)val "[[u], [v]]" = all_value |> UnparseC.terms ctxt
783 (*if*) Model_Def.is_list_descr descr
784 val already_input as [Const ("List.list.Cons", _) $ Free ("v", _) $ _] = feedb |> feedb_values
786 val miss = subtract op= already_input all_value
787 (*+*)val "[[u]]" = miss |> UnparseC.terms ctxt
789 val ts = already_input @ [hd miss]
790 val "[[v], [u]]" = ts |> UnparseC.terms ctxt
793 (*if*) length all_value = length ts
794 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_POS (descr, [values_to_present ts]), pos))
795 (*\\\----------------- step into fill_from_o -----------------------------------------------//*)
796 val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o
797 (*+*)val Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx) = feedb;
798 (*+*)val xxx = xxx |> UnparseC.terms ctxt;
800 (*||------------------ contiue.. item_to_add -------------------------------------------------*)
801 (** )val return_item_to_add = ( **)
802 SOME (m_field, feedb |>
803 (*I_Model.*)feedb_args_to_string ctxt);
804 (*///----------------- step into feedb_args_to_string --------------------------------------\\*)
805 "~~~~~ fun feedb_args_to_string , args:"; val (ctxt, Cor_POS (descr, values)) = (ctxt, feedb);
806 (** )val return_feedb_args_to_string =( **)
807 val return_feedb_args_to_string_STEP =
808 UnparseC.term ctxt (descr $ values_to_present values);
809 (*\\\----------------- step into feedb_args_to_string --------------------------------------//*)
810 (*\\------------------ step into item_to_add -----------------------------------------------//*)
811 val calling_code as SOME ("#Find", "AdditionalValues [v, u]") = return_item_to_add;
812 (*\------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------//*)
815 (** fun item_to_add: Constants Extremum (A = 2 * u * v - u \<up> 2) ============================= **);
816 val i_single : I_Model.single_POS =
817 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Extremum}, []) , Position.none)))
818 val SOME ("#Relate", "Extremum (A = 2 * u * v - u \<up> 2)")
819 = item_to_add ctxt o_model_test [i_single];
821 (** fun item_to_add: Constants SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ============ **);
822 val i_single : I_Model.single_POS =
823 ((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term SideConditions}, []) , Position.none)))
824 val SOME ("#Relate", "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]")
825 = item_to_add ctxt o_model_test [i_single];
827 (** fun item_to_add: Solutions L ============================================================ **);
828 val i_single : I_Model.single_POS =
829 (3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term solutions}, []) , Position.none))
830 val SOME ("#Find", "solutions L") = item_to_add ctxt o_model_test [i_single];
833 (*** fun item_to_add Biegelinie-exammple =================================================== ***);
834 "----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";
835 "----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";
837 (** fun item_to_add: solveForVars [c] ======================================================= **);
838 val (descr $ t) = @{term "solveForVars [c, c_2, c_3, c_4]"}
839 val [Const ("List.list.Cons", _) $ Free ("c", _) $ Const ("List.list.Nil", _),
840 Const ("List.list.Cons", _) $ Free ("c_2", _) $ Const ("List.list.Nil", _),
841 Const ("List.list.Cons", _) $ Free ("c_3", _) $ Const ("List.list.Nil", _),
842 Const ("List.list.Cons", _) $ Free ("c_4", _) $ Const ("List.list.Nil", _)]
843 = make_values (descr, t)
845 val o_model_test : O_Model.T = [(0, [1], "#Given", descr, make_values (descr, t))]
846 val i_model_test : I_Model.T_POS = [
847 (0, [1], false, "get-from-o_model", (Inc_POS (descr, []) , Position.none))]
848 val SOME ("#Given", "solveForVars [c]") = item_to_add ctxt o_model_test i_model_test;
850 (** fun item_to_add: solveForVars [c, c_2] ================================================== **);
851 val i_model_test : I_Model.T_POS = [
852 (0, [1], false, "get-from-o_model", (Inc_POS (descr,
853 [nth 1 (make_values (descr, t))]) , Position.none))]
854 val SOME ("#Given", "solveForVars [c, c_2]") = item_to_add ctxt o_model_test i_model_test;
856 (** fun item_to_add: solveForVars [c, c_2, c_3] ============================================= **);
857 val i_model_test : I_Model.T_POS = [
858 (0, [1], false, "get-from-o_model", (Inc_POS (descr,
859 (nth 1 (make_values (descr, t))) :: (nth 2 (make_values (descr, t))) :: []) , Position.none))]
860 val SOME ("#Given", "solveForVars [c, c_2, c_3]") = item_to_add ctxt o_model_test i_model_test;