|
1 (* intermediately stores !ptyps |
|
2 WN.16.9.01 |
|
3 use"tests/refine.sml"; |
|
4 *) |
|
5 |
|
6 |
|
7 "----------------------- store test-pbtyps ----------------------------"; |
|
8 "----------------------- refin test-pbtyps ----------------------------"; |
|
9 "----------------------- refine_ori test-pbtyps ----------------------------"; |
|
10 "----------------------- refine test-pbtyps ----------------------------"; |
|
11 "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------"; |
|
12 |
|
13 |
|
14 |
|
15 |
|
16 "----------------------- store test-pbtyps ----------------------------"; |
|
17 val intermediate_ptyps = !ptyps; |
|
18 ptyps:= ([]:ptyps); |
|
19 |
|
20 store_pbt |
|
21 (prep_pbt DiffApp.thy |
|
22 (["pbla"], |
|
23 [("#Given", ["fixedValues a_"])], e_rls, None, [])); |
|
24 store_pbt |
|
25 (prep_pbt DiffApp.thy |
|
26 (["pbla1","pbla"], |
|
27 [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, None, [])); |
|
28 store_pbt |
|
29 (prep_pbt DiffApp.thy |
|
30 (["pbla2","pbla"], |
|
31 [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, None, [])); |
|
32 store_pbt |
|
33 (prep_pbt DiffApp.thy |
|
34 (["pbla2x","pbla2","pbla"], |
|
35 [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])], |
|
36 e_rls, None, [])); |
|
37 store_pbt |
|
38 (prep_pbt DiffApp.thy |
|
39 (["pbla2y","pbla2","pbla"], |
|
40 [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])], |
|
41 e_rls, None, [])); |
|
42 store_pbt |
|
43 (prep_pbt DiffApp.thy |
|
44 (["pbla2z","pbla2","pbla"], |
|
45 [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])], |
|
46 e_rls, None, [])); |
|
47 store_pbt |
|
48 (prep_pbt DiffApp.thy |
|
49 (["pbla3","pbla"], |
|
50 [("#Given" ,["fixedValues a_","relations a3_"])], |
|
51 e_rls, None, [])); |
|
52 |
|
53 show_ptyps(); |
|
54 |
|
55 (*case 1: no refinement *) |
|
56 val thy = Isac.thy; |
|
57 val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy)) |
|
58 "fixedValues [aaa=0]"); |
|
59 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) |
|
60 "errorBound (ddd=0)"); |
|
61 val ori1 = [(1,[1],"#Given",d1,ts1), |
|
62 (2,[1],"#Given",d2,ts2)]:ori list; |
|
63 |
|
64 |
|
65 (*case 2: refined to pbt without children *) |
|
66 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) |
|
67 "relations aaa333"); |
|
68 val ori2 = [(1,[1],"#Given",d1,ts1), |
|
69 (2,[1],"#Given",d2,ts2)]:ori list; |
|
70 |
|
71 |
|
72 (*case 3: refined to pbt with children *) |
|
73 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) |
|
74 "valuesFor aaa222"); |
|
75 val ori3 = [(1,[1],"#Given",d1,ts1), |
|
76 (2,[1],"#Given",d2,ts2)]:ori list; |
|
77 |
|
78 |
|
79 (*case 4: refined to children (without child)*) |
|
80 val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy)) |
|
81 "boundVariable aaa222yyy"); |
|
82 val ori4 = [(1,[1],"#Given",d1,ts1), |
|
83 (2,[1],"#Given",d2,ts2), |
|
84 (3,[1],"#Given",d3,ts3)]:ori list; |
|
85 |
|
86 "----------------------- refin test-pbtyps ----------------------------"; |
|
87 |
|
88 (*case 1: no refinement *) |
|
89 refin [] ori1 (hd (!ptyps)); |
|
90 (*val it = Some ["pbla"] : pblID option*) |
|
91 |
|
92 (*case 2: refined to pbt without children *) |
|
93 refin [] ori2 (hd (!ptyps)); |
|
94 (*val it = Some ["pbla","pbla3"] : pblID option*) |
|
95 |
|
96 (*case 3: refined to pbt with children *) |
|
97 refin [] ori3 (hd (!ptyps)); |
|
98 (*val it = Some ["pbla","pbla2"] : pblID option*) |
|
99 |
|
100 (*case 4: refined to children (without child)*) |
|
101 refin [] ori4 (hd (!ptyps)); |
|
102 (*val it = Some ["pbla","pbla2","pbla2y"] : pblID option*) |
|
103 |
|
104 (*case 5: start refinement somewhere in ptyps*) |
|
105 val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps; |
|
106 refin ["pbla"] ori4 ppp; |
|
107 (*val it = Some ["pbla2","pbla2y"] : pblRD option*) |
|
108 |
|
109 |
|
110 "----------------------- refine_ori test-pbtyps ----------------------------"; |
|
111 |
|
112 (*case 1: no refinement *) |
|
113 refine_ori ori1 ["pbla"]; |
|
114 (*val it = None : pblID option !!!!*) |
|
115 |
|
116 (*case 2: refined to pbt without children *) |
|
117 refine_ori ori2 ["pbla"]; |
|
118 (*val it = Some ["pbla3","pbla"] : pblID option*) |
|
119 |
|
120 (*case 3: refined to pbt with children *) |
|
121 refine_ori ori3 ["pbla"]; |
|
122 (*val it = Some ["pbla2","pbla"] : pblID option*) |
|
123 |
|
124 (*case 4: refined to children (without child)*) |
|
125 val opt = refine_ori ori4 ["pbla"]; |
|
126 if opt = Some ["pbla2y","pbla2","pbla"] then () |
|
127 else raise error "new behaviour in refine.sml case 4"; |
|
128 |
|
129 (*case 5: start refinement somewhere in ptyps*) |
|
130 refine_ori ori4 ["pbla2","pbla"]; |
|
131 (*val it = Some ["pbla2y","pbla2","pbla"] : pblID option*) |
|
132 |
|
133 |
|
134 "----------------------- refine test-pbtyps ----------------------------"; |
|
135 |
|
136 val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"]; |
|
137 val fmz2 = ["fixedValues [aaa=0]","relations aaa333"]; |
|
138 val fmz3 = ["fixedValues [aaa=0]","valuesFor aaa222"]; |
|
139 val fmz4 = ["fixedValues [aaa=0]","valuesFor aaa222", |
|
140 "boundVariable aaa222yyy"]; |
|
141 |
|
142 (*case 1: no refinement *) |
|
143 refine fmz1 ["pbla"]; |
|
144 (* |
|
145 *** pass ["pbla"] |
|
146 *** pass ["pbla","pbla1"] |
|
147 *** pass ["pbla","pbla2"] |
|
148 *** pass ["pbla","pbla3"] |
|
149 val it = |
|
150 [Matches |
|
151 (["pbla"], |
|
152 {Find=[], |
|
153 Given=[Correct "fixedValues [aaa = #0]", |
|
154 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), |
|
155 NoMatch |
|
156 (["pbla1","pbla"], |
|
157 {Find=[], |
|
158 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", |
|
159 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), |
|
160 NoMatch |
|
161 (["pbla2","pbla"], |
|
162 {Find=[], |
|
163 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", |
|
164 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), |
|
165 NoMatch |
|
166 (["pbla3","pbla"], |
|
167 {Find=[], |
|
168 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", |
|
169 Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})] |
|
170 : match list*) |
|
171 |
|
172 (*case 2: refined to pbt without children *) |
|
173 refine fmz2 ["pbla"]; |
|
174 (* |
|
175 *** pass ["pbla"] |
|
176 *** pass ["pbla","pbla1"] |
|
177 *** pass ["pbla","pbla2"] |
|
178 *** pass ["pbla","pbla3"] |
|
179 val it = |
|
180 [Matches |
|
181 (["pbla"], |
|
182 {Find=[], |
|
183 Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"], |
|
184 Relate=[],Where=[],With=[]}), |
|
185 NoMatch |
|
186 (["pbla1","pbla"], |
|
187 {Find=[], |
|
188 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", |
|
189 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), |
|
190 NoMatch |
|
191 (["pbla2","pbla"], |
|
192 {Find=[], |
|
193 Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", |
|
194 Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), |
|
195 Matches |
|
196 (["pbla3","pbla"], |
|
197 {Find=[], |
|
198 Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"], |
|
199 Relate=[],Where=[],With=[]})] : match list*) |
|
200 |
|
201 (*case 3: refined to pbt with children *) |
|
202 refine fmz3 ["pbla"]; |
|
203 (* |
|
204 *** pass ["pbla"] |
|
205 *** pass ["pbla","pbla1"] |
|
206 *** pass ["pbla","pbla2"] |
|
207 *** pass ["pbla","pbla2","pbla2x"] |
|
208 *** pass ["pbla","pbla2","pbla2y"] |
|
209 *** pass ["pbla","pbla2","pbla2z"] |
|
210 *** pass ["pbla","pbla3"] |
|
211 val it = |
|
212 [Matches |
|
213 (["pbla"], |
|
214 {Find=[], |
|
215 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"], |
|
216 Relate=[],Where=[],With=[]}), |
|
217 NoMatch |
|
218 (["pbla1","pbla"], |
|
219 {Find=[], |
|
220 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", |
|
221 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}), |
|
222 Matches |
|
223 (["pbla2","pbla"], |
|
224 {Find=[], |
|
225 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"], |
|
226 Relate=[],Where=[],With=[]}), |
|
227 NoMatch |
|
228 (["pbla2x","pbla2","pbla"], |
|
229 {Find=[], |
|
230 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
231 Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}), |
|
232 NoMatch |
|
233 (["pbla2y","pbla2","pbla"], |
|
234 {Find=[], |
|
235 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
236 Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}), |
|
237 NoMatch |
|
238 (["pbla2z","pbla2","pbla"], |
|
239 {Find=[], |
|
240 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
241 Missing "interval a2z_"],Relate=[],Where=[],With=[]}), |
|
242 NoMatch |
|
243 (["pbla3","pbla"], |
|
244 {Find=[], |
|
245 Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", |
|
246 Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})] |
|
247 : match list*) |
|
248 |
|
249 (*case 4: refined to children (without child)*) |
|
250 refine fmz4 ["pbla"]; |
|
251 (* |
|
252 *** pass ["pbla"] |
|
253 *** pass ["pbla","pbla1"] |
|
254 *** pass ["pbla","pbla2"] |
|
255 *** pass ["pbla","pbla2","pbla2x"] |
|
256 *** pass ["pbla","pbla2","pbla2y"] |
|
257 val it = |
|
258 [Matches |
|
259 (["pbla"], |
|
260 {Find=[], |
|
261 Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222", |
|
262 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), |
|
263 NoMatch |
|
264 (["pbla1","pbla"], |
|
265 {Find=[], |
|
266 Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", |
|
267 Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"], |
|
268 Relate=[],Where=[],With=[]}), |
|
269 Matches |
|
270 (["pbla2","pbla"], |
|
271 {Find=[], |
|
272 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
273 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), |
|
274 NoMatch |
|
275 (["pbla2x","pbla2","pbla"], |
|
276 {Find=[], |
|
277 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
278 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], |
|
279 Relate=[],Where=[],With=[]}), |
|
280 Matches |
|
281 (["pbla2y","pbla2","pbla"], |
|
282 {Find=[], |
|
283 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
284 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})] |
|
285 : match list*) |
|
286 |
|
287 (*case 5: start refinement somewhere in ptyps*) |
|
288 refine fmz4 ["pbla2","pbla"]; |
|
289 (* |
|
290 *** pass ["pbla","pbla2"] |
|
291 *** pass ["pbla","pbla2","pbla2x"] |
|
292 *** pass ["pbla","pbla2","pbla2y"] |
|
293 val it = |
|
294 [Matches |
|
295 (["pbla2","pbla"], |
|
296 {Find=[], |
|
297 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
298 Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), |
|
299 NoMatch |
|
300 (["pbla2x","pbla2","pbla"], |
|
301 {Find=[], |
|
302 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
303 Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], |
|
304 Relate=[],Where=[],With=[]}), |
|
305 Matches |
|
306 (["pbla2y","pbla2","pbla"], |
|
307 {Find=[], |
|
308 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", |
|
309 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})] |
|
310 : match list*) |
|
311 |
|
312 |
|
313 ptyps:= intermediate_ptyps; |
|
314 show_ptyps(); |
|
315 |
|
316 |
|
317 |
|
318 "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------"; |
|
319 "----------------refine.sml: miniscript with mini-subpbl -------------"; |
|
320 val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x", |
|
321 "errorBound (eps=0)","solutions L"]; |
|
322 val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
323 ("Test.thy","squ-equ-test-subpbl1")); |
|
324 val p = e_pos'; val c = []; |
|
325 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
326 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
327 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
328 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
329 |
|
330 val nxt = ("Specify_Problem", |
|
331 Specify_Problem ["linear","univariate","equation","test"]); |
|
332 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
333 (*ML> f; |
|
334 val it = Form' (PpcKF (0,EdUndef,0,Nundef, |
|
335 (Problem ["linear","univariate","equation","test"], |
|
336 {Find=[Incompl "solutions []"], |
|
337 Given=[Incompl "errorBound", |
|
338 Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
339 Correct "solveFor x"],Relate=[], |
|
340 Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) |
|
341 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) |
|
342 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) |
|
343 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
344 With=[]}))) : mout |
|
345 |
|
346 val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)")*) |
|
347 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
348 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
349 (*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"] |
|
350 kann nicht gut gehen --------- *) |
|
351 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
352 (*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*) |
|
353 |
|
354 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]); |
|
355 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
356 (*("Specify_Problem",Specify_Problem ["normalize","univariate","equation","test"])*) |
|
357 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
358 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
359 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
360 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
361 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
362 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
363 (*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep |
|
364 in Script "uberdefiniert -^-*) |
|
365 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
366 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation","test"]*) |
|
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
368 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)") *) |
|
369 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
370 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
371 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
372 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
373 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation","test"])*) |
|
374 |
|
375 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]); |
|
376 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
377 (*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*) |
|
378 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
379 (*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*) |
|
380 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
381 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*) |
|
382 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
383 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*) |
|
384 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
385 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
386 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*) |
|
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
388 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*) |
|
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
390 (*("Check_Postcond",Check_Postcond ["normalize","univariate","equation","test"])*) |
|
391 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
392 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
|
393 if (snd nxt)=End_Proof' andalso res="[x = 2]" then () |
|
394 else raise error "new behaviour in test:refine.sml: miniscript with mini-subpbl"; |
|
395 |
|
396 |