1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,1324 @@
1.4 +(* tests for sml/ME/ctree.sml
1.5 + authors: Walther Neuper 060113
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"../smltest/ME/ctree.sml";
1.9 +use"ctree.sml";
1.10 +*)
1.11 +
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
1.17 +"-------------- get_allpos' (from ptree above)--------------------";
1.18 +(**#####################################################################(**)
1.19 +"-------------- cut_level (from ptree above)----------------------";
1.20 +"-------------- cut_tree (from ptree above)-----------------------";
1.21 +"=====new ptree 1a miniscript with mini-subpbl ===================";
1.22 +"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
1.23 +(**)#####################################################################**)
1.24 +"=====new ptree 2 miniscript with mini-subpbl ====================";
1.25 +"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
1.26 +"-------------- cappend (from ptree above)------------------------";
1.27 +"-------------- cappend minisubpbl -------------------------------";
1.28 +
1.29 +"=====new ptree 3 ================================================";
1.30 +"-------------- move_dn ------------------------------------------";
1.31 +"-------------- move_dn: Frm -> Res ------------------------------";
1.32 +"-------------- move_up ------------------------------------------";
1.33 +"------ move into detail -----------------------------------------";
1.34 +"=====new ptree 3a ===============================================";
1.35 +"-------------- move_dn in Incomplete ctree ----------------------";
1.36 +
1.37 +"=====new ptree 4: crooked by cut_level_'_ =======================";
1.38 +(*############## development stopped 0501 ########################*)
1.39 +(******************************************************************)
1.40 +(* val SAVE_get_trace = get_trace; *)
1.41 +(******************************************************************)
1.42 +"-------------- get_interval from ctree: incremental development--";
1.43 +(******************************************************************)
1.44 +(* val get_trace = SAVE_get_trace; *)
1.45 +(******************************************************************)
1.46 +(*############## development stopped 0501 ########################*)
1.47 +
1.48 +"=====new ptree 4 ratequation ====================================";
1.49 +"-------------- pt_extract form, tac, asm<>[] --------------------";
1.50 +"=====new ptree 5 minisubpbl =====================================";
1.51 +"-------------- pt_extract form, tac, asm ------------------------";
1.52 +
1.53 +(**#####################################################################(**)
1.54 +"=====new ptree 6 minisubpbl intersteps ==========================";
1.55 +"-------------- get_allpos' new ----------------------------------";
1.56 +"-------------- cut_tree new (from ptree above)-------------------";
1.57 +(**)#####################################################################**)
1.58 +
1.59 +"-----------------------------------------------------------------";
1.60 +"-----------------------------------------------------------------";
1.61 +"-----------------------------------------------------------------";
1.62 +
1.63 +
1.64 +"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
1.65 +"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
1.66 +"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
1.67 +"this build should be detailed each time a test fails later \
1.68 +\i.e. all the tests should be caught here first \
1.69 +\and linked with a reference to the respective test environment";
1.70 +val fmz = ["equality (x+1=2)",
1.71 + "solveFor x","solutions L"];
1.72 +val (dI',pI',mI') =
1.73 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.74 + ["Test","squ-equ-test-subpbl1"]);
1.75 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.77 +(* nxt = Add_Given "equality (x + 1 = 2)"
1.78 + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.79 + *)
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.81 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.82 + *)
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.84 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.85 + *)
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.88 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.89 +"ctree.sml-------------- get_allpos' new ------------------------\"";
1.90 +val (PP, pp) = split_last [1];
1.91 +val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
1.92 +
1.93 +val cuts = get_allp [] ([], ([],Frm)) pt;
1.94 +val cuts2 = get_allps [] [1] (children pt);
1.95 +"ctree.sml-------------- cut_tree new (from ptree above)----------";
1.96 +val (pt', cuts) = cut_tree pt ([1],Frm);
1.97 +"ctree.sml-------------- cappend on complete ctree from above ----";
1.98 +val (pt', cuts) = cappend_form pt [1] e_istate (str2term "Inform[1]");
1.99 +"----------------------------------------------------------------/";
1.100 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
1.101 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
1.102 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
1.103 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
1.104 +
1.105 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.106 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.107 +(*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
1.108 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.109 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.110 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.111 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.112 +(*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
1.113 +
1.114 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
1.115 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
1.117 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
1.118 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
1.120 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.121 +if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
1.122 +else raise error "new behaviour in test: miniscript with mini-subpbl";
1.123 +
1.124 + show_pt pt;
1.125 +
1.126 +
1.127 +"-------------- get_allpos' (from ptree above)--------------------";
1.128 +"-------------- get_allpos' (from ptree above)--------------------";
1.129 +"-------------- get_allpos' (from ptree above)--------------------";
1.130 +if get_allpos' ([], 1) pt =
1.131 + [([], Frm),
1.132 + ([1], Frm),
1.133 + ([1], Res),
1.134 + ([2], Res),
1.135 + ([3], Frm),
1.136 + ([3, 1], Frm),
1.137 + ([3, 1], Res),
1.138 + ([3, 2], Res),
1.139 + ([3], Res),
1.140 + ([4], Res),
1.141 + ([], Res)]
1.142 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 1";
1.143 +
1.144 +if get_allpos's ([], 1) (children pt) =
1.145 + [([1], Frm),
1.146 + ([1], Res),
1.147 + ([2], Res),
1.148 + ([3], Frm),
1.149 + ([3, 1], Frm),
1.150 + ([3, 1], Res),
1.151 + ([3, 2], Res),
1.152 + ([3], Res),
1.153 + ([4], Res)]
1.154 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 2";
1.155 +
1.156 +if get_allpos's ([], 2) (takerest (1, children pt)) =
1.157 + [([2], Res),
1.158 + ([3], Frm),
1.159 + ([3, 1], Frm),
1.160 + ([3, 1], Res),
1.161 + ([3, 2], Res),
1.162 + ([3], Res),
1.163 + ([4], Res)]
1.164 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 3";
1.165 +
1.166 +if get_allpos's ([], 3) (takerest (2, children pt)) =
1.167 + [([3], Frm),
1.168 + ([3, 1], Frm),
1.169 + ([3, 1], Res),
1.170 + ([3, 2], Res),
1.171 + ([3], Res),
1.172 + ([4], Res)]
1.173 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 4";
1.174 +
1.175 +if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
1.176 + [([3, 1], Frm),
1.177 + ([3, 1], Res),
1.178 + ([3, 2], Res)]
1.179 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 5";
1.180 +
1.181 +if get_allpos' ([3], 1) (nth 3 (children pt)) =
1.182 + [([3], Frm),
1.183 + ([3, 1], Frm),
1.184 + ([3, 1], Res),
1.185 + ([3, 2], Res),
1.186 + ([3], Res)]
1.187 +then () else raise error "ctree.sml: diff:behav. in get_allpos' 6";
1.188 +
1.189 +
1.190 +(**##############################################################(**)
1.191 +
1.192 +"-------------- cut_level (from ptree above)----------------------";
1.193 +"-------------- cut_level (from ptree above)----------------------";
1.194 +"-------------- cut_level (from ptree above)----------------------";
1.195 +show_pt pt;
1.196 +show_pt pt';
1.197 +print_depth 99; cuts; print_depth 3;
1.198 +
1.199 +(*if cuts = [([2], Res),
1.200 + ([3], Frm),
1.201 + ([3, 1], Frm),
1.202 + ([3, 1], Res),
1.203 + ([3, 2], Res),
1.204 + ([3], Res),
1.205 + ([4], Res)]
1.206 +then () else raise error "ctree.sml: diff:behav. in cut_level 1a";
1.207 +val (res,asm) = get_obj g_result pt' [2];
1.208 +if res = e_term andalso asm = [] then () else
1.209 +raise error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
1.210 +if not (existpt [2] pt') then () else
1.211 +raise error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
1.212 +
1.213 +val (res,asm) = get_obj g_result pt' [];
1.214 +if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
1.215 +raise error "ctree.sml: diff:behav. in cut_level 1ab";
1.216 +if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.217 + [([], Frm),
1.218 + ([1], Frm),
1.219 + ([1], Res),
1.220 + ([2], Res),(*, e_term in cut_tree!!!*)
1.221 + ([], Res)] then () else
1.222 +raise error "ctree.sml: diff:behav. in cut_level 1b";
1.223 +
1.224 +
1.225 +val (pt',cuts) = cut_level [] [] pt ([2],Res);
1.226 +if cuts = [([3], Frm),
1.227 + ([3, 1], Frm),
1.228 + ([3, 1], Res),
1.229 + ([3, 2], Res),
1.230 + ([3], Res),
1.231 + ([4], Res)]
1.232 +then () else raise error "ctree.sml: diff:behav. in cut_level 2a";
1.233 +
1.234 +if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
1.235 +then () else raise error "ctree.sml: diff:behav. in cut_level 2b";
1.236 +
1.237 +val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
1.238 +if cuts = [([3, 1], Res), ([3, 2], Res)]
1.239 +then () else raise error "ctree.sml: diff:behav. in cut_level 3a";
1.240 +if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
1.241 +then () else raise error "ctree.sml: diff:behav. in cut_level 3b";
1.242 +
1.243 +val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
1.244 +if cuts = [([3, 2], Res)]
1.245 +then () else raise error "ctree.sml: diff:behav. in cut_level 4a";
1.246 +if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
1.247 +then () else raise error "ctree.sml: diff:behav. in cut_level 4b";
1.248 +
1.249 +
1.250 +"-------------- cut_tree (from ptree above)-----------------------";
1.251 +"-------------- cut_tree (from ptree above)-----------------------";
1.252 +"-------------- cut_tree (from ptree above)-----------------------";
1.253 +val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
1.254 +if cuts = [([2], Res),
1.255 + ([3], Frm),
1.256 + ([3, 1], Frm),
1.257 + ([3, 1], Res),
1.258 + ([3, 2], Res),
1.259 + ([3], Res),
1.260 + ([4], Res),
1.261 + ([], Res)]
1.262 +then () else raise error "ctree.sml: diff:behav. in cut_tree 1a";
1.263 +
1.264 +val (res,asm) = get_obj g_result pt' [2];
1.265 +if res = e_term (*WN050219 done by cut_level*) then () else
1.266 +raise error "ctree.sml: diff:behav. in cut_tree 1aa";
1.267 +
1.268 +val form = get_obj g_form pt' [2];
1.269 +if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
1.270 +raise error "ctree.sml: diff:behav. in cut_tree 1ab";
1.271 +
1.272 +val (res,asm) = get_obj g_result pt' [];
1.273 +if res = e_term (*WN050219 done by cut_tree*) then () else
1.274 +raise error "ctree.sml: diff:behav. in cut_tree 1ac";
1.275 +
1.276 +if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.277 + [([], Frm),
1.278 + ([1], Frm),
1.279 + ([1], Res)] then () else
1.280 +raise error "ctree.sml: diff:behav. in cut_tree 1ad";
1.281 +
1.282 +val (pt', cuts) = cut_tree pt ([2],Res);
1.283 +if cuts = [([3], Frm),
1.284 + ([3, 1], Frm),
1.285 + ([3, 1], Res),
1.286 + ([3, 2], Res),
1.287 + ([3], Res),
1.288 + ([4], Res),
1.289 + ([], Res)]
1.290 +then () else raise error "ctree.sml: diff:behav. in cut_tree 2";
1.291 +
1.292 +val (pt', cuts) = cut_tree pt ([3,1],Frm);
1.293 +if cuts = [([3, 1], Res),
1.294 + ([3, 2], Res),
1.295 + ([3], Res),
1.296 + ([4], Res),
1.297 + ([], Res)]
1.298 +then () else raise error "ctree.sml: diff:behav. in cut_tree 3";
1.299 +
1.300 +val (pt', cuts) = cut_tree pt ([3,1],Res);
1.301 +if cuts = [([3, 2], Res),
1.302 + ([3], Res),
1.303 + ([4], Res),
1.304 + ([], Res)]
1.305 +then () else raise error "ctree.sml: diff:behav. in cut_tree 4";
1.306 +
1.307 +
1.308 +"=====new ptree 1a miniscript with mini-subpbl ===================";
1.309 +"=====new ptree 1a miniscript with mini-subpbl ===================";
1.310 +"=====new ptree 1a miniscript with mini-subpbl ===================";
1.311 +val fmz = ["equality (x+1=2)",
1.312 + "solveFor x","solutions L"];
1.313 +val (dI',pI',mI') =
1.314 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.315 + ["Test","squ-equ-test-subpbl1"]);
1.316 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.317 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.318 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.319 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.320 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.321 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.322 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.323 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.324 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.325 +show_pt pt;
1.326 +
1.327 +"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
1.328 +"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
1.329 +"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
1.330 +
1.331 +val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
1.332 +if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
1.333 +then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
1.334 +
1.335 +val (pt', cuts) = cut_tree pt ([1],Frm);
1.336 +if cuts = []
1.337 +then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
1.338 +
1.339 +(*WN050219
1.340 +val pos as ([p],_) = ([1],Frm);
1.341 +val pt as Nd (b,_) = pt;
1.342 +
1.343 +
1.344 +show_pt pt;
1.345 +show_pt pt';
1.346 +print_depth 99;cuts;print_depth 3;
1.347 +print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
1.348 +####################################################################*)*)
1.349 +
1.350 +"=====new ptree 2 miniscript with mini-subpbl ====================";
1.351 +"=====new ptree 2 miniscript with mini-subpbl ====================";
1.352 +"=====new ptree 2 miniscript with mini-subpbl ====================";
1.353 + states:=[];
1.354 + CalcTree
1.355 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.356 + ("Test.thy",
1.357 + ["sqroot-test","univariate","equation","test"],
1.358 + ["Test","squ-equ-test-subpbl1"]))];
1.359 + Iterator 1; moveActiveRoot 1;
1.360 + autoCalculate 1 CompleteCalc;
1.361 +
1.362 + interSteps 1 ([3,2],Res);
1.363 +
1.364 + val ((pt,_),_) = get_calc 1;
1.365 + show_pt pt;
1.366 +
1.367 +"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
1.368 +"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
1.369 +"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
1.370 +(*WN050225 intermed. outcommented
1.371 + val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
1.372 + if cuts = [([3, 2, 1], Res),
1.373 + ([3, 2, 2], Res),
1.374 + ([3, 2], Res),
1.375 + ([3], Res),
1.376 + ([4], Res)]
1.377 + then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
1.378 +
1.379 + val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1.380 + if cuts = [([3, 2, 2], Res),
1.381 + ([3, 2], Res),
1.382 + ([3], Res),
1.383 + ([4], Res)]
1.384 + then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
1.385 +
1.386 +
1.387 +"-------------- cappend (from ptree above)------------------------";
1.388 +"-------------- cappend (from ptree above)------------------------";
1.389 +"-------------- cappend (from ptree above)------------------------";
1.390 +val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
1.391 +if cuts = [([3, 2, 1], Res),
1.392 + ([3, 2, 2], Res),
1.393 + ([3, 2], Res),
1.394 + ([3], Res),
1.395 + ([4], Res),
1.396 + ([], Res)]
1.397 +then () else raise error "ctree.sml: diff:behav. in cappend_form";
1.398 +if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
1.399 + get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
1.400 + term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
1.401 + then () else raise error "ctree.sml: diff:behav. in cappend 1";
1.402 +
1.403 +val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
1.404 + (Tac "test") (str2term "newresult",[]) Complete;
1.405 +if cuts = [([3, 2, 1], Res), (*?????????????*)
1.406 + ([3, 2, 2], Res),
1.407 + ([3, 2], Res),
1.408 + ([3], Res),
1.409 + ([4], Res),
1.410 + ([], Res)]
1.411 +then () else raise error "ctree.sml: diff:behav. in cappend_atomic";
1.412 +
1.413 +
1.414 +
1.415 +"-------------- cappend minisubpbl -------------------------------";
1.416 +"-------------- cappend minisubpbl -------------------------------";
1.417 +"-------------- cappend minisubpbl -------------------------------";
1.418 +"=====new ptree 1 miniscript with mini-subpbl ====================";
1.419 +val fmz = ["equality (x+1=2)",
1.420 + "solveFor x","solutions L"];
1.421 +val (dI',pI',mI') =
1.422 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.423 + ["Test","squ-equ-test-subpbl1"]);
1.424 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.425 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.426 +(* nxt = Add_Given "equality (x + 1 = 2)"
1.427 + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.428 + *)
1.429 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.430 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.431 + *)
1.432 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.433 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
1.434 + *)
1.435 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.436 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.437 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.438 +(*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
1.439 +val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
1.440 +
1.441 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
1.442 +val p = ([1], Frm);
1.443 +val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
1.444 +val form = get_obj g_form pt (fst p);
1.445 +val (res,_) = get_obj g_result pt (fst p);
1.446 +if term2str form = "x + 1 = 2" andalso res = e_term then () else
1.447 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
1.448 +if not (existpt ((lev_on o fst) p) pt) then () else
1.449 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
1.450 +
1.451 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
1.452 +val p = ([1], Res);
1.453 +val (pt,cuts) =
1.454 + cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
1.455 + Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
1.456 +val form = get_obj g_form pt (fst p);
1.457 +val (res,_) = get_obj g_result pt (fst p);
1.458 +if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
1.459 +then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
1.460 +if not (existpt ((lev_on o fst) p) pt) then () else
1.461 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
1.462 +
1.463 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
1.464 +val p = ([2], Res);
1.465 +val (pt,cuts) =
1.466 + cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
1.467 + Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
1.468 +val form = get_obj g_form pt (fst p);
1.469 +val (res,_) = get_obj g_result pt (fst p);
1.470 +if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
1.471 +then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
1.472 +if not (existpt ((lev_on o fst) p) pt) then () else
1.473 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
1.474 +
1.475 +
1.476 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
1.477 +val p = ([3], Pbl);
1.478 +val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
1.479 +if is_pblobj (get_obj I pt (fst p)) then () else
1.480 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
1.481 +if not (existpt ((lev_on o fst) p) pt) then () else
1.482 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
1.483 +
1.484 +(* ...complete calchead skipped...*)
1.485 +
1.486 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
1.487 +val p = ([3, 1], Frm);
1.488 +val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
1.489 +val form = get_obj g_form pt (fst p);
1.490 +val (res,_) = get_obj g_result pt (fst p);
1.491 +if term2str form = "-1 + x = 0" andalso res = e_term then () else
1.492 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
1.493 +if not (existpt ((lev_on o fst) p) pt) then () else
1.494 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
1.495 +
1.496 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
1.497 +val p = ([3, 1], Res);
1.498 +val (pt,cuts) =
1.499 + cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
1.500 + Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
1.501 +val form = get_obj g_form pt (fst p);
1.502 +val (res,_) = get_obj g_result pt (fst p);
1.503 +if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
1.504 +else raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
1.505 +if not (existpt ((lev_on o fst) p) pt) then () else
1.506 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
1.507 +
1.508 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
1.509 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
1.510 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
1.511 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
1.512 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
1.513 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
1.514 +
1.515 +WN050225 intermed. outcommented---*)
1.516 +
1.517 +"=====new ptree 3 ================================================";
1.518 +"=====new ptree 3 ================================================";
1.519 +"=====new ptree 3 ================================================";
1.520 + states:=[];
1.521 + CalcTree
1.522 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.523 + ("Test.thy",
1.524 + ["sqroot-test","univariate","equation","test"],
1.525 + ["Test","squ-equ-test-subpbl1"]))];
1.526 + Iterator 1; moveActiveRoot 1;
1.527 + autoCalculate 1 CompleteCalc;
1.528 +
1.529 + val ((pt,_),_) = get_calc 1;
1.530 + show_pt pt;
1.531 +
1.532 +"-------------- move_dn ------------------------------------------";
1.533 +"-------------- move_dn ------------------------------------------";
1.534 +"-------------- move_dn ------------------------------------------";
1.535 + val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
1.536 + val p = move_dn [] pt p (*-> ([1],Res)*);
1.537 + val p = move_dn [] pt p (*-> ([2],Res)*);
1.538 + val p = move_dn [] pt p (*-> ([3],Pbl)*);
1.539 + val p = move_dn [] pt p (*-> ([3,1],Frm)*);
1.540 + val p = move_dn [] pt p (*-> ([3,1],Res)*);
1.541 + val p = move_dn [] pt p (*-> ([3,2],Res)*);
1.542 + val p = move_dn [] pt p (*-> ([3],Res)*);
1.543 +(* term2str (get_obj g_res pt [3]);
1.544 + term2str (get_obj g_form pt [4]);
1.545 + *)
1.546 + val p = move_dn [] pt p (*-> ([4],Res)*);
1.547 + val p = move_dn [] pt p (*-> ([],Res)*);
1.548 +(*
1.549 + val p = (move_dn [] pt p) handle e => print_exn_G e;
1.550 + Exception PTREE end of calculation*)
1.551 +if p=([],Res) then () else raise error "ctree.sml: diff:behav. in move_dn";
1.552 +
1.553 +
1.554 +"-------------- move_dn: Frm -> Res ------------------------------";
1.555 +"-------------- move_dn: Frm -> Res ------------------------------";
1.556 +"-------------- move_dn: Frm -> Res ------------------------------";
1.557 + states := [];
1.558 + CalcTree (*start of calculation, return No.1*)
1.559 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.560 + ("Test.thy",
1.561 + ["linear","univariate","equation","test"],
1.562 + ["Test","solve_linear"]))];
1.563 + Iterator 1; moveActiveRoot 1;
1.564 + autoCalculate 1 CompleteCalcHead;
1.565 + autoCalculate 1 (Step 1);
1.566 + refFormula 1 (get_pos 1 1);
1.567 +
1.568 + moveActiveRoot 1;
1.569 + moveActiveDown 1;
1.570 + if get_pos 1 1 = ([1], Frm) then ()
1.571 + else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.572 + moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.573 +
1.574 + autoCalculate 1 (Step 1);
1.575 + refFormula 1 (get_pos 1 1);
1.576 +
1.577 + moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.578 + if get_pos 1 1 = ([1], Res) then ()
1.579 + else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.580 + moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.581 +
1.582 +
1.583 +"-------------- move_up ------------------------------------------";
1.584 +"-------------- move_up ------------------------------------------";
1.585 +"-------------- move_up ------------------------------------------";
1.586 + val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
1.587 + val p = move_up [] pt p; (*-> ([3],Res)*)
1.588 + val p = move_up [] pt p; (*-> ([3,2],Res)*)
1.589 + val p = move_up [] pt p; (*-> ([3,1],Res)*)
1.590 + val p = move_up [] pt p; (*-> ([3,1],Frm)*)
1.591 + val p = move_up [] pt p; (*-> ([3],Pbl)*)
1.592 + val p = move_up [] pt p; (*-> ([2],Res)*)
1.593 + val p = move_up [] pt p; (*-> ([1],Res)*)
1.594 + val p = move_up [] pt p; (*-> ([1],Frm)*)
1.595 + val p = move_up [] pt p; (*-> ([],Pbl)*)
1.596 +(*val p = (move_up [] pt p) handle e => print_exn_G e;
1.597 + Exception PTREE begin of calculation*)
1.598 +if p=([],Pbl) then () else raise error "ctree.sml: diff.behav. in move_up";
1.599 +
1.600 +
1.601 +"------ move into detail -----------------------------------------";
1.602 +"------ move into detail -----------------------------------------";
1.603 +"------ move into detail -----------------------------------------";
1.604 + states:=[];
1.605 + CalcTree
1.606 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.607 + ("Test.thy",
1.608 + ["sqroot-test","univariate","equation","test"],
1.609 + ["Test","squ-equ-test-subpbl1"]))];
1.610 + Iterator 1; moveActiveRoot 1;
1.611 + autoCalculate 1 CompleteCalc;
1.612 + moveActiveRoot 1;
1.613 + moveActiveDown 1;
1.614 + moveActiveDown 1;
1.615 + moveActiveDown 1;
1.616 + refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
1.617 +
1.618 + interSteps 1 ([2],Res);
1.619 +
1.620 + val ((pt,_),_) = get_calc 1; show_pt pt;
1.621 + val p = get_pos 1 1;
1.622 +
1.623 + val p = move_up [] pt p; (*([2, 6], Res)*);
1.624 + val p = movelevel_up [] pt p;(*([2], Frm)*);
1.625 + val p = move_dn [] pt p; (*([2, 1], Frm)*);
1.626 + val p = move_dn [] pt p; (*([2, 1], Res)*);
1.627 + val p = move_dn [] pt p; (*([2, 2], Res)*);
1.628 + val p = move_dn [] pt p; (*([2, 3], Res)*);
1.629 + val p = move_dn [] pt p; (*([2, 4], Res)*);
1.630 + val p = move_dn [] pt p; (*([2, 5], Res)*);
1.631 + val p = move_dn [] pt p; (*([2, 6], Res)*);
1.632 + if p = ([2, 6], Res) then()
1.633 + else raise error "ctree.sml: diff.behav. in move into detail";
1.634 +
1.635 +"=====new ptree 3a ===============================================";
1.636 +"=====new ptree 3a ===============================================";
1.637 +"=====new ptree 3a ===============================================";
1.638 + states:=[];
1.639 + CalcTree
1.640 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.641 + ("Test.thy",
1.642 + ["sqroot-test","univariate","equation","test"],
1.643 + ["Test","squ-equ-test-subpbl1"]))];
1.644 + Iterator 1; moveActiveRoot 1;
1.645 + autoCalculate 1 CompleteCalcHead;
1.646 + autoCalculate 1 (Step 1);
1.647 + autoCalculate 1 (Step 1);
1.648 + autoCalculate 1 (Step 1);
1.649 + val ((pt,_),_) = get_calc 1;
1.650 + val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
1.651 + val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
1.652 + val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
1.653 + (*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
1.654 +
1.655 + moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
1.656 + moveDown 1 ([1],Frm) (*-> ([1],Res)*);
1.657 + moveDown 1 ([1],Res) (*-> ([2],Res)*);
1.658 + moveDown 1 ([2],Res) (*-> pos does not exist*);
1.659 +(*
1.660 + get_obj g_ostate pt [1];
1.661 + show_pt pt;
1.662 +*)
1.663 +
1.664 +"-------------- move_dn in Incomplete ctree ----------------------";
1.665 +"-------------- move_dn in Incomplete ctree ----------------------";
1.666 +"-------------- move_dn in Incomplete ctree ----------------------";
1.667 +
1.668 +
1.669 +
1.670 +"=====new ptree 4: crooked by cut_level_'_ =======================";
1.671 +"=====new ptree 4: crooked by cut_level_'_ =======================";
1.672 +"=====new ptree 4: crooked by cut_level_'_ =======================";
1.673 +states:=[];
1.674 +CalcTree
1.675 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.676 + "solveFor x","solutions L"],
1.677 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
1.678 +Iterator 1; moveActiveRoot 1;
1.679 +autoCalculate 1 CompleteCalc;
1.680 +
1.681 +getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
1.682 +getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
1.683 +getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
1.684 +getTactic 1 ([4,1],Res);(*Rewrite all_left*)
1.685 +getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
1.686 +getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
1.687 +
1.688 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
1.689 +moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
1.690 +moveActiveFormula 1 ([3],Res)(*3.1.*);
1.691 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
1.692 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
1.693 +
1.694 +moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
1.695 +interSteps 1 ([1],Res)(*..is activeFormula !?!*);
1.696 +
1.697 +getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
1.698 +getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
1.699 +getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
1.700 +getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
1.701 +
1.702 +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
1.703 +interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
1.704 +val ((pt,_),_) = get_calc 1;
1.705 +writeln(pr_ptree pr_short pt);
1.706 +(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
1.707 + ###########################################################################*)
1.708 +val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
1.709 +writeln(pr_ptree pr_short pt);
1.710 +
1.711 +
1.712 +"-------------- get_interval from ctree: incremental development--";
1.713 +"-------------- get_interval from ctree: incremental development--";
1.714 +"-------------- get_interval from ctree: incremental development--";
1.715 +"--- level 1: get pos from start b to end p ----------------------";
1.716 +"--- level 1: get pos from start b to end p ----------------------";
1.717 +"--- level 1: get pos from start b to end p ----------------------";
1.718 +(******************************************************************)
1.719 +(**) val SAVE_get_trace = get_trace; (**)
1.720 +(******************************************************************)
1.721 +(*'getnds' below is structured as such:*)
1.722 +fun www _ [x] = "l+r-margin"
1.723 + | www true [x1,x2] = "l-margin, r-margin"
1.724 + | www _ [x1,x2] = "intern, r-margin"
1.725 + | www true (x::(xs as _::_)) = "l-margin " ^ www false xs
1.726 + | www _ (x::(xs as _::_)) = "intern " ^ www false xs;
1.727 +www true [1,2,3,4,5];
1.728 +(*val it = "from intern intern intern to" : string*)
1.729 +www true [1,2];
1.730 +(*val it = "from to" : string*)
1.731 +www true [1];
1.732 +(*val it = "from+to" : string*)
1.733 +
1.734 +local
1.735 +(*specific values of hd of pos p,q for simple handling take_fromto,
1.736 + from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
1.737 + ... can be used even for positions _below_ p or q*)
1.738 +fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1.739 +fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1.740 +(*analoguous for tl*)
1.741 +fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1.742 +fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1.743 +
1.744 +(*see modspec.sml#pt_form
1.745 +fun pt_form (PrfObj {form,...}) = term2str form
1.746 + | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1.747 + let val (dI, pI, _) = get_somespec' spec spec'
1.748 + val {cas,...} = get_pbt pI
1.749 + in case cas of
1.750 + NONE => term2str (pblterm dI pI)
1.751 + | SOME t => term2str (subst_atomic (mk_env probl) t)
1.752 + end;
1.753 +*)
1.754 +(*.get an 'interval' from ptree down to a certain level
1.755 + by 'take_fromto children' of the nodes with specific 'from' and 'to';
1.756 + 'i > 0' suppresses output during recursive descent towards 'from'
1.757 + b: the 'from' incremented to the actual pos
1.758 + p,q: specific 'from','to' for simple use of 'take_fromto'*)
1.759 +fun getnd i (b,p) q (Nd (po, nds)) =
1.760 + (if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
1.761 +
1.762 + @ (writeln("getnd : b="^(ints2str' b)^", p="^
1.763 + (ints2str' p)^", q="^(ints2str' q));
1.764 +
1.765 + getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1.766 + (take_fromto (hdp p) (hdq q) nds))
1.767 +
1.768 +and getnds _ _ _ _ [] = [] (*no children*)
1.769 + | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1.770 + | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1.771 + (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
1.772 + ", q="^ ints2str' q);
1.773 + (getnd i ( b, p ) [99999] n1) @
1.774 + (getnd ~99999 (lev_on b,[0]) q n2))
1.775 + | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1.776 + (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
1.777 + ", q="^ ints2str' q);
1.778 + (getnd i ( b,[0]) [99999] n1) @
1.779 + (getnd ~99999 (lev_on b,[0]) q n2))
1.780 + | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1.781 + (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
1.782 + ", q="^ ints2str' q);
1.783 + (getnd i ( b, p ) [99999] nd) @
1.784 + (getnds ~99999 false (lev_on b,[0]) q nds))
1.785 + | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1.786 + (getnd i ( b,[0]) [99999] nd) @
1.787 + (getnds ~99999 false (lev_on b,[0]) q nds);
1.788 +in
1.789 +(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1.790 + where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1.791 +(1) the 'f' are given
1.792 +(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1.793 +(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1.794 +(2) the 't' ar given
1.795 +(2a) by 'to' if 't' = the respective element of 'to' (right margin)
1.796 +(2b) inifinity, if 't' < the respective element of 'to (internal node)'
1.797 +the 'f' and 't' are set by hdp,... *)
1.798 +fun get_trace pt p q =
1.799 + (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1.800 + (take_fromto (hdp p) (hdq q) (children pt));
1.801 +end;
1.802 +
1.803 +writeln(pr_ptree pr_short pt);
1.804 +case get_trace pt [1,3] [4,1,1] of
1.805 + [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
1.806 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
1.807 +case get_trace pt [2] [4,3,2] of
1.808 + [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
1.809 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
1.810 +case get_trace pt [1,4] [4,3,1] of
1.811 + [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
1.812 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
1.813 +case get_trace pt [4,2] [5] of
1.814 + (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
1.815 + ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
1.816 + [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
1.817 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
1.818 +case get_trace pt [] [4,4,2] of
1.819 + [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.820 + [4,3],[4,3,1],[4,3,2]] => ()
1.821 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
1.822 +case get_trace pt [] [] of
1.823 + [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.824 + [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
1.825 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
1.826 +case get_trace pt [4,3] [4,3] of
1.827 + [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
1.828 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
1.829 +
1.830 +"--- level 2: get pos' from start b to end p ---------------------";
1.831 +"--- level 2: get pos' from start b to end p ---------------------";
1.832 +"--- level 2: get pos' from start b to end p ---------------------";
1.833 +(*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
1.834 + development stopped in favour of move_dn, see get_interval
1.835 + actually used (inefficient) version with move_dn: see modspec.sml
1.836 +*)
1.837 +(*
1.838 +case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
1.839 + [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
1.840 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
1.841 +case get_trace pt ([],Pbl) ([],Res) of
1.842 + [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
1.843 + [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
1.844 + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
1.845 +*)
1.846 +
1.847 +(******************************************************************)
1.848 +(**) val get_trace = SAVE_get_trace; (**)
1.849 +(******************************************************************)
1.850 +
1.851 +
1.852 +"=====new ptree 4 ratequation ====================================";
1.853 +"=====new ptree 4 ratequation ====================================";
1.854 +"=====new ptree 4 ratequation ====================================";
1.855 +states:=[];
1.856 +CalcTree
1.857 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.858 + "solveFor x","solutions L"],
1.859 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
1.860 +Iterator 1; moveActiveRoot 1;
1.861 +autoCalculate 1 CompleteCalc;
1.862 +val ((pt,_),_) = get_calc 1;
1.863 +show_pt pt;
1.864 +
1.865 +
1.866 +"-------------- pt_extract form, tac, asm<>[] --------------------";
1.867 +"-------------- pt_extract form, tac, asm<>[] --------------------";
1.868 +"-------------- pt_extract form, tac, asm<>[] --------------------";
1.869 +val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
1.870 +case (term2str form, tac, terms2strs asm) of
1.871 + ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
1.872 + Subproblem
1.873 + ("PolyEq.thy",
1.874 + ["normalize", "polynomial", "univariate", "equation"]),
1.875 + ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
1.876 + | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.877 +(*WN060717 unintentionally changed some rls/ord while
1.878 + completing knowl. for thes2file...
1.879 +
1.880 + case (term2str form, tac, terms2strs asm) of
1.881 + ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
1.882 + *)Subproblem
1.883 + ("PolyEq.thy",
1.884 + ["normalize", "polynomial", "univariate", "equation"]),
1.885 + ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
1.886 + | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.887 +
1.888 +.... but it became even better*)
1.889 +
1.890 +
1.891 +
1.892 +"=====new ptree 5 minisubpbl =====================================";
1.893 +"=====new ptree 5 minisubpbl =====================================";
1.894 +"=====new ptree 5 minisubpbl =====================================";
1.895 +states:=[];
1.896 +CalcTree
1.897 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.898 + ("Test.thy",
1.899 + ["sqroot-test","univariate","equation","test"],
1.900 + ["Test","squ-equ-test-subpbl1"]))];
1.901 +Iterator 1; moveActiveRoot 1;
1.902 +autoCalculate 1 CompleteCalc;
1.903 +val ((pt,_),_) = get_calc 1;
1.904 +show_pt pt;
1.905 +
1.906 +"-------------- pt_extract form, tac, asm ------------------------";
1.907 +"-------------- pt_extract form, tac, asm ------------------------";
1.908 +"-------------- pt_extract form, tac, asm ------------------------";
1.909 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
1.910 +case (term2str form, tac, terms2strs asm) of
1.911 + ("solve (x + 1 = 2, x)",
1.912 + Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.913 + []) => ()
1.914 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
1.915 +
1.916 +val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
1.917 +case (term2str form, tac, terms2strs asm) of
1.918 + ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
1.919 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
1.920 +
1.921 +val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
1.922 +case (term2str form, tac, terms2strs asm) of
1.923 + ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
1.924 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
1.925 +
1.926 +val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
1.927 +case (term2str form, tac, terms2strs asm) of
1.928 + ("-1 + x = 0",
1.929 + Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
1.930 + []) => ()
1.931 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
1.932 +
1.933 +val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
1.934 +case (term2str form, tac, terms2strs asm) of
1.935 + ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
1.936 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
1.937 +
1.938 +val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
1.939 +case (term2str form, tac, terms2strs asm) of
1.940 + ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
1.941 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
1.942 +
1.943 +val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
1.944 +case (term2str form, tac, terms2strs asm) of
1.945 + ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
1.946 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
1.947 +
1.948 +val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
1.949 +case (term2str form, tac, terms2strs asm) of
1.950 + ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
1.951 + []) => ()
1.952 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
1.953 +
1.954 +val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
1.955 +case (term2str form, tac, terms2strs asm) of
1.956 + ("[x = 1]", Check_elementwise "Assumptions", []) => ()
1.957 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
1.958 +
1.959 +val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
1.960 +case (term2str form, tac, terms2strs asm) of
1.961 + ("[x = 1]",
1.962 + Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
1.963 + []) => ()
1.964 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
1.965 +
1.966 +val (Form form, tac, asm) = pt_extract (pt, ([], Res));
1.967 +case (term2str form, tac, terms2strs asm) of
1.968 + ("[x = 1]", NONE, []) => ()
1.969 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Res)";
1.970 +
1.971 +"=====new ptree 6 minisubpbl intersteps ==========================";
1.972 +"=====new ptree 6 minisubpbl intersteps ==========================";
1.973 +"=====new ptree 6 minisubpbl intersteps ==========================";
1.974 +states:=[];
1.975 +CalcTree
1.976 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.977 + ("Test.thy",
1.978 + ["sqroot-test","univariate","equation","test"],
1.979 + ["Test","squ-equ-test-subpbl1"]))];
1.980 +Iterator 1; moveActiveRoot 1;
1.981 +autoCalculate 1 CompleteCalc;
1.982 +interSteps 1 ([2],Res);
1.983 +interSteps 1 ([3,2],Res);
1.984 +val ((pt,_),_) = get_calc 1;
1.985 +show_pt pt;
1.986 +
1.987 +(**##############################################################**)
1.988 +"-------------- get_allpos' new ----------------------------------";
1.989 +"-------------- get_allpos' new ----------------------------------";
1.990 +"-------------- get_allpos' new ----------------------------------";
1.991 +"--- whole ctree";
1.992 +print_depth 99;
1.993 +val cuts = get_allp [] ([], ([],Frm)) pt;
1.994 +print_depth 3;
1.995 +if cuts =
1.996 + [(*never returns the first pos'*)
1.997 + ([1], Frm),
1.998 + ([1], Res),
1.999 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1000 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1001 + ([2], Res),
1.1002 + ([3], Pbl),
1.1003 + ([3, 1], Frm), ([3, 1], Res),
1.1004 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1005 + ([3, 2], Res),
1.1006 + ([3], Res),
1.1007 + ([4], Res),
1.1008 + ([], Res)] then () else
1.1009 +raise error "ctree.sml diff.behav. get_allp new []";
1.1010 +
1.1011 +print_depth 99;
1.1012 +val cuts2 = get_allps [] [1] (children pt);
1.1013 +print_depth 3;
1.1014 +if cuts = cuts2 @ [([], Res)] then () else
1.1015 +raise error "ctree.sml diff.behav. get_allps new []";
1.1016 +
1.1017 +"---(3) on S(606)..S(608)--------";
1.1018 +"--- nd [2] with 6 children---------------------------------";
1.1019 +val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
1.1020 +if cuts =
1.1021 + [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1022 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1023 + ([2], Res)] then () else
1.1024 +raise error "ctree.sml diff.behav. get_allp new [2]";
1.1025 +
1.1026 +val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
1.1027 +if cuts = cuts2 @ [([2], Res)] then () else
1.1028 +raise error "ctree.sml diff.behav. get_allps new [2]";
1.1029 +
1.1030 +
1.1031 +"---(4) on S(606)..S(608)--------";
1.1032 +"--- nd [3] subproblem--------------------------------------";
1.1033 +val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
1.1034 +if cuts =
1.1035 + [([3, 1], Frm),
1.1036 + ([3, 1], Res),
1.1037 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1038 + ([3, 2], Res),
1.1039 + ([3], Res)] then () else
1.1040 +raise error "ctree.sml diff.behav. get_allp new [3]";
1.1041 +
1.1042 +val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
1.1043 +if cuts = cuts2 @ [([3], Res)] then () else
1.1044 +raise error "ctree.sml diff.behav. get_allps new [3]";
1.1045 +
1.1046 +"--- nd [3,2] with 2 children--------------------------------";
1.1047 +val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
1.1048 +if cuts =
1.1049 + [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1050 + ([3, 2], Res)] then () else
1.1051 +raise error "ctree.sml diff.behav. get_allp new [3,2]";
1.1052 +
1.1053 +val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
1.1054 +if cuts = cuts2 @ [([3, 2], Res)] then () else
1.1055 +raise error "ctree.sml diff.behav. get_allps new [3,2]";
1.1056 +
1.1057 +"---(5a) on S(606)..S(608)--------";
1.1058 +"--- nd [3,2,1] with 0 children------------------------------";
1.1059 +val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
1.1060 +if cuts =
1.1061 + [] then () else
1.1062 +raise error "ctree.sml diff.behav. get_allp new [3,2,1]";
1.1063 +
1.1064 +val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
1.1065 +if cuts = cuts2 @ [] then () else
1.1066 +raise error "ctree.sml diff.behav. get_allps new [3,2,1]";
1.1067 +
1.1068 +
1.1069 +(**#################################################################**)
1.1070 +"-------------- cut_tree new (from ptree above)-------------------";
1.1071 +"-------------- cut_tree new (from ptree above)-------------------";
1.1072 +"-------------- cut_tree new (from ptree above)-------------------";
1.1073 +show_pt pt;
1.1074 +val b = get_obj g_branch pt [];
1.1075 +if b = TransitiveB then () else
1.1076 +raise error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1.1077 +val b = get_obj g_branch pt [3];
1.1078 +if b = TransitiveB then () else
1.1079 +raise error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1.1080 +
1.1081 +"---(2) on S(606)..S(608)--------";
1.1082 +val (pt', cuts) = cut_tree pt ([1],Res);
1.1083 +print_depth 99;
1.1084 +cuts;
1.1085 +print_depth 3;
1.1086 +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1087 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.1088 + ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.1089 + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.1090 +(*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
1.1091 +raise error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1.1092 +
1.1093 +
1.1094 +"---(3) on S(606)..S(608)--------";
1.1095 +val (pt', cuts) = cut_tree pt ([2],Res);
1.1096 +print_depth 99;
1.1097 +cuts;
1.1098 +print_depth 3;
1.1099 +if cuts = [(*preceding step on WS was ([1]),Res*)
1.1100 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1101 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1102 + ([2], Res),
1.1103 + ([3], Pbl),
1.1104 + ([3, 1], Frm),
1.1105 + ([3, 1], Res),
1.1106 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1107 + ([3, 2], Res),
1.1108 + ([3], Res),
1.1109 + ([4], Res),
1.1110 +(*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
1.1111 +else raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1.1112 +
1.1113 +"---(4) on S(606)..S(608)--------";
1.1114 +val (pt', cuts) = cut_tree pt ([3],Pbl);
1.1115 +print_depth 99;
1.1116 +cuts;
1.1117 +print_depth 3;
1.1118 +if cuts = [([3], Pbl),
1.1119 + ([3, 1], Frm), ([3, 1], Res),
1.1120 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1121 + ([3, 2], Res),
1.1122 + ([3], Res),
1.1123 + ([4], Res),
1.1124 +(*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
1.1125 +then () else raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1.1126 +
1.1127 +"---(5a) on S(606)..S(608) cut_tree --------";
1.1128 +val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1.1129 +print_depth 99;
1.1130 +cuts;
1.1131 +print_depth 1;
1.1132 +if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.1133 +(*WN060727 added after replacing cutlevup by test_trans:*)
1.1134 +([3], Res), ([4], Res),([],Res)] then ()
1.1135 +else raise error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1.1136 +show_pt pt';
1.1137 +
1.1138 +
1.1139 +"-------------- cappend on complete ctree from above -------------";
1.1140 +"-------------- cappend on complete ctree from above -------------";
1.1141 +"-------------- cappend on complete ctree from above -------------";
1.1142 +show_pt pt;
1.1143 +
1.1144 +"---(2) on S(606)..S(608)--------";
1.1145 +val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
1.1146 + (Tac "test") (str2term "Inres[1]",[]) Complete;
1.1147 +print_depth 99;
1.1148 +cuts;
1.1149 +print_depth 3;
1.1150 +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1151 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.1152 + ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.1153 + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.1154 +(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.1155 +else raise error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1.1156 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1157 +print_depth 99;
1.1158 +afterins;
1.1159 +print_depth 3;
1.1160 +if afterins = [([1], Frm), ([1], Res)
1.1161 +(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1.1162 +else raise error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1.1163 +show_pt pt';
1.1164 +
1.1165 +"---(3) on S(606)..S(608)--------";
1.1166 +show_pt pt;
1.1167 +val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
1.1168 + (Tac "test") (str2term "Inres[2]",[]) Complete;
1.1169 +print_depth 99;
1.1170 +cuts;
1.1171 +print_depth 3;
1.1172 +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1173 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.1174 + ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.1175 + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.1176 +(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.1177 +else raise error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1.1178 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1179 +print_depth 99;
1.1180 +afterins;
1.1181 +print_depth 3;
1.1182 +if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1.1183 +(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1.1184 +then () else
1.1185 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1.1186 +show_pt pt';
1.1187 +(*
1.1188 + val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1.1189 + val p = move_dn [] pt' p (*-> ([1],Res)*);
1.1190 + val p = move_dn [] pt' p (*-> ([2],Frm)*);
1.1191 + val p = move_dn [] pt' p (*-> ([2],Res)*);
1.1192 +
1.1193 + term2str (get_obj g_form pt' [2]);
1.1194 + term2str (get_obj g_res pt' [2]);
1.1195 + ostate2str (get_obj g_ostate pt' [2]);
1.1196 + *)
1.1197 +
1.1198 +"---(4) on S(606)..S(608)--------";
1.1199 +val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
1.1200 + ([],e_spec, str2term "Inhead[3]");
1.1201 +print_depth 99;
1.1202 +cuts;
1.1203 +print_depth 3;
1.1204 +if cuts = [([3], Pbl),
1.1205 + ([3, 1], Frm), ([3, 1], Res),
1.1206 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1207 + ([3, 2], Res),
1.1208 + ([3], Res), ([4], Res),
1.1209 +(*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
1.1210 +raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1.1211 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1212 +print_depth 99;
1.1213 +afterins;
1.1214 +print_depth 3;
1.1215 +if afterins =
1.1216 + [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1217 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
1.1218 + ([3], Pbl)] then () else
1.1219 +raise error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1.1220 +(* use"systest/ctree.sml";
1.1221 + use"ctree.sml";
1.1222 + *)
1.1223 +
1.1224 +"---(6-1) on S(606)..S(608)--------";
1.1225 +val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
1.1226 + (Tac "test") (str2term "Inres[3,1]",[]) Complete;
1.1227 +print_depth 99;
1.1228 +cuts;
1.1229 +print_depth 3;
1.1230 +if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1231 + ([3, 2], Res),
1.1232 +(*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
1.1233 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1.1234 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1235 +print_depth 99;
1.1236 +afterins;
1.1237 +print_depth 3;
1.1238 +(*WN060727 replaced after overwriting cutlevup by test_trans
1.1239 +if afterins = [([1], Frm), ([1], Res),
1.1240 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1241 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1242 + ([2], Res),
1.1243 + ([3], Pbl),
1.1244 + ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
1.1245 + ([3], Res)(*cutlevup=false*),
1.1246 + ([4], Res),
1.1247 + ([], Res)(*cutlevup=false*)] then () else
1.1248 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.1249 +*)
1.1250 +if afterins = [([1], Frm), ([1], Res),
1.1251 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1252 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1253 + ([2], Res),
1.1254 + ([3], Pbl),
1.1255 + ([3, 1], Frm), ([3, 1], Res)] then () else
1.1256 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.1257 +
1.1258 +if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
1.1259 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1.1260 +
1.1261 +"---(6) on S(606)..S(608)--------";
1.1262 +val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
1.1263 + (Tac "test") (str2term "Inres[3,2]",[]) Complete;
1.1264 +print_depth 99;
1.1265 +cuts;
1.1266 +print_depth 3;
1.1267 +if cuts = [(*just after is: cutlevup=false in [3]*)
1.1268 +(*WN060727 after test_trans instead cutlevup added:*)
1.1269 + ([3], Res), ([4], Res), ([], Res)] then () else
1.1270 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1.1271 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1272 +print_depth 99;
1.1273 +afterins;
1.1274 +print_depth 3;
1.1275 +(*WN060727 replaced after overwriting cutlevup by test_trans
1.1276 +if afterins = [([1], Frm), ([1], Res),
1.1277 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1278 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1279 + ([2], Res),
1.1280 + ([3], Pbl),
1.1281 + ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
1.1282 + ([3], Res),
1.1283 + ([4], Res), ([], Res)] then () else
1.1284 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.1285 +*)
1.1286 +if afterins = [([1], Frm), ([1], Res),
1.1287 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1288 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1289 + ([2], Res),
1.1290 + ([3], Pbl),
1.1291 + ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
1.1292 +then () else
1.1293 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.1294 +
1.1295 +if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
1.1296 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1.1297 +
1.1298 +"---(6++) on S(606)..S(608)--------";
1.1299 +(**)
1.1300 +val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
1.1301 + (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
1.1302 +print_depth 99;
1.1303 +cuts;
1.1304 +print_depth 1;
1.1305 +if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.1306 +(*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
1.1307 +then () else
1.1308 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1.1309 +val afterins = get_allp [] ([], ([],Frm)) pt';
1.1310 +print_depth 99;
1.1311 +afterins;
1.1312 +print_depth 3;
1.1313 +if afterins = [([1], Frm), ([1], Res),
1.1314 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.1315 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.1316 + ([2], Res),
1.1317 + ([3], Pbl),
1.1318 + ([3, 1], Frm), ([3, 1], Res),
1.1319 + ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
1.1320 +raise error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1.1321 +if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
1.1322 +raise error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1.1323 +(*
1.1324 +show_pt pt';
1.1325 +show_pt pt;
1.1326 +*)
1.1327 +