wneuper/isa: test/Tools/isac/MathEngBasic/ctree.sml@df00a2b5c4cc

     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 "-------------- fun get_ctxt, g_ctxt -----------------------------";

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

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

    16 "-------------- cut_level (from ctree above)----------------------";

    17 "-------------- cut_tree (from ctree above)-----------------------";

    18 "=====new ctree 1a miniscript with mini-subpbl ===================";

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

    20 "=====new ctree 2 miniscript with mini-subpbl ====================";

    21 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

    22 "-------------- cappend (from ctree above)------------------------";

    23 "-------------- cappend minisubpbl -------------------------------";

    24 "=====new ctree 3 ================================================";

    25 "-------------- move_dn ------------------------------------------";

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

    27 "-------------- move_up ------------------------------------------";

    28 "------ move into detail -----------------------------------------";

    29 "=====new ctree 3a ===============================================";

    30 "-------------- move_dn in Incomplete ctree ----------------------";

    31 "=====new ctree 4: crooked by cut_level_'_ =======================";

    32 (*//############## development stopped 0501 ########################\\*)

    33 (******************************************************************)

    34 (*              val SAVE_get_trace = get_trace;                   *)

    35 (******************************************************************)

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

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

    38 (*              val get_trace = SAVE_get_trace;                   *)

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

    40 (*\\############## development stopped 0501 ########################//*)

    41 "=====new ctree 4 ratequation ====================================";

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

    43 "=====new ctree 5 minisubpbl =====================================";

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

    45 "=====new ctree 6 minisubpbl intersteps ==========================";

    46 "-------------- get_allpos' new ----------------------------------";

    47 "-------------- cut_tree new (from ctree above)-------------------";

    48 "-------------- repl_app------------------------------------------";

    49 "-----------------------------------------------------------------";

    50 "-----------------------------------------------------------------";

    51 "-----------------------------------------------------------------";

    54 "-------------- fun get_ctxt, g_ctxt -----------------------------";

    55 "-------------- fun get_ctxt, g_ctxt -----------------------------";

    56 "-------------- fun get_ctxt, g_ctxt -----------------------------";

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

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

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

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

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

    62 (get_ctxt pt p)

    63   handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";

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

    65 (get_ctxt pt p)

    66   handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";

    68 val pt = EmptyPtree;

    69 val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term, e_ctxt) pt;

    70 val ctxt = get_obj g_ctxt pt [];

    71 if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";

    73 "-------------- check positions in miniscript --------------------";

    74 "-------------- check positions in miniscript --------------------";

    75 "-------------- check positions in miniscript --------------------";

    76 val fmz = ["equality (x+1=(2::real))",

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

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

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

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

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

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

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

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

    85    *)

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

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

    88    *)

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

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

    91    *)

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

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

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

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

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

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

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

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

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

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

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

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

   105 "----------------------------------------------------------------/";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   127 val FormKF res = f;

   128 if res = "[x = 1]"

   129 then case nxt of End_Proof' => ()

   130   | _ => error "new behaviour in test: miniscript with mini-subpbl 1"

   131 else error "new behaviour in test: miniscript with mini-subpbl 2"

   133  show_pt pt;

   135 "-------------- get_allpos' (from ctree above)--------------------";

   136 "-------------- get_allpos' (from ctree above)--------------------";

   137 "-------------- get_allpos' (from ctree above)--------------------";

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

   139    [([], Frm),

   140     ([1], Frm),

   141     ([1], Res),

   142     ([2], Res),

   143     ([3], Frm),

   144     ([3, 1], Frm),

   145     ([3, 1], Res),

   146     ([3, 2], Res),

   147     ([3], Res),

   148     ([4], Res),

   149     ([], Res)]

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

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

   153    [([1], Frm),

   154     ([1], Res),

   155     ([2], Res),

   156     ([3], Frm),

   157     ([3, 1], Frm),

   158     ([3, 1], Res),

   159     ([3, 2], Res),

   160     ([3], Res),

   161     ([4], Res)]

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

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

   165    [([2], Res),

   166     ([3], Frm),

   167     ([3, 1], Frm),

   168     ([3, 1], Res),

   169     ([3, 2], Res),

   170     ([3], Res),

   171     ([4], Res)]

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

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

   175    [([3], Frm),

   176     ([3, 1], Frm),

   177     ([3, 1], Res),

   178     ([3, 2], Res),

   179     ([3], Res),

   180     ([4], Res)]

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

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

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

   185     ([3, 1], Res),

   186     ([3, 2], Res)]

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

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

   190    [([3], Frm),

   191     ([3, 1], Frm),

   192     ([3, 1], Res),

   193     ([3, 2], Res),

   194     ([3], Res)]

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

   202 "-------------- cut_level (from ctree above)----------------------";

   203 "-------------- cut_level (from ctree above)----------------------";

   204 "-------------- cut_level (from ctree above)----------------------";

   205 show_pt pt;

   206 show_pt pt';

   207 (*default_print_depth 99*) cuts; (*default_print_depth 3*)

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

   210 	   ([3], Frm),

   211 	   ([3, 1], Frm),

   212 	   ([3, 1], Res),

   213 	   ([3, 2], Res),

   214 	   ([3], Res),

   215 	   ([4], Res)]

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

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

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

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

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

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

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

   225 (*============ inhibit exn AK110726 ==============================================

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

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

   228 ============ inhibit exn AK110726 ==============================================*)

   229 (*============ inhibit exn AK110726 ==============================================

   230 if map fst3 (get_interval ([],Frm) ([],Res) 9999 pt') =

   231    [([], Frm),

   232     ([1], Frm),

   233     ([1], Res),

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

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

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

   237 ============ inhibit exn AK110726 ==============================================*)

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

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

   241 	   ([3, 1], Frm),

   242 	   ([3, 1], Res),

   243 	   ([3, 2], Res),

   244 	   ([3], Res),

   245 	   ([4], Res)]

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

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

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

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

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

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

   254 if pr_ctree 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"

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

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

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

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

   260 if pr_ctree 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"

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

   264 "-------------- cut_tree (from ctree above)-----------------------";

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

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

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

   269 (*============ inhibit exn AK110726 ==============================================

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

   271 	   ([3], Frm),

   272 	   ([3, 1], Frm),

   273 	   ([3, 1], Res),

   274 	   ([3, 2], Res),

   275 	   ([3], Res),

   276 	   ([4], Res),

   277 	   ([], Res)]

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

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

   281 ============ inhibit exn AK110726 ==============================================*)

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

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

   286 (*============ inhibit exn AK110726 ==============================================

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

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

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

   290 ============ inhibit exn AK110726 ==============================================*)

   291 (* AK110727 Debuging

   292   (* get_obj g_form pt' [2];

   293     (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"

   294           raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)

   295 "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)

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

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

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

   301 if map fst3 (get_interval ([],Frm) ([],Res) 9999 pt') =

   302    [([], Frm),

   303     ([1], Frm),

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

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

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

   308 (*============ inhibit exn AK110726 ==============================================

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

   310 	   ([3, 1], Frm),

   311 	   ([3, 1], Res),

   312 	   ([3, 2], Res),

   313 	   ([3], Res),

   314 	   ([4], Res),

   315 	   ([], Res)]

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

   317 ============ inhibit exn AK110726 ==============================================*)

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

   320 (*============ inhibit exn AK110726 ==============================================

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

   322 	   ([3, 2], Res),

   323 	   ([3], Res),

   324 	   ([4], Res),

   325 	   ([], Res)]

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

   327 ============ inhibit exn AK110726 ==============================================*)

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

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

   331 	   ([3], Res),

   332 	   ([4], Res),

   333 	   ([], Res)]

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

   336 "=====new ctree 1a miniscript with mini-subpbl ===================";

   337 "=====new ctree 1a miniscript with mini-subpbl ===================";

   338 "=====new ctree 1a miniscript with mini-subpbl ===================";

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

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

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

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

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

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

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

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

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

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

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

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

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

   352 show_pt pt;

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

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

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

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

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

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

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

   363 if cuts = []

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

   366 (*WN050219

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

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

   371 show_pt pt;

   372 show_pt pt';

   373 (*default_print_depth 99;*)cuts;(*default_print_depth 3;*)

   374 (*default_print_depth 99;*)map fst3 (get_interval ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)

   375 ####################################################################*)

   379 "=====new ctree 2 miniscript with mini-subpbl ====================";

   380 "=====new ctree 2 miniscript with mini-subpbl ====================";

   381 "=====new ctree 2 miniscript with mini-subpbl ====================";

   382 reset_states ();

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

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

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

   386  Iterator 1; moveActiveRoot 1;

   387  autoCalculate 1 CompleteCalc;

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

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

   392  show_pt pt;

   394 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()

   395 else error "mini-subpbl interSteps broken";

   397 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   398 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   399 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   400 (*WN050225 intermed. outcommented

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

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

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

   404 	    ([3, 2], Res),

   405 	    ([3], Res),

   406 	    ([4], Res)]

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

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

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

   411 	    ([3, 2], Res),

   412 	    ([3], Res),

   413 	    ([4], Res)]

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

   417 "-------------- cappend (from ctree above)------------------------";

   418 "-------------- cappend (from ctree above)------------------------";

   419 "-------------- cappend (from ctree above)------------------------";

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

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

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

   423 	   ([3, 2], Res),

   424 	   ([3], Res),

   425 	   ([4], Res),

   426 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   437 	   ([3, 2], Res),

   438 	   ([3], Res),

   439 	   ([4], Res),

   440 	   ([], Res)]

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

   445 "-------------- cappend minisubpbl -------------------------------";

   446 "-------------- cappend minisubpbl -------------------------------";

   447 "-------------- cappend minisubpbl -------------------------------";

   448 "=====new ctree 1 miniscript with mini-subpbl ====================";

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

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

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

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

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

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

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

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

   457    *)

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

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

   460    *)

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

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

   463    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   482 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   494 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   513 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   527 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   544 WN050225 intermed. outcommented---*)

   546 "=====new ctree 3 ================================================";

   547 "=====new ctree 3 ================================================";

   548 "=====new ctree 3 ================================================";

   550 reset_states ();

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

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

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

   554  Iterator 1; moveActiveRoot 1;

   555  autoCalculate 1 CompleteCalc;

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

   558  show_pt pt;

   560 "-------------- move_dn ------------------------------------------";

   561 "-------------- move_dn ------------------------------------------";

   562 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   572    term2str (get_obj g_form pt [4]);

   573    *)

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

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

   576 (*

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

   578                                   Exception PTREE end of calculation*)

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

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

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

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

   585  reset_states ();

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

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

   588        ("Test",

   589 	["LINEAR","univariate","equation","test"],

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

   591  Iterator 1; moveActiveRoot 1;

   592  autoCalculate 1 CompleteCalcHead;

   593  autoCalculate 1 (Steps 1);

   594  refFormula 1 (get_pos 1 1);

   596  moveActiveRoot 1;

   597  moveActiveDown 1;

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

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

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

   602  autoCalculate 1 (Steps 1);

   603  refFormula 1 (get_pos 1 1);

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

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

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

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

   611 "-------------- move_up ------------------------------------------";

   612 "-------------- move_up ------------------------------------------";

   613 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   625                                   Exception PTREE begin of calculation*)

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

   629 "------ move into detail -----------------------------------------";

   630 "------ move into detail -----------------------------------------";

   631 "------ move into detail -----------------------------------------";

   632  reset_states ();

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

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

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

   636  Iterator 1; moveActiveRoot 1;

   637  autoCalculate 1 CompleteCalc;

   638  moveActiveRoot 1;

   639  moveActiveDown 1;

   640  moveActiveDown 1;

   641  moveActiveDown 1;

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

   644  interSteps 1 ([2],Res);

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

   647  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   661 "=====new ctree 3a ===============================================";

   662 "=====new ctree 3a ===============================================";

   663 "=====new ctree 3a ===============================================";

   664  reset_states ();

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

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

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

   668  Iterator 1; moveActiveRoot 1;

   669  autoCalculate 1 CompleteCalcHead;

   670  autoCalculate 1 (Steps 1);

   671  autoCalculate 1 (Steps 1);

   672  autoCalculate 1 (Steps 1);

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

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

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

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

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

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

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

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

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

   683 (*

   684  get_obj g_ostate pt [1];

   685  show_pt pt;

   686 *)

   688 "-------------- move_dn in Incomplete ctree ----------------------";

   689 "-------------- move_dn in Incomplete ctree ----------------------";

   690 "-------------- move_dn in Incomplete ctree ----------------------";

   694 "=====new ctree 4: crooked by cut_level_'_ =======================";

   695 "=====new ctree 4: crooked by cut_level_'_ =======================";

   696 "=====new ctree 4: crooked by cut_level_'_ =======================";

   697 reset_states ();

   698 CalcTree

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

   700 	   "solveFor x","solutions L"],

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

   702 Iterator 1; moveActiveRoot 1;

   703 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   729 writeln(pr_ctree pr_short pt);

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

   731  ###########################################################################*)

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

   733 writeln(pr_ctree pr_short pt);

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

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

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

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

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

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

   745 (******************************************************************)

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

   747 (******************************************************************)

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

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

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

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

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

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

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

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

   756 www true [1,2];

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

   758 www true [1];

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

   761 local

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

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

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

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

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

   767 (*analoguous for tl*)

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

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

   771 (*see modspec.sml#pt_form

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

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

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

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

   776     in case cas of

   777 	   NONE => term2str (pblterm dI pI)

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

   779     end;

   780 *)

   781 (*.get an 'interval' from ctree down to a certain level

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   815 in

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

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

   818 (1) the 'f' are given

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

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

   821 (2) the 't' ar given

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

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

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

   825 fun get_trace pt p q =

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

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

   828 end;

   830 writeln(pr_ctree pr_short pt);

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

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

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

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

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

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

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

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

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

   843 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

   849 ========== inhibit exn AK110719 ==============================================*)

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

   852     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   856 (*========== inhibit exn AK110719 ==============================================

   857 case get_trace pt [] [] of

   858     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

   864 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   870   development stopped in favour of move_dn, see get_interval

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

   872 *)

   873 (*

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

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

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

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

   878     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   881 *)

   883 (******************************************************************)

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

   885 (******************************************************************)

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

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

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

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

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

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

   893      Subproblem

   894          ("PolyEq",

   895           ["normalise", "polynomial", "univariate", "equation"]),

   896 	 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]) => ()

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

   898 (*WN060717 unintentionally changed some rls/ord while

   899      completing knowl. for thes2file...

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

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

   903      *)Subproblem

   904          ("PolyEq",

   905           ["normalise", "polynomial", "univariate", "equation"]),

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

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

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

   913 "=====new ctree 5 minisubpbl =====================================";

   914 "=====new ctree 5 minisubpbl =====================================";

   915 "=====new ctree 5 minisubpbl =====================================";

   916 reset_states ();

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

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

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

   920 Iterator 1; moveActiveRoot 1;

   921 autoCalculate 1 CompleteCalc;

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

   923 show_pt pt;

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

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

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

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

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

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

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

   932      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   947     ("-1 + x = 0",

   948      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

   949      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   969     ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],

   970      []) => ()

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

   973 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

   981     ("[x = 1]",

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

   983      []) => ()

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

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

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

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

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

   990 ========== inhibit exn AK110719 ==============================================*)

   992 "=====new ctree 6 minisubpbl intersteps ==========================";

   993 "=====new ctree 6 minisubpbl intersteps ==========================";

   994 "=====new ctree 6 minisubpbl intersteps ==========================";

   995 reset_states ();

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

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

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

   999 Iterator 1; moveActiveRoot 1;

  1000 autoCalculate 1 CompleteCalc;

  1001 interSteps 1 ([2],Res);

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

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

  1004 show_pt pt;

  1006 (**##############################################################**)

  1007 "-------------- get_allpos' new ----------------------------------";

  1008 "-------------- get_allpos' new ----------------------------------";

  1009 "-------------- get_allpos' new ----------------------------------";

  1010 "--- whole ctree";

  1011 (*default_print_depth 99;*)

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

  1013 (*default_print_depth 3;*)

  1014 if cuts =

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

  1016     ([1], Frm),

  1017     ([1], Res),

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

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

  1020     ([2], Res),

  1021     ([3], Pbl),

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

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

  1024     ([3, 2], Res),

  1025     ([3], Res),

  1026     ([4], Res),

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

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

  1030 (*default_print_depth 99;*)

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

  1032 (*default_print_depth 3;*)

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

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

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

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

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

  1039 if cuts =

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

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

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

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

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

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

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

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

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

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

  1053 if cuts =

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

  1055     ([3, 1], Res),

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

  1057     ([3, 2], Res),

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

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

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

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

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

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

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

  1067 if cuts =

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

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

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

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

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

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

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

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

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

  1079 if cuts =

  1080    [] then () else

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

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

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

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

  1088 (**#################################################################**)

  1089 "-------------- cut_tree new (from ctree above)-------------------";

  1090 "-------------- cut_tree new (from ctree above)-------------------";

  1091 "-------------- cut_tree new (from ctree above)-------------------";

  1092 show_pt pt;

  1093 val b = get_obj g_branch pt [];

  1094 if b = TransitiveB then () else

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

  1096 val b = get_obj g_branch pt [3];

  1097 if b = TransitiveB then () else

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

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

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

  1102 (*default_print_depth 99;*)

  1103 cuts;

  1104 (*default_print_depth 3;*)

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

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

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

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

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

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

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

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

  1115 (*default_print_depth 99;*)

  1116 cuts;

  1117 (*default_print_depth 3;*)

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

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

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

  1121 	   ([2], Res),

  1122 	   ([3], Pbl),

  1123 	   ([3, 1], Frm),

  1124 	   ([3, 1], Res),

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

  1126 	   ([3, 2], Res),

  1127 	   ([3], Res),

  1128 	   ([4], Res),

  1129 	   ([],Res)] then ()

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

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

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

  1134 (*default_print_depth 99;*)

  1135 cuts;

  1136 (*default_print_depth 3;*)

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

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

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

  1140 	   ([3, 2], Res),

  1141 	   ([3], Res),

  1142 	   ([4], Res),

  1143 	   ([], Res)]

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

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

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

  1148 (*default_print_depth 99;*)

  1149 cuts;

  1150 (*default_print_depth 1;*)

  1151 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then ()

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

  1153 show_pt pt';

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

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

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

  1159 show_pt pt;

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

  1162 (*========== inhibit exn AK110726 ==============================================

  1163 (* ERROR: Can't unify istate to istate * Proof.context *)

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

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

  1167 (*default_print_depth 99;*)

  1168 cuts;

  1169 (*default_print_depth 3;*)

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

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

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

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

  1174 	    ([], Res)] then ()

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

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

  1178 (*default_print_depth 99;*)

  1179 afterins;

  1180 (*default_print_depth 3;*)

  1181 if afterins = [([1], Frm), ([1], Res)] then()

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

  1183 show_pt pt';

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

  1185 show_pt pt;

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

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

  1188 (*default_print_depth 99;*)

  1189 cuts;

  1190 (*default_print_depth 3;*)

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

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

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

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

  1196 	    ([], Res)] then ()

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

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

  1201 (*default_print_depth 99;*)

  1202 afterins;

  1203 (*default_print_depth 3;*)

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

  1206 then () else

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

  1208 show_pt pt';

  1211 (*

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

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

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

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

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

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

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

  1220  *)

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

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

  1224 				  ([],e_spec, str2term "Inhead[3]", e_ctxt);

  1225 (*default_print_depth 99;*)

  1226 cuts;

  1227 (*default_print_depth 3;*)

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

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

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

  1231 	   ([3, 2], Res),

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

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

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

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

  1236 (*default_print_depth 99;*)

  1237 afterins;

  1238 (*default_print_depth 3;*)

  1239 if afterins =

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

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

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

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

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

  1245    use"ctree.sml";

  1246    *)

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

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

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

  1251 (*default_print_depth 99;*)

  1252 cuts;

  1253 (*default_print_depth 3;*)

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

  1255 	   ([3, 2], Res),

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

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

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

  1260 (*default_print_depth 99;*)

  1261 afterins;

  1262 (*default_print_depth 3;*)

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

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

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

  1266 	       ([2], Res),

  1267 	       ([3], Pbl),

  1268 	       ([3, 1], Frm), ([3, 1], Res)] then () else

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

  1271 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else

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

  1274 "---(6) on S(606)..S(608)--------";

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

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

  1277 (*default_print_depth 99;*)

  1278 cuts;

  1279 (*default_print_depth 3;*)

  1280 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else

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

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

  1283 (*default_print_depth 99;*)

  1284 afterins;

  1285 (*default_print_depth 3;*)

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

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

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

  1289 	       ([2], Res),

  1290 	       ([3], Pbl),

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

  1292 then () else

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

  1295 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else

  1296 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";

  1298 "---(6++) on S(606)..S(608)--------";

  1299 (**)

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

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

  1302 (*default_print_depth 99;*)

  1303 cuts;

  1304 (*default_print_depth 1;*)

  1305 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)]

  1306 then () else

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

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

  1309 (*default_print_depth 99;*)

  1310 afterins;

  1311 (*default_print_depth 3;*)

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

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

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

  1315 	       ([2], Res),

  1316 	       ([3], Pbl),

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

  1318 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1319 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

  1320 if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else

  1321 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";

  1322 (*

  1323 show_pt pt';

  1324 show_pt pt;

  1325 *)

  1326 ========== inhibit exn AK110726 ==============================================*)

  1327 "-------------- repl_app------------------------------------------";

  1328 "-------------- repl_app------------------------------------------";

  1329 "-------------- repl_app------------------------------------------";

  1330 (*

  1331 > repl [1,2,3] 2 22222;

  1332 val it = [1,22222,3] : int list

  1333 > repl_app [1,2,3,4] 5 5555;

  1334 val it = [1,2,3,4,5555] : int list

  1335 > repl_app [1,2,3] 2 22222;

  1336 val it = [1,22222,3] : int list

  1337 > repl_app [1] 2 22222 ;

  1338 val it = [1,22222] : int list

  1339 *)

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 23 Mar 2020 17:51:35 +0100
changeset 59835	df00a2b5c4cc
parent 59821	09ba73ae512d
child 59841	aeeec4898fd1
permissions	-rw-r--r--