1.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:43:36 2010 +0200
1.3 @@ -3,8 +3,8 @@
1.4 051013,
1.5 (c) due to copyright terms
1.6
1.7 -use"../smltest/ME/calchead.sml";
1.8 -use"calchead.sml";
1.9 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.10 + 10 20 30 40 50 60 70 80
1.11 *)
1.12
1.13 "--------------------------------------------------------";
1.14 @@ -16,15 +16,16 @@
1.15 "--------- maximum example with 'specify', fmz = [] -----";
1.16 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.17 "--------- regression test fun is_copy_named ------------";
1.18 +"--------- regr.test fun cpy_nam ------------------------";
1.19 "--------------------------------------------------------";
1.20 "--------------------------------------------------------";
1.21 "--------------------------------------------------------";
1.22
1.23 -(*==========================================================================
1.24 -"--------- get_interval after replace} other 2 -------------------";
1.25 -"--------- get_interval after replace} other 2 -------------------";
1.26 -"--------- get_interval after replace} other 2 -------------------";
1.27 - states:=[];
1.28 +(*WN100914======================================================================
1.29 +"--------- get_interval after replace} other 2 ----------";
1.30 +"--------- get_interval after replace} other 2 ----------";
1.31 +"--------- get_interval after replace} other 2 ----------";
1.32 +states := [];
1.33 CalcTree
1.34 [(["equality (x+1=2)", "solveFor x","solutions L"],
1.35 ("Test.thy",
1.36 @@ -324,96 +325,199 @@
1.37 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
1.38 (*val nxt = Empty_Tac : tac*)
1.39
1.40 +====================================================================WN100914*)
1.41
1.42 -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.43 -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.44 -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.45 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.46 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.47 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.48 val Const ("Script.SubProblem",_) $
1.49 (Const ("Pair",_) $
1.50 Free (dI',_) $
1.51 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.52 (*...copied from stac2tac_*)
1.53 - str2term
1.54 - "SubProblem (EqSystem_, [linear, system], [no_met])\
1.55 - \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
1.56 - \ REAL_LIST [c, c_2]]";
1.57 + str2term (
1.58 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.59 + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.60 + " REAL_LIST [c, c_2]]");
1.61 val ags = isalist2list ags';
1.62 val pI = ["linear","system"];
1.63 val pats = (#ppc o get_pbt) pI;
1.64 -case match_ags Isac.thy pats ags of
1.65 +"-a1-----------------------------------------------------";
1.66 +(*match_ags = fn : theory -> pat list -> term list -> ori list*)
1.67 +val xxx = match_ags (theory "EqSystem") pats ags;
1.68 +"-a2-----------------------------------------------------";
1.69 +case match_ags (theory "Isac") pats ags of
1.70 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.71 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.72 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
1.73 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
1.74 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
1.75 =>()
1.76 - | _ => raise error "calchead.sml match_ags 2 args OK -----------------";
1.77 + | _ => raise error "calchead.sml match_ags 2 args Nok ----------------";
1.78
1.79
1.80 +"-b------------------------------------------------------";
1.81 val Const ("Script.SubProblem",_) $
1.82 (Const ("Pair",_) $
1.83 Free (dI',_) $
1.84 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.85 (*...copied from stac2tac_*)
1.86 - str2term
1.87 - "SubProblem (EqSystem_, [linear, system], [no_met])\
1.88 - \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
1.89 - \ REAL_LIST [c, c_2], BOOL_LIST ss___]";
1.90 + str2term (
1.91 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.92 + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.93 + " REAL_LIST [c, c_2], BOOL_LIST ss''']");
1.94 val ags = isalist2list ags';
1.95 val pI = ["linear","system"];
1.96 val pats = (#ppc o get_pbt) pI;
1.97 -case match_ags Isac.thy pats ags of
1.98 +"-b1-----------------------------------------------------";
1.99 +val xxx = match_ags (theory "Isac") pats ags;
1.100 +"-b2-----------------------------------------------------";
1.101 +case match_ags (theory "EqSystem") pats ags of
1.102 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.103 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.104 [_ $ Free ("c", _) $ _,
1.105 _ $ Free ("c_2", _) $ _]),
1.106 - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
1.107 - (* type of Find: [Free ("ss___", "bool List.list")]*)
1.108 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]
1.109 + (* type of Find: [Free ("ss'''", "bool List.list")]*)
1.110 =>()
1.111 | _ => raise error "calchead.sml match_ags copy-named dropped --------";
1.112
1.113
1.114 +"-c---ERROR case: stac is missing #Given equalities e_s--";
1.115 val stac as Const ("Script.SubProblem",_) $
1.116 (Const ("Pair",_) $
1.117 Free (dI',_) $
1.118 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.119 (*...copied from stac2tac_*)
1.120 - str2term
1.121 - "SubProblem (EqSystem_, [linear, system], [no_met])\
1.122 - \ [REAL_LIST [c, c_2]]";
1.123 -val ags = isalist2list ags';
1.124 + str2term (
1.125 + "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.126 + " [REAL_LIST [c, c_2]]");
1.127 +val ags = isalist2list ags';
1.128 val pI = ["linear","system"];
1.129 val pats = (#ppc o get_pbt) pI;
1.130 -case ((match_ags Isac.thy pats ags)
1.131 - handle TYPE _ => []) of
1.132 +(*===inhibit exn provided by this testcase==========================
1.133 +val xxx = match_ags (theory "EqSystem") pats ags;
1.134 +===================================================================*)
1.135 +"-c1-----------------------------------------------------";
1.136 +"--------------------------step through code match_ags---";
1.137 +val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
1.138 +fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.139 + val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
1.140 + val cy = filter is_copy_named pbt; (*=solution*)
1.141 +(*===inhibit exn provided by this testcase==========================
1.142 + val oris' = matc thy pbt' ags [];
1.143 +===================================================================*)
1.144 +"-------------------------------step through code matc---";
1.145 +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
1.146 +(is_copy_named_idstr o free2str) t;
1.147 +"---if False:...";
1.148 +(*===inhibit exn provided by this testcase==========================
1.149 +val opt = mtc thy p a;
1.150 +===================================================================*)
1.151 +"--------------------------------step through code mtc---";
1.152 +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.153 +cterm_of;
1.154 +val ttt = (dsc $ var);
1.155 +(*===inhibit exn provided by this testcase==========================
1.156 +cterm_of thy (dsc $ var);
1.157 +===================================================================*)
1.158 +"-------------------------------------step through end---";
1.159 +
1.160 +case ((match_ags (theory "EqSystem") pats ags)
1.161 + handle ERROR _ => []) of (*why not TYPE ?WN100920*)
1.162 [] => match_ags_msg pI stac ags
1.163 | _ => raise error "calchead.sml match_ags 1st arg missing --------";
1.164
1.165 -(*
1.166 -use"../smltest/ME/calchead.sml";
1.167 -*)
1.168
1.169 +"-d------------------------------------------------------";
1.170 val stac as Const ("Script.SubProblem",_) $
1.171 (Const ("Pair",_) $
1.172 Free (dI',_) $
1.173 (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.174 (*...copied from stac2tac_*)
1.175 - str2term
1.176 - "SubProblem (Test_,[univariate,equation,test],\
1.177 - \ [no_met]) [BOOL (x+1=2), REAL x]";
1.178 -val ags = isalist2list ags';
1.179 + str2term (
1.180 + "SubProblem (Test',[univariate,equation,test]," ^
1.181 + " [no_met]) [BOOL (x+1=2), REAL x]");
1.182 +val AGS = isalist2list ags';
1.183 val pI = ["univariate","equation","test"];
1.184 -val pats = (#ppc o get_pbt) pI;
1.185 -case match_ags Isac.thy pats ags of
1.186 - [(1, [1], "#Given",
1.187 - Const ("Descript.equality", _),
1.188 - [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),
1.189 - (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
1.190 - (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
1.191 - (* type of Find: [Free ("x_i", "bool List.list")]*)
1.192 +val PATS = (#ppc o get_pbt) pI;
1.193 +"-d1-----------------------------------------------------";
1.194 +"--------------------------step through code match_ags---";
1.195 +val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS);
1.196 +fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.197 + val pbt' = filter_out is_copy_named pbt;
1.198 + val cy = filter is_copy_named pbt;
1.199 + val oris' = matc thy pbt' ags [];
1.200 +"-------------------------------step through code matc---";
1.201 +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
1.202 +(is_copy_named_idstr o free2str) t;
1.203 +"---if False:...";
1.204 +val opt = mtc thy p a;
1.205 +"--------------------------------step through code mtc---";
1.206 +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.207 +val ttt = (dsc $ var);
1.208 +cterm_of thy (dsc $ var);
1.209 +val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
1.210 +
1.211 +"-d2-----------------------------------------------------";
1.212 +pbt = []; (*false*)
1.213 +"-------------------------------step through code matc---";
1.214 +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);
1.215 +(is_copy_named_idstr o free2str) t;
1.216 +"---if False:...";
1.217 +val opt = mtc thy p a;
1.218 +"--------------------------------step through code mtc---";
1.219 +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.220 +val ttt = (dsc $ var);
1.221 +cterm_of thy (dsc $ var);
1.222 +val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
1.223 +"-d3-----------------------------------------------------";
1.224 +pbt = []; (*true, base case*)
1.225 +"-----------------continue step through code match_ags---";
1.226 + val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
1.227 +"--------------------------------step through cpy_nam----";
1.228 +val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);
1.229 +(*t = "v_v'i'" : term OLD: t = "v_i_"*)
1.230 +"--------------------------------------------------------";
1.231 +fun is_copy_named_generating_idstr str =
1.232 + if is_copy_named_idstr str
1.233 + then case (rev o explode) str of
1.234 + (*"_"::"_"::"_"::_ => false*)
1.235 + "'"::"'"::"'"::_ => false
1.236 + | _ => true
1.237 + else false;
1.238 +fun is_copy_named_generating (_, (_, t)) =
1.239 + (is_copy_named_generating_idstr o free2str) t;
1.240 +"--------------------------------------------------------";
1.241 +is_copy_named_generating p (*true*);
1.242 + fun sel (_,_,d,ts) = comp_ts (d, ts);
1.243 + val cy' = (implode o (drop_last_n 3) o explode o free2str) t;
1.244 + (*"v_v" OLD: "v_"*)
1.245 + val ext = (last_elem o drop_last o explode o free2str) t;
1.246 + (*"i" OLD: "i"*)
1.247 + val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);
1.248 + (*["e_e", "v_v"] OLD: ["e_", "v_"]*)
1.249 + val vals = map sel oris;
1.250 + (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
1.251 +vars' ~~ vals;
1.252 +(*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
1.253 +(assoc (vars'~~vals, cy'));
1.254 +(*Some (Free ("x", "RealDef.real")) : term option*)
1.255 + val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
1.256 + (*x_i*)
1.257 +"-----------------continue step through code match_ags---";
1.258 + val cy' = map (cpy_nam pbt' oris') cy;
1.259 + (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)
1.260 +"-------------------------------------step through end---";
1.261 +
1.262 +case match_ags thy PATS AGS of
1.263 +[(1, [1], "#Given", Const ("Descript.equality", _),
1.264 + [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $
1.265 + Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
1.266 + (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
1.267 + (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
1.268 => ()
1.269 | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
1.270
1.271 -==========================================================================*)
1.272
1.273 "--------- regression test fun is_copy_named ------------";
1.274 "--------- regression test fun is_copy_named ------------";
1.275 @@ -431,3 +535,37 @@
1.276 val trm = (1, (2, @{term "L'''"}));
1.277 if is_copy_named_generating trm then raise error "regr. is_copy_named" else ();
1.278 *)
1.279 +
1.280 +"--------- regr.test fun cpy_nam ------------------------";
1.281 +"--------- regr.test fun cpy_nam ------------------------";
1.282 +"--------- regr.test fun cpy_nam ------------------------";
1.283 +(*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)
1.284 +(*the model-pattern, is_copy_named are filter_out*)
1.285 +pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),
1.286 + ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];
1.287 +(*the model specific for an example*)
1.288 +oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),
1.289 + ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];
1.290 +cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];
1.291 +(*...all must be true*)
1.292 +
1.293 +case cpy_nam pbt oris (hd cy) of
1.294 + ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()
1.295 + | _ => raise error "calchead.sml regr.test cpy_nam-1-";
1.296 +
1.297 +(*new data: cpy_nam without changing the name*)
1.298 +@{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
1.299 +@{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
1.300 +@{term "solution"}; type_of @{term "ss''' :: bool list"};
1.301 +(*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
1.302 +val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
1.303 + ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
1.304 +(*the model specific for an example*)
1.305 +val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),
1.306 + ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];
1.307 +val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))
1.308 + (*could be more than 1*)];
1.309 +
1.310 +case cpy_nam pbt oris (hd cy) of
1.311 + ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
1.312 + | _ => raise error "calchead.sml regr.test cpy_nam-2-";