1 (* Title: "Specify/i-model.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- investigate fun add_single in I_Model ---------------------------------------------";
10 "----------- build I_Model.init_TEST -----------------------------------------------------------";
11 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
12 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
13 "----------- build I_Model.s_make_complete -----------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
23 "----------- investigate fun add_single in I_Model -------------------------------------------";
24 "----------- investigate fun add_single in I_Model -------------------------------------------";
25 "----------- investigate fun add_single in I_Model -------------------------------------------";
26 val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
27 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
28 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
29 "AbleitungBiegelinie dy"];
30 val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
31 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
32 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
33 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)
35 (*[], Pbl*)val return_me_Add_Given =
36 me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
37 (*/------------------- step into me Add_Given ----------------------------------------------\\*)
38 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
40 val ("ok", (_, _, ptp)) = (*case*)
41 Step.by_tactic tac (pt, p) (*of*);
42 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
44 val Applicable.Yes tac' = (*case*)
45 Step.check tac (pt, p) (*of*);
46 (*if*) Tactic.for_specify' tac' (*then*);
48 Step_Specify.by_tactic tac' ptp;
49 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
51 val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)
52 Specify.by_Add_ "#Given" ct (pt, p);
53 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
54 ("#Given", ct, (pt, p));
55 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
56 val (i_model, m_patt) =
59 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
62 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
64 (*+*)if O_Model.to_string @{context} oris = "[\n" ^
65 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
66 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
67 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
68 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
69 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
70 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
71 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
72 (*+*)then () else error "INITIAL O_Model CHANGED";
73 (*+*)if I_Model.to_string ctxt pbl = "[\n" ^
74 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
75 "(2 ,[1] ,false ,#Given ,Inc Streckenlast , pen2str), \n" ^
76 "(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
77 "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
78 (*+*)then () else error "INITIAL I_Model CHANGED";
80 val return_check_single = (*case*)
81 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
82 (*//------------------ step into check_single ----------------------------------------------\\*)
83 "~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
84 = (ctxt, m_field, oris, i_model, m_patt, ct);
85 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
86 handle ERROR msg => error (msg (*^ Position.here pp*))
88 (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
89 (*if*) m_field <> m_field' (*else*);
91 (**)val ("", ori', all) =(**)
92 (*case*) O_Model.contains ctxt m_field o_model t (*of*);
94 (*+*)O_Model.single_to_string @{context} ori';
95 (*+*)val [Free ("q_0", _)] = all;
97 (**)val ("", itm) =(**)
98 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
100 (*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm
101 (*\\------------------ step into check_single ----------------------------------------------//*)
102 val return_check_single = Add itm;
104 "~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);
105 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
106 val tac' = I_Model.make_tactic m_field (ct, i_model')
108 (*+*)if I_Model.to_string ctxt i_model' = "[\n" ^
109 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
110 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
111 "(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
112 "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
113 (*+*)then () else error "FINAL I_Model CHANGED";
115 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
117 val return_by_Add_ = ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
119 (*-------------------- stop into me Add_Given ------------------------------------------------*)
120 (*\------------------- step into me Add_Given ----------------------------------------------//*)
121 val (p,_,f,nxt,_,pt) = return_me_Add_Given
123 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
125 (* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )
126 if p = ([], Pbl) then
127 case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _
128 => error "investigate fun add_single CHANGED 1"
129 else error "investigate fun add_single CHANGED 2"
130 ( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)
131 if p = ([], Pbl) then
132 case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _
133 => error "investigate fun add_single CHANGED 1"
134 else error "investigate fun add_single CHANGED 2"
136 "----------- build I_Model.init_TEST -----------------------------------------------------------";
137 "----------- build I_Model.init_TEST -----------------------------------------------------------";
138 "----------- build I_Model.init_TEST -----------------------------------------------------------";
139 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
141 (* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
142 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
144 val model_input = (*type Position.T is hidden, thus redefinition*)
145 [("#Given", [("Constants [r = 7]", Position.none)]),
146 ("#Where", [("0 < r", Position.none)]),
148 [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
150 [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
151 ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
152 : (Model_Pattern.m_field * (string * Position.T) list) list
153 val example_id = "Diff_App-No.123a";
154 (*----------------------------------------- init state -----------------------------------------*)
155 set_data CTbasic_TEST.EmptyPtree @{theory Calculation};
156 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
158 val CTbasic_TEST.EmptyPtree =
159 (*case*) the_data @{theory Calculation} (*of*);
162 "~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);
163 val example_id' = References_Def.explode_id example_id
164 val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
165 Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
166 val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id
167 val (o_model, ctxt) = O_Model.init thy model model_patt
169 (*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
170 (*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
174 I_Model.init_TEST o_model model_patt;
175 "~~~~~ fun init_TEST , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
177 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
178 = I_Model.to_string_TEST @{context} empty_i_model;
181 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
182 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
183 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
184 fun check str = if str = "true" then true else false
185 fun complete str = if str = "true" then true else false
187 val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]
189 val result_all_variants =
190 map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;
191 (*----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
193 val [NONE, NONE, NONE] = result_all_variants: int list option list
195 (*+*)val true = forall is_none result_all_variants
197 val variants_complete =
198 if forall is_none result_all_variants
200 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
202 val NONE = variants_complete: int list option
205 (*more significant result ..*)
206 val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list
208 in case the result is null, no I_Model is_complete,
209 in case the result contains more than 1 variant, this might determine the decision for MethodC.
211 val variants_complete =
212 if forall is_none result_all_variants
214 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
216 val SOME [11, 13] = variants_complete: int list option;
218 (*/----- reactivate with CS "remove sep_variants_envs"-----\* )
219 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
220 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
221 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
222 (*see Outer_Syntax: val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
225 (*//------------------ test data setup -----------------------------------------------------\\*)
227 *****************************************************************************************
228 ***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****
229 ***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists) *****
230 *****************************************************************************************
231 The ERROR occurred somewhere since introducing structure or since transition to PIDE.
232 *****************************************************************************************
233 We complete the two single_TEST "1" and "5" below and replace them in empty_input;
234 we add "6" as variant of "5" to the empty input.
235 later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).
236 The test intermediatly pairs (feedback_TEST, Position.T) in I_Model.T_TEST
237 and leaves the rest as is.
239 I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,
240 I_Model.is_complete_TEST NO instantiation (done in Template.show):
241 it serves to maintain the OLD test/*
243 val thy = @{theory Calculation}
247 CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id
248 | _(*state (*FOR TEST*)*) => (**)the_data thy(**)
250 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
251 CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data
253 probl: Model_Def.i_model_TEST
254 (*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
255 (2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
256 (3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
257 (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
258 (5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
260 val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)
261 (1, [1,2,3], true, "#Given",
262 (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
263 (@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::
264 nth 2 probl :: nth 3 probl :: nth 4 probl ::
265 (5, [1,2], true, "#Relate",
266 (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
267 (@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::
268 (6, [3], true, "#Relate",
269 (Cor_TEST ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),
270 (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
273 val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
274 Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")
276 val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $
277 Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD
278 (*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition
279 AND as "id" in Subst.T [("fixes", [0 < x])] *);
280 (model_patt |> Model_Pattern.to_string ctxt) =
281 "[\"(#Given, (Constants, fixes))\", " ^
282 "\"(#Find, (Maximum, maxx))\", " ^
283 "\"(#Find, (AdditionalValues, vals))\", " ^
284 "\"(#Relate, (Extremum, extr))\", " ^
285 "\"(#Relate, (SideConditions, sideconds))\"]";
286 val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})
287 (*\\------------------ test data setup -----------------------------------------------------//*)
289 (*/------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------\*)
290 (*\------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------/*)
291 ( *\----- reactivate with CS "remove sep_variants_envs"-----/*)
294 "----------- build I_Model.s_make_complete -----------------------------------------------------";
295 "----------- build I_Model.s_make_complete -----------------------------------------------------";
296 "----------- build I_Model.s_make_complete -----------------------------------------------------";
297 val (_(*example text*),
298 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
299 "Extremum (A = 2 * u * v - u \<up> 2)" ::
300 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
301 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
302 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
303 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
304 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
305 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
306 "ErrorBound (\<epsilon> = (0::real))" :: []),
308 ["univariate_calculus", "Optimisation"],
309 ["Optimisation", "by_univariate_calculus"])))
310 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
313 val (p,_,f,nxt,_,pt) =
314 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
315 val (p,_,f,nxt,_,pt) = me nxt p c pt;
317 (*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
318 val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
319 PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
320 => (o_model, (pbl_imod, met_imod), (pI, mI))
321 | _ => raise ERROR ""
323 val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
324 val {model = met_patt, ...} = MethodC.from_store ctxt mI;
326 val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
327 (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
328 [@{term "[r = (7::real)]"}]), Position.none)),
329 (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
330 [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
332 val met_imod = [ (*1 item for creating code*)
333 (8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
335 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
336 (*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
337 (*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
338 (*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
339 (*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
340 (*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
341 (*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
342 (*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
343 (*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
344 (*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
345 (*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
346 (*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
347 (*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
348 then () else error "setup test data for I_Model.s_make_complete CHANGED";
349 (*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
351 val return_s_make_complete =
352 s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
353 (*/------------------- step into s_make_complete -------------------------------------------\\*)
354 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
355 (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
356 val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
357 val i_from_pbl = map (fn (_, (descr, _)) =>
358 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
360 (*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
361 "~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
362 (@{term Constants}, pbl_max_vnts, pbl_imod);
363 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
364 | SOME descr' => if descr = descr' then true else false) i_model
366 (*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_TEST
368 val return_get_descr_vnt_1 =
369 case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
370 [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
371 | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
372 (*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
374 (*|------------------- continue s_make_complete ----------------------------------------------*)
375 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
376 if is_empty_single_TEST i_single
378 case get_descr_vnt' feedb pbl_max_vnts o_model of
379 (*-----------^^^^^^^^^^^^^^-----------------------------*)
380 [] => raise ERROR (msg pbl_max_vnts feedb)
381 | o_singles => map transfer_terms o_singles
382 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
384 (*+*)val [2, 1] = vnts;
385 (*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
386 "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
387 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
388 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
389 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
390 "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
391 then () else error "pbl_from_o_model CHANGED"
393 (*//------------------ step into map ((fn i_single -----------------------------------------\\*)
394 "~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
395 (*if*) is_empty_single_TEST i_single (*else*);
396 get_descr_vnt' feedb pbl_max_vnts o_model;
398 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
399 if is_empty_single_TEST i_single
401 case get_descr_vnt' feedb pbl_max_vnts o_model of
402 (*---------- ^^^^^^^^^^^^^^ ----------------------------*)
403 [] => raise ERROR (msg pbl_max_vnts feedb)
404 | o_singles => map transfer_terms o_singles
405 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
406 (*\\------------------ step into map ((fn i_single -----------------------------------------//*)
408 (*|------------------- continue s_make_complete ----------------------------------------------*)
409 val i_from_met = map (fn (_, (descr, _)) =>
410 (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
412 (*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
413 "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
414 "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
415 "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
416 "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
417 "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
418 (*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
419 "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
420 "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
421 "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
422 (*+*)then () else error "s_make_complete: from_met CHANGED";
424 val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
425 (*+*)val [2] = met_max_vnts
427 val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
428 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
429 if is_empty_single_TEST i_single
431 case get_descr_vnt' feedb [met_max_vnt] o_model of
432 [] => raise ERROR (msg [met_max_vnt] feedb)
433 | o_singles => map transfer_terms o_singles
434 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
436 (*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
437 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
438 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
439 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
440 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
441 "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
442 "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
443 "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
444 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
445 (*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
447 val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
448 (*\------------------- step into s_make_complete -------------------------------------------//*)
450 if return_s_make_complete = return_s_make_complete_step
451 then () else error "s_make_complete: stewise construction <> value of fun"