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 mark --------------------------------------------------------------------------";
11 "----------- fun coll_variants -----------------------------------------------------------------";
12 "----------- fun add_enumerate ------------------------------------------------------------------------";
13 "----------- fun filter_vat --------------------------------------------------------------------";
14 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
15 "----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
17 "-----------------------------------------------------------------------------------------------";
18 "-----------------------------------------------------------------------------------------------";
20 "----------- fun init for O_Model.T ------------------------------------------------------------";
21 "----------- fun init for O_Model.T ------------------------------------------------------------";
22 "----------- fun init for O_Model.T ------------------------------------------------------------";
24 val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
25 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
26 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
27 "AbleitungBiegelinie dy"];
28 val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
29 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
31 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp)] = [(f_model, f_spec)];
33 (* val ((pt, p), tacis) =*)
34 Step_Specify.nxt_specify_init_calc (fmz, sp);
35 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
36 val thy = ThyC.get_theory dI;
37 (*if*) mI = ["no_met"] (*else*);
38 val (pI, pors, mI) = (pI, Problem.from_store pI |> #ppc |> init thy fmz, mI);
40 (*+*)Problem.from_store pI: Problem.T;
41 (*+*)(Problem.from_store pI |> #ppc): Model_Pattern.T;
43 (*+*)val o_model = (Problem.from_store pI |> #ppc |>
44 O_Model.init thy fmz);
45 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store pI |> #ppc);
46 val ori = (map (fn str => str
47 |> TermC.parseNEW'' thy
48 |> Input_Descript.split
49 |> add_field thy pbt) fmz)
53 (*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
54 (*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
55 (*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
56 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
57 (*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),
58 ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),
59 ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),
60 ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),
61 [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $
62 Const (\<^const_name>\<open>Nil\<close>, _),
63 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $
64 Const (\<^const_name>\<open>Nil\<close>, _),
65 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"0"*)) $
66 Const (\<^const_name>\<open>Nil\<close>, _),
67 Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ Free ("L", _)) $ _(*"0"*)) $
68 Const (\<^const_name>\<open>Nil\<close>, _)]),
69 ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
72 |> TermC.parseNEW'' thy
73 |> Input_Descript.split
74 |> add_field thy pbt) fmz);
75 (*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
76 _, _, _, _, _, _] = add_variants ddd;
78 val maxv = map fst ori |> max;
79 val maxv = if maxv = 0 then 1 else maxv;
82 |> map (replace_0 maxv |> apfst)
87 (*+*)val fff as [([0], ("#Given", _, _)), _, _, _, _, _, _] = ori |> coll_variants;
88 (*+*)val ggg as [([1], ("#Given", _, _)), _, _, _, _, _, _] = fff |> map (replace_0 maxv |> apfst);
89 (*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_enumerate;
90 (*+*)val iii = hhh |> map flattup;
91 (*+*)val iii as [(1, [1], "#Given", _, _), (2, [1], "#Given", _, _), _, _, _, _, _] = hhh |> map flattup;
93 (oris, ctxt) (*return from O_Model.init*);
94 "~~~~~ from fun O_Model.init \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);
97 (*+*)if O_Model.to_string pors = "[\n" ^
98 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
99 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
100 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
101 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
102 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
103 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
104 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
105 then () else error "O_Model.init CHANGED";
108 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
109 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
110 "----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";
111 val ctxt = ContextC.initialise' thy f_model;
112 case parseNEW ctxt "L" of
113 SOME (Free ("L", Type (\<^type_name>\<open>real\<close>, []))) => ()
114 | _ => error "ContextC.initialise' CHANGED";
116 "----------- fun mark --------------------------------------------------------------------------";
117 "----------- fun mark --------------------------------------------------------------------------";
118 "----------- fun mark --------------------------------------------------------------------------";
119 val xs = [1,1,1,2,4,4,5];
120 val xxx = mark (op=) xs;
121 if xxx = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
122 then () else error "fun mark CHANGED";
124 "----------- fun coll_variants -----------------------------------------------------------------";
125 "----------- fun coll_variants -----------------------------------------------------------------";
126 "----------- fun coll_variants -----------------------------------------------------------------";
127 val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
129 if coll_variants xs = [([1, 2, 3], 1), ([0], 2), ([1, 2], 4), ([0], 5)]
130 then () else error "fun coll_variants CHANGED";
132 "----------- fun add_enumerate ------------------------------------------------------------------------";
133 "----------- fun add_enumerate ------------------------------------------------------------------------";
134 "----------- fun add_enumerate ------------------------------------------------------------------------";
135 val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
136 val xxx = add_enumerate xs;
138 if add_enumerate xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]
139 then () else error "fun add_enumerate CHANGED";
142 "----------- fun filter_vat --------------------------------------------------------------------";
143 "----------- fun filter_vat --------------------------------------------------------------------";
144 "----------- fun filter_vat --------------------------------------------------------------------";
146 "fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
147 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
148 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
149 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
150 (* \<up> these are the elements for the root-problem (in variants)*)
151 (*vvv these are elements required for subproblems*)
152 "boundVariable a", "boundVariable b", "boundVariable alpha",
153 "interval {x::real. 0 <= x & x <= 2*r}",
154 "interval {x::real. 0 <= x & x <= 2*r}",
155 "interval {x::real. 0 <= x & x <= pi}",
156 "errorBound (eps=(0::real))"]
157 val pbt as {ppc = ppc,...} =
158 Problem.from_store ["maximum_of", "function"];
159 val o_model = O_Model.init @{theory} formalise ppc;
163 (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>, _)) $ _]),
164 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
165 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
166 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
167 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
168 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
169 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
170 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
171 (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>, _) $ _ $ _)]),
172 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
173 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
175 | _ => error "fun O_Model.init CHANGED";
177 (*/------- unused code -----------------------------------------------------------------------\*)
178 fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;
179 filter_vat : O_Model.T -> int -> O_Model.T;
180 (*\------- unused code -----------------------------------------------------------------------/*)
182 val filtered = map (filter_vat o_model) [1,2,3];
183 (*DIFFERENT ARGUMENT HERE \<up> \<up> ^ DOES not CHANGE ANYTHING .. ?error?*)
187 (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>, _)) $ _]),
188 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
189 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
190 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
191 (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),
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 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
195 (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>, _)) $ _]),
196 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
197 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
198 (4, [1, 2], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
199 (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),
200 (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>, _) $ _ $ _)]),
201 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
203 (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>, _)) $ _]),
204 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]),
205 (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),
206 (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),
207 (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),
208 (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),
209 (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])
211 | _ => error "fun O_Model.filter_vat CHANGED";
214 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
215 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
216 "----------- regression test fun O_Model.is_copy_named -----------------------------------------";
217 val trm = ("1", (TermC.empty, @{term "v'i'"}));
218 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 1";
219 val trm = ("1", (TermC.empty, @{term "e_e"}));
220 if O_Model.is_copy_named trm then error "regr. O_Model.is_copy_named 2" else ();
221 val trm = ("1", (TermC.empty, @{term "L'''"}));
222 if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 3";
224 (* out-comment 'structure CalcHead'...
225 val trm = (1, (2, @{term "v'i'"}));
226 if is_copy_named_generating trm then () else error "regr. O_Model.is_copy_named";
227 val trm = (1, (2, @{term "L'''"}));
228 if is_copy_named_generating trm then error "regr. O_Model.is_copy_named" else ();
231 "----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
232 "----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
233 "----------- .. CONTINUED regr.test fun O_Model.cpy_nam ----------------------------------------";
234 (*data from above - M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!)-:*)
235 (*the model-pattern, O_Model.is_copy_named are filter_out*)
236 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
237 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
238 (*the model specific for an example*)
239 val oris = [([1], "#Given", @{term "equality"} , [TermC.str2term "x+1= 2"]),
240 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
241 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
242 (*...all must be true*)
244 case O_Model.cpy_nam pbt oris (hd cy) of
245 ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()
246 | _ => error "calchead.sml regr.test O_Model.cpy_nam-1-";
248 (*new data: O_Model.cpy_nam without changing the name*)
249 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
250 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
251 @{term "solution"}; type_of @{term "ss''' :: bool list"};
252 (*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*)
253 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
254 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
255 (*the model specific for an example*)
256 val oris = [([1], "#Given", @{term "equalities"} ,[TermC.str2term "[x_1+1=2,x_2=0]"]),
257 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
258 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
259 (*could be more than 1*)];
261 case O_Model.cpy_nam pbt oris (hd cy) of
262 ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
263 | _ => error "calchead.sml regr.test O_Model.cpy_nam-2-";