1 (* Title: "Specify/o-model.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- initialise O_Model.T --------------------------------------------------------------";
10 "----------- fun partition_variants ------------------------------------------------------------";
11 "----------- fun O_Model.collect_variants ------------------------------------------------------";
12 "----------- fun partition_variants ------------------------------------------------------------";
13 "----------- fun add_enumerate -----------------------------------------------------------------";
14 "----------- fun filter_vat --------------------------------------------------------------------";
15 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
16 "----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";
17 "-----------------------------------------------------------------------------------------------";
18 "-----------------------------------------------------------------------------------------------";
19 "-----------------------------------------------------------------------------------------------";
21 "----------- fun init for O_Model.T ------------------------------------------------------------";
22 "----------- fun init for O_Model.T ------------------------------------------------------------";
23 "----------- fun init for O_Model.T ------------------------------------------------------------";
25 val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
26 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
27 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
28 "AbleitungBiegelinie dy"];
29 val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
30 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
32 "~~~~~ fun init_calc @{context} , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
33 = (@{context}, [(f_model, f_spec)]);
35 val thy = thy_id |> ThyC.get_theory_PIDE ctxt; (*= ..., Isac.Biegelinie}*)
36 (* val ((pt, p), tacis) =*)
37 Step_Specify.initialise' thy (model, refs);
38 "~~~~~ fun initialise' , args:"; val (thy, (model, refs)) = (thy, (model, refs));
39 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
40 Step_Specify.initialise thy (model, refs);
41 "~~~~~ fun initialise , args:"; val (thy, (fmz, (_, pI, mI))) = (thy, (model, refs));
42 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *);
43 (*if*) mI = ["no_met"] (*else*);
44 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
45 (*+*)Problem.from_store ctxt pI: Problem.T;
46 (*+*)(Problem.from_store ctxt pI |> #model): Model_Pattern.T;
48 (*+*)val (o_model, ctxt) = (Problem.from_store ctxt pI |> #model |>
49 O_Model.init thy fmz);
50 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #model);
51 val (ts, ctxt) = ContextC.init_while_parsing fmz thy
54 |> Input_Descript.split
55 |> add_field thy pbt) ts)
59 (*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> ParseC.parse_test @{context};
60 (*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
61 (*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
62 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
63 (*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),
64 ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
65 ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),
66 ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),
67 [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
68 Const (\<^const_name>\<open>Nil\<close>, _),
69 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
70 Const (\<^const_name>\<open>Nil\<close>, _),
71 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"0"*)) $
72 Const (\<^const_name>\<open>Nil\<close>, _),
73 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ Free ("L", _)) $ _(*"0"*)) $
74 Const (\<^const_name>\<open>Nil\<close>, _)]),
75 ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
78 |> ParseC.parse_test @{context}
79 |> Input_Descript.split
80 |> add_field thy pbt) fmz);
81 (*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
82 _, _, _, _, _, _] = add_variants ddd;
84 val maxv = map fst ori |> max_variant;
85 val maxv = if maxv = 0 then 1 else maxv;
87 |> O_Model.collect_variants
88 |> map (replace_0 maxv |> apfst)
93 (*+*)val fff as [([0], ("#Given", _, _)), _, _, _, _, _, _] = ori |> O_Model.collect_variants;
94 (*+*)val ggg as [([1], ("#Given", _, _)), _, _, _, _, _, _] = fff |> map (replace_0 maxv |> apfst);
95 (*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_enumerate;
96 (*+*)val iii = hhh |> map flattup;
97 (*+*)val iii as [(1, [1], "#Given", _, _), (2, [1], "#Given", _, _), _, _, _, _, _] = hhh |> map flattup;
99 (oris, ctxt) (*return from O_Model.init*);
100 "~~~~~ from fun O_Model.init \<longrightarrow>fun initialise' , return:"; val (pors, pctxt) = (oris, ctxt);
103 (*+*)if O_Model.to_string @{context} pors = "[\n" ^
104 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
105 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
106 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
107 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
108 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
109 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
110 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
111 then () else error "O_Model.init CHANGED";
114 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
115 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
116 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
117 case Syntax.read_term ctxt "L" of
118 Free ("L", Type (\<^type_name>\<open>real\<close>, [])) => ()
119 | _ => error "O_Model.init CHANGED";
121 "----------- fun partition_variants ------------------------------------------------------------";
122 "----------- fun partition_variants ------------------------------------------------------------";
123 "----------- fun partition_variants ------------------------------------------------------------";
124 val xs = [1,1,1,2,4,4,5];
125 val xxx = partition_variants (op=) xs;
126 if xxx = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
127 then () else error "fun partition_variants CHANGED";
129 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
130 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
131 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
132 val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
134 if O_Model.collect_variants xs = [([1, 2, 3], 1), ([0], 2), ([1, 2], 4), ([0], 5)]
135 then () else error "fun O_Model.collect_variants CHANGED";
137 (**** fun O_Model.partition_variants #################################################### ****)
138 "----------- fun partition_variants ------------------------------------------------------------";
139 "----------- fun partition_variants ------------------------------------------------------------";
140 if partition_variants op= ["a", "b", "c"] = [(0, "a"), (0, "b"), (0, "c")]
141 then () else error "O_Model.partition_variants CHANGED 1";
143 if partition_variants op= ["a", "b", "b", "b", "c"] = [
145 (1, "b"), (2, "b"), (3, "b"),
146 (0, "c")] then () else error "O_Model.partition_variants CHANGED 2";
148 if partition_variants op= ["a", "b", "b", "b", "c", "c"] = [
150 (1, "b"), (2, "b"), (3, "b"),
151 (1, "c"), (2, "c")] then () else error "O_Model.partition_variants CHANGED 3";
154 "----------- fun add_enumerate -----------------------------------------------------------------";
155 "----------- fun add_enumerate -----------------------------------------------------------------";
156 "----------- fun add_enumerate -----------------------------------------------------------------";
157 val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
158 val xxx = add_enumerate xs;
160 if add_enumerate xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]
161 then () else error "fun add_enumerate CHANGED";
164 "----------- fun filter_vat --------------------------------------------------------------------";
165 "----------- fun filter_vat --------------------------------------------------------------------";
166 "----------- fun filter_vat --------------------------------------------------------------------";
168 "fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
169 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
170 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
171 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
172 (* \<up> these are the elements for the root-problem (in variants)*)
173 (*vvv these are elements required for subproblems*)
174 "boundVariable a", "boundVariable b", "boundVariable alpha",
175 "interval {x::real. 0 <= x & x <= 2*r}",
176 "interval {x::real. 0 <= x & x <= 2*r}",
177 "interval {x::real. 0 <= x & x <= pi}",
178 "errorBound (eps=(0::real))"]
179 val pbt as {model = model,...} =
180 Problem.from_store @{context} ["maximum_of", "function"];
181 val (o_model, ctxt) = O_Model.init @{theory} formalise model;
185 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
186 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
187 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
188 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
189 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
190 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
191 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
192 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
193 (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
194 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
195 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
197 | _ => error "fun O_Model.init CHANGED";
199 (*/------- unused code -----------------------------------------------------------------------\*)
200 fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;
201 filter_vat : O_Model.T -> int -> O_Model.T;
202 (*\------- unused code -----------------------------------------------------------------------/*)
204 val filtered = map (filter_vat o_model) [1,2,3];
205 (*DIFFERENT ARGUMENT HERE \<up> \<up> ^ DOES not CHANGE ANYTHING .. ?error?*)
209 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
210 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
211 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
212 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
213 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
214 (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
215 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
217 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
218 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
219 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
220 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
221 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
222 (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),
223 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
225 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),
226 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
227 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
228 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
229 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
230 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
231 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
233 | _ => error "fun O_Model.filter_vat CHANGED";
236 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
237 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
238 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
239 val trm = ("1", (TermC.empty, @{term "v'i'"}));
240 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 1";
241 val trm = ("1", (TermC.empty, @{term "e_e"}));
242 if O_Model.is_copy_named trm then error "regr. O_Model.is_copy_named 2" else ();
243 val trm = ("1", (TermC.empty, @{term "L'''"}));
244 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 3";
246 (* out-comment 'structure CalcHead'...
247 val trm = (1, (2, @{term "v'i'"}));
248 if is_copy_named_generating trm then () else error "regr. O_Model.is_copy_named";
249 val trm = (1, (2, @{term "L'''"}));
250 if is_copy_named_generating trm then error "regr. O_Model.is_copy_named" else ();
253 "----------- .. CONTINUED regr.test fun O_Model.copy_name -------------------=------------------";
254 "----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";
255 "----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";
256 (*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*)
257 (*the model-pattern, O_Model.is_copy_named are filter_out*)
258 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
259 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
260 (*the model specific for an example*)
261 val oris = [([1], "#Given", @{term "equality"} , [ParseC.parse_test @{context} "x+1= 2"]),
262 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
263 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
264 (*...all must be true*)
266 case O_Model.copy_name pbt oris (hd cy) of
267 ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
268 | _ => error "calchead.sml regr.test O_Model.copy_name-1-";
270 (*new data: O_Model.copy_name without changing the name*)
271 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
272 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
273 @{term "solution"}; type_of @{term "ss''' :: bool list"};
274 (*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*)
275 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
276 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
277 (*the model specific for an example*)
278 val oris = [([1], "#Given", @{term "equalities"} ,[ParseC.parse_test @{context} "[x_1+1=2,x_2=0]"]),
279 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
280 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
281 (*could be more than 1*)];
283 case O_Model.copy_name pbt oris (hd cy) of
284 ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
285 | _ => error "calchead.sml regr.test O_Model.copy_name-2-";