132 Compiler.Control.Print.printDepth:=7; (*4 is default*) |
132 Compiler.Control.Print.printDepth:=7; (*4 is default*) |
133 Compiler.Control.Print.printDepth:=4; (*4 is default*) |
133 Compiler.Control.Print.printDepth:=4; (*4 is default*) |
134 *) |
134 *) |
135 |
135 |
136 (* --vvv-- ausgeliehen von test-root-equ/sml *) |
136 (* --vvv-- ausgeliehen von test-root-equ/sml *) |
137 val loc = e_istate; |
137 val loc = Istate.empty; |
138 val (dI',pI',mI') = |
138 val (dI',pI',mI') = |
139 ("Program",["sqroot-test","univariate","equation"], |
139 ("Program",["sqroot-test","univariate","equation"], |
140 ["Program","squ-equ-test2"]); |
140 ["Program","squ-equ-test2"]); |
141 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
141 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
142 "solveFor x","errorBound (eps=0)", |
142 "solveFor x","errorBound (eps=0)", |
160 (*val pos = ([1,2])*) |
160 (*val pos = ([1,2])*) |
161 val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-extremum ..." |
161 val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-extremum ..." |
162 Empty_Tac ("[1,2]:{(a,b). f_x(a,b) ...",[]) Complete; |
162 Empty_Tac ("[1,2]:{(a,b). f_x(a,b) ...",[]) Complete; |
163 val pos = lev_up pos; |
163 val pos = lev_up pos; |
164 (*val pos = ([1])*) |
164 (*val pos = ([1])*) |
165 val (pt,_) = append_result pt pos e_istate ("[1#]:{(a,b). f_x(a,b) ...",[]) |
165 val (pt,_) = append_result pt pos Istate.empty ("[1#]:{(a,b). f_x(a,b) ...",[]) |
166 Complete; |
166 Complete; |
167 |
167 |
168 val pos = lev_on pos; |
168 val pos = lev_on pos; |
169 (*val pos = ([2]) *) |
169 (*val pos = ([2]) *) |
170 val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x(a,b) ..." |
170 val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x(a,b) ..." |
182 val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx } cup.." |
182 val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx } cup.." |
183 Empty_Tac ("[3,2]:{(a,b). f_x ..} cup ...",[]) Complete; |
183 Empty_Tac ("[3,2]:{(a,b). f_x ..} cup ...",[]) Complete; |
184 |
184 |
185 val pos = lev_up pos; |
185 val pos = lev_up pos; |
186 (*pos = ([3]) *) |
186 (*pos = ([3]) *) |
187 val (pt,_) = append_result pt pos e_istate ("[3#]:{(a,b). f_x ..} cup..",[]) |
187 val (pt,_) = append_result pt pos Istate.empty ("[3#]:{(a,b). f_x ..} cup..",[]) |
188 Complete; |
188 Complete; |
189 val pos = lev_on pos; |
189 val pos = lev_on pos; |
190 (*val pos = [4] : pos *) |
190 (*val pos = [4] : pos *) |
191 val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x ..} cup ..." |
191 val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x ..} cup ..." |
192 Empty_Tac IntersectB; |
192 Empty_Tac IntersectB; |
217 val (pt,_) = cappend_atomic pt pos loc "3x^2 + 0 + d/dx ..." |
217 val (pt,_) = cappend_atomic pt pos loc "3x^2 + 0 + d/dx ..." |
218 Empty_Tac ("[4,1,1,1,3]:3x^2 + 0 -3 ...",[]) Complete; |
218 Empty_Tac ("[4,1,1,1,3]:3x^2 + 0 -3 ...",[]) Complete; |
219 "--- 1 ---"; |
219 "--- 1 ---"; |
220 val pos = lev_up pos; |
220 val pos = lev_up pos; |
221 (*pos = ([4,1,1,1]) *) |
221 (*pos = ([4,1,1,1]) *) |
222 val (pt,_) = append_result pt pos e_istate ("[4,1,1,1#]:3x^2 -3.",[])Complete; |
222 val (pt,_) = append_result pt pos Istate.empty ("[4,1,1,1#]:3x^2 -3.",[])Complete; |
223 "--- 2 ---"; |
223 "--- 2 ---"; |
224 val pos = lev_up pos; |
224 val pos = lev_up pos; |
225 (*val pos = ([4,1,1]) *) |
225 (*val pos = ([4,1,1]) *) |
226 val (pt,_) = append_result pt pos e_istate ("[4,1,1#]:found 3x^2 -3 ...",[]) |
226 val (pt,_) = append_result pt pos Istate.empty ("[4,1,1#]:found 3x^2 -3 ...",[]) |
227 Complete; |
227 Complete; |
228 "--- 3 ---"; |
228 "--- 3 ---"; |
229 val pos = lev_on pos; |
229 val pos = lev_on pos; |
230 (*val pos = ([4,1,2]+) *) |
230 (*val pos = ([4,1,2]+) *) |
231 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x^3 ..." |
231 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x^3 ..." |