1.1 --- a/test/Tools/isac/Interpret/calchead.sml Fri Jun 21 17:53:46 2013 +0200
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Sun Jun 30 17:27:34 2013 +0200
1.3 @@ -52,19 +52,16 @@
1.4 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
1.5 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
1.6
1.7 -
1.8 -
1.9 -
1.10 "--------- maximum example with 'specify' ------------------------";
1.11 "--------- maximum example with 'specify' ------------------------";
1.12 "--------- maximum example with 'specify' ------------------------";
1.13 (*" Specify_Problem (match_itms_oris) ";*)
1.14 val fmz =
1.15 ["fixedValues [r=Arbfix]","maximum A",
1.16 - "valuesFor [a,b]",
1.17 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.18 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.19 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.20 + "valuesFor [a,b::real]",
1.21 + "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
1.22 + "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
1.23 + "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",
1.24
1.25 "boundVariable a","boundVariable b","boundVariable alpha",
1.26 "interval {x::real. 0 <= x & x <= 2*r}",
1.27 @@ -87,32 +84,32 @@
1.28
1.29 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
1.30 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.31 -(*uncaught exception TYPE 6.5.03*)
1.32 -(*========== inhibit exn AK110718 =======================================================
1.33 if ppc<>(Problem [],
1.34 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
1.35 Given=[Correct "fixedValues [r = Arbfix]"],
1.36 - Relate=[Incompl "relations []"], Where=[],With=[]})
1.37 + Relate=[Incompl "relations"], Where=[],With=[]})
1.38 then error "test-maximum.sml: model stepwise - different behaviour"
1.39 -else (); (*different with show_types !!!*)
1.40 -========== inhibit exn AK110718 =======================================================*)
1.41 +else ();
1.42
1.43 -val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
1.44 -(*========== inhibit exn AK110718 =======================================================
1.45 +val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)");
1.46 +(* WN1130630 THE maximum example WORKS IN isabisac09-2;
1.47 + MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt.
1.48 + Some tests have been broken much earlier,
1.49 + see test/../calchead.sml "inhibit exn 010830". *)
1.50 +(*========== inhibit exn WN1130630 maximum example broken =========================
1.51 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.52 +============ inhibit exn WN1130630 maximum example broken =======================*)
1.53 +
1.54 +val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
1.55 +(*========== inhibit exn WN1130630 maximum example broken =========================
1.56 (* ERROR: Exception Bind raised *)
1.57 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.58 -========== inhibit exn AK110718 =======================================================*)
1.59 -
1.60 -val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
1.61 -(*========== inhibit exn AK110718 =======================================================
1.62 -(* ERROR: Exception Bind raised *)
1.63 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.64 -========== inhibit exn AK110718 =======================================================*)
1.65 +============ inhibit exn WN1130630 maximum example broken =======================*)
1.66
1.67 val m = Specify_Problem ["maximum_of","function"];
1.68 val nxt = tac2tac_ pt p m;
1.69 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.70 -(*========== inhibit exn AK110718 =======================================================
1.71 +(*========== inhibit exn WN1130630 maximum example broken =========================
1.72 if ppc<>(Problem ["maximum_of","function"],
1.73 {Find=[Incompl "maximum",Incompl "valuesFor"],
1.74 Given=[Correct "fixedValues [r = Arbfix]"],
1.75 @@ -126,12 +123,11 @@
1.76 Relate=[Missing "relations rs_"],Where=[],With=[]})
1.77 then error "diffappl.sml: Specify_Problem different behaviour"
1.78 else ();*)
1.79 -========== inhibit exn AK110718 =======================================================*)
1.80 +============ inhibit exn WN1130630 maximum example broken =======================*)
1.81
1.82 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
1.83 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.84 -(*========== inhibit exn AK110718 =======================================================
1.85 -
1.86 +(*========== inhibit exn WN1130630 maximum example broken =========================
1.87 if ppc<>(Method ["DiffApp","max_by_calculus"],
1.88 {Find=[Incompl "maximum",Incompl "valuesFor"],
1.89 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
1.90 @@ -147,8 +143,7 @@
1.91 Relate=[Missing "relations rs_"],Where=[],With=[]})
1.92 then error "diffappl.sml: Specify_Method different behaviour"
1.93 else ();*)
1.94 -========== inhibit exn AK110718 =======================================================*)
1.95 -
1.96 +============ inhibit exn WN1130630 maximum example broken =======================*)
1.97
1.98 "--------- maximum example with 'specify', fmz <> [] -------------";
1.99 "--------- maximum example with 'specify', fmz <> [] -------------";
1.100 @@ -316,23 +311,15 @@
1.101 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.102 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
1.103
1.104 -(*========== inhibit exn 010830 =======================================================
1.105 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
1.106 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
1.107 then error "test specify, fmz <> []: nxt <> Add_Relation.."
1.108 else ();
1.109 *)
1.110 -========== inhibit exn 010830 =======================================================*)
1.111 -
1.112 -(*========== inhibit exn 000402 =======================================================
1.113 (* 2.4.00 nach Transfer specify -> hard_gen
1.114 val nxt = Apply_Method ("DiffApp","max_by_calculus");
1.115 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
1.116 (*val nxt = Empty_Tac : tac*)
1.117 -========== inhibit exn 000402 =======================================================*)
1.118 -
1.119 -
1.120 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.121
1.122 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.123 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.124 @@ -351,9 +338,9 @@
1.125 val pats = (#ppc o get_pbt) pI;
1.126 "-a1-----------------------------------------------------";
1.127 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
1.128 -val xxx = match_ags (theory "EqSystem") pats ags;
1.129 +val xxx = match_ags @{theory "EqSystem"} pats ags;
1.130 "-a2-----------------------------------------------------";
1.131 -case match_ags (theory "Isac") pats ags of
1.132 +case match_ags @{theory "Isac"} pats ags of
1.133 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.134 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.135 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
1.136 @@ -361,7 +348,6 @@
1.137 =>()
1.138 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
1.139
1.140 -
1.141 "-b------------------------------------------------------";
1.142 val Const ("Script.SubProblem",_) $
1.143 (Const ("Product_Type.Pair",_) $
1.144 @@ -376,9 +362,9 @@
1.145 val pI = ["linear","system"];
1.146 val pats = (#ppc o get_pbt) pI;
1.147 "-b1-----------------------------------------------------";
1.148 -val xxx = match_ags (theory "Isac") pats ags;
1.149 +val xxx = match_ags @{theory "Isac"} pats ags;
1.150 "-b2-----------------------------------------------------";
1.151 -case match_ags (theory "EqSystem") pats ags of
1.152 +case match_ags @{theory "EqSystem"} pats ags of
1.153 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.154 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.155 [_ $ Free ("c", _) $ _,
1.156 @@ -388,7 +374,6 @@
1.157 =>()
1.158 | _ => error "calchead.sml match_ags copy-named dropped --------";
1.159
1.160 -
1.161 "-c---ERROR case: stac is missing #Given equalities e_s--";
1.162 val stac as Const ("Script.SubProblem",_) $
1.163 (Const ("Product_Type.Pair",_) $
1.164 @@ -406,7 +391,7 @@
1.165 -------------------------------------------------------------------*)
1.166 "-c1-----------------------------------------------------";
1.167 "--------------------------step through code match_ags---";
1.168 -val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
1.169 +val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
1.170 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.171 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
1.172 val cy = filter is_copy_named pbt; (*=solution*)
1.173 @@ -421,19 +406,127 @@
1.174 val opt - mtc thy p a;
1.175 -------------------------------------------------------------------*)
1.176 "--------------------------------step through code mtc---";
1.177 -val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
1.178 +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.179 cterm_of;
1.180 -val ttt - (dsc $ var);
1.181 +val ttt = (dsc $ var);
1.182 +(*---inhibit exn provided by this testcase--------------------------
1.183 +cterm_of thy (dsc $ var);
1.184 +-------------------------------------------------------------------*)
1.185 +
1.186 +"-------------------------------------step through end---";
1.187 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.188 +val Const ("Script.SubProblem",_) $
1.189 + (Const ("Product_Type.Pair",_) $
1.190 + Free (dI',_) $
1.191 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.192 + (*...copied from stac2tac_*)
1.193 + str2term (
1.194 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.195 + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.196 + " REAL_LIST [c, c_2]]");
1.197 +val ags = isalist2list ags';
1.198 +val pI = ["linear","system"];
1.199 +val pats = (#ppc o get_pbt) pI;
1.200 +"-a1-----------------------------------------------------";
1.201 +(*match_ags = fn : theory -> pat list -> term list -> ori list*)
1.202 +val xxx = match_ags @{theory "EqSystem"} pats ags;
1.203 +"-a2-----------------------------------------------------";
1.204 +case match_ags @{theory "Isac"} pats ags of
1.205 + [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.206 + (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.207 + [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
1.208 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
1.209 + =>()
1.210 + | _ => error "calchead.sml match_ags 2 args Nok ----------------";
1.211 +
1.212 +"-b------------------------------------------------------";
1.213 +val Const ("Script.SubProblem",_) $
1.214 + (Const ("Product_Type.Pair",_) $
1.215 + Free (dI',_) $
1.216 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.217 + (*...copied from stac2tac_*)
1.218 + str2term (
1.219 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.220 + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.221 + " REAL_LIST [c, c_2], BOOL_LIST ss''']");
1.222 +val ags = isalist2list ags';
1.223 +val pI = ["linear","system"];
1.224 +val pats = (#ppc o get_pbt) pI;
1.225 +"-b1-----------------------------------------------------";
1.226 +val xxx = match_ags @{theory "Isac"} pats ags;
1.227 +"-b2-----------------------------------------------------";
1.228 +case match_ags @{theory "EqSystem"} pats ags of
1.229 + [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.230 + (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.231 + [_ $ Free ("c", _) $ _,
1.232 + _ $ Free ("c_2", _) $ _]),
1.233 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
1.234 + (* type of Find: [Free ("ss'''", "bool List.list")]*)
1.235 + =>()
1.236 + | _ => error "calchead.sml match_ags copy-named dropped --------";
1.237 +
1.238 +"-c---ERROR case: stac is missing #Given equalities e_s--";
1.239 +val stac as Const ("Script.SubProblem",_) $
1.240 + (Const ("Product_Type.Pair",_) $
1.241 + Free (dI',_) $
1.242 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.243 + (*...copied from stac2tac_*)
1.244 + str2term (
1.245 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.246 + " [REAL_LIST [c, c_2]]");
1.247 +val ags = isalist2list ags';
1.248 +val pI = ["linear","system"];
1.249 +val pats = (#ppc o get_pbt) pI;
1.250 +(*---inhibit exn provided by this testcase--------------------------
1.251 +val xxx - match_ags (theory "EqSystem") pats ags;
1.252 +-------------------------------------------------------------------*)
1.253 +"-c1-----------------------------------------------------";
1.254 +"--------------------------step through code match_ags---";
1.255 +val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
1.256 +fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.257 + val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
1.258 + val cy = filter is_copy_named pbt; (*=solution*)
1.259 +(*---inhibit exn provided by this testcase--------------------------
1.260 + val oris' - matc thy pbt' ags [];
1.261 +-------------------------------------------------------------------*)
1.262 +"-------------------------------step through code matc---";
1.263 +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
1.264 +(is_copy_named_idstr o free2str) t;
1.265 +"---if False:...";
1.266 +(*---inhibit exn provided by this testcase--------------------------
1.267 +val opt - mtc thy p a;
1.268 +-------------------------------------------------------------------*)
1.269 +"--------------------------------step through code mtc---";
1.270 +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.271 +cterm_of;
1.272 +val ttt = (dsc $ var);
1.273 (*---inhibit exn provided by this testcase--------------------------
1.274 cterm_of thy (dsc $ var);
1.275 -------------------------------------------------------------------*)
1.276 "-------------------------------------step through end---";
1.277
1.278 -case ((match_ags (theory "EqSystem") pats ags)
1.279 +case ((match_ags @{theory "EqSystem"} pats ags)
1.280 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
1.281 [] => match_ags_msg pI stac ags
1.282 | _ => error "calchead.sml match_ags 1st arg missing --------";
1.283
1.284 +"-d------------------------------------------------------";
1.285 +val stac as Const ("Script.SubProblem",_) $
1.286 + (Const ("Product_Type.Pair",_) $
1.287 + Free (dI',_) $
1.288 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.289 + (*...copied from stac2tac_*)
1.290 + str2term (
1.291 + "SubProblem (Test',[univariate,equation,test]," ^
1.292 + " [no_met]) [BOOL (x+1=2), REAL x]");
1.293 +val AGS = isalist2list ags';
1.294 +val pI = ["univariate","equation","test"];
1.295 +
1.296 +
1.297 +case ((match_ags @{theory "EqSystem"} pats ags)
1.298 + handle ERROR _ => []) of (*why not TYPE ?WN100920*)
1.299 + [] => match_ags_msg pI stac ags
1.300 + | _ => error "calchead.sml match_ags 1st arg missing --------";
1.301
1.302 "-d------------------------------------------------------";
1.303 val stac as Const ("Script.SubProblem",_) $
1.304 @@ -449,7 +542,7 @@
1.305 val PATS = (#ppc o get_pbt) pI;
1.306 "-d1-----------------------------------------------------";
1.307 "--------------------------step through code match_ags---";
1.308 -val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
1.309 +val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);
1.310 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.311 val pbt' = filter_out is_copy_named pbt;
1.312 val cy = filter is_copy_named pbt;
1.313 @@ -487,7 +580,7 @@
1.314 "--------------------------------------------------------";
1.315 fun is_copy_named_generating_idstr str =
1.316 if is_copy_named_idstr str
1.317 - then case (rev o explode) str of
1.318 + then case (rev o Symbol.explode) str of
1.319 (*"_"::"_"::"_"::_ => false*)
1.320 "'"::"'"::"'"::_ => false
1.321 | _ => true
1.322 @@ -497,9 +590,9 @@
1.323 "--------------------------------------------------------";
1.324 is_copy_named_generating p (*true*);
1.325 fun sel (_,_,d,ts) = comp_ts (d, ts);
1.326 - val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
1.327 + val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
1.328 (*"v_v" OLD: "v_"*)
1.329 - val ext = (last_elem o drop_last o explode o free2str) t;
1.330 + val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
1.331 (*"i" OLD: "i"*)
1.332 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
1.333 (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
1.334 @@ -525,7 +618,6 @@
1.335 => ()
1.336 | _ => error "calchead.sml match_ags [univariate,equation,test]--";
1.337
1.338 -
1.339 "--------- regression test fun is_copy_named ------------";
1.340 "--------- regression test fun is_copy_named ------------";
1.341 "--------- regression test fun is_copy_named ------------";
1.342 @@ -577,9 +669,6 @@
1.343 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
1.344 | _ => error "calchead.sml regr.test cpy_nam-2-";
1.345
1.346 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.347 -
1.348 -
1.349 "--------- check specify phase --------------------------";
1.350 "--------- check specify phase --------------------------";
1.351 "--------- check specify phase --------------------------";