wneuper/isa: test/Tools/isac/Interpret/ctree.sml@1ada058e92bc

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

     2    authors: Walther Neuper 060113

     3    (c) due to copyright terms

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

     6 use"ctree.sml";

     7 *)

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

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

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

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

    13 "-------------- fun get_ctxt -------------------------------------";

    14 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    15 "-------------- check positions in miniscript --------------------";

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

    17 (**#####################################################################(**)

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

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

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

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

    22 (**)#####################################################################**)

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

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

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

    26 "-------------- cappend minisubpbl -------------------------------";

    28 "=====new ptree 3 ================================================";

    29 "-------------- move_dn ------------------------------------------";

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

    31 "-------------- move_up ------------------------------------------";

    32 "------ move into detail -----------------------------------------";

    33 "=====new ptree 3a ===============================================";

    34 "-------------- move_dn in Incomplete ctree ----------------------";

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

    37 (*############## development stopped 0501 ########################*)

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

    39 (*              val SAVE_get_trace = get_trace;                   *)

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

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

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

    43 (*              val get_trace = SAVE_get_trace;                   *)

    44 (******************************************************************)

    45 (*############## development stopped 0501 ########################*)

    47 "=====new ptree 4 ratequation ====================================";

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

    49 "=====new ptree 5 minisubpbl =====================================";

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

    52 (**#####################################################################(**)

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

    54 "-------------- get_allpos' new ----------------------------------";

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

    56 (**)#####################################################################**)

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

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

    60 "-----------------------------------------------------------------";

    63 "-------------- fun get_ctxt -------------------------------------";

    64 "-------------- fun get_ctxt -------------------------------------";

    65 "-------------- fun get_ctxt -------------------------------------";

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

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

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

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

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

    71 (get_ctxt pt p)

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

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

    74 (get_ctxt pt p)

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

    77 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    78 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    79 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    80 val pt = EmptyPtree;

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

    82 val ctxt = get_obj g_ctxt pt [];

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

    84 val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});

    85 if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"

    86 then () else error "--- fun update_ctxt, fun g_ctxt changed";

    88 "-------------- check positions in miniscript --------------------";

    89 "-------------- check positions in miniscript --------------------";

    90 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

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

   100    *)

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

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

   103    *)

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

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

   106    *)

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

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

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

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

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

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

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

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

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

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

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

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

   120 "----------------------------------------------------------------/";

   121 (*========== inhibit exn WN110319 ==============================================

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   146  show_pt pt;

   147 ============ inhibit exn WN110319 ============================================*)

   149 (*=== inhibit exn ?=============================================================

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

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

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

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

   155    [([], Frm),

   156     ([1], Frm),

   157     ([1], Res),

   158     ([2], Res),

   159     ([3], Frm),

   160     ([3, 1], Frm),

   161     ([3, 1], Res),

   162     ([3, 2], Res),

   163     ([3], Res),

   164     ([4], Res),

   165     ([], Res)]

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

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

   169    [([1], Frm),

   170     ([1], Res),

   171     ([2], Res),

   172     ([3], Frm),

   173     ([3, 1], Frm),

   174     ([3, 1], Res),

   175     ([3, 2], Res),

   176     ([3], Res),

   177     ([4], Res)]

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

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

   181    [([2], Res),

   182     ([3], Frm),

   183     ([3, 1], Frm),

   184     ([3, 1], Res),

   185     ([3, 2], Res),

   186     ([3], Res),

   187     ([4], Res)]

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

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

   191    [([3], Frm),

   192     ([3, 1], Frm),

   193     ([3, 1], Res),

   194     ([3, 2], Res),

   195     ([3], Res),

   196     ([4], Res)]

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

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

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

   201     ([3, 1], Res),

   202     ([3, 2], Res)]

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

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

   206    [([3], Frm),

   207     ([3, 1], Frm),

   208     ([3, 1], Res),

   209     ([3, 2], Res),

   210     ([3], Res)]

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

   214 (**##############################################################(**)

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

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

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

   219 show_pt pt;

   220 show_pt pt';

   221 print_depth 99; cuts; print_depth 3;

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

   224 	   ([3], Frm),

   225 	   ([3, 1], Frm),

   226 	   ([3, 1], Res),

   227 	   ([3, 2], Res),

   228 	   ([3], Res),

   229 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

   241    [([], Frm),

   242     ([1], Frm),

   243     ([1], Res),

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

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

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

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

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

   251 	   ([3, 1], Frm),

   252 	   ([3, 1], Res),

   253 	   ([3, 2], Res),

   254 	   ([3], Res),

   255 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   279 	   ([3], Frm),

   280 	   ([3, 1], Frm),

   281 	   ([3, 1], Res),

   282 	   ([3, 2], Res),

   283 	   ([3], Res),

   284 	   ([4], Res),

   285 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

   301    [([], Frm),

   302     ([1], Frm),

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

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

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

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

   308 	   ([3, 1], Frm),

   309 	   ([3, 1], Res),

   310 	   ([3, 2], Res),

   311 	   ([3], Res),

   312 	   ([4], Res),

   313 	   ([], Res)]

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

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

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

   318 	   ([3, 2], Res),

   319 	   ([3], Res),

   320 	   ([4], Res),

   321 	   ([], Res)]

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

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

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

   326 	   ([3], Res),

   327 	   ([4], Res),

   328 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

   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 show_pt pt;

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

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

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

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

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

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

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

   359 if cuts = []

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

   362 (*WN050219

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

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

   367 show_pt pt;

   368 show_pt pt';

   369 print_depth 99;cuts;print_depth 3;

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

   371 ####################################################################*)*)

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

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

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

   376  states:=[];

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

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

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

   380  Iterator 1; moveActiveRoot 1;

   381  autoCalculate 1 CompleteCalc;

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

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

   386  show_pt pt;

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

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

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

   391 (*WN050225 intermed. outcommented

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

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

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

   395 	    ([3, 2], Res),

   396 	    ([3], Res),

   397 	    ([4], Res)]

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

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

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

   402 	    ([3, 2], Res),

   403 	    ([3], Res),

   404 	    ([4], Res)]

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

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

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

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

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

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

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

   414 	   ([3, 2], Res),

   415 	   ([3], Res),

   416 	   ([4], Res),

   417 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   428 	   ([3, 2], Res),

   429 	   ([3], Res),

   430 	   ([4], Res),

   431 	   ([], Res)]

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

   436 "-------------- cappend minisubpbl -------------------------------";

   437 "-------------- cappend minisubpbl -------------------------------";

   438 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   448    *)

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

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

   451    *)

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

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

   454    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   473 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   485 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   504 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   518 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   535 WN050225 intermed. outcommented---*)

   537 "=====new ptree 3 ================================================";

   538 "=====new ptree 3 ================================================";

   539 "=====new ptree 3 ================================================";

   540  states:=[];

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

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

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

   544  Iterator 1; moveActiveRoot 1;

   545  autoCalculate 1 CompleteCalc;

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

   548  show_pt pt;

   550 "-------------- move_dn ------------------------------------------";

   551 "-------------- move_dn ------------------------------------------";

   552 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   562    term2str (get_obj g_form pt [4]);

   563    *)

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

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

   566 (*

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

   568                                   Exception PTREE end of calculation*)

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

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

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

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

   575  states := [];

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

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

   578        ("Test",

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

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

   581  Iterator 1; moveActiveRoot 1;

   582  autoCalculate 1 CompleteCalcHead;

   583  autoCalculate 1 (Step 1);

   584  refFormula 1 (get_pos 1 1);

   586  moveActiveRoot 1;

   587  moveActiveDown 1;

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

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

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

   592  autoCalculate 1 (Step 1);

   593  refFormula 1 (get_pos 1 1);

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

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

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

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

   601 "-------------- move_up ------------------------------------------";

   602 "-------------- move_up ------------------------------------------";

   603 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   615                                   Exception PTREE begin of calculation*)

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

   619 "------ move into detail -----------------------------------------";

   620 "------ move into detail -----------------------------------------";

   621 "------ move into detail -----------------------------------------";

   622  states:=[];

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

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

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

   626  Iterator 1; moveActiveRoot 1;

   627  autoCalculate 1 CompleteCalc;

   628  moveActiveRoot 1;

   629  moveActiveDown 1;

   630  moveActiveDown 1;

   631  moveActiveDown 1;

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

   634  interSteps 1 ([2],Res);

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

   637  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   651 "=====new ptree 3a ===============================================";

   652 "=====new ptree 3a ===============================================";

   653 "=====new ptree 3a ===============================================";

   654  states:=[];

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

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

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

   658  Iterator 1; moveActiveRoot 1;

   659  autoCalculate 1 CompleteCalcHead;

   660  autoCalculate 1 (Step 1);

   661  autoCalculate 1 (Step 1);

   662  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   673 (*

   674  get_obj g_ostate pt [1];

   675  show_pt pt;

   676 *)

   678 "-------------- move_dn in Incomplete ctree ----------------------";

   679 "-------------- move_dn in Incomplete ctree ----------------------";

   680 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   687 states:=[];

   688 CalcTree

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

   690 	   "solveFor x","solutions L"],

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

   692 Iterator 1; moveActiveRoot 1;

   693 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   719 writeln(pr_ptree pr_short pt);

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

   721  ###########################################################################*)

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

   723 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   732 (******************************************************************)

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

   734 (******************************************************************)

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

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

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

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

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

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

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

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

   743 www true [1,2];

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

   745 www true [1];

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

   748 local

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

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

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

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

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

   754 (*analoguous for tl*)

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

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

   758 (*see modspec.sml#pt_form

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

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

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

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

   763     in case cas of

   764 	   NONE => term2str (pblterm dI pI)

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

   766     end;

   767 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   802 in

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

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

   805 (1) the 'f' are given

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

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

   808 (2) the 't' ar given

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

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

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

   812 fun get_trace pt p q =

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

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

   815 end;

   817 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   833     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   836 case get_trace pt [] [] of

   837     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

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

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

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

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

   848   development stopped in favour of move_dn, see get_interval

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

   850 *)

   851 (*

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

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

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

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

   856     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   859 *)

   861 (******************************************************************)

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

   863 (******************************************************************)

   866 "=====new ptree 4 ratequation ====================================";

   867 "=====new ptree 4 ratequation ====================================";

   868 "=====new ptree 4 ratequation ====================================";

   869 states:=[];

   870 CalcTree

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

   872 	   "solveFor x","solutions L"],

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

   874 Iterator 1; moveActiveRoot 1;

   875 autoCalculate 1 CompleteCalc;

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

   877 show_pt pt;

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

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

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

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

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

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

   886      Subproblem

   887          ("PolyEq",

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

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

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

   891 (*WN060717 unintentionally changed some rls/ord while

   892      completing knowl. for thes2file...

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

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

   896      *)Subproblem

   897          ("PolyEq",

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

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

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

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

   906 "=====new ptree 5 minisubpbl =====================================";

   907 "=====new ptree 5 minisubpbl =====================================";

   908 "=====new ptree 5 minisubpbl =====================================";

   909 states:=[];

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

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

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

   913 Iterator 1; moveActiveRoot 1;

   914 autoCalculate 1 CompleteCalc;

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

   916 show_pt pt;

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

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

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

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

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

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

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

   925      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   940     ("-1 + x = 0",

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

   942      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   963      []) => ()

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

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

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

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

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

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

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

   973     ("[x = 1]",

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

   975      []) => ()

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

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

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

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

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

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

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

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

   986 states:=[];

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

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

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

   990 Iterator 1; moveActiveRoot 1;

   991 autoCalculate 1 CompleteCalc;

   992 interSteps 1 ([2],Res);

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

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

   995 show_pt pt;

   997 (**##############################################################**)

   998 "-------------- get_allpos' new ----------------------------------";

   999 "-------------- get_allpos' new ----------------------------------";

  1000 "-------------- get_allpos' new ----------------------------------";

  1001 "--- whole ctree";

  1002 print_depth 99;

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

  1004 print_depth 3;

  1005 if cuts =

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

  1007     ([1], Frm),

  1008     ([1], Res),

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

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

  1011     ([2], Res),

  1012     ([3], Pbl),

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

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

  1015     ([3, 2], Res),

  1016     ([3], Res),

  1017     ([4], Res),

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

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

  1021 print_depth 99;

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

  1023 print_depth 3;

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

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

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

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

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

  1030 if cuts =

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

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

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

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

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

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

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

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

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

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

  1044 if cuts =

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

  1046     ([3, 1], Res),

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

  1048     ([3, 2], Res),

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

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

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

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

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

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

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

  1058 if cuts =

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

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

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

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

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

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

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

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

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

  1070 if cuts =

  1071    [] then () else

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

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

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

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

  1079 (**#################################################################**)

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

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

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

  1083 show_pt pt;

  1084 val b = get_obj g_branch pt [];

  1085 if b = TransitiveB then () else

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

  1087 val b = get_obj g_branch pt [3];

  1088 if b = TransitiveB then () else

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

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

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

  1093 print_depth 99;

  1094 cuts;

  1095 print_depth 3;

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

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

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

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

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

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

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

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

  1106 print_depth 99;

  1107 cuts;

  1108 print_depth 3;

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

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

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

  1112 	   ([2], Res),

  1113 	   ([3], Pbl),

  1114 	   ([3, 1], Frm),

  1115 	   ([3, 1], Res),

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

  1117 	   ([3, 2], Res),

  1118 	   ([3], Res),

  1119 	   ([4], Res),

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

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

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

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

  1125 print_depth 99;

  1126 cuts;

  1127 print_depth 3;

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

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

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

  1131 	   ([3, 2], Res),

  1132 	   ([3], Res),

  1133 	   ([4], Res),

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

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

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

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

  1139 print_depth 99;

  1140 cuts;

  1141 print_depth 1;

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

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

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

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

  1146 show_pt pt';

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

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

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

  1152 show_pt pt;

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

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

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

  1157 print_depth 99;

  1158 cuts;

  1159 print_depth 3;

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

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

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

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

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

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

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

  1167 print_depth 99;

  1168 afterins;

  1169 print_depth 3;

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

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

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

  1173 show_pt pt';

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

  1176 show_pt pt;

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

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

  1179 print_depth 99;

  1180 cuts;

  1181 print_depth 3;

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

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

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

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

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

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

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

  1189 print_depth 99;

  1190 afterins;

  1191 print_depth 3;

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

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

  1194 then () else

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

  1196 show_pt pt';

  1197 (*

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

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

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

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

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

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

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

  1206  *)

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

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

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

  1211 print_depth 99;

  1212 cuts;

  1213 print_depth 3;

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

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

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

  1217 	   ([3, 2], Res),

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

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

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

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

  1222 print_depth 99;

  1223 afterins;

  1224 print_depth 3;

  1225 if afterins =

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

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

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

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

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

  1231    use"ctree.sml";

  1232    *)

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

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

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

  1237 print_depth 99;

  1238 cuts;

  1239 print_depth 3;

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

  1241 	   ([3, 2], Res),

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

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

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

  1245 print_depth 99;

  1246 afterins;

  1247 print_depth 3;

  1248 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1252 	       ([2], Res),

  1253 	       ([3], Pbl),

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

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

  1256 	       ([4], Res),

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

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

  1259 *)

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

  1268 if term2str (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";

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

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

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

  1274 print_depth 99;

  1275 cuts;

  1276 print_depth 3;

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

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

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

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

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

  1282 print_depth 99;

  1283 afterins;

  1284 print_depth 3;

  1285 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1289 	       ([2], Res),

  1290 	       ([3], Pbl),

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

  1292 	       ([3], Res),

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

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

  1295 *)

  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), ([3, 2], Frm), ([3, 2], Res)]

  1302 then () else

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

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

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

  1308 "---(6++) on S(606)..S(608)--------";

  1309 (**)

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

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

  1312 print_depth 99;

  1313 cuts;

  1314 print_depth 1;

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

  1316 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1317 then () else

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

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

  1320 print_depth 99;

  1321 afterins;

  1322 print_depth 3;

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

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

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

  1326 	       ([2], Res),

  1327 	       ([3], Pbl),

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

  1329 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1330 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1333 (*

  1334 show_pt pt';

  1335 show_pt pt;

  1336 *)

  1338 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Sun, 15 May 2011 11:32:41 +0200
branch	decompose-isar
changeset 41992	1ada058e92bc
parent 41990	99e83a0bea44
child 42108	23b6b0033454
permissions	-rw-r--r--