1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/refine.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,396 @@
1.4 +(* intermediately stores !ptyps
1.5 + WN.16.9.01
1.6 + use"tests/refine.sml";
1.7 + *)
1.8 +
1.9 +
1.10 +"----------------------- store test-pbtyps ----------------------------";
1.11 +"----------------------- refin test-pbtyps ----------------------------";
1.12 +"----------------------- refine_ori test-pbtyps ----------------------------";
1.13 +"----------------------- refine test-pbtyps ----------------------------";
1.14 +"----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";
1.15 +
1.16 +
1.17 +
1.18 +
1.19 +"----------------------- store test-pbtyps ----------------------------";
1.20 +val intermediate_ptyps = !ptyps;
1.21 +ptyps:= ([]:ptyps);
1.22 +
1.23 +store_pbt
1.24 + (prep_pbt DiffApp.thy
1.25 + (["pbla"],
1.26 + [("#Given", ["fixedValues a_"])], e_rls, None, []));
1.27 +store_pbt
1.28 + (prep_pbt DiffApp.thy
1.29 + (["pbla1","pbla"],
1.30 + [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, None, []));
1.31 +store_pbt
1.32 + (prep_pbt DiffApp.thy
1.33 + (["pbla2","pbla"],
1.34 + [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, None, []));
1.35 +store_pbt
1.36 + (prep_pbt DiffApp.thy
1.37 + (["pbla2x","pbla2","pbla"],
1.38 + [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])],
1.39 + e_rls, None, []));
1.40 +store_pbt
1.41 + (prep_pbt DiffApp.thy
1.42 + (["pbla2y","pbla2","pbla"],
1.43 + [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])],
1.44 + e_rls, None, []));
1.45 +store_pbt
1.46 + (prep_pbt DiffApp.thy
1.47 + (["pbla2z","pbla2","pbla"],
1.48 + [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])],
1.49 + e_rls, None, []));
1.50 +store_pbt
1.51 + (prep_pbt DiffApp.thy
1.52 + (["pbla3","pbla"],
1.53 + [("#Given" ,["fixedValues a_","relations a3_"])],
1.54 + e_rls, None, []));
1.55 +
1.56 +show_ptyps();
1.57 +
1.58 +(*case 1: no refinement *)
1.59 +val thy = Isac.thy;
1.60 +val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy))
1.61 + "fixedValues [aaa=0]");
1.62 +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
1.63 + "errorBound (ddd=0)");
1.64 +val ori1 = [(1,[1],"#Given",d1,ts1),
1.65 + (2,[1],"#Given",d2,ts2)]:ori list;
1.66 +
1.67 +
1.68 +(*case 2: refined to pbt without children *)
1.69 +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
1.70 + "relations aaa333");
1.71 +val ori2 = [(1,[1],"#Given",d1,ts1),
1.72 + (2,[1],"#Given",d2,ts2)]:ori list;
1.73 +
1.74 +
1.75 +(*case 3: refined to pbt with children *)
1.76 +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
1.77 + "valuesFor aaa222");
1.78 +val ori3 = [(1,[1],"#Given",d1,ts1),
1.79 + (2,[1],"#Given",d2,ts2)]:ori list;
1.80 +
1.81 +
1.82 +(*case 4: refined to children (without child)*)
1.83 +val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy))
1.84 + "boundVariable aaa222yyy");
1.85 +val ori4 = [(1,[1],"#Given",d1,ts1),
1.86 + (2,[1],"#Given",d2,ts2),
1.87 + (3,[1],"#Given",d3,ts3)]:ori list;
1.88 +
1.89 +"----------------------- refin test-pbtyps ----------------------------";
1.90 +
1.91 +(*case 1: no refinement *)
1.92 +refin [] ori1 (hd (!ptyps));
1.93 +(*val it = Some ["pbla"] : pblID option*)
1.94 +
1.95 +(*case 2: refined to pbt without children *)
1.96 +refin [] ori2 (hd (!ptyps));
1.97 +(*val it = Some ["pbla","pbla3"] : pblID option*)
1.98 +
1.99 +(*case 3: refined to pbt with children *)
1.100 +refin [] ori3 (hd (!ptyps));
1.101 +(*val it = Some ["pbla","pbla2"] : pblID option*)
1.102 +
1.103 +(*case 4: refined to children (without child)*)
1.104 +refin [] ori4 (hd (!ptyps));
1.105 +(*val it = Some ["pbla","pbla2","pbla2y"] : pblID option*)
1.106 +
1.107 +(*case 5: start refinement somewhere in ptyps*)
1.108 +val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps;
1.109 +refin ["pbla"] ori4 ppp;
1.110 +(*val it = Some ["pbla2","pbla2y"] : pblRD option*)
1.111 +
1.112 +
1.113 +"----------------------- refine_ori test-pbtyps ----------------------------";
1.114 +
1.115 +(*case 1: no refinement *)
1.116 +refine_ori ori1 ["pbla"];
1.117 +(*val it = None : pblID option !!!!*)
1.118 +
1.119 +(*case 2: refined to pbt without children *)
1.120 +refine_ori ori2 ["pbla"];
1.121 +(*val it = Some ["pbla3","pbla"] : pblID option*)
1.122 +
1.123 +(*case 3: refined to pbt with children *)
1.124 +refine_ori ori3 ["pbla"];
1.125 +(*val it = Some ["pbla2","pbla"] : pblID option*)
1.126 +
1.127 +(*case 4: refined to children (without child)*)
1.128 +val opt = refine_ori ori4 ["pbla"];
1.129 +if opt = Some ["pbla2y","pbla2","pbla"] then ()
1.130 +else raise error "new behaviour in refine.sml case 4";
1.131 +
1.132 +(*case 5: start refinement somewhere in ptyps*)
1.133 +refine_ori ori4 ["pbla2","pbla"];
1.134 +(*val it = Some ["pbla2y","pbla2","pbla"] : pblID option*)
1.135 +
1.136 +
1.137 +"----------------------- refine test-pbtyps ----------------------------";
1.138 +
1.139 +val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];
1.140 +val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];
1.141 +val fmz3 = ["fixedValues [aaa=0]","valuesFor aaa222"];
1.142 +val fmz4 = ["fixedValues [aaa=0]","valuesFor aaa222",
1.143 + "boundVariable aaa222yyy"];
1.144 +
1.145 +(*case 1: no refinement *)
1.146 +refine fmz1 ["pbla"];
1.147 +(*
1.148 +*** pass ["pbla"]
1.149 +*** pass ["pbla","pbla1"]
1.150 +*** pass ["pbla","pbla2"]
1.151 +*** pass ["pbla","pbla3"]
1.152 +val it =
1.153 + [Matches
1.154 + (["pbla"],
1.155 + {Find=[],
1.156 + Given=[Correct "fixedValues [aaa = #0]",
1.157 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
1.158 + NoMatch
1.159 + (["pbla1","pbla"],
1.160 + {Find=[],
1.161 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
1.162 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
1.163 + NoMatch
1.164 + (["pbla2","pbla"],
1.165 + {Find=[],
1.166 + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
1.167 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
1.168 + NoMatch
1.169 + (["pbla3","pbla"],
1.170 + {Find=[],
1.171 + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
1.172 + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
1.173 + : match list*)
1.174 +
1.175 +(*case 2: refined to pbt without children *)
1.176 +refine fmz2 ["pbla"];
1.177 +(*
1.178 +*** pass ["pbla"]
1.179 +*** pass ["pbla","pbla1"]
1.180 +*** pass ["pbla","pbla2"]
1.181 +*** pass ["pbla","pbla3"]
1.182 +val it =
1.183 + [Matches
1.184 + (["pbla"],
1.185 + {Find=[],
1.186 + Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
1.187 + Relate=[],Where=[],With=[]}),
1.188 + NoMatch
1.189 + (["pbla1","pbla"],
1.190 + {Find=[],
1.191 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
1.192 + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
1.193 + NoMatch
1.194 + (["pbla2","pbla"],
1.195 + {Find=[],
1.196 + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
1.197 + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
1.198 + Matches
1.199 + (["pbla3","pbla"],
1.200 + {Find=[],
1.201 + Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
1.202 + Relate=[],Where=[],With=[]})] : match list*)
1.203 +
1.204 +(*case 3: refined to pbt with children *)
1.205 +refine fmz3 ["pbla"];
1.206 +(*
1.207 +*** pass ["pbla"]
1.208 +*** pass ["pbla","pbla1"]
1.209 +*** pass ["pbla","pbla2"]
1.210 +*** pass ["pbla","pbla2","pbla2x"]
1.211 +*** pass ["pbla","pbla2","pbla2y"]
1.212 +*** pass ["pbla","pbla2","pbla2z"]
1.213 +*** pass ["pbla","pbla3"]
1.214 +val it =
1.215 + [Matches
1.216 + (["pbla"],
1.217 + {Find=[],
1.218 + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
1.219 + Relate=[],Where=[],With=[]}),
1.220 + NoMatch
1.221 + (["pbla1","pbla"],
1.222 + {Find=[],
1.223 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
1.224 + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
1.225 + Matches
1.226 + (["pbla2","pbla"],
1.227 + {Find=[],
1.228 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
1.229 + Relate=[],Where=[],With=[]}),
1.230 + NoMatch
1.231 + (["pbla2x","pbla2","pbla"],
1.232 + {Find=[],
1.233 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.234 + Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
1.235 + NoMatch
1.236 + (["pbla2y","pbla2","pbla"],
1.237 + {Find=[],
1.238 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.239 + Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
1.240 + NoMatch
1.241 + (["pbla2z","pbla2","pbla"],
1.242 + {Find=[],
1.243 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.244 + Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
1.245 + NoMatch
1.246 + (["pbla3","pbla"],
1.247 + {Find=[],
1.248 + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
1.249 + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
1.250 + : match list*)
1.251 +
1.252 +(*case 4: refined to children (without child)*)
1.253 +refine fmz4 ["pbla"];
1.254 +(*
1.255 +*** pass ["pbla"]
1.256 +*** pass ["pbla","pbla1"]
1.257 +*** pass ["pbla","pbla2"]
1.258 +*** pass ["pbla","pbla2","pbla2x"]
1.259 +*** pass ["pbla","pbla2","pbla2y"]
1.260 +val it =
1.261 + [Matches
1.262 + (["pbla"],
1.263 + {Find=[],
1.264 + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
1.265 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
1.266 + NoMatch
1.267 + (["pbla1","pbla"],
1.268 + {Find=[],
1.269 + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
1.270 + Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
1.271 + Relate=[],Where=[],With=[]}),
1.272 + Matches
1.273 + (["pbla2","pbla"],
1.274 + {Find=[],
1.275 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.276 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
1.277 + NoMatch
1.278 + (["pbla2x","pbla2","pbla"],
1.279 + {Find=[],
1.280 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.281 + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
1.282 + Relate=[],Where=[],With=[]}),
1.283 + Matches
1.284 + (["pbla2y","pbla2","pbla"],
1.285 + {Find=[],
1.286 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.287 + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
1.288 + : match list*)
1.289 +
1.290 +(*case 5: start refinement somewhere in ptyps*)
1.291 +refine fmz4 ["pbla2","pbla"];
1.292 +(*
1.293 +*** pass ["pbla","pbla2"]
1.294 +*** pass ["pbla","pbla2","pbla2x"]
1.295 +*** pass ["pbla","pbla2","pbla2y"]
1.296 +val it =
1.297 + [Matches
1.298 + (["pbla2","pbla"],
1.299 + {Find=[],
1.300 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.301 + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
1.302 + NoMatch
1.303 + (["pbla2x","pbla2","pbla"],
1.304 + {Find=[],
1.305 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.306 + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
1.307 + Relate=[],Where=[],With=[]}),
1.308 + Matches
1.309 + (["pbla2y","pbla2","pbla"],
1.310 + {Find=[],
1.311 + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.312 + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
1.313 + : match list*)
1.314 +
1.315 +
1.316 +ptyps:= intermediate_ptyps;
1.317 +show_ptyps();
1.318 +
1.319 +
1.320 +
1.321 +"----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";
1.322 +"----------------refine.sml: miniscript with mini-subpbl -------------";
1.323 +val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",
1.324 + "errorBound (eps=0)","solutions L"];
1.325 +val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
1.326 + ("Test.thy","squ-equ-test-subpbl1"));
1.327 +val p = e_pos'; val c = [];
1.328 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.329 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.330 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.331 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.332 +
1.333 +val nxt = ("Specify_Problem",
1.334 + Specify_Problem ["linear","univariate","equation","test"]);
1.335 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.336 +(*ML> f;
1.337 +val it = Form' (PpcKF (0,EdUndef,0,Nundef,
1.338 + (Problem ["linear","univariate","equation","test"],
1.339 + {Find=[Incompl "solutions []"],
1.340 + Given=[Incompl "errorBound",
1.341 + Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.342 + Correct "solveFor x"],Relate=[],
1.343 + Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
1.344 + |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
1.345 + |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
1.346 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1.347 + With=[]}))) : mout
1.348 +
1.349 +val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)")*)
1.350 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.351 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.352 +(*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"]
1.353 + kann nicht gut gehen --------- *)
1.354 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.355 +(*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*)
1.356 +
1.357 +val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
1.358 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.359 +(*("Specify_Problem",Specify_Problem ["normalize","univariate","equation","test"])*)
1.360 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.361 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.362 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.363 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.364 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.365 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.366 +(*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep
1.367 + in Script "uberdefiniert -^-*)
1.368 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.369 +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation","test"]*)
1.370 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.371 +(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)") *)
1.372 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.373 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.374 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.375 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.376 +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation","test"])*)
1.377 +
1.378 +val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
1.379 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.380 +(*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*)
1.381 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.382 +(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)
1.383 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.384 +(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
1.385 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.386 +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
1.387 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.388 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.389 +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
1.390 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.391 +(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
1.392 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.393 +(*("Check_Postcond",Check_Postcond ["normalize","univariate","equation","test"])*)
1.394 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.395 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.396 +if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()
1.397 +else raise error "new behaviour in test:refine.sml: miniscript with mini-subpbl";
1.398 +
1.399 +