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