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@59957
|
9 |
"----------- investigate fun add_single in I_Model ---------------------------------------------";
|
Walther@60690
|
10 |
"----------- build I_Model.init_TEST -----------------------------------------------------------";
|
Walther@60705
|
11 |
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
|
Walther@60705
|
12 |
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
|
walther@59957
|
13 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
14 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
15 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
16 |
|
walther@59957
|
17 |
open I_Model;
|
Walther@60705
|
18 |
open Test_Code;
|
Walther@60705
|
19 |
open Tactic;
|
Walther@60705
|
20 |
open Pos;
|
Walther@60729
|
21 |
|
walther@59957
|
22 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59957
|
23 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59957
|
24 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59997
|
25 |
val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@59957
|
26 |
"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
|
walther@59957
|
27 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
walther@59957
|
28 |
"AbleitungBiegelinie dy"];
|
walther@59957
|
29 |
val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
|
Walther@60571
|
30 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
|
walther@59957
|
31 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
|
walther@59957
|
32 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)
|
walther@59957
|
33 |
|
Walther@60676
|
34 |
(*[], Pbl*)val return_me_Add_Given =
|
Walther@60676
|
35 |
me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
|
Walther@60676
|
36 |
(*/------------------- step into me Add_Given ----------------------------------------------\\*)
|
walther@59957
|
37 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
walther@59957
|
38 |
|
Walther@60676
|
39 |
val ("ok", (_, _, ptp)) = (*case*)
|
walther@59957
|
40 |
Step.by_tactic tac (pt, p) (*of*);
|
walther@59957
|
41 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
Walther@60676
|
42 |
|
walther@59957
|
43 |
val Applicable.Yes tac' = (*case*)
|
walther@59957
|
44 |
Step.check tac (pt, p) (*of*);
|
walther@59957
|
45 |
(*if*) Tactic.for_specify' tac' (*then*);
|
walther@59957
|
46 |
|
walther@59957
|
47 |
Step_Specify.by_tactic tac' ptp;
|
walther@59957
|
48 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
|
walther@59957
|
49 |
|
Walther@60676
|
50 |
val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)
|
walther@60016
|
51 |
Specify.by_Add_ "#Given" ct (pt, p);
|
Walther@60676
|
52 |
"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
|
walther@59957
|
53 |
("#Given", ct, (pt, p));
|
Walther@60676
|
54 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
|
Walther@60676
|
55 |
val (i_model, m_patt) =
|
Walther@60676
|
56 |
if p_ = Pos.Met then
|
Walther@60676
|
57 |
(met,
|
Walther@60676
|
58 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
Walther@60676
|
59 |
else
|
Walther@60676
|
60 |
(pbl,
|
Walther@60676
|
61 |
(if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
|
Walther@60676
|
62 |
;
|
Walther@60655
|
63 |
(*+*)if O_Model.to_string @{context} oris = "[\n" ^
|
walther@59997
|
64 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@59997
|
65 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@59997
|
66 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@59997
|
67 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@59997
|
68 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
walther@59997
|
69 |
"(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
|
walther@59997
|
70 |
"(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
|
walther@59957
|
71 |
(*+*)then () else error "INITIAL O_Model CHANGED";
|
walther@59957
|
72 |
(*+*)if I_Model.to_string ctxt pbl = "[\n" ^
|
Walther@60739
|
73 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
74 |
"(2 ,[1] ,false ,#Given ,Inc Streckenlast , pen2str), \n" ^
|
Walther@60739
|
75 |
"(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
|
Walther@60739
|
76 |
"(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
|
walther@59957
|
77 |
(*+*)then () else error "INITIAL I_Model CHANGED";
|
walther@59957
|
78 |
|
Walther@60676
|
79 |
val return_check_single = (*case*)
|
Walther@60676
|
80 |
I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
|
Walther@60676
|
81 |
(*//------------------ step into check_single ----------------------------------------------\\*)
|
Walther@60676
|
82 |
"~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
|
Walther@60676
|
83 |
= (ctxt, m_field, oris, i_model, m_patt, ct);
|
Walther@60676
|
84 |
val (t as (descriptor $ _)) = Syntax.read_term ctxt str
|
Walther@60676
|
85 |
handle ERROR msg => error (msg (*^ Position.here pp*))
|
Walther@60676
|
86 |
val SOME m_field' =
|
Walther@60676
|
87 |
(*case*) Model_Pattern.get_field descriptor m_patt (*of*);
|
Walther@60676
|
88 |
(*if*) m_field <> m_field' (*else*);
|
Walther@60676
|
89 |
|
walther@59957
|
90 |
(**)val ("", ori', all) =(**)
|
Walther@60469
|
91 |
(*case*) O_Model.contains ctxt m_field o_model t (*of*);
|
walther@59957
|
92 |
|
Walther@60655
|
93 |
(*+*)O_Model.single_to_string @{context} ori';
|
walther@59957
|
94 |
(*+*)val [Free ("q_0", _)] = all;
|
walther@59957
|
95 |
|
walther@59957
|
96 |
(**)val ("", itm) =(**)
|
walther@59957
|
97 |
(*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
|
walther@59957
|
98 |
|
Walther@60676
|
99 |
(*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm
|
Walther@60676
|
100 |
(*\\------------------ step into check_single ----------------------------------------------//*)
|
Walther@60676
|
101 |
val return_check_single = Add itm;
|
walther@59957
|
102 |
|
Walther@60676
|
103 |
"~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);
|
Walther@60676
|
104 |
val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
|
Walther@60676
|
105 |
val tac' = I_Model.make_tactic m_field (ct, i_model')
|
Walther@60676
|
106 |
;
|
Walther@60676
|
107 |
(*+*)if I_Model.to_string ctxt i_model' = "[\n" ^
|
Walther@60739
|
108 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
109 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
|
Walther@60739
|
110 |
"(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
|
Walther@60739
|
111 |
"(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
|
walther@59957
|
112 |
(*+*)then () else error "FINAL I_Model CHANGED";
|
walther@59957
|
113 |
|
Walther@60676
|
114 |
val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59957
|
115 |
|
Walther@60676
|
116 |
val return_by_Add_ = ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
|
Walther@60676
|
117 |
[], (pt', pos)));
|
Walther@60676
|
118 |
(*-------------------- stop into me Add_Given ------------------------------------------------*)
|
Walther@60676
|
119 |
(*\------------------- step into me Add_Given ----------------------------------------------//*)
|
Walther@60676
|
120 |
val (p,_,f,nxt,_,pt) = return_me_Add_Given
|
walther@59957
|
121 |
|
Walther@60676
|
122 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
|
walther@59957
|
123 |
|
Walther@60729
|
124 |
(* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )
|
walther@59957
|
125 |
if p = ([], Pbl) then
|
Walther@60729
|
126 |
case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _
|
Walther@60729
|
127 |
=> error "investigate fun add_single CHANGED 1"
|
Walther@60729
|
128 |
else error "investigate fun add_single CHANGED 2"
|
Walther@60729
|
129 |
( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)
|
Walther@60729
|
130 |
if p = ([], Pbl) then
|
Walther@60729
|
131 |
case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _
|
Walther@60729
|
132 |
=> error "investigate fun add_single CHANGED 1"
|
walther@59957
|
133 |
else error "investigate fun add_single CHANGED 2"
|
Walther@60690
|
134 |
|
Walther@60690
|
135 |
"----------- build I_Model.init_TEST -----------------------------------------------------------";
|
Walther@60690
|
136 |
"----------- build I_Model.init_TEST -----------------------------------------------------------";
|
Walther@60690
|
137 |
"----------- build I_Model.init_TEST -----------------------------------------------------------";
|
Walther@60690
|
138 |
(*/---------------------------------------- mimic input from PIDE -----------------------------\*)
|
Walther@60690
|
139 |
|
Walther@60690
|
140 |
(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
|
Walther@60690
|
141 |
val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
|
Walther@60690
|
142 |
val thy = @{theory}
|
Walther@60690
|
143 |
val model_input = (*type Position.T is hidden, thus redefinition*)
|
Walther@60690
|
144 |
[("#Given", [("Constants [r = 7]", Position.none)]),
|
Walther@60690
|
145 |
("#Where", [("0 < r", Position.none)]),
|
Walther@60690
|
146 |
("#Find",
|
Walther@60690
|
147 |
[("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
|
Walther@60690
|
148 |
("#Relate",
|
Walther@60690
|
149 |
[("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
|
Walther@60690
|
150 |
("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
|
Walther@60690
|
151 |
: (Model_Pattern.m_field * (string * Position.T) list) list
|
Walther@60690
|
152 |
val example_id = "Diff_App-No.123a";
|
Walther@60690
|
153 |
(*----------------------------------------- init state -----------------------------------------*)
|
Walther@60704
|
154 |
set_data CTbasic_TEST.EmptyPtree @{theory Calculation};
|
Walther@60690
|
155 |
(*\---------------------------------------- mimic input from PIDE -----------------------------/*)
|
Walther@60690
|
156 |
|
Walther@60704
|
157 |
val CTbasic_TEST.EmptyPtree =
|
Walther@60694
|
158 |
(*case*) the_data @{theory Calculation} (*of*);
|
Walther@60690
|
159 |
|
Walther@60690
|
160 |
(* Calculation..*)
|
Walther@60704
|
161 |
"~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);
|
Walther@60690
|
162 |
val example_id' = References_Def.explode_id example_id
|
Walther@60690
|
163 |
val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
|
Walther@60690
|
164 |
Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
|
Walther@60690
|
165 |
val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id
|
Walther@60690
|
166 |
val (o_model, ctxt) = O_Model.init thy model model_patt
|
Walther@60690
|
167 |
;
|
Walther@60690
|
168 |
(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
|
Walther@60690
|
169 |
(*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
|
Walther@60695
|
170 |
(*+*) refs
|
Walther@60690
|
171 |
|
Walther@60694
|
172 |
val empty_i_model =
|
Walther@60702
|
173 |
I_Model.init_TEST o_model model_patt;
|
Walther@60694
|
174 |
"~~~~~ fun init_TEST , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
|
Walther@60694
|
175 |
;
|
Walther@60733
|
176 |
(*+*)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))]"
|
Walther@60733
|
177 |
= I_Model.to_string_TEST @{context} empty_i_model;
|
Walther@60705
|
178 |
|
Walther@60705
|
179 |
|
Walther@60705
|
180 |
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
|
Walther@60705
|
181 |
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
|
Walther@60705
|
182 |
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
|
Walther@60705
|
183 |
fun check str = if str = "true" then true else false
|
Walther@60705
|
184 |
fun complete str = if str = "true" then true else false
|
Walther@60705
|
185 |
|
Walther@60705
|
186 |
val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]
|
Walther@60705
|
187 |
|
Walther@60705
|
188 |
val result_all_variants =
|
Walther@60705
|
189 |
map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;
|
Walther@60705
|
190 |
(*----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
Walther@60705
|
191 |
;
|
Walther@60705
|
192 |
val [NONE, NONE, NONE] = result_all_variants: int list option list
|
Walther@60705
|
193 |
|
Walther@60705
|
194 |
(*+*)val true = forall is_none result_all_variants
|
Walther@60705
|
195 |
|
Walther@60705
|
196 |
val variants_complete =
|
Walther@60705
|
197 |
if forall is_none result_all_variants
|
Walther@60705
|
198 |
then NONE
|
Walther@60705
|
199 |
else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
|
Walther@60705
|
200 |
;
|
Walther@60705
|
201 |
val NONE = variants_complete: int list option
|
Walther@60705
|
202 |
|
Walther@60705
|
203 |
|
Walther@60705
|
204 |
(*more significant result ..*)
|
Walther@60705
|
205 |
val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list
|
Walther@60705
|
206 |
(*
|
Walther@60705
|
207 |
in case the result is null, no I_Model is_complete,
|
Walther@60705
|
208 |
in case the result contains more than 1 variant, this might determine the decision for MethodC.
|
Walther@60705
|
209 |
*)
|
Walther@60705
|
210 |
val variants_complete =
|
Walther@60705
|
211 |
if forall is_none result_all_variants
|
Walther@60705
|
212 |
then NONE
|
Walther@60705
|
213 |
else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
|
Walther@60705
|
214 |
;
|
Walther@60705
|
215 |
val SOME [11, 13] = variants_complete: int list option;
|
Walther@60705
|
216 |
|
Walther@60714
|
217 |
(*/----- reactivate with CS "remove sep_variants_envs"-----\* )
|
Walther@60705
|
218 |
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
|
Walther@60705
|
219 |
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
|
Walther@60705
|
220 |
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
|
Walther@60705
|
221 |
(*see Outer_Syntax: val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
|
Walther@60705
|
222 |
open I_Model
|
Walther@60705
|
223 |
open Pre_Conds;
|
Walther@60705
|
224 |
(*//------------------ test data setup -----------------------------------------------------\\*)
|
Walther@60705
|
225 |
(*
|
Walther@60705
|
226 |
*****************************************************************************************
|
Walther@60705
|
227 |
***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****
|
Walther@60705
|
228 |
***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists) *****
|
Walther@60705
|
229 |
*****************************************************************************************
|
Walther@60705
|
230 |
The ERROR occurred somewhere since introducing structure or since transition to PIDE.
|
Walther@60705
|
231 |
*****************************************************************************************
|
Walther@60705
|
232 |
We complete the two single_TEST "1" and "5" below and replace them in empty_input;
|
Walther@60705
|
233 |
we add "6" as variant of "5" to the empty input.
|
Walther@60705
|
234 |
later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).
|
Walther@60705
|
235 |
The test intermediatly pairs (feedback_TEST, Position.T) in I_Model.T_TEST
|
Walther@60705
|
236 |
and leaves the rest as is.
|
Walther@60705
|
237 |
|
Walther@60705
|
238 |
I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,
|
Walther@60705
|
239 |
I_Model.is_complete_TEST NO instantiation (done in Template.show):
|
Walther@60705
|
240 |
it serves to maintain the OLD test/*
|
Walther@60705
|
241 |
*)
|
Walther@60705
|
242 |
val thy = @{theory Calculation}
|
Walther@60705
|
243 |
|
Walther@60705
|
244 |
val state =
|
Walther@60705
|
245 |
case the_data thy of
|
Walther@60705
|
246 |
CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id
|
Walther@60705
|
247 |
| _(*state (*FOR TEST*)*) => (**)the_data thy(**)
|
Walther@60705
|
248 |
(*let*)
|
Walther@60705
|
249 |
val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
|
Walther@60705
|
250 |
CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data
|
Walther@60705
|
251 |
;
|
Walther@60705
|
252 |
probl: Model_Def.i_model_TEST
|
Walther@60705
|
253 |
(*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
|
Walther@60705
|
254 |
(2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
|
Walther@60705
|
255 |
(3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
|
Walther@60716
|
256 |
(4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
|
Walther@60705
|
257 |
(5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
|
Walther@60705
|
258 |
;
|
Walther@60705
|
259 |
val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)
|
Walther@60705
|
260 |
(1, [1,2,3], true, "#Given",
|
Walther@60705
|
261 |
(Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
|
Walther@60705
|
262 |
(@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::
|
Walther@60705
|
263 |
nth 2 probl :: nth 3 probl :: nth 4 probl ::
|
Walther@60705
|
264 |
(5, [1,2], true, "#Relate",
|
Walther@60705
|
265 |
(Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
|
Walther@60705
|
266 |
(@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::
|
Walther@60705
|
267 |
(6, [3], true, "#Relate",
|
Walther@60705
|
268 |
(Cor_TEST ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),
|
Walther@60705
|
269 |
(@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
|
Walther@60705
|
270 |
:: [];
|
Walther@60705
|
271 |
|
Walther@60705
|
272 |
val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
|
Walther@60705
|
273 |
Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")
|
Walther@60705
|
274 |
;
|
Walther@60705
|
275 |
val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $
|
Walther@60705
|
276 |
Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD
|
Walther@60705
|
277 |
(*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition
|
Walther@60705
|
278 |
AND as "id" in Subst.T [("fixes", [0 < x])] *);
|
Walther@60705
|
279 |
(model_patt |> Model_Pattern.to_string ctxt) =
|
Walther@60705
|
280 |
"[\"(#Given, (Constants, fixes))\", " ^
|
Walther@60705
|
281 |
"\"(#Find, (Maximum, maxx))\", " ^
|
Walther@60705
|
282 |
"\"(#Find, (AdditionalValues, vals))\", " ^
|
Walther@60705
|
283 |
"\"(#Relate, (Extremum, extr))\", " ^
|
Walther@60705
|
284 |
"\"(#Relate, (SideConditions, sideconds))\"]";
|
Walther@60705
|
285 |
val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})
|
Walther@60705
|
286 |
(*\\------------------ test data setup -----------------------------------------------------//*)
|
Walther@60705
|
287 |
|
Walther@60705
|
288 |
(*/------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------\*)
|
Walther@60705
|
289 |
;
|
Walther@60705
|
290 |
|
Walther@60705
|
291 |
I_Model.is_complete_OLD ctxt model_patt where_rls where_OLD probl_POS;
|
Walther@60705
|
292 |
(*//------------------ step into is_complete_OLD -------------------------------------------\\*)
|
Walther@60705
|
293 |
"~~~~~ fun is_complete_OLD , args:"; val (ctxt, model_patt, where_rls, pres, i_model) =
|
Walther@60705
|
294 |
(ctxt, model_patt, where_rls, where_OLD,
|
Walther@60705
|
295 |
(** )filter (fn (_, _, _, m_field, _) => m_field = "#Given")( **) probl_POS);
|
Walther@60705
|
296 |
(*for Pre_Conds.eval we only need ------------------^^^^^^^^, -UNCOMMENT EITHER HER OR THERE-*)
|
Walther@60705
|
297 |
|
Walther@60705
|
298 |
(*+*)val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $
|
Walther@60705
|
299 |
Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", xxx(*"real"*))] = pres;
|
Walther@60705
|
300 |
(*+*) if I_Model.to_string_TEST @{context} i_model = "[\n" ^
|
Walther@60705
|
301 |
"(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n" ^
|
Walther@60705
|
302 |
"(2, [1, 2, 3], false ,#Find, (Inp_TEST Maximum __, Position.T)), \n" ^
|
Walther@60705
|
303 |
"(3, [1, 2, 3], false ,#Find, (Inp_TEST AdditionalValues [__, __], Position.T)), \n" ^
|
Walther@60716
|
304 |
"(4, [1, 2, 3], false ,#Relate, (Inp_TEST Extremum (__=__), Position.T)), \n" ^
|
Walther@60705
|
305 |
"(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [??.empty]), Position.T)), \n" ^
|
Walther@60705
|
306 |
"(6, [3], true ,#Relate, (Cor_TEST SideConditions\n [(2::'a) * u = r * sin \<alpha>, (2::'a) * v = r * cos \<alpha>] ,(sideconds, [??.empty]), Position.T))]"
|
Walther@60705
|
307 |
then () else raise error "I_Model.to_string_TEST i_model CHANGED";
|
Walther@60705
|
308 |
|
Walther@60710
|
309 |
val no_model_items = length model_patt
|
Walther@60710
|
310 |
(*+*)val 5 = no_model_items;
|
Walther@60705
|
311 |
sep_variants_envs model_patt i_model;
|
Walther@60710
|
312 |
|
Walther@60705
|
313 |
(*///----------------- step into sep_variants_envs ----------------------------------------\\\*)
|
Walther@60705
|
314 |
(*+*)sep_variants_envs: Model_Pattern.T -> I_Model.T_TEST ->
|
Walther@60705
|
315 |
((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;
|
Walther@60705
|
316 |
"~~~~~ fun sep_variants_envs , args:"; val (model_patt, i_model) = (model_patt, i_model);
|
Walther@60705
|
317 |
val equal_descr_pairs =
|
Walther@60705
|
318 |
map (get_equal_descr i_model) model_patt
|
Walther@60705
|
319 |
|> flat
|
Walther@60705
|
320 |
(*+*)val
|
Walther@60705
|
321 |
[(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _))),
|
Walther@60705
|
322 |
(1, [1, 2, 3], true, "#Given", _)),
|
Walther@60705
|
323 |
(*"#Given"^^^^ would be appropriate for pre-conditions, but kept to build code:...*)
|
Walther@60705
|
324 |
(("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),
|
Walther@60705
|
325 |
(5, [1, 2], true, "#Relate", _)),
|
Walther@60705
|
326 |
(("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),
|
Walther@60705
|
327 |
(6, [3], true, "#Relate", _) )] = equal_descr_pairs
|
Walther@60705
|
328 |
|
Walther@60705
|
329 |
val all_variants =
|
Walther@60705
|
330 |
map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
|
Walther@60705
|
331 |
|> flat
|
Walther@60705
|
332 |
|> distinct op =
|
Walther@60705
|
333 |
val variants_separated = map (filter_variants equal_descr_pairs) all_variants
|
Walther@60705
|
334 |
(*+*)val
|
Walther@60705
|
335 |
[
|
Walther@60705
|
336 |
[(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),
|
Walther@60710
|
337 |
(1, [1(*#*), 2, 3], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),
|
Walther@60705
|
338 |
[_ $ (Const ("HOL.eq", _) $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),
|
Walther@60705
|
339 |
(("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),
|
Walther@60710
|
340 |
(5, [1(*#*), 2], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),
|
Walther@60705
|
341 |
[_ $ (_ $ (_ $ (_ $ (_ $ Free ("u", _) $ _) $ _) $ _) $ _) $ _]), _(*eliminate*)), _)))],
|
Walther@60705
|
342 |
[(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),
|
Walther@60710
|
343 |
(1, [1, 2(*#*), 3], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),
|
Walther@60705
|
344 |
[_ $ (_ $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),
|
Walther@60705
|
345 |
(("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),
|
Walther@60710
|
346 |
(5, [1, 2(*#*)], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),
|
Walther@60705
|
347 |
[_ $ (_ $ (_ $ (_ $ (_ $ Free ("u", _) $ _) $ _) $ _) $ _) $ _]), _(*eliminate*)), _)))],
|
Walther@60705
|
348 |
[(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),
|
Walther@60710
|
349 |
(1, [1, 2, 3(*#*)], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),
|
Walther@60705
|
350 |
[_ $ (Const ("HOL.eq", _) $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),
|
Walther@60705
|
351 |
(("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),
|
Walther@60710
|
352 |
(6, [3(*#*)], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),
|
Walther@60705
|
353 |
[_ $ (_ $ _ $ (_ $ _ $ (Const ("Transcendental.sin", _) $ Free ("\<alpha>", _)))) $ _]), _), _)))]]
|
Walther@60710
|
354 |
(*+*) = variants_separated (*#*):
|
Walther@60705
|
355 |
(Model_Pattern.single * single_TEST) list list
|
Walther@60705
|
356 |
|
Walther@60710
|
357 |
val i_models = map (map snd) variants_separated; (*drop Model_Pattern.T from pair*)
|
Walther@60705
|
358 |
(*+*)i_models: I_Model.T_TEST list;
|
Walther@60705
|
359 |
|
Walther@60705
|
360 |
val envs_subst = map mk_env_subst variants_separated;
|
Walther@60705
|
361 |
(*+*)envs_subst: Pre_Conds.env_subst list;
|
Walther@60705
|
362 |
|
Walther@60705
|
363 |
val envs_eval = map mk_env_eval variants_separated;
|
Walther@60705
|
364 |
(*+*)envs_eval: Pre_Conds.env_subst list;
|
Walther@60705
|
365 |
|
Walther@60705
|
366 |
val return_sep_variants_envs = arrange_args2 i_models envs_subst envs_eval (1, all_variants);
|
Walther@60705
|
367 |
|
Walther@60705
|
368 |
(*+*)return_sep_variants_envs:
|
Walther@60705
|
369 |
((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;
|
Walther@60705
|
370 |
(*\\\----------------- step into sep_variants_envs ----------------------------------------///*)
|
Walther@60705
|
371 |
|
Walther@60705
|
372 |
(*||------------------ continuing is_complete_OLD --------------------------------------------*)
|
Walther@60705
|
373 |
(*+*)val [[(Free ("fixes", _), Free ("r", _))], (*.. vor 3 variants*)
|
Walther@60705
|
374 |
[(Free ("fixes", _), Free ("r", _))],
|
Walther@60705
|
375 |
[(Free ("fixes", _), Free ("r", _))]] = envs_subst;
|
Walther@60705
|
376 |
|
Walther@60705
|
377 |
(*taken from local environment -----------------------vvvvvvvvvv, ----vvvvvvvvv*)
|
Walther@60705
|
378 |
check_variant_envs ctxt where_rls pres (hd envs_subst) (hd envs_eval);
|
Walther@60705
|
379 |
(*+*)val (true,
|
Walther@60705
|
380 |
[(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
|
Walther@60705
|
381 |
Free ("r", _))])
|
Walther@60705
|
382 |
= check_variant_envs ctxt where_rls pres (hd envs_subst) (hd envs_eval);;
|
Walther@60705
|
383 |
(*///----------------- step into check_variant_envs --------------------------------------\\\*)
|
Walther@60705
|
384 |
(*these come in variants..*)
|
Walther@60705
|
385 |
val variant_envs as ((_, env_subst, env_eval), _) = hd return_sep_variants_envs;
|
Walther@60705
|
386 |
(*args of is_complete_OLD -------------------vvvv--vvvvvvvvv--vvvv*)
|
Walther@60705
|
387 |
"~~~~~ fun check_variant_envs , args:"; val (ctxt, where_rls, pres, env_subst, env_eval) =
|
Walther@60705
|
388 |
(ctxt, where_rls, pres, hd envs_subst, hd envs_eval);
|
Walther@60705
|
389 |
|
Walther@60705
|
390 |
(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
|
Walther@60705
|
391 |
Free ("fixes", _)] = pres
|
Walther@60705
|
392 |
(*+*)val [(Free ("fixes", _), Free ("r", _))] = env_subst
|
Walther@60705
|
393 |
(*+*)val [(Free ("r", _), Const ("Num.numeral_class.numeral", _) $ _ )] = env_eval (*env2*)
|
Walther@60705
|
394 |
|
Walther@60705
|
395 |
val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
|
Walther@60705
|
396 |
(*+*)val [(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
|
Walther@60705
|
397 |
Free ("r", _))] = pres_subst
|
Walther@60705
|
398 |
|
Walther@60705
|
399 |
val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
|
Walther@60705
|
400 |
(*+*)val [(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
|
Walther@60705
|
401 |
(Const ("Num.numeral_class.numeral", _) $ _ ))] = full_subst
|
Walther@60705
|
402 |
|
Walther@60705
|
403 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60705
|
404 |
(*+*)val [(true,
|
Walther@60705
|
405 |
Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
|
Walther@60705
|
406 |
(Const ("Num.numeral_class.numeral", _) $ _ ))] = evals
|
Walther@60705
|
407 |
|
Walther@60705
|
408 |
(*-------------- fixpoint of foldl -----vvvv*)
|
Walther@60705
|
409 |
val return_check_variant = (foldl and_ (true, map fst evals), pres_subst)
|
Walther@60705
|
410 |
(*+*)val (true, [(true, Const ("Orderings.ord_class.less", _) $
|
Walther@60705
|
411 |
Const ("Groups.zero_class.zero", _) $ Free ("r", _))]) = return_check_variant
|
Walther@60705
|
412 |
(*\\\----------------- step into check_variant_envs --------------------------------------///*)
|
Walther@60705
|
413 |
|
Walther@60705
|
414 |
(*||------------------ continuing is_complete_OLD --------------------------------------------*)
|
Walther@60705
|
415 |
(*+*)val false = is_complete_variant no_model_items i_model
|
Walther@60705
|
416 |
|
Walther@60705
|
417 |
val variants_envs = sep_variants_envs model_patt i_model;
|
Walther@60705
|
418 |
(*+*)variants_envs: ((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;
|
Walther@60705
|
419 |
|
Walther@60705
|
420 |
val result_all_variants = map
|
Walther@60705
|
421 |
(fn ((i_model, env_subst, env_eval), variant) =>
|
Walther@60705
|
422 |
if fst (check_variant_envs ctxt where_rls pres env_subst env_eval)
|
Walther@60705
|
423 |
andalso is_complete_variant no_model_items i_model
|
Walther@60705
|
424 |
then SOME [variant] else NONE) variants_envs;
|
Walther@60705
|
425 |
(*+*)result_all_variants: variant list option list;
|
Walther@60705
|
426 |
(*+*)val [NONE, NONE, NONE] = result_all_variants
|
Walther@60705
|
427 |
|
Walther@60705
|
428 |
val variants_complete =
|
Walther@60705
|
429 |
if forall is_none result_all_variants
|
Walther@60705
|
430 |
then NONE
|
Walther@60705
|
431 |
else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat);
|
Walther@60705
|
432 |
(*+*)variants_complete: variant list option;
|
Walther@60705
|
433 |
|
Walther@60705
|
434 |
val return_is_complete_OLD = variants_complete;
|
Walther@60705
|
435 |
(*\\------------------ step into into is_complete_OLD --------------------------------------//*)
|
Walther@60705
|
436 |
(*\------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------/*)
|
Walther@60714
|
437 |
( *\----- reactivate with CS "remove sep_variants_envs"-----/*)
|