wneuper/isa: test/Tools/isac/Interpret/ctree.sml@22c5483e9bfb

     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 "-------------- check positions in miniscript --------------------";

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

    15 (**#####################################################################(**)

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

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

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

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

    20 (**)#####################################################################**)

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

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

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

    24 "-------------- cappend minisubpbl -------------------------------";

    26 "=====new ptree 3 ================================================";

    27 "-------------- move_dn ------------------------------------------";

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

    29 "-------------- move_up ------------------------------------------";

    30 "------ move into detail -----------------------------------------";

    31 "=====new ptree 3a ===============================================";

    32 "-------------- move_dn in Incomplete ctree ----------------------";

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

    35 (*############## development stopped 0501 ########################*)

    36 (******************************************************************)

    37 (*              val SAVE_get_trace = get_trace;                   *)

    38 (******************************************************************)

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

    40 (******************************************************************)

    41 (*              val get_trace = SAVE_get_trace;                   *)

    42 (******************************************************************)

    43 (*############## development stopped 0501 ########################*)

    45 "=====new ptree 4 ratequation ====================================";

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

    47 "=====new ptree 5 minisubpbl =====================================";

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

    50 (**#####################################################################(**)

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

    52 "-------------- get_allpos' new ----------------------------------";

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

    54 (**)#####################################################################**)

    56 "-----------------------------------------------------------------";

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

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

    61 "-------------- check positions in miniscript --------------------";

    62 "-------------- check positions in miniscript --------------------";

    63 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

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

    73    *)

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

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

    76    *)

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

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

    79    *)

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

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

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

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

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

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

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

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

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

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

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

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

    93 "----------------------------------------------------------------/";

    94 (*========== inhibit exn WN110319 ==============================================

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   119  show_pt pt;

   120 ============ inhibit exn WN110319 ============================================*)

   122 (*=== inhibit exn ?=============================================================

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

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

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

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

   128    [([], Frm),

   129     ([1], Frm),

   130     ([1], Res),

   131     ([2], Res),

   132     ([3], Frm),

   133     ([3, 1], Frm),

   134     ([3, 1], Res),

   135     ([3, 2], Res),

   136     ([3], Res),

   137     ([4], Res),

   138     ([], Res)]

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

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

   142    [([1], Frm),

   143     ([1], Res),

   144     ([2], Res),

   145     ([3], Frm),

   146     ([3, 1], Frm),

   147     ([3, 1], Res),

   148     ([3, 2], Res),

   149     ([3], Res),

   150     ([4], Res)]

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

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

   154    [([2], Res),

   155     ([3], Frm),

   156     ([3, 1], Frm),

   157     ([3, 1], Res),

   158     ([3, 2], Res),

   159     ([3], Res),

   160     ([4], Res)]

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

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

   164    [([3], Frm),

   165     ([3, 1], Frm),

   166     ([3, 1], Res),

   167     ([3, 2], Res),

   168     ([3], Res),

   169     ([4], Res)]

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

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

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

   174     ([3, 1], Res),

   175     ([3, 2], Res)]

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

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

   179    [([3], Frm),

   180     ([3, 1], Frm),

   181     ([3, 1], Res),

   182     ([3, 2], Res),

   183     ([3], Res)]

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

   187 (**##############################################################(**)

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

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

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

   192 show_pt pt;

   193 show_pt pt';

   194 print_depth 99; cuts; print_depth 3;

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

   197 	   ([3], Frm),

   198 	   ([3, 1], Frm),

   199 	   ([3, 1], Res),

   200 	   ([3, 2], Res),

   201 	   ([3], Res),

   202 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

   214    [([], Frm),

   215     ([1], Frm),

   216     ([1], Res),

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

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

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

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

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

   224 	   ([3, 1], Frm),

   225 	   ([3, 1], Res),

   226 	   ([3, 2], Res),

   227 	   ([3], Res),

   228 	   ([4], Res)]

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

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

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

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

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

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

   237 if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"

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

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

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

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

   243 if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"

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

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

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

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

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

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

   252 	   ([3], Frm),

   253 	   ([3, 1], Frm),

   254 	   ([3, 1], Res),

   255 	   ([3, 2], Res),

   256 	   ([3], Res),

   257 	   ([4], Res),

   258 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

   274    [([], Frm),

   275     ([1], Frm),

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

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

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

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

   281 	   ([3, 1], Frm),

   282 	   ([3, 1], Res),

   283 	   ([3, 2], Res),

   284 	   ([3], Res),

   285 	   ([4], Res),

   286 	   ([], Res)]

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

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

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

   291 	   ([3, 2], Res),

   292 	   ([3], Res),

   293 	   ([4], Res),

   294 	   ([], Res)]

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

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

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

   299 	   ([3], Res),

   300 	   ([4], Res),

   301 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   321 show_pt pt;

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

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

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

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

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

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

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

   332 if cuts = []

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

   335 (*WN050219

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

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

   340 show_pt pt;

   341 show_pt pt';

   342 print_depth 99;cuts;print_depth 3;

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

   344 ####################################################################*)*)

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

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

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

   349  states:=[];

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

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

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

   353  Iterator 1; moveActiveRoot 1;

   354  autoCalculate 1 CompleteCalc;

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

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

   359  show_pt pt;

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

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

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

   364 (*WN050225 intermed. outcommented

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

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

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

   368 	    ([3, 2], Res),

   369 	    ([3], Res),

   370 	    ([4], Res)]

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

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

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

   375 	    ([3, 2], Res),

   376 	    ([3], Res),

   377 	    ([4], Res)]

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

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

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

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

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

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

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

   387 	   ([3, 2], Res),

   388 	   ([3], Res),

   389 	   ([4], Res),

   390 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   401 	   ([3, 2], Res),

   402 	   ([3], Res),

   403 	   ([4], Res),

   404 	   ([], Res)]

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

   409 "-------------- cappend minisubpbl -------------------------------";

   410 "-------------- cappend minisubpbl -------------------------------";

   411 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   421    *)

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

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

   424    *)

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

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

   427    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   446 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   458 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   477 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   491 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   508 WN050225 intermed. outcommented---*)

   510 "=====new ptree 3 ================================================";

   511 "=====new ptree 3 ================================================";

   512 "=====new ptree 3 ================================================";

   513  states:=[];

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

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

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

   517  Iterator 1; moveActiveRoot 1;

   518  autoCalculate 1 CompleteCalc;

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

   521  show_pt pt;

   523 "-------------- move_dn ------------------------------------------";

   524 "-------------- move_dn ------------------------------------------";

   525 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   535    term2str (get_obj g_form pt [4]);

   536    *)

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

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

   539 (*

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

   541                                   Exception PTREE end of calculation*)

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

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

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

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

   548  states := [];

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

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

   551        ("Test",

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

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

   554  Iterator 1; moveActiveRoot 1;

   555  autoCalculate 1 CompleteCalcHead;

   556  autoCalculate 1 (Step 1);

   557  refFormula 1 (get_pos 1 1);

   559  moveActiveRoot 1;

   560  moveActiveDown 1;

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

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

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

   565  autoCalculate 1 (Step 1);

   566  refFormula 1 (get_pos 1 1);

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

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

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

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

   574 "-------------- move_up ------------------------------------------";

   575 "-------------- move_up ------------------------------------------";

   576 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   588                                   Exception PTREE begin of calculation*)

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

   592 "------ move into detail -----------------------------------------";

   593 "------ move into detail -----------------------------------------";

   594 "------ move into detail -----------------------------------------";

   595  states:=[];

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

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

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

   599  Iterator 1; moveActiveRoot 1;

   600  autoCalculate 1 CompleteCalc;

   601  moveActiveRoot 1;

   602  moveActiveDown 1;

   603  moveActiveDown 1;

   604  moveActiveDown 1;

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

   607  interSteps 1 ([2],Res);

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

   610  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   624 "=====new ptree 3a ===============================================";

   625 "=====new ptree 3a ===============================================";

   626 "=====new ptree 3a ===============================================";

   627  states:=[];

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

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

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

   631  Iterator 1; moveActiveRoot 1;

   632  autoCalculate 1 CompleteCalcHead;

   633  autoCalculate 1 (Step 1);

   634  autoCalculate 1 (Step 1);

   635  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   646 (*

   647  get_obj g_ostate pt [1];

   648  show_pt pt;

   649 *)

   651 "-------------- move_dn in Incomplete ctree ----------------------";

   652 "-------------- move_dn in Incomplete ctree ----------------------";

   653 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   660 states:=[];

   661 CalcTree

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

   663 	   "solveFor x","solutions L"],

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

   665 Iterator 1; moveActiveRoot 1;

   666 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   692 writeln(pr_ptree pr_short pt);

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

   694  ###########################################################################*)

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

   696 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   705 (******************************************************************)

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

   707 (******************************************************************)

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

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

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

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

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

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

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

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

   716 www true [1,2];

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

   718 www true [1];

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

   721 local

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

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

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

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

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

   727 (*analoguous for tl*)

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

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

   731 (*see modspec.sml#pt_form

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

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

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

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

   736     in case cas of

   737 	   NONE => term2str (pblterm dI pI)

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

   739     end;

   740 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   775 in

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

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

   778 (1) the 'f' are given

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

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

   781 (2) the 't' ar given

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

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

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

   785 fun get_trace pt p q =

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

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

   788 end;

   790 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   806     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   809 case get_trace pt [] [] of

   810     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

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

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

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

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

   821   development stopped in favour of move_dn, see get_interval

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

   823 *)

   824 (*

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

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

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

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

   829     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   832 *)

   834 (******************************************************************)

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

   836 (******************************************************************)

   839 "=====new ptree 4 ratequation ====================================";

   840 "=====new ptree 4 ratequation ====================================";

   841 "=====new ptree 4 ratequation ====================================";

   842 states:=[];

   843 CalcTree

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

   845 	   "solveFor x","solutions L"],

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

   847 Iterator 1; moveActiveRoot 1;

   848 autoCalculate 1 CompleteCalc;

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

   850 show_pt pt;

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

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

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

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

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

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

   859      Subproblem

   860          ("PolyEq",

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

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

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

   864 (*WN060717 unintentionally changed some rls/ord while

   865      completing knowl. for thes2file...

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

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

   869      *)Subproblem

   870          ("PolyEq",

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

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

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

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

   879 "=====new ptree 5 minisubpbl =====================================";

   880 "=====new ptree 5 minisubpbl =====================================";

   881 "=====new ptree 5 minisubpbl =====================================";

   882 states:=[];

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

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

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

   886 Iterator 1; moveActiveRoot 1;

   887 autoCalculate 1 CompleteCalc;

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

   889 show_pt pt;

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

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

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

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

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

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

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

   898      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   913     ("-1 + x = 0",

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

   915      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   936      []) => ()

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

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

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

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

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

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

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

   946     ("[x = 1]",

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

   948      []) => ()

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

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

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

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

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

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

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

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

   959 states:=[];

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

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

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

   963 Iterator 1; moveActiveRoot 1;

   964 autoCalculate 1 CompleteCalc;

   965 interSteps 1 ([2],Res);

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

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

   968 show_pt pt;

   970 (**##############################################################**)

   971 "-------------- get_allpos' new ----------------------------------";

   972 "-------------- get_allpos' new ----------------------------------";

   973 "-------------- get_allpos' new ----------------------------------";

   974 "--- whole ctree";

   975 print_depth 99;

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

   977 print_depth 3;

   978 if cuts =

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

   980     ([1], Frm),

   981     ([1], Res),

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

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

   984     ([2], Res),

   985     ([3], Pbl),

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

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

   988     ([3, 2], Res),

   989     ([3], Res),

   990     ([4], Res),

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

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

   994 print_depth 99;

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

   996 print_depth 3;

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

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

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

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

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

  1003 if cuts =

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

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

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

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

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

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

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

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

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

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

  1017 if cuts =

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

  1019     ([3, 1], Res),

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

  1021     ([3, 2], Res),

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

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

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

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

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

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

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

  1031 if cuts =

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

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

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

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

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

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

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

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

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

  1043 if cuts =

  1044    [] then () else

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

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

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

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

  1052 (**#################################################################**)

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

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

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

  1056 show_pt pt;

  1057 val b = get_obj g_branch pt [];

  1058 if b = TransitiveB then () else

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

  1060 val b = get_obj g_branch pt [3];

  1061 if b = TransitiveB then () else

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

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

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

  1066 print_depth 99;

  1067 cuts;

  1068 print_depth 3;

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

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

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

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

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

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

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

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

  1079 print_depth 99;

  1080 cuts;

  1081 print_depth 3;

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

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

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

  1085 	   ([2], Res),

  1086 	   ([3], Pbl),

  1087 	   ([3, 1], Frm),

  1088 	   ([3, 1], Res),

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

  1090 	   ([3, 2], Res),

  1091 	   ([3], Res),

  1092 	   ([4], Res),

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

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

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

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

  1098 print_depth 99;

  1099 cuts;

  1100 print_depth 3;

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

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

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

  1104 	   ([3, 2], Res),

  1105 	   ([3], Res),

  1106 	   ([4], Res),

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

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

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

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

  1112 print_depth 99;

  1113 cuts;

  1114 print_depth 1;

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

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

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

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

  1119 show_pt pt';

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

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

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

  1125 show_pt pt;

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

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

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

  1130 print_depth 99;

  1131 cuts;

  1132 print_depth 3;

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

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

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

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

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

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

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

  1140 print_depth 99;

  1141 afterins;

  1142 print_depth 3;

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

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

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

  1146 show_pt pt';

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

  1149 show_pt pt;

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

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

  1152 print_depth 99;

  1153 cuts;

  1154 print_depth 3;

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

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

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

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

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

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

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

  1162 print_depth 99;

  1163 afterins;

  1164 print_depth 3;

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

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

  1167 then () else

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

  1169 show_pt pt';

  1170 (*

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

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

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

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

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

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

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

  1179  *)

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

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

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

  1184 print_depth 99;

  1185 cuts;

  1186 print_depth 3;

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

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

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

  1190 	   ([3, 2], Res),

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

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

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

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

  1195 print_depth 99;

  1196 afterins;

  1197 print_depth 3;

  1198 if afterins =

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

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

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

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

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

  1204    use"ctree.sml";

  1205    *)

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

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

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

  1210 print_depth 99;

  1211 cuts;

  1212 print_depth 3;

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

  1214 	   ([3, 2], Res),

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

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

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

  1218 print_depth 99;

  1219 afterins;

  1220 print_depth 3;

  1221 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1225 	       ([2], Res),

  1226 	       ([3], Pbl),

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

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

  1229 	       ([4], Res),

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

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

  1232 *)

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

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

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

  1236 	       ([2], Res),

  1237 	       ([3], Pbl),

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

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

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

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

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

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

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

  1247 print_depth 99;

  1248 cuts;

  1249 print_depth 3;

  1250 if cuts = [(*just after is: cutlevup=false in [3]*)

  1251 (*WN060727 after test_trans instead cutlevup added:*)

  1252 	   ([3], Res), ([4], Res), ([], Res)] then () else

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

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

  1255 print_depth 99;

  1256 afterins;

  1257 print_depth 3;

  1258 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1262 	       ([2], Res),

  1263 	       ([3], Pbl),

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

  1265 	       ([3], Res),

  1266 	       ([4], Res), ([], Res)] then () else

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

  1268 *)

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

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

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

  1272 	       ([2], Res),

  1273 	       ([3], Pbl),

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

  1275 then () else

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

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

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

  1281 "---(6++) on S(606)..S(608)--------";

  1282 (**)

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

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

  1285 print_depth 99;

  1286 cuts;

  1287 print_depth 1;

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

  1289 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1290 then () else

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

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

  1293 print_depth 99;

  1294 afterins;

  1295 print_depth 3;

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

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

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

  1299 	       ([2], Res),

  1300 	       ([3], Pbl),

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

  1302 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1303 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1306 (*

  1307 show_pt pt';

  1308 show_pt pt;

  1309 *)

  1311 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 04 May 2011 09:01:10 +0200
branch	decompose-isar
changeset 41972	22c5483e9bfb
parent 41970	25957ffe68e8
child 41989	235f3990c9b7
permissions	-rw-r--r--