1 (* Title: "Specify/m-match.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- fun match_pbl ---------------------------------------------------------------------";
10 "----------- fun match_oris --------------------------------------------------------------------";
11 "----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
17 "----------- fun match_pbl ---------------------------------------------------------------------";
18 "----------- fun match_pbl ---------------------------------------------------------------------";
19 "----------- fun match_pbl ---------------------------------------------------------------------";
20 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
21 "solveFor x", "errorBound (eps=0)", "solutions L"];
22 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
23 Problem.from_store @{context} ["univariate", "equation"];
24 val xxx = M_Match.match_pbl fmz pbt;
28 {Find = [Correct "solutions L"],
30 Correct "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))",
32 Superfl "errorBound (eps = (0::'a))"],
34 Where = [Correct "matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"],
36 | _ => error "M_Match.match_pbl CHANGED";
39 "----------- fun match_oris --------------------------------------------------------------------";
40 "----------- fun match_oris --------------------------------------------------------------------";
41 "----------- fun match_oris --------------------------------------------------------------------";
42 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
43 "solveFor x", "errorBound (eps=0)", "solutions L"];
44 val pbt as {ppc = ppc,...} =
45 Problem.from_store @{context} ["univariate", "equation"];
46 val o_model = O_Model.init @{theory} fmz ppc
47 val py = Problem.from_store @{context} ["equation"];
48 val py = Problem.from_store @{context} ["univariate", "equation"];
49 val py = Problem.from_store @{context} ["sq", "rootX", "univariate", "equation"];
51 if match_oris @{theory} (#prls py) o_model (#ppc py, #where_ py)
52 then () else error "fun match_oris CHANGED";
55 "----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ------------=-------";
56 "----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ------------=-------";
57 "----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";
58 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
59 (Const (\<^const_name>\<open>Pair\<close>,_) $
61 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
62 (*...copied from LItool.tac_from_prog*)
63 TermC.parse_test @{context} (
64 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
65 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^
66 " REAL_LIST [c, c_2]]");
67 val ags = isalist2list ags';
68 val pI = ["LINEAR", "system"];
69 val pats = (#ppc o Problem.from_store @{context}) pI;
70 "-a1-----------------------------------------------------";
71 (*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)
72 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
73 "-a2-----------------------------------------------------";
74 case M_Match.arguments @{theory "Isac_Knowledge"} pats ags of
75 [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
76 (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
77 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
78 (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
80 | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";
82 "-b------------------------------------------------------";
83 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
84 (Const (\<^const_name>\<open>Pair\<close>,_) $
86 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
87 (*...copied from LItool.tac_from_prog*)
88 TermC.parse_test @{context} (
89 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
90 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^
91 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
92 val ags = isalist2list ags';
93 val pI = ["LINEAR", "system"];
94 val pats = (#ppc o Problem.from_store @{context}) pI;
95 "-b1-----------------------------------------------------";
96 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
97 "-b2-----------------------------------------------------";
98 case M_Match.arguments @{theory "EqSystem"} pats ags of
99 [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
100 (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
101 [_ $ Free ("c", _) $ _,
102 _ $ Free ("c_2", _) $ _]),
103 (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
104 (* type of Find: [Free ("ss'''", "bool List.list")]*)
106 | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";
108 "-c---ERROR case: stac is missing #Given equalities e_s--";
109 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
110 (Const (\<^const_name>\<open>Pair\<close>,_) $
112 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
113 (*...copied from LItool.tac_from_prog*)
114 TermC.parse_test @{context} (
115 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
116 " [REAL_LIST [c, c_2]]");
117 val ags = isalist2list ags';
118 val pI = ["LINEAR", "system"];
119 val pats = (#ppc o Problem.from_store @{context}) pI;
120 (*============ inhibit exn AK110726 ==============================================
121 val xxx - M_Match.arguments (theory "EqSystem") pats ags;
122 ============ inhibit exn AK110726 ==============================================*)
123 "-c1-----------------------------------------------------";
124 "--------------------------step through code M_Match.arguments---";
125 val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);
126 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
127 val pbt' = filter_out O_Model.is_copy_named pbt; (*=equalities, solveForVars*)
128 val cy = filter O_Model.is_copy_named pbt; (*=solution*)
129 (*============ inhibit exn AK110726 ==============================================
130 val oris' - O_Model.matc thy pbt' ags [];
131 ============ inhibit exn AK110726 ==============================================*)
132 "-------------------------------step through code O_Model.matc---";
133 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
134 (O_Model.is_copy_named' o free2str) t;
136 (*============ inhibit exn AK110726 ==============================================
137 val opt - mtc thy p a;
138 ============ inhibit exn AK110726 ==============================================*)
139 "--------------------------------step through code mtc---";
140 val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
142 val ttt = (dsc $ var);
143 (*============ inhibit exn AK110726 ==============================================
144 Thm.global_cterm_of thy (dsc $ var);
145 ============ inhibit exn AK110726 ==============================================*)
147 "-------------------------------------step through end---";
148 "--------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)--";
149 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
150 (Const (\<^const_name>\<open>Pair\<close>,_) $
152 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
153 (*...copied from LItool.tac_from_prog*)
154 TermC.parse_test @{context} (
155 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
156 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^
157 " REAL_LIST [c, c_2]]");
158 val ags = isalist2list ags';
159 val pI = ["LINEAR", "system"];
160 val pats = (#ppc o Problem.from_store @{context}) pI;
161 "-a1-----------------------------------------------------";
162 (*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)
163 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
164 "-a2-----------------------------------------------------";
165 case M_Match.arguments @{theory "Isac_Knowledge"} pats ags of
166 [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
167 (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
168 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
169 (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
171 | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";
173 "-b------------------------------------------------------";
174 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
175 (Const (\<^const_name>\<open>Pair\<close>,_) $
177 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
178 (*...copied from LItool.tac_from_prog*)
179 TermC.parse_test @{context} (
180 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
181 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^
182 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
183 val ags = isalist2list ags';
184 val pI = ["LINEAR", "system"];
185 val pats = (#ppc o Problem.from_store @{context}) pI;
186 "-b1-----------------------------------------------------";
187 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
188 "-b2-----------------------------------------------------";
189 case M_Match.arguments @{theory "EqSystem"} pats ags of
190 [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),
191 (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),
192 [_ $ Free ("c", _) $ _,
193 _ $ Free ("c_2", _) $ _]),
194 (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]
195 (* type of Find: [Free ("ss'''", "bool List.list")]*)
197 | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";
199 "-c---ERROR case: stac is missing #Given equalities e_s--";
200 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
201 (Const (\<^const_name>\<open>Pair\<close>,_) $
203 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
204 (*...copied from LItool.tac_from_prog*)
205 TermC.parse_test @{context} (
206 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
207 " [REAL_LIST [c, c_2]]");
208 val ags = isalist2list ags';
209 val pI = ["LINEAR", "system"];
210 val pats = (#ppc o Problem.from_store @{context}) pI;
211 (*============ inhibit exn AK110726 ==============================================
212 val xxx - M_Match.arguments (theory "EqSystem") pats ags;
213 -------------------------------------------------------------------*)
214 "-c1-----------------------------------------------------";
215 "--------------------------step through code M_Match.arguments---";
216 val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);
217 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
218 val pbt' = filter_out O_Model.is_copy_named pbt; (*=equalities, solveForVars*)
219 val cy = filter O_Model.is_copy_named pbt; (*=solution*)
220 (*============ inhibit exn AK110726 ==============================================
221 val oris' - O_Model.matc thy pbt' ags [];
222 -------------------------------------------------------------------*)
223 "-------------------------------step through code O_Model.matc---";
224 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
225 (O_Model.is_copy_named' o free2str) t;
227 (*============ inhibit exn AK110726 ==============================================
228 val opt - mtc thy p a;
229 -------------------------------------------------------------------*)
230 "--------------------------------step through code mtc---";
231 val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
233 val ttt = (dsc $ var);
234 (*============ inhibit exn AK110726 ==============================================
235 Thm.global_cterm_of thy (dsc $ var);
236 -------------------------------------------------------------------*)
237 "-------------------------------------step through end---";
239 case ((M_Match.arguments @{theory "EqSystem"} pats ags)
240 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
241 [] => M_Match.arguments_msg @{context} pI stac ags
242 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
244 "-d------------------------------------------------------";
245 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $
246 (Const (\<^const_name>\<open>Pair\<close>,_) $
248 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
249 (*...copied from LItool.tac_from_prog*)
250 TermC.parse_test @{context} (
251 "SubProblem (TestX,[univariate,equation,test]," ^
252 " [no_met]) [BOOL (x+1=2), REAL x]");
253 val AGS = isalist2list ags';
254 val pI = ["univariate", "equation", "test"];
257 case ((M_Match.arguments @{theory "EqSystem"} pats ags)
258 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
259 [] => M_Match.arguments_msg @{context} pI stac ags
260 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
262 "-d------------------------------------------------------";
263 val stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $
264 (Const (\<^const_name>\<open>Pair\<close>,_) $
266 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =
267 (*...copied from LItool.tac_from_prog*)
268 TermC.parse_test @{context} (
269 "SubProblem (TestX,[univariate,equation,test]," ^
270 " [no_met]) [BOOL (x+1=2), REAL x]");
271 val AGS = isalist2list ags';
272 val pI = ["univariate", "equation", "test"];
273 val PATS = (#ppc o Problem.from_store @{context}) pI;
274 "-d1-----------------------------------------------------";
275 "--------------------------step through code M_Match.arguments---";
276 val (thy, pbt: Model_Pattern.T, ags) = (@{theory "Test"}, PATS, AGS);
277 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
278 val pbt' = filter_out O_Model.is_copy_named pbt;
279 val cy = filter O_Model.is_copy_named pbt;
280 val oris' = M_Match.matc thy pbt' ags [];
281 "-------------------------------step through code O_Model.matc---";
282 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
283 (O_Model.is_copy_named' o free2str) t;
285 val opt = mtc thy p a;
286 "--------------------------------step through code mtc---";
287 val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
288 val ttt = (dsc $ var);
289 Thm.global_cterm_of thy (dsc $ var);
290 val ori = ((([1], str, dsc, (*[var]*) Input_Descript.split' (dsc, var))): O_Model.preori);
292 "-d2-----------------------------------------------------";
294 "-------------------------------step through code O_Model.matc---";
295 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
296 (O_Model.is_copy_named' o free2str) t;
298 val opt = mtc thy p a;
299 "--------------------------------step through code mtc---";
300 val (thy, (str, (dsc, _)):Model_Pattern.single, ty $ var) = (thy, p, a);
301 val ttt = (dsc $ var);
302 Thm.global_cterm_of thy (dsc $ var);
303 val ori = ((([1], str, dsc, (*[var]*) Input_Descript.split' (dsc, var))): O_Model.preori);
304 "-d3-----------------------------------------------------";
305 pbt = []; (*true, base case*)
306 "-----------------continue step through code M_Match.arguments---";
307 val oris' = oris @ [ori]; (*result 2 oris, O_Model.copy_name added later*)
308 "--------------------------------step through O_Model.copy_name----";
309 val (pbt, oris, p as (field, (dsc, t)):Model_Pattern.single) = (pbt', oris', hd cy);
310 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
311 "--------------------------------------------------------";
312 fun is_copy_named_generating_idstr str =
313 if O_Model.is_copy_named' str
314 then case (rev o Symbol.explode) str of
315 (*"_"::"_"::"_"::_ => false*)
316 "'"::"'"::"'"::_ => false
319 fun is_copy_named_generating (_, (_, t)) =
320 (is_copy_named_generating_idstr o free2str) t;
321 "--------------------------------------------------------";
322 is_copy_named_generating p (*true*);
323 fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts);
324 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
326 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
328 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
329 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
330 val vals = map sel oris;
331 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
333 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
334 (LibraryC.assoc (vars'~~vals, cy'));
335 (*SOME (Free ("x", "Real.real")) : term option*)
336 val cy_ext = (free2str o the) (LibraryC.assoc (vars'~~vals, cy'))^"_"^ext;
338 "-----------------continue step through code M_Match.arguments---";
339 val cy' = map (O_Model.copy_name pbt' oris') cy;
340 (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
341 "-------------------------------------step through end---";
343 case M_Match.arguments thy PATS AGS of
344 [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equality\<close>, _),
345 [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $
346 Free ("x", _) $ _(*1*)) $ _(*1*)]),
347 (2, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, _), [Free ("x", _)]),
348 (3, [1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)])]
350 | _ => error "calchead.sml M_Match.arguments [univariate,equation,test]--";