1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,413 @@
1.4 +(* tests on calchead.sml
1.5 + author: Walther Neuper
1.6 + 051013,
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"../smltest/ME/calchead.sml";
1.10 +use"calchead.sml";
1.11 +*)
1.12 +
1.13 +"-----------------------------------------------------------------";
1.14 +"table of contents -----------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"--------- get_interval after replace} other 2 -------------------";
1.17 +"--------- maximum example with 'specify' ------------------------";
1.18 +"--------- maximum example with 'specify', fmz <> [] -------------";
1.19 +"--------- maximum example with 'specify', fmz = [] --------------";
1.20 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.21 +"-----------------------------------------------------------------";
1.22 +"-----------------------------------------------------------------";
1.23 +"-----------------------------------------------------------------";
1.24 +
1.25 +
1.26 +"--------- get_interval after replace} other 2 -------------------";
1.27 +"--------- get_interval after replace} other 2 -------------------";
1.28 +"--------- get_interval after replace} other 2 -------------------";
1.29 + states:=[];
1.30 + CalcTree
1.31 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.32 + ("Test.thy",
1.33 + ["sqroot-test","univariate","equation","test"],
1.34 + ["Test","squ-equ-test-subpbl1"]))];
1.35 + Iterator 1;
1.36 + moveActiveRoot 1;
1.37 + autoCalculate 1 CompleteCalc;
1.38 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.39 + replaceFormula 1 "x = 1";
1.40 + (*... returns calcChangedEvent with ...*)
1.41 + val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1.42 + val ((pt,_),_) = get_calc 1;
1.43 +
1.44 +print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
1.45 +if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) =
1.46 + [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm),
1.47 + ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.48 + ([3, 2], Res)] then () else
1.49 +raise error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
1.50 +
1.51 +print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
1.52 +print_depth 3;
1.53 +if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
1.54 + [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
1.55 +raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
1.56 +
1.57 +
1.58 +
1.59 +
1.60 +"--------- maximum example with 'specify' ------------------------";
1.61 +"--------- maximum example with 'specify' ------------------------";
1.62 +"--------- maximum example with 'specify' ------------------------";
1.63 +(*" Specify_Problem (match_itms_oris) ";*)
1.64 +val fmz =
1.65 + ["fixedValues [r=Arbfix]","maximum A",
1.66 + "valuesFor [a,b]",
1.67 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.68 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.69 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.70 +
1.71 + "boundVariable a","boundVariable b","boundVariable alpha",
1.72 + "interval {x::real. 0 <= x & x <= 2*r}",
1.73 + "interval {x::real. 0 <= x & x <= 2*r}",
1.74 + "interval {x::real. 0 <= x & x <= pi}",
1.75 + "errorBound (eps=(0::real))"];
1.76 +val (dI',pI',mI') =
1.77 + ("DiffApp.thy",["maximum_of","function"],
1.78 + ["DiffApp","max_by_calculus"]);
1.79 +val c = []:cid;
1.80 +
1.81 +(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
1.82 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
1.83 +*)
1.84 +val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.85 +val nxt = tac2tac_ pt p nxt;
1.86 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.87 +(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
1.88 +
1.89 +val nxt = tac2tac_ pt p nxt;
1.90 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.91 +(**)
1.92 +
1.93 +(*---6.5.03
1.94 +val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
1.95 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.96 +(*uncaught exception TYPE 6.5.03*)
1.97 +
1.98 +if ppc<>(Problem [],
1.99 + {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
1.100 + Given=[Correct "fixedValues [r = Arbfix]"],
1.101 + Relate=[Incompl "relations []"], Where=[],With=[]})
1.102 +then raise error "test-maximum.sml: model stepwise - different behaviour"
1.103 +else (); (*different with show_types !!!*)
1.104 +6.5.03---*)
1.105 +
1.106 +(*-----appl_add should not create Error', but accept as Sup,Syn
1.107 +val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
1.108 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.109 +(**)
1.110 +val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
1.111 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.112 +(**)---*)
1.113 +
1.114 +val m = Specify_Problem ["maximum_of","function"];
1.115 +val nxt = tac2tac_ pt p m;
1.116 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.117 +(**)
1.118 +
1.119 +if ppc<>(Problem ["maximum_of","function"],
1.120 + {Find=[Incompl "maximum",Incompl "valuesFor"],
1.121 + Given=[Correct "fixedValues [r = Arbfix]"],
1.122 + Relate=[Incompl "relations []"], Where=[],With=[]})
1.123 +then raise error "diffappl.sml: Specify_Problem different behaviour"
1.124 +else ();
1.125 +(* WN.3.9.03 (#391) Model_Specify did init_pbl newly
1.126 +if ppc<>(Problem ["maximum_of","function"],
1.127 + {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
1.128 + Given=[Correct "fixedValues [r = Arbfix]"],
1.129 + Relate=[Missing "relations rs_"],Where=[],With=[]})
1.130 +then raise error "diffappl.sml: Specify_Problem different behaviour"
1.131 +else ();*)
1.132 +
1.133 +val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
1.134 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.135 +(**)
1.136 +
1.137 +if ppc<>(Method ["DiffApp","max_by_calculus"],
1.138 + {Find=[Incompl "maximum",Incompl "valuesFor"],
1.139 + Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",
1.140 + Missing "interval itv_",Missing "errorBound err_"],
1.141 + Relate=[Incompl "relations []"],Where=[],With=[]})
1.142 +then raise error "diffappl.sml: Specify_Method different behaviour"
1.143 +else ();
1.144 +(* WN.3.9.03 (#391) Model_Specify did init_pbl newly
1.145 +if ppc<>(Method ["DiffApp","max_by_calculus"],
1.146 + {Find=[Missing "maximum m_",Missing "valuesFor vs_"],
1.147 + Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",
1.148 + Missing "interval itv_",Missing "errorBound err_"],
1.149 + Relate=[Missing "relations rs_"],Where=[],With=[]})
1.150 +then raise error "diffappl.sml: Specify_Method different behaviour"
1.151 +else ();*)
1.152 +
1.153 +
1.154 +
1.155 +"--------- maximum example with 'specify', fmz <> [] -------------";
1.156 +"--------- maximum example with 'specify', fmz <> [] -------------";
1.157 +"--------- maximum example with 'specify', fmz <> [] -------------";
1.158 +val fmz =
1.159 + ["fixedValues [r=Arbfix]","maximum A",
1.160 + "valuesFor [a,b]",
1.161 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.162 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.163 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.164 +
1.165 + "boundVariable a","boundVariable b","boundVariable alpha",
1.166 + "interval {x::real. 0 <= x & x <= 2*r}",
1.167 + "interval {x::real. 0 <= x & x <= 2*r}",
1.168 + "interval {x::real. 0 <= x & x <= pi}",
1.169 + "errorBound (eps=(0::real))"];
1.170 +val (dI',pI',mI') =
1.171 + ("DiffApp.thy",["maximum_of","function"],
1.172 + ["DiffApp","max_by_calculus"]);
1.173 +val c = []:cid;
1.174 +(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
1.175 +val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.176 +
1.177 +val nxt = tac2tac_ pt p nxt;
1.178 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
1.179 +val nxt = tac2tac_ pt p nxt;
1.180 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.181 +(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
1.182 +
1.183 +val nxt = tac2tac_ pt p nxt;
1.184 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.185 +(*val nxt = Add_Find "maximum (A::bool)" : tac*)
1.186 +
1.187 +val nxt = tac2tac_ pt p nxt;
1.188 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.189 +(*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
1.190 +
1.191 +val nxt = tac2tac_ pt p nxt;
1.192 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.193 +(*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
1.194 +
1.195 +val nxt = tac2tac_ pt p nxt;
1.196 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.197 +(*val nxt = Add_Relation "relations [A = a * b]" *)
1.198 +
1.199 +val nxt = tac2tac_ pt p nxt;
1.200 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.201 +(*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
1.202 +
1.203 +(*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
1.204 + nxt_specif <> specify ?!
1.205 +
1.206 +if nxt<>(Add_Relation
1.207 + "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
1.208 +then raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
1.209 +
1.210 +val nxt = tac2tac_ pt p nxt;
1.211 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.212 +------------------------------ FIXXXXME.meNEW !!! ---*)
1.213 +
1.214 +(*val nxt = Specify_Theory "DiffApp.thy" : tac*)
1.215 +
1.216 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
1.217 +
1.218 +val nxt = tac2tac_ pt p nxt;
1.219 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.220 +(*val nxt = Specify_Problem ["maximum_of","function"]*)
1.221 +
1.222 +val nxt = tac2tac_ pt p nxt;
1.223 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.224 +(*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
1.225 +
1.226 +val nxt = tac2tac_ pt p nxt;
1.227 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.228 +(*val nxt = Add_Given "boundVariable a" : tac*)
1.229 +
1.230 +val nxt = tac2tac_ pt p nxt;
1.231 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.232 +(*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
1.233 +
1.234 +val nxt = tac2tac_ pt p nxt;
1.235 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.236 +(*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
1.237 +
1.238 +val nxt = tac2tac_ pt p nxt;
1.239 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.240 +(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
1.241 +if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
1.242 +then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
1.243 +
1.244 +
1.245 +"--------- maximum example with 'specify', fmz = [] --------------";
1.246 +"--------- maximum example with 'specify', fmz = [] --------------";
1.247 +"--------- maximum example with 'specify', fmz = [] --------------";
1.248 +val fmz = [];
1.249 +val (dI',pI',mI') = empty_spec;
1.250 +val c = []:cid;
1.251 +
1.252 +val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
1.253 +(*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
1.254 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
1.255 + EmptyPtree;
1.256 +val nxt = tac2tac_ pt p nxt;
1.257 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.258 +(*val nxt = Specify_Theory "e_domID" : tac*)
1.259 +
1.260 +val nxt = Specify_Theory "DiffApp.thy";
1.261 +val nxt = tac2tac_ pt p nxt;
1.262 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.263 +(*val nxt = Specify_Problem ["e_pblID"] : tac*)
1.264 +
1.265 +val nxt = Specify_Problem ["maximum_of","function"];
1.266 +val nxt = tac2tac_ pt p nxt;
1.267 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.268 +(*val nxt = Add_Given "fixedValues" : tac*)
1.269 +
1.270 +val nxt = Add_Given "fixedValues [r=Arbfix]";
1.271 +val nxt = tac2tac_ pt p nxt;
1.272 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.273 +(*val nxt = Add_Find "maximum" : tac*)
1.274 +
1.275 +val nxt = Add_Find "maximum A";
1.276 +val nxt = tac2tac_ pt p nxt;
1.277 +
1.278 +
1.279 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.280 +(*val nxt = Add_Find "valuesFor" : tac*)
1.281 +
1.282 +val nxt = Add_Find "valuesFor [a]";
1.283 +val nxt = tac2tac_ pt p nxt;
1.284 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.285 +(*val nxt = Add_Relation "relations" ---
1.286 + --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
1.287 +
1.288 +(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
1.289 +if nxt<>(Add_Relation "relations []")
1.290 +then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
1.291 +else (); (*different with show_types !!!*)
1.292 +*)
1.293 +
1.294 +val nxt = Add_Relation "relations [(A=a+b)]";
1.295 +val nxt = tac2tac_ pt p nxt;
1.296 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.297 +(*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
1.298 +
1.299 +val nxt = Specify_Method ["DiffApp","max_by_calculus"];
1.300 +val nxt = tac2tac_ pt p nxt;
1.301 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.302 +(*val nxt = Add_Given "boundVariable" : tac*)
1.303 +
1.304 +val nxt = Add_Given "boundVariable alpha";
1.305 +val nxt = tac2tac_ pt p nxt;
1.306 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.307 +(*val nxt = Add_Given "interval" : tac*)
1.308 +
1.309 +val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
1.310 +val nxt = tac2tac_ pt p nxt;
1.311 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.312 +(*val nxt = Add_Given "errorBound" : tac*)
1.313 +
1.314 +val nxt = Add_Given "errorBound (eps=999)";
1.315 +val nxt = tac2tac_ pt p nxt;
1.316 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.317 +(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
1.318 +(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
1.319 +if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
1.320 +then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
1.321 +else ();
1.322 +*)
1.323 +
1.324 +(* 2.4.00 nach Transfer specify -> hard_gen
1.325 +val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
1.326 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
1.327 +(*val nxt = Empty_Tac : tac*)
1.328 +
1.329 +
1.330 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.331 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.332 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
1.333 +val Const ("Script.SubProblem",_) $
1.334 + (Const ("Pair",_) $
1.335 + Free (dI',_) $
1.336 + (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.337 + (*...copied from stac2tac_*)
1.338 + str2term
1.339 + "SubProblem (EqSystem_, [linear, system], [no_met])\
1.340 + \ [bool_list_ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
1.341 + \ real_list_ [c, c_2]]";
1.342 +val ags = isalist2list ags';
1.343 +val pI = ["linear","system"];
1.344 +val pats = (#ppc o get_pbt) pI;
1.345 +case match_ags Isac.thy pats ags of
1.346 + [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.347 + (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.348 + [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
1.349 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
1.350 + =>()
1.351 + | _ => raise error "calchead.sml match_ags 2 args OK -----------------";
1.352 +
1.353 +
1.354 +val Const ("Script.SubProblem",_) $
1.355 + (Const ("Pair",_) $
1.356 + Free (dI',_) $
1.357 + (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.358 + (*...copied from stac2tac_*)
1.359 + str2term
1.360 + "SubProblem (EqSystem_, [linear, system], [no_met])\
1.361 + \ [bool_list_ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
1.362 + \ real_list_ [c, c_2], bool_list_ ss___]";
1.363 +val ags = isalist2list ags';
1.364 +val pI = ["linear","system"];
1.365 +val pats = (#ppc o get_pbt) pI;
1.366 +case match_ags Isac.thy pats ags of
1.367 + [(1, [1], "#Given", Const ("Descript.equalities", _), _),
1.368 + (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
1.369 + [_ $ Free ("c", _) $ _,
1.370 + _ $ Free ("c_2", _) $ _]),
1.371 + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]
1.372 + (* type of Find: [Free ("ss___", "bool List.list")]*)
1.373 + =>()
1.374 + | _ => raise error "calchead.sml match_ags copy-named dropped --------";
1.375 +
1.376 +
1.377 +val stac as Const ("Script.SubProblem",_) $
1.378 + (Const ("Pair",_) $
1.379 + Free (dI',_) $
1.380 + (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.381 + (*...copied from stac2tac_*)
1.382 + str2term
1.383 + "SubProblem (EqSystem_, [linear, system], [no_met])\
1.384 + \ [real_list_ [c, c_2]]";
1.385 +val ags = isalist2list ags';
1.386 +val pI = ["linear","system"];
1.387 +val pats = (#ppc o get_pbt) pI;
1.388 +case ((match_ags Isac.thy pats ags)
1.389 + handle TYPE _ => []) of
1.390 + [] => match_ags_msg pI stac ags
1.391 + | _ => raise error "calchead.sml match_ags 1st arg missing --------";
1.392 +
1.393 +(*
1.394 +use"../smltest/ME/calchead.sml";
1.395 +*)
1.396 +
1.397 +val stac as Const ("Script.SubProblem",_) $
1.398 + (Const ("Pair",_) $
1.399 + Free (dI',_) $
1.400 + (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.401 + (*...copied from stac2tac_*)
1.402 + str2term
1.403 + "SubProblem (Test_,[univariate,equation,test],\
1.404 + \ [no_met]) [bool_ (x+1=2), real_ x]";
1.405 +val ags = isalist2list ags';
1.406 +val pI = ["univariate","equation","test"];
1.407 +val pats = (#ppc o get_pbt) pI;
1.408 +case match_ags Isac.thy pats ags of
1.409 + [(1, [1], "#Given",
1.410 + Const ("Descript.equality", _),
1.411 + [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),
1.412 + (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
1.413 + (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
1.414 + (* type of Find: [Free ("x_i", "bool List.list")]*)
1.415 + => ()
1.416 + | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";