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) = CalcTreeTEST [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
32 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp)] = [(f_model, f_spec)];
34 (* val ((pt, p), tacis) =*)
35 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
36 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
37 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
38 Step_Specify.initialise (fmz, (dI, pI, mI));
39 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
40 val thy = ThyC.get_theory dI
41 val ctxt = Proof_Context.init_global thy;
42 (*if*) mI = ["no_met"] (*else*);
43 val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
44 (*+*)Problem.from_store ctxt pI: Problem.T;
45 (*+*)(Problem.from_store ctxt pI |> #ppc): Model_Pattern.T;
47 (*+*)val o_model = (Problem.from_store ctxt pI |> #ppc |>
48 O_Model.init thy fmz);
49 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #ppc);
50 val ori = (map (fn str => str
51 |> TermC.parseNEW'' thy
52 |> Input_Descript.split
53 |> add_field thy pbt) fmz)
57 (*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
58 (*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
59 (*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
60 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
61 (*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),
62 ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
63 ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),
64 ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),
65 [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
66 Const (\<^const_name>\<open>Nil\<close>, _),
67 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
68 Const (\<^const_name>\<open>Nil\<close>, _),
69 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"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>, _) $ Free ("L", _)) $ _(*"0"*)) $
72 Const (\<^const_name>\<open>Nil\<close>, _)]),
73 ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
76 |> TermC.parseNEW'' thy
77 |> Input_Descript.split
78 |> add_field thy pbt) fmz);
79 (*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
80 _, _, _, _, _, _] = add_variants ddd;
82 val maxv = map fst ori |> max_variant;
83 val maxv = if maxv = 0 then 1 else maxv;
85 |> O_Model.collect_variants
86 |> map (replace_0 maxv |> apfst)
91 (*+*)val fff as [([0], ("#Given", _, _)), _, _, _, _, _, _] = ori |> O_Model.collect_variants;
92 (*+*)val ggg as [([1], ("#Given", _, _)), _, _, _, _, _, _] = fff |> map (replace_0 maxv |> apfst);
93 (*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_enumerate;
94 (*+*)val iii = hhh |> map flattup;
95 (*+*)val iii as [(1, [1], "#Given", _, _), (2, [1], "#Given", _, _), _, _, _, _, _] = hhh |> map flattup;
97 (oris, ctxt) (*return from O_Model.init*);
98 "~~~~~ from fun O_Model.init \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);
101 (*+*)if O_Model.to_string pors = "[\n" ^
102 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
103 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
104 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
105 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
106 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
107 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
108 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
109 then () else error "O_Model.init CHANGED";
112 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
113 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
114 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
115 val ctxt = ContextC.initialise' thy f_model;
116 case parseNEW ctxt "L" of
117 SOME (Free ("L", Type (\<^type_name>\<open>real\<close>, []))) => ()
118 | _ => error "ContextC.initialise' CHANGED";
120 "----------- fun partition_variants ------------------------------------------------------------";
121 "----------- fun partition_variants ------------------------------------------------------------";
122 "----------- fun partition_variants ------------------------------------------------------------";
123 val xs = [1,1,1,2,4,4,5];
124 val xxx = partition_variants (op=) xs;
125 if xxx = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
126 then () else error "fun partition_variants CHANGED";
128 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
129 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
130 "----------- fun O_Model.collect_variants -----------------------------------------------------------------";
131 val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
133 if O_Model.collect_variants xs = [([1, 2, 3], 1), ([0], 2), ([1, 2], 4), ([0], 5)]
134 then () else error "fun O_Model.collect_variants CHANGED";
136 (**** fun O_Model.partition_variants #################################################### ****)
137 "----------- fun partition_variants ------------------------------------------------------------";
138 "----------- fun partition_variants ------------------------------------------------------------";
139 if partition_variants op= ["a", "b", "c"] = [(0, "a"), (0, "b"), (0, "c")]
140 then () else error "O_Model.partition_variants CHANGED 1";
142 if partition_variants op= ["a", "b", "b", "b", "c"] = [
144 (1, "b"), (2, "b"), (3, "b"),
145 (0, "c")] then () else error "O_Model.partition_variants CHANGED 2";
147 if partition_variants op= ["a", "b", "b", "b", "c", "c"] = [
149 (1, "b"), (2, "b"), (3, "b"),
150 (1, "c"), (2, "c")] then () else error "O_Model.partition_variants CHANGED 3";
153 "----------- fun add_enumerate -----------------------------------------------------------------";
154 "----------- fun add_enumerate -----------------------------------------------------------------";
155 "----------- fun add_enumerate -----------------------------------------------------------------";
156 val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
157 val xxx = add_enumerate xs;
159 if add_enumerate xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]
160 then () else error "fun add_enumerate CHANGED";
163 "----------- fun filter_vat --------------------------------------------------------------------";
164 "----------- fun filter_vat --------------------------------------------------------------------";
165 "----------- fun filter_vat --------------------------------------------------------------------";
167 "fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
168 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
169 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
170 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
171 (* \<up> these are the elements for the root-problem (in variants)*)
172 (*vvv these are elements required for subproblems*)
173 "boundVariable a", "boundVariable b", "boundVariable alpha",
174 "interval {x::real. 0 <= x & x <= 2*r}",
175 "interval {x::real. 0 <= x & x <= 2*r}",
176 "interval {x::real. 0 <= x & x <= pi}",
177 "errorBound (eps=(0::real))"]
178 val pbt as {ppc = ppc,...} =
179 Problem.from_store @{context} ["maximum_of", "function"];
180 val o_model = O_Model.init @{theory} formalise ppc;
184 (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>, _)) $ _]),
185 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
186 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
187 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
188 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
189 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
190 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
191 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
192 (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>, _) $ _ $ _)]),
193 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
194 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
196 | _ => error "fun O_Model.init CHANGED";
198 (*/------- unused code -----------------------------------------------------------------------\*)
199 fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;
200 filter_vat : O_Model.T -> int -> O_Model.T;
201 (*\------- unused code -----------------------------------------------------------------------/*)
203 val filtered = map (filter_vat o_model) [1,2,3];
204 (*DIFFERENT ARGUMENT HERE \<up> \<up> ^ DOES not CHANGE ANYTHING .. ?error?*)
208 (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>, _)) $ _]),
209 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
210 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
211 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
212 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
213 (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>, _) $ _ $ _)]),
214 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
216 (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>, _)) $ _]),
217 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
218 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
219 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
220 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
221 (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>, _) $ _ $ _)]),
222 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
224 (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>, _)) $ _]),
225 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
226 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
227 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
228 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
229 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
230 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
232 | _ => error "fun O_Model.filter_vat CHANGED";
235 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
236 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
237 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
238 val trm = ("1", (TermC.empty, @{term "v'i'"}));
239 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 1";
240 val trm = ("1", (TermC.empty, @{term "e_e"}));
241 if O_Model.is_copy_named trm then error "regr. O_Model.is_copy_named 2" else ();
242 val trm = ("1", (TermC.empty, @{term "L'''"}));
243 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 3";
245 (* out-comment 'structure CalcHead'...
246 val trm = (1, (2, @{term "v'i'"}));
247 if is_copy_named_generating trm then () else error "regr. O_Model.is_copy_named";
248 val trm = (1, (2, @{term "L'''"}));
249 if is_copy_named_generating trm then error "regr. O_Model.is_copy_named" else ();
252 "----------- .. CONTINUED regr.test fun O_Model.copy_name -------------------=------------------";
253 "----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";
254 "----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";
255 (*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*)
256 (*the model-pattern, O_Model.is_copy_named are filter_out*)
257 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
258 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
259 (*the model specific for an example*)
260 val oris = [([1], "#Given", @{term "equality"} , [TermC.parse_test @{context} "x+1= 2"]),
261 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
262 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
263 (*...all must be true*)
265 case O_Model.copy_name pbt oris (hd cy) of
266 ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
267 | _ => error "calchead.sml regr.test O_Model.copy_name-1-";
269 (*new data: O_Model.copy_name without changing the name*)
270 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
271 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
272 @{term "solution"}; type_of @{term "ss''' :: bool list"};
273 (*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*)
274 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
275 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
276 (*the model specific for an example*)
277 val oris = [([1], "#Given", @{term "equalities"} ,[TermC.parse_test @{context} "[x_1+1=2,x_2=0]"]),
278 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
279 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
280 (*could be more than 1*)];
282 case O_Model.copy_name pbt oris (hd cy) of
283 ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
284 | _ => error "calchead.sml regr.test O_Model.copy_name-2-";