1.1 --- a/test/Tools/isac/Interpret/calchead.sml Wed Dec 14 09:37:01 2016 +0100
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Wed Dec 14 10:45:41 2016 +0100
1.3 @@ -80,15 +80,15 @@
1.4
1.5 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.6 val nxt = tac2tac_ pt p nxt;
1.7 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.8 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.9 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
1.10
1.11 val nxt = tac2tac_ pt p nxt;
1.12 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.13 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.14 (**)
1.15
1.16 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
1.17 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.18 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.19 if ppc<>(Problem [],
1.20 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
1.21 Given=[Correct "fixedValues [r = Arbfix]"],
1.22 @@ -102,18 +102,18 @@
1.23 Some tests have been broken much earlier,
1.24 see test/../calchead.sml "inhibit exn 010830". *)
1.25 (*========== inhibit exn WN1130630 maximum example broken =========================
1.26 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.27 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.28 ============ inhibit exn WN1130630 maximum example broken =======================*)
1.29
1.30 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
1.31 (*========== inhibit exn WN1130630 maximum example broken =========================
1.32 (* ERROR: Exception Bind raised *)
1.33 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.34 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.35 ============ inhibit exn WN1130630 maximum example broken =======================*)
1.36
1.37 val m = Specify_Problem ["maximum_of","function"];
1.38 val nxt = tac2tac_ pt p m;
1.39 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.40 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.41 (*========== inhibit exn WN1130630 maximum example broken =========================
1.42 if ppc<>(Problem ["maximum_of","function"],
1.43 {Find=[Incompl "maximum",Incompl "valuesFor"],
1.44 @@ -131,7 +131,7 @@
1.45 ============ inhibit exn WN1130630 maximum example broken =======================*)
1.46
1.47 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
1.48 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.49 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.50 (*========== inhibit exn WN1130630 maximum example broken =========================
1.51 if ppc<>(Method ["DiffApp","max_by_calculus"],
1.52 {Find=[Incompl "maximum",Incompl "valuesFor"],
1.53 @@ -173,29 +173,29 @@
1.54 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.55
1.56 val nxt = tac2tac_ pt p nxt;
1.57 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
1.58 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
1.59 val nxt = tac2tac_ pt p nxt;
1.60 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.61 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.62 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
1.63
1.64 val nxt = tac2tac_ pt p nxt;
1.65 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.66 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.67 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
1.68
1.69 val nxt = tac2tac_ pt p nxt;
1.70 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.71 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.72 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
1.73
1.74 val nxt = tac2tac_ pt p nxt;
1.75 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.76 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.77 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
1.78
1.79 val nxt = tac2tac_ pt p nxt;
1.80 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.81 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.82 (*val nxt = Add_Relation "relations [A = a * b]" *)
1.83
1.84 val nxt = tac2tac_ pt p nxt;
1.85 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.86 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.87 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
1.88
1.89 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
1.90 @@ -206,7 +206,7 @@
1.91 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
1.92
1.93 val nxt = tac2tac_ pt p nxt;
1.94 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.95 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.96 ------------------------------ FIXXXXME.meNEW !!! ---*)
1.97
1.98 (*val nxt = Specify_Theory "DiffApp" : tac*)
1.99 @@ -214,27 +214,27 @@
1.100 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
1.101
1.102 val nxt = tac2tac_ pt p nxt;
1.103 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.104 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.105 (*val nxt = Specify_Problem ["maximum_of","function"]*)
1.106
1.107 val nxt = tac2tac_ pt p nxt;
1.108 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.109 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.110 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
1.111
1.112 val nxt = tac2tac_ pt p nxt;
1.113 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.114 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.115 (*val nxt = Add_Given "boundVariable a" : tac*)
1.116
1.117 val nxt = tac2tac_ pt p nxt;
1.118 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.119 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.120 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
1.121
1.122 val nxt = tac2tac_ pt p nxt;
1.123 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.124 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.125 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
1.126
1.127 val nxt = tac2tac_ pt p nxt;
1.128 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.129 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.130 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
1.131 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
1.132 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
1.133 @@ -249,37 +249,37 @@
1.134
1.135 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
1.136 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
1.137 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
1.138 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
1.139 EmptyPtree;
1.140 val nxt = tac2tac_ pt p nxt;
1.141 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.142 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.143 (*val nxt = Specify_Theory "e_domID" : tac*)
1.144
1.145 val nxt = Specify_Theory "DiffApp";
1.146 val nxt = tac2tac_ pt p nxt;
1.147 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.148 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.149 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
1.150
1.151 val nxt = Specify_Problem ["maximum_of","function"];
1.152 val nxt = tac2tac_ pt p nxt;
1.153 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.154 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.155 (*val nxt = Add_Given "fixedValues" : tac*)
1.156
1.157 val nxt = Add_Given "fixedValues [r=Arbfix]";
1.158 val nxt = tac2tac_ pt p nxt;
1.159 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.160 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.161 (*val nxt = Add_Find "maximum" : tac*)
1.162
1.163 val nxt = Add_Find "maximum A";
1.164 val nxt = tac2tac_ pt p nxt;
1.165
1.166
1.167 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.168 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.169 (*val nxt = Add_Find "valuesFor" : tac*)
1.170
1.171 val nxt = Add_Find "valuesFor [a]";
1.172 val nxt = tac2tac_ pt p nxt;
1.173 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.174 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.175 (*val nxt = Add_Relation "relations" ---
1.176 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
1.177
1.178 @@ -293,27 +293,27 @@
1.179
1.180 val nxt = Add_Relation "relations [(A=a+b)]";
1.181 val nxt = tac2tac_ pt p nxt;
1.182 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.183 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.184 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
1.185
1.186 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
1.187 val nxt = tac2tac_ pt p nxt;
1.188 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.189 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.190 (*val nxt = Add_Given "boundVariable" : tac*)
1.191
1.192 val nxt = Add_Given "boundVariable alpha";
1.193 val nxt = tac2tac_ pt p nxt;
1.194 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.195 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.196 (*val nxt = Add_Given "interval" : tac*)
1.197
1.198 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
1.199 val nxt = tac2tac_ pt p nxt;
1.200 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.201 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.202 (*val nxt = Add_Given "errorBound" : tac*)
1.203
1.204 val nxt = Add_Given "errorBound (eps=999)";
1.205 val nxt = tac2tac_ pt p nxt;
1.206 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
1.207 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
1.208 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
1.209
1.210 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
1.211 @@ -323,7 +323,7 @@
1.212 *)
1.213 (* 2.4.00 nach Transfer specify -> hard_gen
1.214 val nxt = Apply_Method ("DiffApp","max_by_calculus");
1.215 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
1.216 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
1.217 (*val nxt = Empty_Tac : tac*)
1.218
1.219 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";