1.1 --- a/doc-src/isac/akargl/ferialprakt.tex Mon Jul 18 09:51:51 2011 +0200
1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex Tue Jul 19 09:43:01 2011 +0200
1.3 @@ -42,7 +42,8 @@
1.4 & ML- Programmierung & 2.5 \\
1.5 & Einf\"uhrung ML/\sisac\ V & 1.0 \\
1.6 & ML- Programmierung & 3.0 \\ \hline
1.7 - & & \\
1.8 +18.7.2011
1.9 + & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.10 \end{tabular}
1.11 \end{center}
1.12
2.1 --- a/test/Tools/isac/Frontend/interface.sml Mon Jul 18 09:51:51 2011 +0200
2.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue Jul 19 09:43:01 2011 +0200
2.3 @@ -136,7 +136,6 @@
2.4
2.5 (*-------------------------------------------------------------------------*)
2.6 fetchProposedTactic 1;
2.7 -(*========== inhibit exn 110310 ================================================
2.8 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.9
2.10 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
2.11 @@ -168,9 +167,9 @@
2.12 (*exception just above means: 'ModSpec' has been returned: error anyway*)
2.13 if term2str f = "[x = 1]" then () else
2.14 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
2.15 -============ inhibit exn 110310 ==============================================*)
2.16
2.17 -(*========== inhibit exn 110620 ================================================
2.18 +
2.19 +
2.20 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.21 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.22 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.23 @@ -193,7 +192,7 @@
2.24 if get_pos 1 1 = ([], Res) then () else
2.25 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
2.26 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
2.27 -============ inhibit exn 110620 ==============================================*)
2.28 +
2.29
2.30 "--------- miniscript with mini-subpbl ------------------";
2.31 "--------- miniscript with mini-subpbl ------------------";
2.32 @@ -371,13 +370,12 @@
2.33
2.34 DEconstrCalcTree 1;
2.35
2.36 -(*========== inhibit exn 110620 ================================================
2.37 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.38 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.39 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.40 states:=[];
2.41 CalcTree
2.42 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
2.43 + [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"],
2.44 ("Test",
2.45 ["linear","univariate","equation","test"],
2.46 ["Test","solve_linear"]))];
2.47 @@ -389,7 +387,12 @@
2.48 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.49 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.50
2.51 +(*========== inhibit exn 110718 ================================================
2.52 +
2.53 val ((pt,_),_) = get_calc 1;
2.54 +
2.55 +
2.56 +
2.57 val p = get_pos 1 1;
2.58 val (Form f, tac, asms) = pt_extract (pt, p);
2.59 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.60 @@ -398,7 +401,9 @@
2.61 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.62 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.63 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.64 - states:=[];
2.65 +========== inhibit exn 110718 ================================================*)
2.66 +
2.67 +states:=[];
2.68 CalcTree
2.69 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
2.70 ("Test",
2.71 @@ -407,14 +412,17 @@
2.72 Iterator 1;
2.73 moveActiveRoot 1;
2.74 autoCalculate 1 CompleteCalcHead;
2.75 +(*========== inhibit exn 110718 ================================================
2.76 +
2.77 refFormula 1 (get_pos 1 1);
2.78 +
2.79 val ((pt,p),_) = get_calc 1;
2.80
2.81 autoCalculate 1 CompleteCalc;
2.82 val ((pt,p),_) = get_calc 1;
2.83 if p=([], Res) then () else
2.84 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
2.85 -============ inhibit exn 110620 ==============================================*)
2.86 +============ inhibit exn 110718 ==============================================*)
2.87
2.88 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.89 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.90 @@ -426,9 +434,9 @@
2.91 Iterator 1;
2.92 moveActiveRoot 1;
2.93 autoCalculate 1 CompleteCalc;
2.94 -(*========== inhibit exn 110620 ================================================
2.95 +
2.96 val ((pt,p),_) = get_calc 1; show_pt pt;
2.97 - ERROR 110620 there is only 1 PblObj
2.98 + (*ERROR 110620 there is only 1 PblObj*)
2.99 (*
2.100 getTactic 1 ([1],Frm);
2.101 getTactic 1 ([1],Res);
2.102 @@ -446,7 +454,7 @@
2.103 val (Form f, tac, asms) = pt_extract (pt, p);
2.104 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.105 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
2.106 -============ inhibit exn 110620 ==============================================*)
2.107 +
2.108
2.109
2.110 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.111 @@ -481,7 +489,7 @@
2.112 Iterator 1;
2.113 moveActiveRoot 1;
2.114 autoCalculate 1 CompleteModel;
2.115 -(*========== inhibit exn 110622 ================================================
2.116 +(*========== inhibit exn 110718 ================================================
2.117 refFormula 1 (get_pos 1 1);
2.118 <ERROR> error in kernel </ERROR>
2.119 get_pos: calc 1 not existent
2.120 @@ -499,20 +507,25 @@
2.121 ["linear", "univariate","equation","test"],
2.122 ["Test","solve_linear"]) then ()
2.123 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
2.124 +============ inhibit exn 110718 ==============================================*)
2.125
2.126 autoCalculate 1 CompleteCalcHead;
2.127 +(*========== inhibit exn 110718 ================================================
2.128 refFormula 1 (get_pos 1 1);
2.129 +============ inhibit exn 110718 ==============================================*)
2.130 autoCalculate 1 CompleteCalc;
2.131 moveActiveDown 1;
2.132 moveActiveDown 1;
2.133 moveActiveDown 1;
2.134 +(*========== inhibit exn 110718 ================================================
2.135 +
2.136 refFormula 1 (get_pos 1 1);
2.137 val ((pt,_),_) = get_calc 1;
2.138 val p = get_pos 1 1;
2.139 val (Form f, tac, asms) = pt_extract (pt, p);
2.140 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.141 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
2.142 -============ inhibit exn 110622 ==============================================*)
2.143 +============ inhibit exn 110718 ==============================================*)
2.144
2.145
2.146 "--------- setContext..Thy ------------------------------";
2.147 @@ -544,12 +557,12 @@
2.148 autoCalculate 1 CompleteCalc;
2.149 val ((pt,p),_) = get_calc 1; show_pt pt;
2.150 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
2.151 -(*========== inhibit exn 110622 ================================================
2.152 +(*========== inhibit exn 110718 ================================================
2.153 ERROR still 3 lines
2.154 val (Form f, tac, asms) = pt_extract (pt, p);
2.155 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.156 error "--- setContext..Thy --- autoCalculate CompleteCalc";
2.157 -============ inhibit exn 110622 ==============================================*)
2.158 +============ inhibit exn 110718 ==============================================*)
2.159
2.160 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.161 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.162 @@ -576,17 +589,15 @@
2.163 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
2.164 val ((pt,_),_) = get_calc 1;
2.165 val p = get_pos 1 1;
2.166 -(*========== inhibit exn 110622 ================================================
2.167 +
2.168 val (Form f, tac, asms) = pt_extract (pt, p);
2.169 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.170 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
2.171 -============ inhibit exn 110622 ==============================================*)
2.172
2.173
2.174 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.175 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.176 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.177 -(*========== inhibit exn 110622 ================================================
2.178 states:=[];
2.179 CalcTree
2.180 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
2.181 @@ -594,8 +605,12 @@
2.182 Iterator 1;
2.183 moveActiveRoot 1;
2.184 fetchProposedTactic 1;
2.185 - setNextTactic 1 (Model_Problem );
2.186 +
2.187 +(*========== inhibit exn 110718 ================================================
2.188 +(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
2.189 +setNextTactic 1 (Model_Problem );
2.190 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.191 +
2.192 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
2.193 setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
2.194 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.195 @@ -604,6 +619,8 @@
2.196 setNextTactic 1 (Add_Find "solutions L");
2.197 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.198 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
2.199 +
2.200 +
2.201 setNextTactic 1 (Specify_Theory "RatEq");
2.202 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.203 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
2.204 @@ -618,6 +635,7 @@
2.205 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.206 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
2.207 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.208 +
2.209 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
2.210 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
2.211 "univariate","equation"]));
2.212 @@ -708,7 +726,7 @@
2.213 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
2.214 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
2.215 ============ inhibit exn 2009 ================================================*)
2.216 -============ inhibit exn 110622 ==============================================*)
2.217 +============ inhibit exn 110718 ==============================================*)
2.218
2.219
2.220 "--------- tryMatchProblem, tryRefineProblem ------------";
2.221 @@ -791,15 +809,16 @@
2.222
2.223 fetchProposedTactic 1;
2.224 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
2.225 -(*========== inhibit exn 110622 ================================================
2.226 - vvvvvvvvvvvv
2.227 autoCalculate 1 CompleteCalc;
2.228 val ((pt,_),_) = get_calc 1;
2.229 show_pt pt;
2.230 val p = get_pos 1 1;
2.231 val (Form f, tac, asms) = pt_extract (pt, p);
2.232 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.233 +
2.234 +(*========== inhibit exn 110718 ================================================
2.235 +if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.236 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.237 +========== inhibit exn 110718 ================================================*)
2.238
2.239 (*------------^^^-inserted-----------------------------------------------*)
2.240 (*WN050904 the fetchProposedTactic's below may not have worked like that
2.241 @@ -820,10 +839,13 @@
2.242 rootthy pt;
2.243 show_pt pt;
2.244 val p = get_pos 1 1;
2.245 +(*========== inhibit exn 110718 ================================================
2.246 +
2.247 val (Form f, tac, asms) = pt_extract (pt, p);
2.248 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.249 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.250 -============ inhibit exn 110622 ==============================================*)
2.251 +
2.252 +============ inhibit exn 110718 ==============================================*)
2.253
2.254
2.255 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.256 @@ -1124,13 +1146,15 @@
2.257 Iterator 1; moveActiveRoot 1;
2.258
2.259 fetchProposedTactic 1;
2.260 -(*========== inhibit exn 110628 ================================================
2.261 - ERROR get_calc 1 not existent
2.262 +(*========== inhibit exn 110719 ================================================
2.263 + (*ERROR get_calc 1 not existent*)
2.264 setNextTactic 1 (Model_Problem );
2.265 autoCalculate 1 (Step 1);
2.266 +========== inhibit exn 110719 ================================================*)
2.267
2.268 fetchProposedTactic 1;
2.269 fetchProposedTactic 1;
2.270 +(*========== inhibit exn 110719 ================================================
2.271
2.272 setNextTactic 1 (Add_Find "solutions L");
2.273 setNextTactic 1 (Add_Find "solutions L");
2.274 @@ -1155,14 +1179,18 @@
2.275 setNextTactic 1 (Rewrite_Set "Test_simplify");
2.276 fetchProposedTactic 1;
2.277 autoCalculate 1 (Step 1);
2.278 +============ inhibit exn 110719 ==============================================*)
2.279
2.280 autoCalculate 1 CompleteCalc;
2.281 +(*============ inhibit exn 110719 ==============================================
2.282 +
2.283 val ((pt,_),_) = get_calc 1;
2.284 val p = get_pos 1 1;
2.285 val (Form f, tac, asms) = pt_extract (pt, p);
2.286 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.287 error "FE-interface.sml: diff.behav. in combinations of steps";
2.288 -============ inhibit exn 11062 ==============================================*)
2.289 +============ inhibit exn 110719 ==============================================*)
2.290 +
2.291
2.292
2.293 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
2.294 @@ -1235,10 +1263,8 @@
2.295 val ((pt,_),_) = get_calc 1;
2.296 val p = get_pos 1 1;
2.297 val (Form f, tac, asms) = pt_extract (pt, p);
2.298 -(*========== inhibit exn 110628 ================================================
2.299 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
2.300 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
2.301 -============ inhibit exn 110682 ==============================================*)
2.302
2.303
2.304 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
2.305 @@ -1279,7 +1305,6 @@
2.306
2.307 val ((pt,_),_) = get_calc 1;
2.308 val p = get_pos 1 1;
2.309 -(*========== inhibit exn 110628 ================================================
2.310 val (Form f, tac, asms) = pt_extract (pt, p);
2.311 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.312 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
2.313 @@ -1287,7 +1312,6 @@
2.314 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
2.315 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
2.316 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
2.317 - ============ inhibit exn 110682 ==============================================*)
2.318
2.319 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
2.320 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.321 @@ -1302,7 +1326,6 @@
2.322
2.323 val ((pt,_),_) = get_calc 2;
2.324 val p = get_pos 2 1;
2.325 -(*========== inhibit exn 110628 ================================================
2.326 val (Form f, tac, asms) = pt_extract (pt, p);
2.327 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.328 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
2.329 @@ -1310,9 +1333,7 @@
2.330 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
2.331 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
2.332 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
2.333 - ============ inhibit exn 110682 ==============================================*)
2.334
2.335 -(*========== inhibit exn 110628 ================================================
2.336 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.337 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.338 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.339 @@ -1399,6 +1420,5 @@
2.340 val (Form f, tac, asms) = pt_extract (pt, p);
2.341 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.342 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
2.343 -============ inhibit exn 110628 ==============================================*)
2.344
2.345
3.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Jul 18 09:51:51 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/calchead.sml Tue Jul 19 09:43:01 2011 +0200
3.3 @@ -1,4 +1,5 @@
3.4 -(* Title: tests on calchead.sml
3.5 +
3.6 + (* Title: tests on calchead.sml
3.7 Author: Walther Neuper 051013,
3.8 (c) due to copyright terms
3.9
3.10 @@ -21,7 +22,7 @@
3.11 "--------------------------------------------------------";
3.12 "--------------------------------------------------------";
3.13
3.14 -(*========== inhibit exn =======================================================
3.15 +
3.16 "--------- get_interval after replace} other 2 ----------";
3.17 "--------- get_interval after replace} other 2 ----------";
3.18 "--------- get_interval after replace} other 2 ----------";
3.19 @@ -75,9 +76,6 @@
3.20 ["DiffApp","max_by_calculus"]);
3.21 val c = []:cid;
3.22
3.23 -(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));
3.24 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
3.25 -*)
3.26 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.27 val nxt = tac2tac_ pt p nxt;
3.28 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.29 @@ -87,7 +85,7 @@
3.30 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.31 (**)
3.32
3.33 -(*---6.5.03
3.34 +(*========== inhibit exn AK110718 =======================================================
3.35 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
3.36 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.37 (*uncaught exception TYPE 6.5.03*)
3.38 @@ -98,21 +96,21 @@
3.39 Relate=[Incompl "relations []"], Where=[],With=[]})
3.40 then error "test-maximum.sml: model stepwise - different behaviour"
3.41 else (); (*different with show_types !!!*)
3.42 -6.5.03---*)
3.43 +========== inhibit exn AK110718 =======================================================*)
3.44
3.45 -(*-----appl_add should not create Error', but accept as Sup,Syn
3.46 +(*========== inhibit exn AK110718 =======================================================
3.47 val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
3.48 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.49 -(**)
3.50 +
3.51 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
3.52 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.53 -(**)---*)
3.54 +========== inhibit exn AK110718 =======================================================*)
3.55
3.56 val m = Specify_Problem ["maximum_of","function"];
3.57 val nxt = tac2tac_ pt p m;
3.58 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.59 (**)
3.60 -
3.61 +(*========== inhibit exn AK110718 =======================================================
3.62 if ppc<>(Problem ["maximum_of","function"],
3.63 {Find=[Incompl "maximum",Incompl "valuesFor"],
3.64 Given=[Correct "fixedValues [r = Arbfix]"],
3.65 @@ -146,7 +144,7 @@
3.66 Relate=[Missing "relations rs_"],Where=[],With=[]})
3.67 then error "diffappl.sml: Specify_Method different behaviour"
3.68 else ();*)
3.69 -
3.70 +========== inhibit exn AK110718 =======================================================*)
3.71
3.72
3.73 "--------- maximum example with 'specify', fmz <> [] -------------";
3.74 @@ -282,11 +280,13 @@
3.75 (*val nxt = Add_Relation "relations" ---
3.76 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
3.77
3.78 +(*========== inhibit exn 010830 =======================================================
3.79 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
3.80 if nxt<>(Add_Relation "relations []")
3.81 then error "test specify, fmz <> []: nxt <> Add_Relation.."
3.82 else (); (*different with show_types !!!*)
3.83 *)
3.84 +========== inhibit exn 010830 =======================================================*)
3.85
3.86 val nxt = Add_Relation "relations [(A=a+b)]";
3.87 val nxt = tac2tac_ pt p nxt;
3.88 @@ -312,18 +312,22 @@
3.89 val nxt = tac2tac_ pt p nxt;
3.90 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
3.91 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
3.92 +
3.93 +(*========== inhibit exn 010830 =======================================================
3.94 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
3.95 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
3.96 then error "test specify, fmz <> []: nxt <> Add_Relation.."
3.97 else ();
3.98 *)
3.99 +========== inhibit exn 010830 =======================================================*)
3.100
3.101 +(*========== inhibit exn 000402 =======================================================
3.102 (* 2.4.00 nach Transfer specify -> hard_gen
3.103 val nxt = Apply_Method ("DiffApp","max_by_calculus");
3.104 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
3.105 (*val nxt = Empty_Tac : tac*)
3.106 +========== inhibit exn 000402 =======================================================*)
3.107
3.108 -============ inhibit exn =====================================================*)
3.109
3.110 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.111
3.112 @@ -721,3 +725,4 @@
3.113
3.114 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.115 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.116 +
4.1 --- a/test/Tools/isac/Interpret/ctree.sml Mon Jul 18 09:51:51 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 09:43:01 2011 +0200
4.3 @@ -118,7 +118,7 @@
4.4 "ctree.sml-------------- cappend on complete ctree from above ----";
4.5 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
4.6 "----------------------------------------------------------------/";
4.7 -(*========== inhibit exn WN110319 ==============================================
4.8 +
4.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
4.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
4.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
4.12 @@ -144,6 +144,7 @@
4.13 else error "new behaviour in test: miniscript with mini-subpbl";
4.14
4.15 show_pt pt;
4.16 +(*========== inhibit exn WN110319 ==============================================
4.17 ============ inhibit exn WN110319 ============================================*)
4.18
4.19 (*=== inhibit exn ?=============================================================
5.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Jul 18 09:51:51 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Tue Jul 19 09:43:01 2011 +0200
5.3 @@ -1,3 +1,6 @@
5.4 +
5.5 +
5.6 +
5.7 (* test for sml/ME/mathengine.sml
5.8 authors: Walther Neuper 2000, 2006
5.9 (c) due to copyright terms
5.10 @@ -151,7 +154,6 @@
5.11 "===== tactic Subproblem: from environment to origin";
5.12 "----- TODO";
5.13
5.14 -(*=== inhibit exn ?=============================================================
5.15
5.16 "----------- debugging setContext..pbl_ -----------------";
5.17 "----------- debugging setContext..pbl_ -----------------";
5.18 @@ -217,9 +219,12 @@
5.19 val pIopt = get_pblID (pt,ip);
5.20 ip = ([],Res) (*false*);
5.21 val SOME pI = pIopt;
5.22 +(*=== inhibit exn 110718 ? =============================================================
5.23 +
5.24 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
5.25 (*^^^^^^^^: Apply_Method without init_form*)
5.26 -===== inhibit exn ?===========================================================*)
5.27 +
5.28 +===== inhibit exn 110718 ? ===========================================================*)
5.29
5.30 "----------- fun step -----------------------------------";
5.31 "----------- fun step -----------------------------------";
5.32 @@ -239,7 +244,7 @@
5.33 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
5.34 "----- step 5: returns tac = ---";
5.35
5.36 -(*========== inhibit exn =======================================================
5.37 +(*========== inhibit exn 110718 =======================================================
5.38 2002 stops here as well: TODO review actual arguments:
5.39 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
5.40 "----- step 6: returns tac = ---";
5.41 @@ -248,7 +253,7 @@
5.42 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
5.43 "----- step 8: returns tac = ---";
5.44 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
5.45 -============ inhibit exn =====================================================*)
5.46 +============ inhibit exn 110718 =====================================================*)
5.47
5.48
5.49 "----------- fun autocalc -------------------------------";
5.50 @@ -333,10 +338,9 @@
5.51 autoCalculate 1 (Step 1);
5.52 val (ptp as (_, p), _) = get_calc 1;
5.53 val (Form t,_,_) = pt_extract ptp;
5.54 -(*========== inhibit exn 110310 ================================================
5.55 +
5.56 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
5.57 else error "mathengine.sml -- fun autoCalculate -- end";
5.58 -============ inhibit exn 110310 ==============================================*)
5.59
5.60 "----------- fun autoCalculate..CompleteCalc ------------";
5.61 "----------- fun autoCalculate..CompleteCalc ------------";
5.62 @@ -348,3 +352,6 @@
5.63 Iterator 1;
5.64 moveActiveRoot 1;
5.65
5.66 +
5.67 +
5.68 +
6.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Jul 18 09:51:51 2011 +0200
6.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Jul 19 09:43:01 2011 +0200
6.3 @@ -63,13 +63,13 @@
6.4 map (Thm.derivation_name o #2) symthms;
6.5
6.6
6.7 -(*=== inhibit exn ?=============================================================
6.8 "----------- fun collect_isab_thys ----------------------";
6.9 "----------- fun collect_isab_thys ----------------------";
6.10 "----------- fun collect_isab_thys ----------------------";
6.11 -val ancestors = Theory.ancestors_of (theory "Complex_Main");
6.12 +val ancestors = Theory.ancestors_of @{theory "Complex_Main"};
6.13 val isabthms = (flat o (map Theory.axioms_of)) ancestors;
6.14
6.15 +(*=== inhibit exn ?=============================================================
6.16 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');
6.17 (*thms from rulesets*)
6.18 val isacrlsthms = ((map rep_thm_G') o flat o
6.19 @@ -218,6 +218,7 @@
6.20 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
6.21 (#1 : calc -> string)) (rev (!calclist'));
6.22 WN100819 =====================================================*)
6.23 +=== inhibit exn ?=============================================================*)
6.24
6.25 "----------- initContext Thy_ Integration-demo ----------";
6.26 "----------- initContext Thy_ Integration-demo ----------";
6.27 @@ -229,16 +230,13 @@
6.28 ["diff","integration"]))];
6.29 Iterator 1;
6.30 moveActiveRoot 1;
6.31 -(*TODO.new_c: cvs before 071227, 11:50------------------
6.32 autoCalculate 1 CompleteCalc;
6.33 interSteps 1 ([1],Res);
6.34 interSteps 1 ([1,1],Res);
6.35 val ((pt,p),_) = get_calc 1; show_pt pt;
6.36 if existpt' ([1,1,1], Frm) pt then ()
6.37 else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
6.38 -
6.39 initContext 1 Thy_ ([1,1,1], Frm);
6.40 ---------------------TODO.new_c: cvs before 071227, 11:50*)
6.41
6.42 "----------- initContext..Thy_, fun context_thm ---------";
6.43 "----------- initContext..Thy_, fun context_thm ---------";
6.44 @@ -254,7 +252,6 @@
6.45 val p = ([], Res);
6.46 initContext 1 Thy_ p;
6.47
6.48 -
6.49 interSteps 1 ([2], Res);
6.50 interSteps 1 ([3,1], Res);
6.51 val ((pt,_),_) = get_calc 1; show_pt pt;
6.52 @@ -269,6 +266,7 @@
6.53 andalso term2str result = "-2 + (1 + x) = 0" then ()
6.54 else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
6.55
6.56 +
6.57 val p = ([3,1,1], Frm);
6.58 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
6.59 initContext 1 Thy_ p;
6.60 @@ -367,7 +365,6 @@
6.61 andalso term2str result = "x = 0 + -1 * -1" then ()
6.62 else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
6.63
6.64 -
6.65 "----------- checkContext..Thy_ on last formula ---------";
6.66 "----------- checkContext..Thy_ on last formula ---------";
6.67 "----------- checkContext..Thy_ on last formula ---------";
6.68 @@ -393,6 +390,7 @@
6.69 "----------- fun guh2theID ------------------------------";
6.70 "----------- fun guh2theID ------------------------------";
6.71 val guh = "thy_scri_ListG-thm-zip_Nil";
6.72 +(*========== inhibit exn 110718 ================================================
6.73
6.74 take_fromto 1 4 (explode guh);
6.75 take_fromto 5 9 (explode guh);
6.76 @@ -410,12 +408,13 @@
6.77
6.78 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
6.79 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
6.80 +============ inhibit exn 110718 ==============================================*)
6.81
6.82
6.83 "----------- debugging on Tests/solve_linear_as_rootpbl -";
6.84 "----------- debugging on Tests/solve_linear_as_rootpbl -";
6.85 "----------- debugging on Tests/solve_linear_as_rootpbl -";
6.86 ------ initContext -----";
6.87 +"----- initContext -----";
6.88 states:=[];
6.89 CalcTree
6.90 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
6.91 @@ -424,12 +423,14 @@
6.92 ["Test","solve_linear"]))];
6.93 Iterator 1; moveActiveRoot 1;
6.94 autoCalculate 1 CompleteCalcHead;
6.95 +(*========== inhibit exn 110718 ================================================
6.96
6.97 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.98 if is_curr_endof_calc pt ([1],Frm) then ()
6.99 else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
6.100
6.101 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.102 +========== inhibit exn 110718 ================================================*)
6.103 if not (is_curr_endof_calc pt ([1],Frm)) then ()
6.104 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
6.105 if is_curr_endof_calc pt ([1],Res) then ()
6.106 @@ -447,16 +448,19 @@
6.107 Iterator 1; moveActiveRoot 1;
6.108 autoCalculate 1 CompleteCalc;
6.109 interSteps 1 ([1],Res);
6.110 +(*========== inhibit exn 110718 ================================================
6.111 +
6.112 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.113 -
6.114 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
6.115
6.116 interSteps 1 ([2],Res);
6.117 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.118 +========== inhibit exn 110718 ================================================*)
6.119
6.120 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
6.121 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
6.122
6.123 +(*========== inhibit exn 110718 ================================================
6.124
6.125 "----------- fun string_of_thmI for_[.]_) ---------------";
6.126 "----------- fun string_of_thmI for_[.]_) ---------------";
6.127 @@ -472,6 +476,7 @@
6.128 val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
6.129 applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
6.130 "- compose stac as done in | appy (*leaf*) by handle_leaf";
6.131 +
6.132 val (th, sr, E, a, v, t) =
6.133 ("Biegelinie",
6.134 (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
6.135 @@ -497,7 +502,7 @@
6.136 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
6.137 else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
6.138 " = " ^ string_of_thmI thm);
6.139 -
6.140 +========== inhibit exn 110718 ================================================*)
6.141
6.142 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
6.143 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
6.144 @@ -514,6 +519,8 @@
6.145 autoCalculate 1 CompleteCalcHead;
6.146 autoCalculate 1 (Step 1) (*Apply_Method*);
6.147 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
6.148 +(*========== inhibit exn 110718 ================================================
6.149 +
6.150 "--- this was corrupted before 'fun string_of_thmI'";
6.151 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
6.152 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
6.153 @@ -521,7 +528,6 @@
6.154 else error "rewtools.sml: string_of_thmI ?!?";
6.155
6.156 getTactic 1 ([1],Frm);
6.157 -
6.158 "----------- fun filter_appl_rews -----------------------";
6.159 "----------- fun filter_appl_rews -----------------------";
6.160 "----------- fun filter_appl_rews -----------------------";
6.161 @@ -537,6 +543,7 @@
6.162 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
6.163 Calculate "plus"] then ()
6.164 else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
6.165 +============ inhibit exn 110718 ==============================================*)
6.166
6.167
6.168 "----------- fun is_contained_in ------------------------";
6.169 @@ -553,4 +560,3 @@
6.170 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
6.171 if not (contains_rule r1 Test_simplify) then ()
6.172 else error "rewtools.sml contains_rule Calc";
6.173 -===== inhibit exn ?===========================================================*)
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 18 09:51:51 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 19 09:43:01 2011 +0200
7.3 @@ -5,12 +5,17 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 +ML{* writeln "**** run the test ***************************************" *}
7.8 +
7.9 +use"../../../test/Tools/isac/Frontend/interface.sml"
7.10 +
7.11 +
7.12 ML {*
7.13 +
7.14 *}
7.15
7.16 -ML{* writeln "**** run the test ***************************************" *}
7.17
7.18 -use"../../../test/Tools/isac/Interpret/script.sml"
7.19 +
7.20
7.21 end
7.22
7.23 @@ -19,12 +24,8 @@
7.24 ===== inhibit exn ?===========================================================*)
7.25
7.26
7.27 -(*========== inhibit exn 110415 ================================================
7.28 -
7.29 -"########### testcode inserted vvv ###########################################";
7.30 -"########### testcode inserted ^^^ ###########################################";
7.31 -
7.32 -============ inhibit exn 110415 ==============================================*)
7.33 +(*========== inhibit exn 110718 ================================================
7.34 +============ inhibit exn 110718 ==============================================*)
7.35
7.36
7.37 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.