1.1 --- a/test/Tools/isac/Interpret/ptyps.sml Sat Mar 10 14:53:18 2012 +0100
1.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Tue Mar 13 15:04:09 2012 +0100
1.3 @@ -1,11 +1,7 @@
1.4 (* Title: tests for ME/ptyps.sml
1.5 CAUTION: intermediately stores !ptyps THUS EVALUATE IN 1 GO
1.6 - uthor: Walther Neuper
1.7 - 010916,
1.8 + Author: Walther Neuper 010916
1.9 (c) due to copyright terms
1.10 -
1.11 -use"../smltest/ME/ptyps.sml";
1.12 -use"ptyps.sml";
1.13 *)
1.14
1.15 "--------------------------------------------------------";
1.16 @@ -33,74 +29,59 @@
1.17 "----------- store test-pbtyps -----------------------------------";
1.18 "----------- store test-pbtyps -----------------------------------";
1.19 ptyps:= ([]:ptyps);
1.20 -(*========== inhibit exn AK110725 ======================================================
1.21 store_pbt
1.22 (prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
1.23 (["pbla"],
1.24 - [("#Given", ["fixedValues a_"])], e_rls, NONE, []));
1.25 + [("#Given", ["fixedValues a_a"])], e_rls, NONE, []));
1.26 store_pbt
1.27 - (prep_pbt DiffApp.thy "pbl_pbla1" [] e_pblID
1.28 + (prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID
1.29 (["pbla1","pbla"],
1.30 - [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, NONE, []));
1.31 + [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []));
1.32 store_pbt
1.33 - (prep_pbt DiffApp.thy "pbl_pbla2" [] e_pblID
1.34 + (prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID
1.35 (["pbla2","pbla"],
1.36 - [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, NONE, []));
1.37 + [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []));
1.38 store_pbt
1.39 - (prep_pbt DiffApp.thy "pbl_pbla2x" [] e_pblID
1.40 + (prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID
1.41 (["pbla2x","pbla2","pbla"],
1.42 - [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])],
1.43 + [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
1.44 e_rls, NONE, []));
1.45 store_pbt
1.46 - (prep_pbt DiffApp.thy "pbl_pbla2y" [] e_pblID
1.47 + (prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID
1.48 (["pbla2y","pbla2","pbla"],
1.49 - [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])],
1.50 + [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
1.51 e_rls, NONE, []));
1.52 store_pbt
1.53 - (prep_pbt DiffApp.thy "pbl_pbla2z" [] e_pblID
1.54 + (prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID
1.55 (["pbla2z","pbla2","pbla"],
1.56 - [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])],
1.57 + [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
1.58 e_rls, NONE, []));
1.59 store_pbt
1.60 - (prep_pbt DiffApp.thy "pbl_pbla3" [] e_pblID
1.61 + (prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID
1.62 (["pbla3","pbla"],
1.63 - [("#Given" ,["fixedValues a_","relations a3_"])],
1.64 + [("#Given" ,["fixedValues a_a","relations a_3"])],
1.65 e_rls, NONE, []));
1.66
1.67 show_ptyps();
1.68 -========== inhibit exn AK110725 ======================================================*)
1.69 +val thy = @{theory "Isac"};
1.70 +val ctxt = ProofContext.init_global @{theory "Isac"};
1.71
1.72 (*case 1: no refinement *)
1.73 -val thy = (@{theory "Isac"});
1.74 -(*========== inhibit exn AK110725 ======================================================
1.75 -val (d1,ts1) = split_dts thy ((term_of o the o (parse thy)) "fixedValues [aaa=0]");
1.76 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) "errorBound (ddd=0)");
1.77 -
1.78 -val ori1 = [(1,[1],"#Given",d1,ts1),
1.79 - (2,[1],"#Given",d2,ts2)]:ori list;
1.80 -
1.81 +val (d1,ts1) = split_dts ((term_of o the o (parse thy)) "fixedValues [aaa = 0]");
1.82 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "errorBound (ddd = 0)");
1.83 +val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
1.84
1.85 (*case 2: refined to pbt without children *)
1.86 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
1.87 - "relations [aaa333]");
1.88 -val ori2 = [(1,[1],"#Given",d1,ts1),
1.89 - (2,[1],"#Given",d2,ts2)]:ori list;
1.90 -
1.91 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "relations [aaa333]");
1.92 +val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
1.93
1.94 (*case 3: refined to pbt with children *)
1.95 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
1.96 - "valuesFor [aaa222]");
1.97 -val ori3 = [(1,[1],"#Given",d1,ts1),
1.98 - (2,[1],"#Given",d2,ts2)]:ori list;
1.99 -
1.100 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "valuesFor [aaa222]");
1.101 +val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
1.102
1.103 (*case 4: refined to children (without child)*)
1.104 -val (d3,ts3) = split_dts thy ((term_of o the o (parse thy))
1.105 - "boundVariable aaa222yyy");
1.106 -val ori4 = [(1,[1],"#Given",d1,ts1),
1.107 - (2,[1],"#Given",d2,ts2),
1.108 - (3,[1],"#Given",d3,ts3)]:ori list;
1.109 -
1.110 +val (d3,ts3) = split_dts ((term_of o the o (parse thy)) "boundVariable aaa222yyy");
1.111 +val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
1.112
1.113 "----------- refin test-pbtyps -----------------------------------";
1.114 "----------- refin test-pbtyps -----------------------------------";
1.115 @@ -126,7 +107,6 @@
1.116 refin ["pbla"] ori4 ppp;
1.117 (*val it = SOME ["pbla2","pbla2y"] : pblRD option*)
1.118
1.119 -
1.120 "----------- refine_ori test-pbtyps ------------------------------";
1.121 "----------- refine_ori test-pbtyps ------------------------------";
1.122 "----------- refine_ori test-pbtyps ------------------------------";
1.123 @@ -150,8 +130,6 @@
1.124 (*case 5: start refinement somewhere in ptyps*)
1.125 refine_ori ori4 ["pbla2","pbla"];
1.126 (*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*)
1.127 -========== inhibit exn AK110725 ======================================================*)
1.128 -
1.129
1.130 "----------- refine test-pbtyps ----------------------------------";
1.131 "----------- refine test-pbtyps ----------------------------------";
1.132 @@ -162,9 +140,13 @@
1.133 val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
1.134 "boundVariable aaa222yyy"];
1.135
1.136 -(*========== inhibit exn AK110725 ======================================================
1.137 (*case 1: no refinement *)
1.138 -refine fmz1 ["pbla"];
1.139 +case refine fmz1 ["pbla"] of
1.140 + [Matches (["pbla"], _),
1.141 + NoMatch (["pbla1", "pbla"], _),
1.142 + NoMatch (["pbla2", "pbla"], _),
1.143 + NoMatch (["pbla3", "pbla"], _)] => ()
1.144 + | _ => error "--- refine test-pbtyps --- broken with case 1";
1.145 (*
1.146 *** pass ["pbla"]
1.147 *** pass ["pbla","pbla1"]
1.148 @@ -195,7 +177,12 @@
1.149
1.150
1.151 (*case 2: refined to pbt without children *)
1.152 -refine fmz2 ["pbla"];
1.153 +case refine fmz2 ["pbla"] of
1.154 + [Matches (["pbla"], _),
1.155 + NoMatch (["pbla1", "pbla"], _),
1.156 + NoMatch (["pbla2", "pbla"], _),
1.157 + Matches (["pbla3", "pbla"], _)] => ()
1.158 + | _ => error "--- refine test-pbtyps --- broken with case 2";
1.159 (*
1.160 *** pass ["pbla"]
1.161 *** pass ["pbla","pbla1"]
1.162 @@ -224,7 +211,15 @@
1.163 Relate=[],Where=[],With=[]})] : match list*)
1.164
1.165 (*case 3: refined to pbt with children *)
1.166 -refine fmz3 ["pbla"];
1.167 +case refine fmz3 ["pbla"] of
1.168 + [Matches (["pbla"], _),
1.169 + NoMatch (["pbla1", "pbla"], _),
1.170 + Matches (["pbla2", "pbla"], _),
1.171 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
1.172 + NoMatch (["pbla2y", "pbla2", "pbla"], _),
1.173 + NoMatch (["pbla2z", "pbla2", "pbla"], _),
1.174 + NoMatch (["pbla3", "pbla"], _)] => ()
1.175 + | _ => error "--- refine test-pbtyps --- broken with case 3";
1.176 (*
1.177 *** pass ["pbla"]
1.178 *** pass ["pbla","pbla1"]
1.179 @@ -272,7 +267,13 @@
1.180 : match list*)
1.181
1.182 (*case 4: refined to children (without child)*)
1.183 -refine fmz4 ["pbla"];
1.184 +case refine fmz4 ["pbla"] of
1.185 + [Matches (["pbla"], _),
1.186 + NoMatch (["pbla1", "pbla"], _),
1.187 + Matches (["pbla2", "pbla"], _),
1.188 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
1.189 + Matches (["pbla2y", "pbla2", "pbla"], _)] => ()
1.190 + | _ => error "--- refine test-pbtyps --- broken with case 4";
1.191 (*
1.192 *** pass ["pbla"]
1.193 *** pass ["pbla","pbla1"]
1.194 @@ -310,7 +311,11 @@
1.195 : match list*)
1.196
1.197 (*case 5: start refinement somewhere in ptyps*)
1.198 -refine fmz4 ["pbla2","pbla"];
1.199 +case refine fmz4 ["pbla2","pbla"] of
1.200 + [Matches (["pbla2", "pbla"], _),
1.201 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
1.202 + Matches (["pbla2y", "pbla2", "pbla"], _)] => ()
1.203 + | _ => error "--- refine test-pbtyps --- broken with case 5";
1.204 (*
1.205 *** pass ["pbla","pbla2"]
1.206 *** pass ["pbla","pbla2","pbla2x"]
1.207 @@ -333,38 +338,44 @@
1.208 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
1.209 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
1.210 : match list*)
1.211 -========== inhibit exn AK110725 ======================================================*)
1.212
1.213
1.214 "###### ptyps:= intermediate_ptyps;###############################";
1.215 "###### ptyps:= intermediate_ptyps;###############################";
1.216 "###### ptyps:= intermediate_ptyps;###############################";
1.217 ptyps:= intermediate_ptyps;
1.218 +if length (! ptyps) = 12 then () else error "test setup with intermediate_ptyps broken";
1.219 show_ptyps();
1.220
1.221 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
1.222 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
1.223 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
1.224 -val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",
1.225 +(*WN120313: attention: the 'nxt' in the comments are not correct!*)
1.226 +val c = [];
1.227 +val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))","solveFor x",
1.228 "errorBound (eps=0)","solutions L"];
1.229 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
1.230 ["Test","squ-equ-test-subpbl1"]);
1.231 -(*========== inhibit exn AK110725 ======================================================
1.232 -(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
1.233 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.234 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.235 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.236 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Add_Find", Add_Find "solutions L")*)
1.237
1.238 +val nxt = ("Specify_Problem", Specify_Problem ["linear","univariate","equation","test"]);
1.239 +(*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.240 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.241 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.242 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.243 -(*nxt = ("Add_Find", Add_Find "solutions L")*)
1.244 -
1.245 -
1.246 -val nxt = ("Specify_Problem",(*vvvv---specify a not-matching problem*)
1.247 - Specify_Problem ["linear","univariate","equation","test"]);
1.248 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.249 +if f = Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
1.250 + {Find = [Incompl "solutions"], With = [],
1.251 + Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
1.252 + Where = [False ("matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
1.253 + "matches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
1.254 + "matches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
1.255 + "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)")],
1.256 + Relate = []}))) then ()
1.257 +else error "--- Refine_Problem broken 1";
1.258 (*ML> f;
1.259 val it = Form' (PpcKF (0,EdUndef,0,Nundef,
1.260 - (Problem ["linear","univariate","equation","test"],
1.261 + (Problem ["linear","univariate","equation","test"], <<<<<===== diff.to above WN120313
1.262 {Find=[Incompl "solutions []"],
1.263 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1.264 Correct "solveFor x"],Relate=[],
1.265 @@ -375,12 +386,13 @@
1.266 With=[]}))) : mout
1.267 val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)
1.268
1.269 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
1.270 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*NEW2*);
1.271 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e*);
1.272 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.273 (*val nxt = ("Empty_Tac",Empty_Tac)
1.274 ... Refine_Problem ["linear"..] fails internally 040312: works!?!*)
1.275
1.276 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
1.277 +(*=== refine problem -----------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.278 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.279 (*("Specify_Problem", Specify_Problem ["normalize", "univariate", ...])*)
1.280 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.281 @@ -396,14 +408,13 @@
1.282 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.283 (*Subproblem ("Test", ["linear", "univariate", "equation", "test"]*)
1.284
1.285 -
1.286 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.287 (*nxt = Model_Problem ["linear","univariate","equation","test"]*)
1.288 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.289 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
1.290 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.291 (**)
1.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt;2
1.293 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.294 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.295 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.296 (*nxt = Specify_Problem ["linear","univariate","equation","test"])*)
1.297 @@ -428,10 +439,9 @@
1.298 (*Check_Postcond ["normalize","univariate","equation","test"])*)
1.299 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.300 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;
1.301 -if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()
1.302 +
1.303 +if (snd nxt) = End_Proof' andalso res = "[x = 2]" then ()
1.304 else error "new behaviour in test:refine.sml:miniscript with mini-subpb";
1.305 -========== inhibit exn AK110725 ======================================================*)
1.306 -
1.307
1.308 "----------- fun coll_guhs ---------------------------------------";
1.309 "----------- fun coll_guhs ---------------------------------------";
1.310 @@ -465,7 +475,6 @@
1.311 "----------- fun guh2kestoreID -----------------------------------";
1.312 "----------- fun guh2kestoreID -----------------------------------";
1.313 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
1.314 -(*========== inhibit exn AK110725 ======================================================
1.315 (* ERROR: Exception Bind raised *)
1.316 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
1.317 Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);
1.318 @@ -486,4 +495,4 @@
1.319 nodes [] guh3 (!ptyps);
1.320 nodes [] guh21 (!ptyps);
1.321 *)
1.322 -============ inhibit exn AK110725 ====================================================*)
1.323 +