wneuper/isa: test/Tools/isac/Interpret/ctree.sml@235f3990c9b7

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    38 (*              val SAVE_get_trace = get_trace;                   *)

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

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

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

    42 (*              val get_trace = SAVE_get_trace;                   *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    62 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    63 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    64 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

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

    66 if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)

    67     = "Interpret"

    68 then () else error "TODO";

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

    70 if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)

    71     = "Isac"

    72 then () else error "TODO";

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

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

    76 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

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

    86    *)

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

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

    89    *)

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

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

    92    *)

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

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

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

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

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

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

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

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

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

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

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

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

   106 "----------------------------------------------------------------/";

   107 (*========== inhibit exn WN110319 ==============================================

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   132  show_pt pt;

   133 ============ inhibit exn WN110319 ============================================*)

   135 (*=== inhibit exn ?=============================================================

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

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

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

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

   141    [([], Frm),

   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     ([], Res)]

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

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

   155    [([1], Frm),

   156     ([1], Res),

   157     ([2], Res),

   158     ([3], Frm),

   159     ([3, 1], Frm),

   160     ([3, 1], Res),

   161     ([3, 2], Res),

   162     ([3], Res),

   163     ([4], Res)]

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

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

   167    [([2], Res),

   168     ([3], Frm),

   169     ([3, 1], Frm),

   170     ([3, 1], Res),

   171     ([3, 2], Res),

   172     ([3], Res),

   173     ([4], Res)]

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

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

   177    [([3], Frm),

   178     ([3, 1], Frm),

   179     ([3, 1], Res),

   180     ([3, 2], Res),

   181     ([3], Res),

   182     ([4], Res)]

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

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

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

   187     ([3, 1], Res),

   188     ([3, 2], Res)]

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

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

   192    [([3], Frm),

   193     ([3, 1], Frm),

   194     ([3, 1], Res),

   195     ([3, 2], Res),

   196     ([3], Res)]

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

   200 (**##############################################################(**)

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

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

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

   205 show_pt pt;

   206 show_pt pt';

   207 print_depth 99; cuts; print_depth 3;

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

   210 	   ([3], Frm),

   211 	   ([3, 1], Frm),

   212 	   ([3, 1], Res),

   213 	   ([3, 2], Res),

   214 	   ([3], Res),

   215 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

   227    [([], Frm),

   228     ([1], Frm),

   229     ([1], Res),

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

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

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

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

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

   237 	   ([3, 1], Frm),

   238 	   ([3, 1], Res),

   239 	   ([3, 2], Res),

   240 	   ([3], Res),

   241 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   265 	   ([3], Frm),

   266 	   ([3, 1], Frm),

   267 	   ([3, 1], Res),

   268 	   ([3, 2], Res),

   269 	   ([3], Res),

   270 	   ([4], Res),

   271 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

   287    [([], Frm),

   288     ([1], Frm),

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

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

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

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

   294 	   ([3, 1], Frm),

   295 	   ([3, 1], Res),

   296 	   ([3, 2], Res),

   297 	   ([3], Res),

   298 	   ([4], Res),

   299 	   ([], Res)]

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

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

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

   304 	   ([3, 2], Res),

   305 	   ([3], Res),

   306 	   ([4], Res),

   307 	   ([], Res)]

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

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

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

   312 	   ([3], Res),

   313 	   ([4], Res),

   314 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   334 show_pt pt;

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

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

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

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

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

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

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

   345 if cuts = []

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

   348 (*WN050219

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

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

   353 show_pt pt;

   354 show_pt pt';

   355 print_depth 99;cuts;print_depth 3;

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

   357 ####################################################################*)*)

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

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

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

   362  states:=[];

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

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

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

   366  Iterator 1; moveActiveRoot 1;

   367  autoCalculate 1 CompleteCalc;

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

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

   372  show_pt pt;

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

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

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

   377 (*WN050225 intermed. outcommented

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

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

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

   381 	    ([3, 2], Res),

   382 	    ([3], Res),

   383 	    ([4], Res)]

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

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

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

   388 	    ([3, 2], Res),

   389 	    ([3], Res),

   390 	    ([4], Res)]

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

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

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

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

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

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

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

   400 	   ([3, 2], Res),

   401 	   ([3], Res),

   402 	   ([4], Res),

   403 	   ([], Res)]

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

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

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

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

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

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

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

   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_atomic";

   422 "-------------- cappend minisubpbl -------------------------------";

   423 "-------------- cappend minisubpbl -------------------------------";

   424 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   434    *)

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

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

   437    *)

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

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

   440    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   459 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   471 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   490 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   504 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   521 WN050225 intermed. outcommented---*)

   523 "=====new ptree 3 ================================================";

   524 "=====new ptree 3 ================================================";

   525 "=====new ptree 3 ================================================";

   526  states:=[];

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

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

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

   530  Iterator 1; moveActiveRoot 1;

   531  autoCalculate 1 CompleteCalc;

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

   534  show_pt pt;

   536 "-------------- move_dn ------------------------------------------";

   537 "-------------- move_dn ------------------------------------------";

   538 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   548    term2str (get_obj g_form pt [4]);

   549    *)

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

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

   552 (*

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

   554                                   Exception PTREE end of calculation*)

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

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

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

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

   561  states := [];

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

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

   564        ("Test",

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

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

   567  Iterator 1; moveActiveRoot 1;

   568  autoCalculate 1 CompleteCalcHead;

   569  autoCalculate 1 (Step 1);

   570  refFormula 1 (get_pos 1 1);

   572  moveActiveRoot 1;

   573  moveActiveDown 1;

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

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

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

   578  autoCalculate 1 (Step 1);

   579  refFormula 1 (get_pos 1 1);

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

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

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

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

   587 "-------------- move_up ------------------------------------------";

   588 "-------------- move_up ------------------------------------------";

   589 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   601                                   Exception PTREE begin of calculation*)

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

   605 "------ move into detail -----------------------------------------";

   606 "------ move into detail -----------------------------------------";

   607 "------ move into detail -----------------------------------------";

   608  states:=[];

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

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

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

   612  Iterator 1; moveActiveRoot 1;

   613  autoCalculate 1 CompleteCalc;

   614  moveActiveRoot 1;

   615  moveActiveDown 1;

   616  moveActiveDown 1;

   617  moveActiveDown 1;

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

   620  interSteps 1 ([2],Res);

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

   623  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   637 "=====new ptree 3a ===============================================";

   638 "=====new ptree 3a ===============================================";

   639 "=====new ptree 3a ===============================================";

   640  states:=[];

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

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

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

   644  Iterator 1; moveActiveRoot 1;

   645  autoCalculate 1 CompleteCalcHead;

   646  autoCalculate 1 (Step 1);

   647  autoCalculate 1 (Step 1);

   648  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   659 (*

   660  get_obj g_ostate pt [1];

   661  show_pt pt;

   662 *)

   664 "-------------- move_dn in Incomplete ctree ----------------------";

   665 "-------------- move_dn in Incomplete ctree ----------------------";

   666 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   673 states:=[];

   674 CalcTree

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

   676 	   "solveFor x","solutions L"],

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

   678 Iterator 1; moveActiveRoot 1;

   679 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   705 writeln(pr_ptree pr_short pt);

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

   707  ###########################################################################*)

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

   709 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   718 (******************************************************************)

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

   720 (******************************************************************)

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

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

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

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

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

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

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

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

   729 www true [1,2];

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

   731 www true [1];

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

   734 local

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

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

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

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

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

   740 (*analoguous for tl*)

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

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

   744 (*see modspec.sml#pt_form

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

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

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

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

   749     in case cas of

   750 	   NONE => term2str (pblterm dI pI)

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

   752     end;

   753 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   788 in

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

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

   791 (1) the 'f' are given

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

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

   794 (2) the 't' ar given

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

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

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

   798 fun get_trace pt p q =

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

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

   801 end;

   803 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   819     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   822 case get_trace pt [] [] of

   823     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

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

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

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

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

   834   development stopped in favour of move_dn, see get_interval

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

   836 *)

   837 (*

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

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

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

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

   842     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   845 *)

   847 (******************************************************************)

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

   849 (******************************************************************)

   852 "=====new ptree 4 ratequation ====================================";

   853 "=====new ptree 4 ratequation ====================================";

   854 "=====new ptree 4 ratequation ====================================";

   855 states:=[];

   856 CalcTree

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

   858 	   "solveFor x","solutions L"],

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

   860 Iterator 1; moveActiveRoot 1;

   861 autoCalculate 1 CompleteCalc;

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

   863 show_pt pt;

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

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

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

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

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

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

   872      Subproblem

   873          ("PolyEq",

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

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

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

   877 (*WN060717 unintentionally changed some rls/ord while

   878      completing knowl. for thes2file...

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

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

   882      *)Subproblem

   883          ("PolyEq",

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

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

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

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

   892 "=====new ptree 5 minisubpbl =====================================";

   893 "=====new ptree 5 minisubpbl =====================================";

   894 "=====new ptree 5 minisubpbl =====================================";

   895 states:=[];

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

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

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

   899 Iterator 1; moveActiveRoot 1;

   900 autoCalculate 1 CompleteCalc;

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

   902 show_pt pt;

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

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

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

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

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

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

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

   911      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   926     ("-1 + x = 0",

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

   928      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   949      []) => ()

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

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

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

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

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

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

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

   959     ("[x = 1]",

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

   961      []) => ()

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

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

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

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

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

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

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

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

   972 states:=[];

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

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

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

   976 Iterator 1; moveActiveRoot 1;

   977 autoCalculate 1 CompleteCalc;

   978 interSteps 1 ([2],Res);

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

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

   981 show_pt pt;

   983 (**##############################################################**)

   984 "-------------- get_allpos' new ----------------------------------";

   985 "-------------- get_allpos' new ----------------------------------";

   986 "-------------- get_allpos' new ----------------------------------";

   987 "--- whole ctree";

   988 print_depth 99;

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

   990 print_depth 3;

   991 if cuts =

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

   993     ([1], Frm),

   994     ([1], Res),

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

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

   997     ([2], Res),

   998     ([3], Pbl),

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

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

  1001     ([3, 2], Res),

  1002     ([3], Res),

  1003     ([4], Res),

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

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

  1007 print_depth 99;

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

  1009 print_depth 3;

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

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

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

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

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

  1016 if cuts =

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

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

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

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

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

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

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

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

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

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

  1030 if cuts =

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

  1032     ([3, 1], Res),

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

  1034     ([3, 2], Res),

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

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

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

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

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

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

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

  1044 if cuts =

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

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

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

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

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

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

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

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

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

  1056 if cuts =

  1057    [] then () else

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

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

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

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

  1065 (**#################################################################**)

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

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

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

  1069 show_pt pt;

  1070 val b = get_obj g_branch pt [];

  1071 if b = TransitiveB then () else

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

  1073 val b = get_obj g_branch pt [3];

  1074 if b = TransitiveB then () else

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

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

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

  1079 print_depth 99;

  1080 cuts;

  1081 print_depth 3;

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

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

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

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

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

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

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

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

  1092 print_depth 99;

  1093 cuts;

  1094 print_depth 3;

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

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

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

  1098 	   ([2], Res),

  1099 	   ([3], Pbl),

  1100 	   ([3, 1], Frm),

  1101 	   ([3, 1], Res),

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

  1103 	   ([3, 2], Res),

  1104 	   ([3], Res),

  1105 	   ([4], Res),

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

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

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

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

  1111 print_depth 99;

  1112 cuts;

  1113 print_depth 3;

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

  1115 	   ([3, 1], Frm), ([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)]

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

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

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

  1125 print_depth 99;

  1126 cuts;

  1127 print_depth 1;

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

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

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

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

  1132 show_pt pt';

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

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

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

  1138 show_pt pt;

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

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

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

  1143 print_depth 99;

  1144 cuts;

  1145 print_depth 3;

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

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

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

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

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

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

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

  1153 print_depth 99;

  1154 afterins;

  1155 print_depth 3;

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

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

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

  1159 show_pt pt';

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

  1162 show_pt pt;

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

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

  1165 print_depth 99;

  1166 cuts;

  1167 print_depth 3;

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

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

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

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

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

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

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

  1175 print_depth 99;

  1176 afterins;

  1177 print_depth 3;

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

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

  1180 then () else

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

  1182 show_pt pt';

  1183 (*

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

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

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

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

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

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

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

  1192  *)

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

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

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

  1197 print_depth 99;

  1198 cuts;

  1199 print_depth 3;

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

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

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

  1203 	   ([3, 2], Res),

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

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

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

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

  1208 print_depth 99;

  1209 afterins;

  1210 print_depth 3;

  1211 if afterins =

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

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

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

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

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

  1217    use"ctree.sml";

  1218    *)

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

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

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

  1223 print_depth 99;

  1224 cuts;

  1225 print_depth 3;

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

  1227 	   ([3, 2], Res),

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

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

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

  1231 print_depth 99;

  1232 afterins;

  1233 print_depth 3;

  1234 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1238 	       ([2], Res),

  1239 	       ([3], Pbl),

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

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

  1242 	       ([4], Res),

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

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

  1245 *)

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

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

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

  1249 	       ([2], Res),

  1250 	       ([3], Pbl),

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

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

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

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

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

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

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

  1260 print_depth 99;

  1261 cuts;

  1262 print_depth 3;

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

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

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

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

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

  1268 print_depth 99;

  1269 afterins;

  1270 print_depth 3;

  1271 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1275 	       ([2], Res),

  1276 	       ([3], Pbl),

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

  1278 	       ([3], Res),

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

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

  1281 *)

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

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

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

  1285 	       ([2], Res),

  1286 	       ([3], Pbl),

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

  1288 then () else

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

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

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

  1294 "---(6++) on S(606)..S(608)--------";

  1295 (**)

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

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

  1298 print_depth 99;

  1299 cuts;

  1300 print_depth 1;

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

  1302 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1303 then () else

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

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

  1306 print_depth 99;

  1307 afterins;

  1308 print_depth 3;

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

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

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

  1312 	       ([2], Res),

  1313 	       ([3], Pbl),

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

  1315 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1316 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1319 (*

  1320 show_pt pt';

  1321 show_pt pt;

  1322 *)

  1324 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 13 May 2011 14:15:59 +0200
branch	decompose-isar
changeset 41989	235f3990c9b7
parent 41972	22c5483e9bfb
child 41990	99e83a0bea44
permissions	-rw-r--r--