test/Tools/isac/MathEngBasic/ctree.sml
author Walther Neuper <walther.neuper@jku.at>
Wed, 22 Apr 2020 11:23:30 +0200
changeset 59902 e7910a62eaf2
parent 59898 68883c046963
child 59903 5037ca1b112b
permissions -rw-r--r--
rename file according to struct.; start renaming with "Spec"
     1 (* tests for sml/ME/ctree.sml
     2    authors: Walther Neuper 060113
     3    (c) due to copyright terms
     4 
     5 use"../smltest/ME/ctree.sml";
     6 use"ctree.sml";
     7 *)
     8 
     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 "-----------------------------------------------------------------";
    52 
    53 
    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";
    67 
    68 val pt = EmptyPtree;
    69 val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.Spec.empty, TermC.empty, ContextC.empty) pt;
    70 val ctxt = get_obj g_ctxt pt [];
    71 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
    72 
    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);
    98 
    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] (Istate.empty, ContextC.empty) (str2term "Inform[1]");
   105 "----------------------------------------------------------------/";
   106 
   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]*);
   111 
   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"])*)
   120 
   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" 
   132 
   133  show_pt pt;
   134 
   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";
   151 
   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";
   163 
   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";
   173 
   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";
   182 
   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";
   188 
   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";
   196 
   197 
   198 
   199 
   200 
   201 
   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*)
   208 
   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 = TermC.empty 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*);
   222 
   223 val (res,asm) = get_obj g_result pt' [];
   224 
   225 (*============ inhibit exn AK110726 ==============================================
   226 if UnparseC.term res = "[x = 1]" (*WN050219 TermC.empty 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),(*, TermC.empty in cut_tree!!!*)
   235     ([], Res)] then () else 
   236 error "ctree.sml: diff:behav. in cut_level 1b";
   237 ============ inhibit exn AK110726 ==============================================*)
   238 
   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";
   247 
   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";
   250 
   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";
   256 
   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";
   262 
   263 
   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*)
   268 
   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";
   279 
   280 val (res,asm) = get_obj g_result pt' [2];
   281 ============ inhibit exn AK110726 ==============================================*)
   282 
   283 if res = TermC.empty (*WN050219 done by cut_level*) then () else
   284 error "ctree.sml: diff:behav. in cut_tree 1aa";
   285 
   286 (*============ inhibit exn AK110726 ==============================================
   287 val form = get_obj g_form pt' [2];
   288 if UnparseC.term 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]);*)
   296 
   297 val (res,asm) = get_obj g_result pt' [];
   298 if res = TermC.empty (*WN050219 done by cut_tree*) then () else
   299 error "ctree.sml: diff:behav. in cut_tree 1ac";
   300 
   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";
   306 
   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 ==============================================*)
   318 
   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 ==============================================*)
   328 
   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";
   335 
   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;
   353 
   354 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
   355 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
   356 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
   357 
   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";
   361 
   362 val (pt', cuts) = cut_tree pt ([1],Frm);
   363 if cuts = []
   364 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
   365 
   366 (*WN050219
   367 val pos as ([p],_) = ([1],Frm);
   368 val pt as Nd (b,_) = pt;
   369 
   370 
   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 ####################################################################*)
   376 
   377 
   378 
   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; 
   388 
   389  interSteps 1 ([3,2],Res);
   390 
   391  val ((pt,_),_) = get_calc 1;
   392  show_pt pt;
   393 
   394 if (UnparseC.term o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
   395 else error "mini-subpbl interSteps broken";
   396 
   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";
   408 
   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";
   415 
   416 
   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] Istate.empty (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 UnparseC.term (get_obj g_form pt' [3,2,1]) = "newnew" andalso
   429    get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
   430    UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
   431  then () else error "ctree.sml: diff:behav. in cappend 1";
   432 
   433 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (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";
   442 
   443 
   444 
   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"])*)
   469 
   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) Istate.empty (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 UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty 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";
   479 
   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) Istate.empty (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 UnparseC.term form = "x + 1 = 2" andalso UnparseC.term 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";
   491 
   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) Istate.empty (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 UnparseC.term form = "x + 1 + -1 * 2 = 0" andalso UnparseC.term 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";
   503 
   504 
   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) Istate.empty e_fmz ([],Spec.empty,TermC.empty, ContextC.empty);
   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";
   512 
   513 (* ...complete calchead skipped...*)
   514 
   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) Istate.empty (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 UnparseC.term form = "-1 + x = 0" andalso res = TermC.empty 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";
   524 
   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) Istate.empty (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 UnparseC.term form = "-1 + x = 0" andalso UnparseC.term 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";
   536 
   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 =[]*);
   543 
   544 WN050225 intermed. outcommented---*)
   545 
   546 "=====new ctree 3 ================================================";
   547 "=====new ctree 3 ================================================";
   548 "=====new ctree 3 ================================================";
   549 
   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; 
   556 
   557  val ((pt,_),_) = get_calc 1;
   558  show_pt pt;
   559 
   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 (* UnparseC.term (get_obj g_res pt [3]);
   572    UnparseC.term (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*)
   579 
   580 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
   581 
   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);
   595 
   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>*)
   601 
   602  autoCalculate 1 (Steps 1);
   603  refFormula 1 (get_pos 1 1);
   604 
   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>*)
   609 
   610 
   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*)
   626 
   627 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
   628 
   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> *);
   643 
   644  interSteps 1 ([2],Res);
   645 
   646  val ((pt,_),_) = get_calc 1; show_pt pt;
   647  val p = get_pos 1 1;
   648 
   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";
   660 
   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"*);
   678 
   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 *)
   687 
   688 "-------------- move_dn in Incomplete ctree ----------------------";
   689 "-------------- move_dn in Incomplete ctree ----------------------";
   690 "-------------- move_dn in Incomplete ctree ----------------------";
   691 
   692 
   693 
   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; 
   704 
   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*)
   711 
   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_=*);
   717 
   718 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
   719 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
   720 
   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*)
   725 
   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);
   734 
   735 
   736 "-------------- get_interval from ctree: incremental development--";
   737 "-------------- get_interval from ctree: incremental development--";
   738 "-------------- get_interval from ctree: incremental development--";
   739 "--- level 1: get pos from start b to end p ----------------------";
   740 "--- level 1: get pos from start b to end p ----------------------";
   741 "--- level 1: get pos from start b to end p ----------------------";
   742 (******************************************************************)
   743 (**)            val SAVE_get_trace = get_trace;                 (**)
   744 (******************************************************************)
   745 (*'getnds' below is structured as such:*)
   746 fun www _ [x] = "l+r-margin"
   747   | www true [x1,x2] = "l-margin,  r-margin"
   748   | www _ [x1,x2] = "intern,  r-margin"
   749   | www true (x::(xs as _::_)) = "l-margin  " ^ www false xs
   750   | www _ (x::(xs as _::_)) = "intern  " ^ www false xs;
   751 www true [1,2,3,4,5];
   752 (*val it = "from  intern  intern  intern  to" : string*)
   753 www true [1,2];
   754 (*val it = "from  to" : string*)
   755 www true [1];
   756 (*val it = "from+to" : string*)
   757 
   758 local
   759 (*specific values of hd of pos p,q for simple handling take_fromto,
   760   from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
   761   ... can be used even for positions _below_ p or q*)
   762 fun hdp [] = 1     | hdp [0] = 1     | hdp x = hd x;(*start with first*)
   763 fun hdq	[] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
   764 (*analoguous for tl*)
   765 fun tlp [] = [0]     | tlp [_] = [0]     | tlp x = tl x;
   766 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
   767 
   768 (*see modspec.sml#pt_form
   769 fun pt_form (PrfObj {form,...}) = UnparseC.term form
   770   | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
   771     let val (dI, pI, _) = get_somespec' spec spec'
   772 	val {cas,...} = get_pbt pI
   773     in case cas of
   774 	   NONE => UnparseC.term (pblterm dI pI)
   775 	 | SOME t => UnparseC.term (subst_atomic (mk_env probl) t)
   776     end;
   777 *)
   778 (*.get an 'interval' from ctree down to a certain level
   779    by 'take_fromto children' of the nodes with specific 'from' and 'to';
   780    'i > 0' suppresses output during recursive descent towards 'from'
   781    b: the 'from' incremented to the actual pos
   782    p,q: specific 'from','to' for simple use of 'take_fromto'*)
   783 fun getnd i (b,p) q (Nd (po, nds)) =
   784     (if  i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
   785  
   786     @ (writeln("getnd  : b="^(ints2str' b)^", p="^
   787 	       (ints2str' p)^", q="^(ints2str' q));
   788 
   789        getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
   790 	       (take_fromto (hdp p) (hdq q) nds))
   791 
   792 and getnds _ _ _ _ [] = []                         (*no children*)
   793   | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
   794   | getnds i true (b,p) q [n1, n2] =               (*l-margin,  r-margin*)
   795     (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
   796 	     ", q="^ ints2str' q);
   797     (getnd i      (       b, p ) [99999] n1) @
   798     (getnd ~99999 (lev_on b,[0]) q       n2))
   799   | getnds i _    (b,p) q [n1, n2] =               (*intern,  r-margin*)
   800     (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
   801 	     ", q="^ ints2str' q);
   802     (getnd i      (       b,[0]) [99999] n1) @
   803     (getnd ~99999 (lev_on b,[0]) q       n2))
   804   | getnds i true (b,p) q (nd::(nds as _::_)) =    (*l-margin, intern*)
   805     (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
   806 	     ", q="^ ints2str' q);
   807     (getnd i             (       b, p ) [99999] nd) @
   808     (getnds ~99999 false (lev_on b,[0]) q nds)) 
   809   | getnds i _ (b,p) q (nd::(nds as _::_)) =       (*intern, ...*)
   810     (getnd i             (       b,[0]) [99999] nd) @
   811     (getnds ~99999 false (lev_on b,[0]) q nds); 
   812 in
   813 (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
   814   where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
   815 (1) the 'f' are given 
   816 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
   817 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
   818 (2) the 't' ar given
   819 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
   820 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
   821 the 'f' and 't' are set by hdp,... *)
   822 fun get_trace pt p q =
   823     (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) 
   824 	(take_fromto (hdp p) (hdq q) (children pt));
   825 end;
   826 
   827 writeln(pr_ctree pr_short pt);
   828 
   829 case get_trace pt [1,3] [4,1,1] of
   830     [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => () 
   831   | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
   832 case get_trace pt [2] [4,3,2] of
   833     [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
   834   | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
   835 case get_trace pt [1,4] [4,3,1] of
   836     [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => () 
   837   | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
   838 
   839 
   840 (*========== inhibit exn AK110719 ==============================================
   841 case get_trace pt [4,2] [5] of
   842    (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
   843     ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
   844     [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
   845   | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
   846 ========== inhibit exn AK110719 ==============================================*)
   847 
   848 case get_trace pt [] [4,4,2] of
   849     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
   850      [4,3],[4,3,1],[4,3,2]] => () 
   851   | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
   852 
   853 (*========== inhibit exn AK110719 ==============================================
   854 case get_trace pt [] [] of
   855     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
   856      [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => () 
   857   | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
   858 case get_trace pt [4,3] [4,3] of
   859     [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => () 
   860   | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
   861 ========== inhibit exn AK110719 ==============================================*)
   862 
   863 "--- level 2: get pos' from start b to end p ---------------------";
   864 "--- level 2: get pos' from start b to end p ---------------------";
   865 "--- level 2: get pos' from start b to end p ---------------------";
   866 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
   867   development stopped in favour of move_dn, see get_interval
   868   actually used (inefficient) version with move_dn: see modspec.sml
   869 *)
   870 (*
   871 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
   872     [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => () 
   873   | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
   874 case get_trace pt ([],Pbl) ([],Res) of
   875     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
   876      [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => () 
   877   | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
   878 *)
   879 
   880 (******************************************************************)
   881 (**)            val get_trace = SAVE_get_trace;                 (**)
   882 (******************************************************************)
   883 
   884 "-------------- pt_extract form, tac, asm<>[] --------------------";
   885 "-------------- pt_extract form, tac, asm<>[] --------------------";
   886 "-------------- pt_extract form, tac, asm<>[] --------------------";
   887 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
   888 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   889     ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
   890      Subproblem
   891          ("PolyEq",
   892           ["normalise", "polynomial", "univariate", "equation"]),
   893 	 ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]) => ()
   894   | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
   895 (*WN060717 unintentionally changed some rls/ord while 
   896      completing knowl. for thes2file...
   897 
   898   case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   899     ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
   900      *)Subproblem
   901          ("PolyEq",
   902           ["normalise", "polynomial", "univariate", "equation"]),
   903 	 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
   904   | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
   905 
   906 .... but it became even better*)
   907 
   908 
   909 
   910 "=====new ctree 5 minisubpbl =====================================";
   911 "=====new ctree 5 minisubpbl =====================================";
   912 "=====new ctree 5 minisubpbl =====================================";
   913 reset_states ();
   914 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
   915    ("Test", ["sqroot-test","univariate","equation","test"],
   916     ["Test","squ-equ-test-subpbl1"]))];
   917 Iterator 1; moveActiveRoot 1;
   918 autoCalculate 1 CompleteCalc; 
   919 val ((pt,_),_) = get_calc 1;
   920 show_pt pt;
   921 
   922 "-------------- pt_extract form, tac, asm ------------------------";
   923 "-------------- pt_extract form, tac, asm ------------------------";
   924 "-------------- pt_extract form, tac, asm ------------------------";
   925 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
   926 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   927     ("solve (x + 1 = 2, x)", 
   928     Apply_Method ["Test", "squ-equ-test-subpbl1"],
   929      []) => ()
   930   | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
   931 
   932 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
   933 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   934     ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
   935   | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
   936 
   937 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
   938 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   939     ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
   940   | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
   941 
   942 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
   943 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   944     ("-1 + x = 0",
   945      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
   946      []) => ()
   947   | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
   948 
   949 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
   950 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   951     ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
   952   | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
   953 
   954 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
   955 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   956     ("-1 + x = 0", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), []) => ()
   957   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
   958 
   959 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
   960 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   961     ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
   962   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
   963 
   964 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
   965 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   966     ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"], 
   967      []) => ()
   968   | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
   969 
   970 (*========== inhibit exn AK110719 ==============================================
   971 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
   972 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   973     ("[x = 1]", Check_elementwise "Assumptions", []) => ()
   974   | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
   975 
   976 val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
   977 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   978     ("[x = 1]",
   979      Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
   980      []) => ()
   981   | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
   982 
   983 val (Form form, tac, asm) = pt_extract (pt, ([], Res));
   984 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
   985     ("[x = 1]", NONE, []) => ()
   986   | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
   987 ========== inhibit exn AK110719 ==============================================*)
   988 
   989 "=====new ctree 6 minisubpbl intersteps ==========================";
   990 "=====new ctree 6 minisubpbl intersteps ==========================";
   991 "=====new ctree 6 minisubpbl intersteps ==========================";
   992 reset_states ();
   993 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
   994    ("Test", ["sqroot-test","univariate","equation","test"],
   995     ["Test","squ-equ-test-subpbl1"]))];
   996 Iterator 1; moveActiveRoot 1;
   997 autoCalculate 1 CompleteCalc;
   998 interSteps 1 ([2],Res);
   999 interSteps 1 ([3,2],Res);
  1000 val ((pt,_),_) = get_calc 1;
  1001 show_pt pt;
  1002 
  1003 (**##############################################################**)
  1004 "-------------- get_allpos' new ----------------------------------";
  1005 "-------------- get_allpos' new ----------------------------------";
  1006 "-------------- get_allpos' new ----------------------------------";
  1007 "--- whole ctree";
  1008 (*default_print_depth 99;*)
  1009 val cuts = get_allp [] ([], ([],Frm)) pt;
  1010 (*default_print_depth 3;*)
  1011 if cuts = 
  1012    [(*never returns the first pos'*)
  1013     ([1], Frm), 
  1014     ([1], Res), 
  1015     ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), 
  1016     ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1017     ([2], Res),
  1018     ([3], Pbl), 
  1019     ([3, 1], Frm), ([3, 1], Res), 
  1020     ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1021     ([3, 2], Res), 
  1022     ([3], Res),
  1023     ([4], Res), 
  1024     ([], Res)] then () else
  1025 error "ctree.sml diff.behav. get_allp new []";
  1026 
  1027 (*default_print_depth 99;*)
  1028 val cuts2 = get_allps [] [1] (children pt);
  1029 (*default_print_depth 3;*)
  1030 if cuts = cuts2 @ [([], Res)] then () else
  1031 error "ctree.sml diff.behav. get_allps new []";
  1032 
  1033 "---(3) on S(606)..S(608)--------";
  1034 "--- nd [2] with 6 children---------------------------------";
  1035 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
  1036 if cuts = 
  1037    [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  1038     ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1039     ([2], Res)] then () else
  1040 error "ctree.sml diff.behav. get_allp new [2]";
  1041 
  1042 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
  1043 if cuts = cuts2 @ [([2], Res)] then () else
  1044 error "ctree.sml diff.behav. get_allps new [2]";
  1045 
  1046 
  1047 "---(4) on S(606)..S(608)--------";
  1048 "--- nd [3] subproblem--------------------------------------";
  1049 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
  1050 if cuts = 
  1051    [([3, 1], Frm), 
  1052     ([3, 1], Res), 
  1053     ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1054     ([3, 2], Res), 
  1055     ([3], Res)] then () else
  1056 error "ctree.sml diff.behav. get_allp new [3]";
  1057 
  1058 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
  1059 if cuts = cuts2 @ [([3], Res)] then () else
  1060 error "ctree.sml diff.behav. get_allps new [3]";
  1061 
  1062 "--- nd [3,2] with 2 children--------------------------------";
  1063 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
  1064 if cuts = 
  1065    [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1066     ([3, 2], Res)] then () else
  1067 error "ctree.sml diff.behav. get_allp new [3,2]";
  1068 
  1069 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
  1070 if cuts = cuts2 @ [([3, 2], Res)] then () else
  1071 error "ctree.sml diff.behav. get_allps new [3,2]";
  1072 
  1073 "---(5a) on S(606)..S(608)--------";
  1074 "--- nd [3,2,1] with 0 children------------------------------";
  1075 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
  1076 if cuts = 
  1077    [] then () else
  1078 error "ctree.sml diff.behav. get_allp new [3,2,1]";
  1079 
  1080 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
  1081 if cuts = cuts2 @ [] then () else
  1082 error "ctree.sml diff.behav. get_allps new [3,2,1]";
  1083 
  1084 
  1085 (**#################################################################**)
  1086 "-------------- cut_tree new (from ctree above)-------------------";
  1087 "-------------- cut_tree new (from ctree above)-------------------";
  1088 "-------------- cut_tree new (from ctree above)-------------------";
  1089 show_pt pt;
  1090 val b = get_obj g_branch pt [];
  1091 if b = TransitiveB then () else
  1092 error ("ctree.sml diff.behav. in [] branch="^branch2str b);
  1093 val b = get_obj g_branch pt [3];
  1094 if b = TransitiveB then () else
  1095 error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
  1096 
  1097 "---(2) on S(606)..S(608)--------";
  1098 val (pt', cuts) = cut_tree pt ([1],Res);
  1099 (*default_print_depth 99;*)
  1100 cuts;
  1101 (*default_print_depth 3;*)
  1102 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  1103       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
  1104       ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
  1105       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
  1106       ([], Res)] then () else 
  1107 error "ctree.sml: diff.behav. cut_tree ([1],Res)";
  1108 
  1109 
  1110 "---(3) on S(606)..S(608)--------";
  1111 val (pt', cuts) = cut_tree pt ([2],Res);
  1112 (*default_print_depth 99;*)
  1113 cuts;
  1114 (*default_print_depth 3;*)
  1115 if cuts = [(*preceding step on WS was ([1]),Res*)
  1116 	   ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  1117 	   ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1118 	   ([2], Res),
  1119 	   ([3], Pbl), 
  1120 	   ([3, 1], Frm),
  1121 	   ([3, 1], Res), 
  1122 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
  1123 	   ([3, 2], Res), 
  1124 	   ([3], Res), 
  1125 	   ([4], Res),
  1126 	   ([],Res)] then () 
  1127 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
  1128 
  1129 "---(4) on S(606)..S(608)--------";
  1130 val (pt', cuts) = cut_tree pt ([3],Pbl);
  1131 (*default_print_depth 99;*)
  1132 cuts;
  1133 (*default_print_depth 3;*)
  1134 if cuts = [([3], Pbl),
  1135 	   ([3, 1], Frm), ([3, 1], Res), 
  1136 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1137 	   ([3, 2], Res), 
  1138 	   ([3], Res), 
  1139 	   ([4], Res),
  1140 	   ([], Res)] 
  1141 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
  1142 
  1143 "---(5a) on S(606)..S(608) cut_tree --------";
  1144 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
  1145 (*default_print_depth 99;*)
  1146 cuts;
  1147 (*default_print_depth 1;*)
  1148 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then () 
  1149 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
  1150 show_pt pt';
  1151 
  1152 
  1153 "-------------- cappend on complete ctree from above -------------";
  1154 "-------------- cappend on complete ctree from above -------------";
  1155 "-------------- cappend on complete ctree from above -------------";
  1156 show_pt pt;
  1157 
  1158 "---(2) on S(606)..S(608)--------";
  1159 (*========== inhibit exn AK110726 ==============================================
  1160 (* ERROR: Can't unify istate to istate * Proof.context *)
  1161 val (pt', cuts) = cappend_atomic pt [1] Istate.empty (str2term "Inform[1]")
  1162     (Tac "test") (str2term "Inres[1]",[]) Complete;
  1163 
  1164 (*default_print_depth 99;*)
  1165 cuts;
  1166 (*default_print_depth 3;*)
  1167 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  1168       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
  1169       ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
  1170       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
  1171 	    ([], Res)] then ()
  1172 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
  1173 
  1174 val afterins = get_allp [] ([], ([],Frm)) pt';
  1175 (*default_print_depth 99;*)
  1176 afterins;
  1177 (*default_print_depth 3;*)
  1178 if afterins = [([1], Frm), ([1], Res)] then()
  1179 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
  1180 show_pt pt';
  1181 "---(3) on S(606)..S(608)--------";
  1182 show_pt pt;
  1183 val (pt', cuts) = cappend_atomic pt [2] Istate.empty (str2term "Inform[2]")
  1184     (Tac "test") (str2term "Inres[2]",[]) Complete;
  1185 (*default_print_depth 99;*)
  1186 cuts;
  1187 (*default_print_depth 3;*)
  1188 
  1189 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  1190       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl), 
  1191       ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), 
  1192       ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
  1193 	    ([], Res)] then () 
  1194 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
  1195 
  1196 
  1197 val afterins = get_allp [] ([], ([],Frm)) pt';
  1198 (*default_print_depth 99;*)
  1199 afterins;
  1200 (*default_print_depth 3;*)
  1201 
  1202 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)] 
  1203 then () else
  1204 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
  1205 show_pt pt';
  1206 
  1207 
  1208 (*
  1209  val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
  1210  val p = move_dn [] pt' p        (*-> ([1],Res)*);
  1211  val p = move_dn [] pt' p        (*-> ([2],Frm)*);
  1212  val p = move_dn [] pt' p        (*-> ([2],Res)*);
  1213 
  1214  UnparseC.term (get_obj g_form pt' [2]);
  1215  UnparseC.term (get_obj g_res pt' [2]);
  1216  ostate2str (get_obj g_ostate pt' [2]);
  1217  *)
  1218 
  1219 "---(4) on S(606)..S(608)--------";
  1220 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],Spec.empty)
  1221 				  ([],Spec.empty, str2term "Inhead[3]", ContextC.empty);
  1222 (*default_print_depth 99;*)
  1223 cuts;
  1224 (*default_print_depth 3;*)
  1225 if cuts = [([3], Pbl),
  1226 	   ([3, 1], Frm), ([3, 1], Res), 
  1227 	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1228 	   ([3, 2], Res), 
  1229 	   ([3], Res), ([4], Res),
  1230 	   ([], Res)] then ()else
  1231 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
  1232 val afterins = get_allp [] ([], ([],Frm)) pt';
  1233 (*default_print_depth 99;*)
  1234 afterins;
  1235 (*default_print_depth 3;*)
  1236 if afterins = 
  1237    [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  1238     ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
  1239     ([3], Pbl)] then () else
  1240 error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
  1241 (* use"systest/ctree.sml";
  1242    use"ctree.sml";
  1243    *)
  1244 
  1245 "---(6-1) on S(606)..S(608)--------";
  1246 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (str2term "Inform[3,1]")
  1247     (Tac "test") (str2term "Inres[3,1]",[]) Complete;
  1248 (*default_print_depth 99;*)
  1249 cuts;
  1250 (*default_print_depth 3;*)
  1251 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  1252 	   ([3, 2], Res),
  1253 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
  1254 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
  1255 
  1256 val afterins = get_allp [] ([], ([],Frm)) pt';
  1257 (*default_print_depth 99;*)
  1258 afterins;
  1259 (*default_print_depth 3;*)
  1260 if afterins = [([1], Frm), ([1], Res), 
  1261 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  1262 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1263 	       ([2], Res),
  1264 	       ([3], Pbl), 
  1265 	       ([3, 1], Frm), ([3, 1], Res)] then () else
  1266 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
  1267 
  1268 if UnparseC.term (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
  1269 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
  1270 
  1271 "---(6) on S(606)..S(608)--------";
  1272 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (str2term "Inform[3,2]")
  1273     (Tac "test") (str2term "Inres[3,2]",[]) Complete;
  1274 (*default_print_depth 99;*)
  1275 cuts;
  1276 (*default_print_depth 3;*)
  1277 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else
  1278 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
  1279 val afterins = get_allp [] ([], ([],Frm)) pt';
  1280 (*default_print_depth 99;*)
  1281 afterins;
  1282 (*default_print_depth 3;*)
  1283 if afterins = [([1], Frm), ([1], Res), 
  1284 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  1285 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1286 	       ([2], Res),
  1287 	       ([3], Pbl), 
  1288 	       ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
  1289 then () else
  1290 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
  1291 
  1292 if UnparseC.term (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
  1293 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
  1294 
  1295 "---(6++) on S(606)..S(608)--------";
  1296 (**)
  1297 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (str2term "Inform[3,2,1]")
  1298     (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
  1299 (*default_print_depth 99;*)
  1300 cuts;
  1301 (*default_print_depth 1;*)
  1302 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] 
  1303 then () else
  1304 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
  1305 val afterins = get_allp [] ([], ([],Frm)) pt';
  1306 (*default_print_depth 99;*)
  1307 afterins;
  1308 (*default_print_depth 3;*)
  1309 if afterins = [([1], Frm), ([1], Res), 
  1310 	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  1311 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
  1312 	       ([2], Res),
  1313 	       ([3], Pbl), 
  1314 	       ([3, 1], Frm), ([3, 1], Res), 
  1315 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
  1316 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
  1317 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
  1318 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
  1319 (*
  1320 show_pt pt';
  1321 show_pt pt;
  1322 *)
  1323 ========== inhibit exn AK110726 ==============================================*)
  1324 "-------------- repl_app------------------------------------------";
  1325 "-------------- repl_app------------------------------------------";
  1326 "-------------- repl_app------------------------------------------";
  1327 (*  
  1328 > repl [1,2,3] 2 22222;
  1329 val it = [1,22222,3] : int list
  1330 > repl_app [1,2,3,4] 5 5555;
  1331 val it = [1,2,3,4,5555] : int list
  1332 > repl_app [1,2,3] 2 22222;
  1333 val it = [1,22222,3] : int list
  1334 > repl_app [1] 2 22222 ;
  1335 val it = [1,22222] : int list
  1336 *)