wneuper/isa: test/Tools/isac/Interpret/ctree.sml@25957ffe68e8

     1 (* tests for sml/ME/ctree.sml

     2    authors: Walther Neuper 060113

     3    (c) due to copyright terms

     5 use"../smltest/ME/ctree.sml";

     6 use"ctree.sml";

     7 *)

     9 "-----------------------------------------------------------------";

    10 "table of contents -----------------------------------------------";

    11 "-----------------------------------------------------------------";

    12 "-----------------------------------------------------------------";

    13 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";

    14 "-------------- check positions in miniscript --------------------";

    15 "-------------- get_allpos' (from ptree above)--------------------";

    16 (**#####################################################################(**)

    17 "-------------- cut_level (from ptree above)----------------------";

    18 "-------------- cut_tree (from ptree above)-----------------------";

    19 "=====new ptree 1a miniscript with mini-subpbl ===================";

    20 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

    21 (**)#####################################################################**)

    22 "=====new ptree 2 miniscript with mini-subpbl ====================";

    23 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

    24 "-------------- cappend (from ptree above)------------------------";

    25 "-------------- cappend minisubpbl -------------------------------";

    27 "=====new ptree 3 ================================================";

    28 "-------------- move_dn ------------------------------------------";

    29 "-------------- move_dn: Frm -> Res ------------------------------";

    30 "-------------- move_up ------------------------------------------";

    31 "------ move into detail -----------------------------------------";

    32 "=====new ptree 3a ===============================================";

    33 "-------------- move_dn in Incomplete ctree ----------------------";

    35 "=====new ptree 4: crooked by cut_level_'_ =======================";

    36 (*############## development stopped 0501 ########################*)

    37 (******************************************************************)

    38 (*              val SAVE_get_trace = get_trace;                   *)

    39 (******************************************************************)

    40 "-------------- get_interval from ctree: incremental development--";

    41 (******************************************************************)

    42 (*              val get_trace = SAVE_get_trace;                   *)

    43 (******************************************************************)

    44 (*############## development stopped 0501 ########################*)

    46 "=====new ptree 4 ratequation ====================================";

    47 "-------------- pt_extract form, tac, asm<>[] --------------------";

    48 "=====new ptree 5 minisubpbl =====================================";

    49 "-------------- pt_extract form, tac, asm ------------------------";

    51 (**#####################################################################(**)

    52 "=====new ptree 6 minisubpbl intersteps ==========================";

    53 "-------------- get_allpos' new ----------------------------------";

    54 "-------------- cut_tree new (from ptree above)-------------------";

    55 (**)#####################################################################**)

    57 "-----------------------------------------------------------------";

    58 "-----------------------------------------------------------------";

    59 "-----------------------------------------------------------------";

    62 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";

    63 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";

    64 "-------------- build miniscript stepwise BEFORE ALL TESTS -------";

    65 "this build should be detailed each time a test fails later       ";

    66 "i.e. all the tests should be caught here first                   ";

    67 "and linked with a reference to the respective test environment   ";

    68 val fmz = ["equality (x+1=(2::int))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];

    69 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],

    70   ["Test","squ-equ-test-subpbl1"]);

    71 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    72 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    73 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    74 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    79 "-------------- check positions in miniscript --------------------";

    80 "-------------- check positions in miniscript --------------------";

    81 "-------------- check positions in miniscript --------------------";

    82 val fmz = ["equality (x+1=(2::int))",

    83 	   "solveFor x","solutions L"];

    84 val (dI',pI',mI') =

    85   ("Test",["sqroot-test","univariate","equation","test"],

    86    ["Test","squ-equ-test-subpbl1"]);

    87 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    89 (* nxt = Add_Given "equality (x + 1 = 2)"

    90    (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

    91    *)

    92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    93 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

    94    *)

    95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    96 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

    97    *)

    98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   101 "ctree.sml-------------- get_allpos' new ------------------------\"";

   102 val (PP, pp) = split_last [1];

   103 val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);

   105 val cuts = get_allp [] ([], ([],Frm)) pt;

   106 val cuts2 = get_allps [] [1] (children pt);

   107 "ctree.sml-------------- cut_tree new (from ptree above)----------";

   108 val (pt', cuts) = cut_tree pt ([1],Frm);

   109 "ctree.sml-------------- cappend on complete ctree from above ----";

   110 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");

   111 "----------------------------------------------------------------/";

   112 (*========== inhibit exn WN110319 ==============================================

   113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);

   114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);

   115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);

   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);

   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   120 (*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)

   121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   125 (*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)

   127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);

   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);

   129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);

   130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);

   131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);

   132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);

   133 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

   134 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()

   135 else error "new behaviour in test: miniscript with mini-subpbl";

   137  show_pt pt;

   138 ============ inhibit exn WN110319 ============================================*)

   140 (*=== inhibit exn ?=============================================================

   142 "-------------- get_allpos' (from ptree above)--------------------";

   143 "-------------- get_allpos' (from ptree above)--------------------";

   144 "-------------- get_allpos' (from ptree above)--------------------";

   145 if get_allpos' ([], 1) pt =

   146    [([], Frm),

   147     ([1], Frm),

   148     ([1], Res),

   149     ([2], Res),

   150     ([3], Frm),

   151     ([3, 1], Frm),

   152     ([3, 1], Res),

   153     ([3, 2], Res),

   154     ([3], Res),

   155     ([4], Res),

   156     ([], Res)]

   157 then () else error "ctree.sml: diff:behav. in get_allpos' 1";

   159 if get_allpos's ([], 1) (children pt) =

   160    [([1], Frm),

   161     ([1], Res),

   162     ([2], Res),

   163     ([3], Frm),

   164     ([3, 1], Frm),

   165     ([3, 1], Res),

   166     ([3, 2], Res),

   167     ([3], Res),

   168     ([4], Res)]

   169 then () else error "ctree.sml: diff:behav. in get_allpos' 2";

   171 if get_allpos's ([], 2) (takerest (1, children pt)) =

   172    [([2], Res),

   173     ([3], Frm),

   174     ([3, 1], Frm),

   175     ([3, 1], Res),

   176     ([3, 2], Res),

   177     ([3], Res),

   178     ([4], Res)]

   179 then () else error "ctree.sml: diff:behav. in get_allpos' 3";

   181 if get_allpos's ([], 3) (takerest (2, children pt)) =

   182    [([3], Frm),

   183     ([3, 1], Frm),

   184     ([3, 1], Res),

   185     ([3, 2], Res),

   186     ([3], Res),

   187     ([4], Res)]

   188 then () else error "ctree.sml: diff:behav. in get_allpos' 4";

   190 if get_allpos's ([3], 1) (children (nth 3 (children pt))) =

   191    [([3, 1], Frm),

   192     ([3, 1], Res),

   193     ([3, 2], Res)]

   194 then () else error "ctree.sml: diff:behav. in get_allpos' 5";

   196 if get_allpos' ([3], 1) (nth 3 (children pt)) =

   197    [([3], Frm),

   198     ([3, 1], Frm),

   199     ([3, 1], Res),

   200     ([3, 2], Res),

   201     ([3], Res)]

   202 then () else error "ctree.sml: diff:behav. in get_allpos' 6";

   205 (**##############################################################(**)

   207 "-------------- cut_level (from ptree above)----------------------";

   208 "-------------- cut_level (from ptree above)----------------------";

   209 "-------------- cut_level (from ptree above)----------------------";

   210 show_pt pt;

   211 show_pt pt';

   212 print_depth 99; cuts; print_depth 3;

   214 (*if cuts = [([2], Res),

   215 	   ([3], Frm),

   216 	   ([3, 1], Frm),

   217 	   ([3, 1], Res),

   218 	   ([3, 2], Res),

   219 	   ([3], Res),

   220 	   ([4], Res)]

   221 then () else error "ctree.sml: diff:behav. in cut_level 1a";

   222 val (res,asm) = get_obj g_result pt' [2];

   223 if res = e_term andalso asm = [] then () else

   224 error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);

   225 if not (existpt [2] pt') then () else

   226 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);

   228 val (res,asm) = get_obj g_result pt' [];

   229 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else

   230 error "ctree.sml: diff:behav. in cut_level 1ab";

   231 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =

   232    [([], Frm),

   233     ([1], Frm),

   234     ([1], Res),

   235     ([2], Res),(*, e_term in cut_tree!!!*)

   236     ([], Res)] then () else

   237 error "ctree.sml: diff:behav. in cut_level 1b";

   240 val (pt',cuts) = cut_level [] [] pt ([2],Res);

   241 if cuts = [([3], Frm),

   242 	   ([3, 1], Frm),

   243 	   ([3, 1], Res),

   244 	   ([3, 2], Res),

   245 	   ([3], Res),

   246 	   ([4], Res)]

   247 then () else error "ctree.sml: diff:behav. in cut_level 2a";

   249 if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"

   250 then () else error "ctree.sml: diff:behav. in cut_level 2b";

   252 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);

   253 if cuts = [([3, 1], Res), ([3, 2], Res)]

   254 then () else error "ctree.sml: diff:behav. in cut_level 3a";

   255 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"

   256 then () else error "ctree.sml: diff:behav. in cut_level 3b";

   258 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);

   259 if cuts = [([3, 2], Res)]

   260 then () else error "ctree.sml: diff:behav. in cut_level 4a";

   261 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"

   262 then () else error "ctree.sml: diff:behav. in cut_level 4b";

   265 "-------------- cut_tree (from ptree above)-----------------------";

   266 "-------------- cut_tree (from ptree above)-----------------------";

   267 "-------------- cut_tree (from ptree above)-----------------------";

   268 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)

   269 if cuts = [([2], Res),

   270 	   ([3], Frm),

   271 	   ([3, 1], Frm),

   272 	   ([3, 1], Res),

   273 	   ([3, 2], Res),

   274 	   ([3], Res),

   275 	   ([4], Res),

   276 	   ([], Res)]

   277 then () else error "ctree.sml: diff:behav. in cut_tree 1a";

   279 val (res,asm) = get_obj g_result pt' [2];

   280 if res = e_term (*WN050219 done by cut_level*) then () else

   281 error "ctree.sml: diff:behav. in cut_tree 1aa";

   283 val form = get_obj g_form pt' [2];

   284 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else

   285 error "ctree.sml: diff:behav. in cut_tree 1ab";

   287 val (res,asm) = get_obj g_result pt' [];

   288 if res = e_term (*WN050219 done by cut_tree*) then () else

   289 error "ctree.sml: diff:behav. in cut_tree 1ac";

   291 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =

   292    [([], Frm),

   293     ([1], Frm),

   294     ([1], Res)] then () else

   295 error "ctree.sml: diff:behav. in cut_tree 1ad";

   297 val (pt', cuts) = cut_tree pt ([2],Res);

   298 if cuts = [([3], Frm),

   299 	   ([3, 1], Frm),

   300 	   ([3, 1], Res),

   301 	   ([3, 2], Res),

   302 	   ([3], Res),

   303 	   ([4], Res),

   304 	   ([], Res)]

   305 then () else error "ctree.sml: diff:behav. in cut_tree 2";

   307 val (pt', cuts) = cut_tree pt ([3,1],Frm);

   308 if cuts = [([3, 1], Res),

   309 	   ([3, 2], Res),

   310 	   ([3], Res),

   311 	   ([4], Res),

   312 	   ([], Res)]

   313 then () else error "ctree.sml: diff:behav. in cut_tree 3";

   315 val (pt', cuts) = cut_tree pt ([3,1],Res);

   316 if cuts = [([3, 2], Res),

   317 	   ([3], Res),

   318 	   ([4], Res),

   319 	   ([], Res)]

   320 then () else error "ctree.sml: diff:behav. in cut_tree 4";

   323 "=====new ptree 1a miniscript with mini-subpbl ===================";

   324 "=====new ptree 1a miniscript with mini-subpbl ===================";

   325 "=====new ptree 1a miniscript with mini-subpbl ===================";

   326 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

   327 val (dI',pI',mI') =

   328   ("Test",["sqroot-test","univariate","equation","test"],

   329    ["Test","squ-equ-test-subpbl1"]);

   330 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   334 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   337 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   339 show_pt pt;

   341 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

   342 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

   343 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

   345 val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)

   346 if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)

   347 then () else error "ctree.sml: diff:behav. in cut_tree 4a";

   349 val (pt', cuts) = cut_tree pt ([1],Frm);

   350 if cuts = []

   351 then () else error "ctree.sml: diff:behav. in cut_tree 4a";

   353 (*WN050219

   354 val pos as ([p],_) = ([1],Frm);

   355 val pt as Nd (b,_) = pt;

   358 show_pt pt;

   359 show_pt pt';

   360 print_depth 99;cuts;print_depth 3;

   361 print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;

   362 ####################################################################*)*)

   364 "=====new ptree 2 miniscript with mini-subpbl ====================";

   365 "=====new ptree 2 miniscript with mini-subpbl ====================";

   366 "=====new ptree 2 miniscript with mini-subpbl ====================";

   367  states:=[];

   368  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   369    ("Test", ["sqroot-test","univariate","equation","test"],

   370     ["Test","squ-equ-test-subpbl1"]))];

   371  Iterator 1; moveActiveRoot 1;

   372  autoCalculate 1 CompleteCalc;

   374  interSteps 1 ([3,2],Res);

   376  val ((pt,_),_) = get_calc 1;

   377  show_pt pt;

   379 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

   380 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

   381 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

   382 (*WN050225 intermed. outcommented

   383  val (pt', cuts) = cut_tree pt ([3,2,1],Frm);

   384  if cuts = [([3, 2, 1], Res),

   385 	    ([3, 2, 2], Res),

   386 	    ([3, 2], Res),

   387 	    ([3], Res),

   388 	    ([4], Res)]

   389  then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";

   391  val (pt', cuts) = cut_tree pt ([3,2,1],Res);

   392  if cuts = [([3, 2, 2], Res),

   393 	    ([3, 2], Res),

   394 	    ([3], Res),

   395 	    ([4], Res)]

   396  then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";

   399 "-------------- cappend (from ptree above)------------------------";

   400 "-------------- cappend (from ptree above)------------------------";

   401 "-------------- cappend (from ptree above)------------------------";

   402 val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");

   403 if cuts = [([3, 2, 1], Res),

   404 	   ([3, 2, 2], Res),

   405 	   ([3, 2], Res),

   406 	   ([3], Res),

   407 	   ([4], Res),

   408 	   ([], Res)]

   409 then () else error "ctree.sml: diff:behav. in cappend_form";

   410 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso

   411    get_obj g_tac pt' [3,2,1] = Empty_Tac andalso

   412    term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"

   413  then () else error "ctree.sml: diff:behav. in cappend 1";

   415 val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")

   416     (Tac "test") (str2term "newresult",[]) Complete;

   417 if cuts = [([3, 2, 1], Res), (*?????????????*)

   418 	   ([3, 2, 2], Res),

   419 	   ([3, 2], Res),

   420 	   ([3], Res),

   421 	   ([4], Res),

   422 	   ([], Res)]

   423 then () else error "ctree.sml: diff:behav. in cappend_atomic";

   427 "-------------- cappend minisubpbl -------------------------------";

   428 "-------------- cappend minisubpbl -------------------------------";

   429 "-------------- cappend minisubpbl -------------------------------";

   430 "=====new ptree 1 miniscript with mini-subpbl ====================";

   431 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

   432 val (dI',pI',mI') =

   433   ("Test",["sqroot-test","univariate","equation","test"],

   434    ["Test","squ-equ-test-subpbl1"]);

   435 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   436 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   437 (* nxt = Add_Given "equality (x + 1 = 2)"

   438    (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   439    *)

   440 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   441 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   442    *)

   443 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   444 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   445    *)

   446 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   447 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   448 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   449 (*###cappend_form: pos =[1]  ... while calculating nxt, which pt is dropped

   450 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)

   452 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);

   453 val p = ([1], Frm);

   454 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");

   455 val form = get_obj g_form pt (fst p);

   456 val (res,_) = get_obj g_result pt (fst p);

   457 if term2str form = "x + 1 = 2" andalso res = e_term then () else

   458 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";

   459 if not (existpt ((lev_on o fst) p) pt) then () else

   460 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";

   462 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);

   463 val p = ([1], Res);

   464 val (pt,cuts) =

   465     cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")

   466 		   Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;

   467 val form = get_obj g_form pt (fst p);

   468 val (res,_) = get_obj g_result pt (fst p);

   469 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"

   470 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";

   471 if not (existpt ((lev_on o fst) p) pt) then () else

   472 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";

   474 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);

   475 val p = ([2], Res);

   476 val (pt,cuts) =

   477     cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")

   478 		   Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;

   479 val form = get_obj g_form pt (fst p);

   480 val (res,_) = get_obj g_result pt (fst p);

   481 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"

   482 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";

   483 if not (existpt ((lev_on o fst) p) pt) then () else

   484 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";

   487 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)

   488 val p = ([3], Pbl);

   489 val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);

   490 if is_pblobj (get_obj I pt (fst p)) then () else

   491 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";

   492 if not (existpt ((lev_on o fst) p) pt) then () else

   493 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";

   495 (* ...complete calchead skipped...*)

   497 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);

   498 val p = ([3, 1], Frm);

   499 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");

   500 val form = get_obj g_form pt (fst p);

   501 val (res,_) = get_obj g_result pt (fst p);

   502 if term2str form = "-1 + x = 0" andalso res = e_term then () else

   503 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";

   504 if not (existpt ((lev_on o fst) p) pt) then () else

   505 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";

   507 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)

   508 val p = ([3, 1], Res);

   509 val (pt,cuts) =

   510     cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")

   511 		   Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;

   512 val form = get_obj g_form pt (fst p);

   513 val (res,_) = get_obj g_result pt (fst p);

   514 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()

   515 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";

   516 if not (existpt ((lev_on o fst) p) pt) then () else

   517 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";

   519 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);

   520 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);

   521 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);

   522 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);

   523 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);

   524 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);

   526 WN050225 intermed. outcommented---*)

   528 "=====new ptree 3 ================================================";

   529 "=====new ptree 3 ================================================";

   530 "=====new ptree 3 ================================================";

   531  states:=[];

   532  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   533    ("Test", ["sqroot-test","univariate","equation","test"],

   534     ["Test","squ-equ-test-subpbl1"]))];

   535  Iterator 1; moveActiveRoot 1;

   536  autoCalculate 1 CompleteCalc;

   538  val ((pt,_),_) = get_calc 1;

   539  show_pt pt;

   541 "-------------- move_dn ------------------------------------------";

   542 "-------------- move_dn ------------------------------------------";

   543 "-------------- move_dn ------------------------------------------";

   544  val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);

   545  val p = move_dn [] pt p        (*-> ([1],Res)*);

   546  val p = move_dn [] pt p        (*-> ([2],Res)*);

   547  val p = move_dn [] pt p        (*-> ([3],Pbl)*);

   548  val p = move_dn [] pt p        (*-> ([3,1],Frm)*);

   549  val p = move_dn [] pt p        (*-> ([3,1],Res)*);

   550  val p = move_dn [] pt p        (*-> ([3,2],Res)*);

   551  val p = move_dn [] pt p        (*-> ([3],Res)*);

   552 (* term2str (get_obj g_res pt [3]);

   553    term2str (get_obj g_form pt [4]);

   554    *)

   555  val p = move_dn [] pt p        (*-> ([4],Res)*);

   556  val p = move_dn [] pt p        (*-> ([],Res)*);

   557 (*

   558  val p = (move_dn [] pt p) handle e => print_exn_G e;

   559                                   Exception PTREE end of calculation*)

   560 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";

   563 "-------------- move_dn: Frm -> Res ------------------------------";

   564 "-------------- move_dn: Frm -> Res ------------------------------";

   565 "-------------- move_dn: Frm -> Res ------------------------------";

   566  states := [];

   567  CalcTree      (*start of calculation, return No.1*)

   568      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

   569        ("Test",

   570 	["linear","univariate","equation","test"],

   571 	["Test","solve_linear"]))];

   572  Iterator 1; moveActiveRoot 1;

   573  autoCalculate 1 CompleteCalcHead;

   574  autoCalculate 1 (Step 1);

   575  refFormula 1 (get_pos 1 1);

   577  moveActiveRoot 1;

   578  moveActiveDown 1;

   579  if get_pos 1 1 = ([1], Frm) then ()

   580  else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";

   581  moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

   583  autoCalculate 1 (Step 1);

   584  refFormula 1 (get_pos 1 1);

   586  moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

   587  if get_pos 1 1 = ([1], Res) then ()

   588  else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";

   589  moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

   592 "-------------- move_up ------------------------------------------";

   593 "-------------- move_up ------------------------------------------";

   594 "-------------- move_up ------------------------------------------";

   595  val p = move_up [] pt ([],Res); (*-> ([4],Res)*)

   596  val p = move_up [] pt p;        (*-> ([3],Res)*)

   597  val p = move_up [] pt p;        (*-> ([3,2],Res)*)

   598  val p = move_up [] pt p;        (*-> ([3,1],Res)*)

   599  val p = move_up [] pt p;        (*-> ([3,1],Frm)*)

   600  val p = move_up [] pt p;        (*-> ([3],Pbl)*)

   601  val p = move_up [] pt p;        (*-> ([2],Res)*)

   602  val p = move_up [] pt p;        (*-> ([1],Res)*)

   603  val p = move_up [] pt p;        (*-> ([1],Frm)*)

   604  val p = move_up [] pt p;        (*-> ([],Pbl)*)

   605 (*val p = (move_up [] pt p) handle e => print_exn_G e;

   606                                   Exception PTREE begin of calculation*)

   607 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";

   610 "------ move into detail -----------------------------------------";

   611 "------ move into detail -----------------------------------------";

   612 "------ move into detail -----------------------------------------";

   613  states:=[];

   614  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   615    ("Test", ["sqroot-test","univariate","equation","test"],

   616     ["Test","squ-equ-test-subpbl1"]))];

   617  Iterator 1; moveActiveRoot 1;

   618  autoCalculate 1 CompleteCalc;

   619  moveActiveRoot 1;

   620  moveActiveDown 1;

   621  moveActiveDown 1;

   622  moveActiveDown 1;

   623  refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);

   625  interSteps 1 ([2],Res);

   627  val ((pt,_),_) = get_calc 1; show_pt pt;

   628  val p = get_pos 1 1;

   630  val p = move_up [] pt p;     (*([2, 6], Res)*);

   631  val p = movelevel_up [] pt p;(*([2], Frm)*);

   632  val p = move_dn [] pt p;     (*([2, 1], Frm)*);

   633  val p = move_dn [] pt p;     (*([2, 1], Res)*);

   634  val p = move_dn [] pt p;     (*([2, 2], Res)*);

   635  val p = move_dn [] pt p;     (*([2, 3], Res)*);

   636  val p = move_dn [] pt p;     (*([2, 4], Res)*);

   637  val p = move_dn [] pt p;     (*([2, 5], Res)*);

   638  val p = move_dn [] pt p;     (*([2, 6], Res)*);

   639  if p = ([2, 6], Res) then()

   640  else error "ctree.sml: diff.behav. in move into detail";

   642 "=====new ptree 3a ===============================================";

   643 "=====new ptree 3a ===============================================";

   644 "=====new ptree 3a ===============================================";

   645  states:=[];

   646  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   647    ("Test", ["sqroot-test","univariate","equation","test"],

   648     ["Test","squ-equ-test-subpbl1"]))];

   649  Iterator 1; moveActiveRoot 1;

   650  autoCalculate 1 CompleteCalcHead;

   651  autoCalculate 1 (Step 1);

   652  autoCalculate 1 (Step 1);

   653  autoCalculate 1 (Step 1);

   654  val ((pt,_),_) = get_calc 1;

   655  val p = move_dn [] pt ([],Pbl)       (*-> ([1], Frm)*);

   656  val p = move_dn [] pt ([1], Frm)     (*-> ([1], Res)*);

   657  val p = move_dn [] pt ([1], Res)     (*-> ([2], Res)*);

   658  (*val p = move_dn [] pt ([2], Res)     ->Exception- PTREE "[] not complete"*);

   660  moveDown 1 ([],Pbl)        (*-> ([1], Frm)*);

   661  moveDown 1 ([1],Frm)       (*-> ([1],Res)*);

   662  moveDown 1 ([1],Res)       (*-> ([2],Res)*);

   663  moveDown 1 ([2],Res)       (*-> pos does not exist*);

   664 (*

   665  get_obj g_ostate pt [1];

   666  show_pt pt;

   667 *)

   669 "-------------- move_dn in Incomplete ctree ----------------------";

   670 "-------------- move_dn in Incomplete ctree ----------------------";

   671 "-------------- move_dn in Incomplete ctree ----------------------";

   675 "=====new ptree 4: crooked by cut_level_'_ =======================";

   676 "=====new ptree 4: crooked by cut_level_'_ =======================";

   677 "=====new ptree 4: crooked by cut_level_'_ =======================";

   678 states:=[];

   679 CalcTree

   680 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

   681 	   "solveFor x","solutions L"],

   682   ("RatEq",["univariate","equation"],["no_met"]))];

   683 Iterator 1; moveActiveRoot 1;

   684 autoCalculate 1 CompleteCalc;

   686 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)

   687 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)

   688 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)

   689 getTactic 1 ([4,1],Res);(*Rewrite all_left*)

   690 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)

   691 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)

   693 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

   694 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);

   695 moveActiveFormula 1 ([3],Res)(*3.1.*);

   696 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

   697 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);

   699 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

   700 interSteps 1 ([1],Res)(*..is activeFormula !?!*);

   702 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)

   703 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)

   704 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)

   705 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)

   707 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

   708 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);

   709 val ((pt,_),_) = get_calc 1;

   710 writeln(pr_ptree pr_short pt);

   711 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:

   712  ###########################################################################*)

   713 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);

   714 writeln(pr_ptree pr_short pt);

   717 "-------------- get_interval from ctree: incremental development--";

   718 "-------------- get_interval from ctree: incremental development--";

   719 "-------------- get_interval from ctree: incremental development--";

   720 "--- level 1: get pos from start b to end p ----------------------";

   721 "--- level 1: get pos from start b to end p ----------------------";

   722 "--- level 1: get pos from start b to end p ----------------------";

   723 (******************************************************************)

   724 (**)            val SAVE_get_trace = get_trace;                 (**)

   725 (******************************************************************)

   726 (*'getnds' below is structured as such:*)

   727 fun www _ [x] = "l+r-margin"

   728   | www true [x1,x2] = "l-margin,  r-margin"

   729   | www _ [x1,x2] = "intern,  r-margin"

   730   | www true (x::(xs as _::_)) = "l-margin  " ^ www false xs

   731   | www _ (x::(xs as _::_)) = "intern  " ^ www false xs;

   732 www true [1,2,3,4,5];

   733 (*val it = "from  intern  intern  intern  to" : string*)

   734 www true [1,2];

   735 (*val it = "from  to" : string*)

   736 www true [1];

   737 (*val it = "from+to" : string*)

   739 local

   740 (*specific values of hd of pos p,q for simple handling take_fromto,

   741   from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...

   742   ... can be used even for positions _below_ p or q*)

   743 fun hdp [] = 1     | hdp [0] = 1     | hdp x = hd x;(*start with first*)

   744 fun hdq	[] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)

   745 (*analoguous for tl*)

   746 fun tlp [] = [0]     | tlp [_] = [0]     | tlp x = tl x;

   747 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;

   749 (*see modspec.sml#pt_form

   750 fun pt_form (PrfObj {form,...}) = term2str form

   751   | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =

   752     let val (dI, pI, _) = get_somespec' spec spec'

   753 	val {cas,...} = get_pbt pI

   754     in case cas of

   755 	   NONE => term2str (pblterm dI pI)

   756 	 | SOME t => term2str (subst_atomic (mk_env probl) t)

   757     end;

   758 *)

   759 (*.get an 'interval' from ptree down to a certain level

   760    by 'take_fromto children' of the nodes with specific 'from' and 'to';

   761    'i > 0' suppresses output during recursive descent towards 'from'

   762    b: the 'from' incremented to the actual pos

   763    p,q: specific 'from','to' for simple use of 'take_fromto'*)

   764 fun getnd i (b,p) q (Nd (po, nds)) =

   765     (if  i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])

   767     @ (writeln("getnd  : b="^(ints2str' b)^", p="^

   768 	       (ints2str' p)^", q="^(ints2str' q));

   770        getnds (i-1) true (b@[hdp p], tlp p) (tlq q)

   771 	       (take_fromto (hdp p) (hdq q) nds))

   773 and getnds _ _ _ _ [] = []                         (*no children*)

   774   | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)

   775   | getnds i true (b,p) q [n1, n2] =               (*l-margin,  r-margin*)

   776     (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^

   777 	     ", q="^ ints2str' q);

   778     (getnd i      (       b, p ) [99999] n1) @

   779     (getnd ~99999 (lev_on b,[0]) q       n2))

   780   | getnds i _    (b,p) q [n1, n2] =               (*intern,  r-margin*)

   781     (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^

   782 	     ", q="^ ints2str' q);

   783     (getnd i      (       b,[0]) [99999] n1) @

   784     (getnd ~99999 (lev_on b,[0]) q       n2))

   785   | getnds i true (b,p) q (nd::(nds as _::_)) =    (*l-margin, intern*)

   786     (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^

   787 	     ", q="^ ints2str' q);

   788     (getnd i             (       b, p ) [99999] nd) @

   789     (getnds ~99999 false (lev_on b,[0]) q nds))

   790   | getnds i _ (b,p) q (nd::(nds as _::_)) =       (*intern, ...*)

   791     (getnd i             (       b,[0]) [99999] nd) @

   792     (getnds ~99999 false (lev_on b,[0]) q nds);

   793 in

   794 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes

   795   where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)

   796 (1) the 'f' are given

   797 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)

   798 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)

   799 (2) the 't' ar given

   800 (2a) by 'to' if 't' = the respective element of 'to' (right margin)

   801 (2b) inifinity, if 't' < the respective element of 'to (internal node)'

   802 the 'f' and 't' are set by hdp,... *)

   803 fun get_trace pt p q =

   804     (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))

   805 	(take_fromto (hdp p) (hdq q) (children pt));

   806 end;

   808 writeln(pr_ptree pr_short pt);

   809 case get_trace pt [1,3] [4,1,1] of

   810     [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()

   811   | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";

   812 case get_trace pt [2] [4,3,2] of

   813     [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()

   814   | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";

   815 case get_trace pt [1,4] [4,3,1] of

   816     [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()

   817   | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";

   818 case get_trace pt [4,2] [5] of

   819    (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),

   820     ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)

   821     [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()

   822   | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";

   823 case get_trace pt [] [4,4,2] of

   824     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

   825      [4,3],[4,3,1],[4,3,2]] => ()

   826   | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";

   827 case get_trace pt [] [] of

   828     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

   829      [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()

   830   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";

   831 case get_trace pt [4,3] [4,3] of

   832     [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()

   833   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";

   835 "--- level 2: get pos' from start b to end p ---------------------";

   836 "--- level 2: get pos' from start b to end p ---------------------";

   837 "--- level 2: get pos' from start b to end p ---------------------";

   838 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to

   839   development stopped in favour of move_dn, see get_interval

   840   actually used (inefficient) version with move_dn: see modspec.sml

   841 *)

   842 (*

   843 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of

   844     [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()

   845   | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";

   846 case get_trace pt ([],Pbl) ([],Res) of

   847     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

   848      [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()

   849   | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";

   850 *)

   852 (******************************************************************)

   853 (**)            val get_trace = SAVE_get_trace;                 (**)

   854 (******************************************************************)

   857 "=====new ptree 4 ratequation ====================================";

   858 "=====new ptree 4 ratequation ====================================";

   859 "=====new ptree 4 ratequation ====================================";

   860 states:=[];

   861 CalcTree

   862 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

   863 	   "solveFor x","solutions L"],

   864   ("RatEq",["univariate","equation"],["no_met"]))];

   865 Iterator 1; moveActiveRoot 1;

   866 autoCalculate 1 CompleteCalc;

   867 val ((pt,_),_) = get_calc 1;

   868 show_pt pt;

   871 "-------------- pt_extract form, tac, asm<>[] --------------------";

   872 "-------------- pt_extract form, tac, asm<>[] --------------------";

   873 "-------------- pt_extract form, tac, asm<>[] --------------------";

   874 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));

   875 case (term2str form, tac, terms2strs asm) of

   876     ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",

   877      Subproblem

   878          ("PolyEq",

   879           ["normalize", "polynomial", "univariate", "equation"]),

   880 	 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()

   881   | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";

   882 (*WN060717 unintentionally changed some rls/ord while

   883      completing knowl. for thes2file...

   885   case (term2str form, tac, terms2strs asm) of

   886     ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",

   887      *)Subproblem

   888          ("PolyEq",

   889           ["normalize", "polynomial", "univariate", "equation"]),

   890 	 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()

   891   | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";

   893 .... but it became even better*)

   897 "=====new ptree 5 minisubpbl =====================================";

   898 "=====new ptree 5 minisubpbl =====================================";

   899 "=====new ptree 5 minisubpbl =====================================";

   900 states:=[];

   901 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   902    ("Test", ["sqroot-test","univariate","equation","test"],

   903     ["Test","squ-equ-test-subpbl1"]))];

   904 Iterator 1; moveActiveRoot 1;

   905 autoCalculate 1 CompleteCalc;

   906 val ((pt,_),_) = get_calc 1;

   907 show_pt pt;

   909 "-------------- pt_extract form, tac, asm ------------------------";

   910 "-------------- pt_extract form, tac, asm ------------------------";

   911 "-------------- pt_extract form, tac, asm ------------------------";

   912 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));

   913 case (term2str form, tac, terms2strs asm) of

   914     ("solve (x + 1 = 2, x)",

   915     Apply_Method ["Test", "squ-equ-test-subpbl1"],

   916      []) => ()

   917   | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";

   919 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));

   920 case (term2str form, tac, terms2strs asm) of

   921     ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()

   922   | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";

   924 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));

   925 case (term2str form, tac, terms2strs asm) of

   926     ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()

   927   | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";

   929 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));

   930 case (term2str form, tac, terms2strs asm) of

   931     ("-1 + x = 0",

   932      Subproblem ("Test", ["linear", "univariate", "equation", "test"]),

   933      []) => ()

   934   | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";

   936 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));

   937 case (term2str form, tac, terms2strs asm) of

   938     ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()

   939   | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";

   941 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));

   942 case (term2str form, tac, terms2strs asm) of

   943     ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()

   944   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";

   946 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));

   947 case (term2str form, tac, terms2strs asm) of

   948     ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()

   949   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";

   951 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));

   952 case (term2str form, tac, terms2strs asm) of

   953     ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],

   954      []) => ()

   955   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";

   957 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));

   958 case (term2str form, tac, terms2strs asm) of

   959     ("[x = 1]", Check_elementwise "Assumptions", []) => ()

   960   | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";

   962 val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));

   963 case (term2str form, tac, terms2strs asm) of

   964     ("[x = 1]",

   965      Check_Postcond ["sqroot-test", "univariate", "equation", "test"],

   966      []) => ()

   967   | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";

   969 val (Form form, tac, asm) = pt_extract (pt, ([], Res));

   970 case (term2str form, tac, terms2strs asm) of

   971     ("[x = 1]", NONE, []) => ()

   972   | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";

   974 "=====new ptree 6 minisubpbl intersteps ==========================";

   975 "=====new ptree 6 minisubpbl intersteps ==========================";

   976 "=====new ptree 6 minisubpbl intersteps ==========================";

   977 states:=[];

   978 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   979    ("Test", ["sqroot-test","univariate","equation","test"],

   980     ["Test","squ-equ-test-subpbl1"]))];

   981 Iterator 1; moveActiveRoot 1;

   982 autoCalculate 1 CompleteCalc;

   983 interSteps 1 ([2],Res);

   984 interSteps 1 ([3,2],Res);

   985 val ((pt,_),_) = get_calc 1;

   986 show_pt pt;

   988 (**##############################################################**)

   989 "-------------- get_allpos' new ----------------------------------";

   990 "-------------- get_allpos' new ----------------------------------";

   991 "-------------- get_allpos' new ----------------------------------";

   992 "--- whole ctree";

   993 print_depth 99;

   994 val cuts = get_allp [] ([], ([],Frm)) pt;

   995 print_depth 3;

   996 if cuts =

   997    [(*never returns the first pos'*)

   998     ([1], Frm),

   999     ([1], Res),

  1000     ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1001     ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1002     ([2], Res),

  1003     ([3], Pbl),

  1004     ([3, 1], Frm), ([3, 1], Res),

  1005     ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1006     ([3, 2], Res),

  1007     ([3], Res),

  1008     ([4], Res),

  1009     ([], Res)] then () else

  1010 error "ctree.sml diff.behav. get_allp new []";

  1012 print_depth 99;

  1013 val cuts2 = get_allps [] [1] (children pt);

  1014 print_depth 3;

  1015 if cuts = cuts2 @ [([], Res)] then () else

  1016 error "ctree.sml diff.behav. get_allps new []";

  1018 "---(3) on S(606)..S(608)--------";

  1019 "--- nd [2] with 6 children---------------------------------";

  1020 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);

  1021 if cuts =

  1022    [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1023     ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1024     ([2], Res)] then () else

  1025 error "ctree.sml diff.behav. get_allp new [2]";

  1027 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));

  1028 if cuts = cuts2 @ [([2], Res)] then () else

  1029 error "ctree.sml diff.behav. get_allps new [2]";

  1032 "---(4) on S(606)..S(608)--------";

  1033 "--- nd [3] subproblem--------------------------------------";

  1034 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);

  1035 if cuts =

  1036    [([3, 1], Frm),

  1037     ([3, 1], Res),

  1038     ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1039     ([3, 2], Res),

  1040     ([3], Res)] then () else

  1041 error "ctree.sml diff.behav. get_allp new [3]";

  1043 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));

  1044 if cuts = cuts2 @ [([3], Res)] then () else

  1045 error "ctree.sml diff.behav. get_allps new [3]";

  1047 "--- nd [3,2] with 2 children--------------------------------";

  1048 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);

  1049 if cuts =

  1050    [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1051     ([3, 2], Res)] then () else

  1052 error "ctree.sml diff.behav. get_allp new [3,2]";

  1054 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));

  1055 if cuts = cuts2 @ [([3, 2], Res)] then () else

  1056 error "ctree.sml diff.behav. get_allps new [3,2]";

  1058 "---(5a) on S(606)..S(608)--------";

  1059 "--- nd [3,2,1] with 0 children------------------------------";

  1060 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);

  1061 if cuts =

  1062    [] then () else

  1063 error "ctree.sml diff.behav. get_allp new [3,2,1]";

  1065 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));

  1066 if cuts = cuts2 @ [] then () else

  1067 error "ctree.sml diff.behav. get_allps new [3,2,1]";

  1070 (**#################################################################**)

  1071 "-------------- cut_tree new (from ptree above)-------------------";

  1072 "-------------- cut_tree new (from ptree above)-------------------";

  1073 "-------------- cut_tree new (from ptree above)-------------------";

  1074 show_pt pt;

  1075 val b = get_obj g_branch pt [];

  1076 if b = TransitiveB then () else

  1077 error ("ctree.sml diff.behav. in [] branch="^branch2str b);

  1078 val b = get_obj g_branch pt [3];

  1079 if b = TransitiveB then () else

  1080 error ("ctree.sml diff.behav. in [3] branch="^branch2str b);

  1082 "---(2) on S(606)..S(608)--------";

  1083 val (pt', cuts) = cut_tree pt ([1],Res);

  1084 print_depth 99;

  1085 cuts;

  1086 print_depth 3;

  1087 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1088       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),

  1089       ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),

  1090       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),

  1091 (*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else

  1092 error "ctree.sml: diff.behav. cut_tree ([1],Res)";

  1095 "---(3) on S(606)..S(608)--------";

  1096 val (pt', cuts) = cut_tree pt ([2],Res);

  1097 print_depth 99;

  1098 cuts;

  1099 print_depth 3;

  1100 if cuts = [(*preceding step on WS was ([1]),Res*)

  1101 	   ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1102 	   ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1103 	   ([2], Res),

  1104 	   ([3], Pbl),

  1105 	   ([3, 1], Frm),

  1106 	   ([3, 1], Res),

  1107 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1108 	   ([3, 2], Res),

  1109 	   ([3], Res),

  1110 	   ([4], Res),

  1111 (*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()

  1112 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";

  1114 "---(4) on S(606)..S(608)--------";

  1115 val (pt', cuts) = cut_tree pt ([3],Pbl);

  1116 print_depth 99;

  1117 cuts;

  1118 print_depth 3;

  1119 if cuts = [([3], Pbl),

  1120 	   ([3, 1], Frm), ([3, 1], Res),

  1121 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1122 	   ([3, 2], Res),

  1123 	   ([3], Res),

  1124 	   ([4], Res),

  1125 (*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]

  1126 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";

  1128 "---(5a) on S(606)..S(608) cut_tree --------";

  1129 val (pt', cuts) = cut_tree pt ([3,2,1],Res);

  1130 print_depth 99;

  1131 cuts;

  1132 print_depth 1;

  1133 if cuts = [([3, 2, 2], Res), ([3, 2], Res),

  1134 (*WN060727 added after replacing cutlevup by test_trans:*)

  1135 ([3], Res), ([4], Res),([],Res)] then ()

  1136 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";

  1137 show_pt pt';

  1140 "-------------- cappend on complete ctree from above -------------";

  1141 "-------------- cappend on complete ctree from above -------------";

  1142 "-------------- cappend on complete ctree from above -------------";

  1143 show_pt pt;

  1145 "---(2) on S(606)..S(608)--------";

  1146 val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")

  1147     (Tac "test") (str2term "Inres[1]",[]) Complete;

  1148 print_depth 99;

  1149 cuts;

  1150 print_depth 3;

  1151 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1152       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),

  1153       ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),

  1154       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),

  1155 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()

  1156 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";

  1157 val afterins = get_allp [] ([], ([],Frm)) pt';

  1158 print_depth 99;

  1159 afterins;

  1160 print_depth 3;

  1161 if afterins = [([1], Frm), ([1], Res)

  1162 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()

  1163 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";

  1164 show_pt pt';

  1166 "---(3) on S(606)..S(608)--------";

  1167 show_pt pt;

  1168 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")

  1169     (Tac "test") (str2term "Inres[2]",[]) Complete;

  1170 print_depth 99;

  1171 cuts;

  1172 print_depth 3;

  1173 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

  1174       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),

  1175       ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),

  1176       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),

  1177 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()

  1178 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";

  1179 val afterins = get_allp [] ([], ([],Frm)) pt';

  1180 print_depth 99;

  1181 afterins;

  1182 print_depth 3;

  1183 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)

  1184 (*,  WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]

  1185 then () else

  1186 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";

  1187 show_pt pt';

  1188 (*

  1189  val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);

  1190  val p = move_dn [] pt' p        (*-> ([1],Res)*);

  1191  val p = move_dn [] pt' p        (*-> ([2],Frm)*);

  1192  val p = move_dn [] pt' p        (*-> ([2],Res)*);

  1194  term2str (get_obj g_form pt' [2]);

  1195  term2str (get_obj g_res pt' [2]);

  1196  ostate2str (get_obj g_ostate pt' [2]);

  1197  *)

  1199 "---(4) on S(606)..S(608)--------";

  1200 val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)

  1201 				  ([],e_spec, str2term "Inhead[3]");

  1202 print_depth 99;

  1203 cuts;

  1204 print_depth 3;

  1205 if cuts = [([3], Pbl),

  1206 	   ([3, 1], Frm), ([3, 1], Res),

  1207 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1208 	   ([3, 2], Res),

  1209 	   ([3], Res), ([4], Res),

  1210 (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else

  1211 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";

  1212 val afterins = get_allp [] ([], ([],Frm)) pt';

  1213 print_depth 99;

  1214 afterins;

  1215 print_depth 3;

  1216 if afterins =

  1217    [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1218     ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),

  1219     ([3], Pbl)] then () else

  1220 error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";

  1221 (* use"systest/ctree.sml";

  1222    use"ctree.sml";

  1223    *)

  1225 "---(6-1) on S(606)..S(608)--------";

  1226 val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")

  1227     (Tac "test") (str2term "Inres[3,1]",[]) Complete;

  1228 print_depth 99;

  1229 cuts;

  1230 print_depth 3;

  1231 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

  1232 	   ([3, 2], Res),

  1233 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else

  1234 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";

  1235 val afterins = get_allp [] ([], ([],Frm)) pt';

  1236 print_depth 99;

  1237 afterins;

  1238 print_depth 3;

  1239 (*WN060727 replaced after overwriting cutlevup by test_trans

  1240 if afterins = [([1], Frm), ([1], Res),

  1241 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1242 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1243 	       ([2], Res),

  1244 	       ([3], Pbl),

  1245 	       ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)

  1246 	       ([3], Res)(*cutlevup=false*),

  1247 	       ([4], Res),

  1248 	       ([], Res)(*cutlevup=false*)] then () else

  1249 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";

  1250 *)

  1251 if afterins = [([1], Frm), ([1], Res),

  1252 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1253 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1254 	       ([2], Res),

  1255 	       ([3], Pbl),

  1256 	       ([3, 1], Frm), ([3, 1], Res)] then () else

  1257 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";

  1259 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else

  1260 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";

  1262 "---(6) on S(606)..S(608)--------";

  1263 val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")

  1264     (Tac "test") (str2term "Inres[3,2]",[]) Complete;

  1265 print_depth 99;

  1266 cuts;

  1267 print_depth 3;

  1268 if cuts = [(*just after is: cutlevup=false in [3]*)

  1269 (*WN060727 after test_trans instead cutlevup added:*)

  1270 	   ([3], Res), ([4], Res), ([], Res)] then () else

  1271 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";

  1272 val afterins = get_allp [] ([], ([],Frm)) pt';

  1273 print_depth 99;

  1274 afterins;

  1275 print_depth 3;

  1276 (*WN060727 replaced after overwriting cutlevup by test_trans

  1277 if afterins = [([1], Frm), ([1], Res),

  1278 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1279 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1280 	       ([2], Res),

  1281 	       ([3], Pbl),

  1282 	       ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),

  1283 	       ([3], Res),

  1284 	       ([4], Res), ([], Res)] then () else

  1285 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";

  1286 *)

  1287 if afterins = [([1], Frm), ([1], Res),

  1288 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1289 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1290 	       ([2], Res),

  1291 	       ([3], Pbl),

  1292 	       ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]

  1293 then () else

  1294 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";

  1296 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else

  1297 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";

  1299 "---(6++) on S(606)..S(608)--------";

  1300 (**)

  1301 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")

  1302     (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;

  1303 print_depth 99;

  1304 cuts;

  1305 print_depth 1;

  1306 if cuts = [([3, 2, 2], Res), ([3, 2], Res),

  1307 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1308 then () else

  1309 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";

  1310 val afterins = get_allp [] ([], ([],Frm)) pt';

  1311 print_depth 99;

  1312 afterins;

  1313 print_depth 3;

  1314 if afterins = [([1], Frm), ([1], Res),

  1315 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),

  1316 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),

  1317 	       ([2], Res),

  1318 	       ([3], Pbl),

  1319 	       ([3, 1], Frm), ([3, 1], Res),

  1320 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1321 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

  1322 if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else

  1323 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";

  1324 (*

  1325 show_pt pt';

  1326 show_pt pt;

  1327 *)

  1329 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 03 May 2011 16:20:55 +0200
branch	decompose-isar
changeset 41970	25957ffe68e8
parent 41968	3228aa46fd30
child 41972	22c5483e9bfb
permissions	-rw-r--r--