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

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

     5    authors: Walther Neuper 060113

     6    (c) due to copyright terms

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

     9 use"ctree.sml";

    10 *)

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

    13 "table of contents -----------------------------------------------";

    14 "-----------------------------------------------------------------";

    15 "-----------------------------------------------------------------";

    16 "-------------- fun get_ctxt -------------------------------------";

    17 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    18 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

    25 (**)#####################################################################**)

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

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

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

    29 "-------------- cappend minisubpbl -------------------------------";

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

    32 "-------------- move_dn ------------------------------------------";

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

    34 "-------------- move_up ------------------------------------------";

    35 "------ move into detail -----------------------------------------";

    36 "=====new ptree 3a ===============================================";

    37 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

    42 (*              val SAVE_get_trace = get_trace;                   *)

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

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

    45 (******************************************************************)

    46 (*              val get_trace = SAVE_get_trace;                   *)

    47 (******************************************************************)

    48 (*############## development stopped 0501 ########################*)

    50 "=====new ptree 4 ratequation ====================================";

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

    52 "=====new ptree 5 minisubpbl =====================================";

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

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

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

    57 "-------------- get_allpos' new ----------------------------------";

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

    59 (**)#####################################################################**)

    61 "-----------------------------------------------------------------";

    62 "-----------------------------------------------------------------";

    63 "-----------------------------------------------------------------";

    66 "-------------- fun get_ctxt -------------------------------------";

    67 "-------------- fun get_ctxt -------------------------------------";

    68 "-------------- fun get_ctxt -------------------------------------";

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

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

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

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

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

    74 (get_ctxt pt p)

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

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

    77 (get_ctxt pt p)

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

    80 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    81 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    82 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    83 val pt = EmptyPtree;

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

    85 val ctxt = get_obj g_ctxt pt [];

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

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

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

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

    91 "-------------- check positions in miniscript --------------------";

    92 "-------------- check positions in miniscript --------------------";

    93 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

   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;

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

   109    *)

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

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

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

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

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

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

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

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

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

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

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

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

   123 "----------------------------------------------------------------/";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   149  show_pt pt;

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

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

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

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

   157    [([], Frm),

   158     ([1], Frm),

   159     ([1], Res),

   160     ([2], Res),

   161     ([3], Frm),

   162     ([3, 1], Frm),

   163     ([3, 1], Res),

   164     ([3, 2], Res),

   165     ([3], Res),

   166     ([4], Res),

   167     ([], Res)]

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

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

   171    [([1], Frm),

   172     ([1], Res),

   173     ([2], Res),

   174     ([3], Frm),

   175     ([3, 1], Frm),

   176     ([3, 1], Res),

   177     ([3, 2], Res),

   178     ([3], Res),

   179     ([4], Res)]

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

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

   183    [([2], Res),

   184     ([3], Frm),

   185     ([3, 1], Frm),

   186     ([3, 1], Res),

   187     ([3, 2], Res),

   188     ([3], Res),

   189     ([4], Res)]

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

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

   193    [([3], Frm),

   194     ([3, 1], Frm),

   195     ([3, 1], Res),

   196     ([3, 2], Res),

   197     ([3], Res),

   198     ([4], Res)]

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

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

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

   203     ([3, 1], Res),

   204     ([3, 2], Res)]

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

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

   208    [([3], Frm),

   209     ([3, 1], Frm),

   210     ([3, 1], Res),

   211     ([3, 2], Res),

   212     ([3], Res)]

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

   216 (**##############################################################(**)

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

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

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

   221 show_pt pt;

   222 show_pt pt';

   223 print_depth 99; cuts; print_depth 3;

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

   226 	   ([3], Frm),

   227 	   ([3, 1], Frm),

   228 	   ([3, 1], Res),

   229 	   ([3, 2], Res),

   230 	   ([3], Res),

   231 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

   243    [([], Frm),

   244     ([1], Frm),

   245     ([1], Res),

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

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

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

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

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

   253 	   ([3, 1], Frm),

   254 	   ([3, 1], Res),

   255 	   ([3, 2], Res),

   256 	   ([3], Res),

   257 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   281 	   ([3], Frm),

   282 	   ([3, 1], Frm),

   283 	   ([3, 1], Res),

   284 	   ([3, 2], Res),

   285 	   ([3], Res),

   286 	   ([4], Res),

   287 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

   303    [([], Frm),

   304     ([1], Frm),

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

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

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

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

   310 	   ([3, 1], Frm),

   311 	   ([3, 1], Res),

   312 	   ([3, 2], Res),

   313 	   ([3], Res),

   314 	   ([4], Res),

   315 	   ([], Res)]

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

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

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

   320 	   ([3, 2], Res),

   321 	   ([3], Res),

   322 	   ([4], Res),

   323 	   ([], Res)]

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

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

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

   328 	   ([3], Res),

   329 	   ([4], Res),

   330 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

   350 show_pt pt;

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

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

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

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

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

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

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

   361 if cuts = []

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

   364 (*WN050219

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

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

   369 show_pt pt;

   370 show_pt pt';

   371 print_depth 99;cuts;print_depth 3;

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

   373 ####################################################################*)*)

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

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

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

   378  states:=[];

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

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

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

   382  Iterator 1; moveActiveRoot 1;

   383  autoCalculate 1 CompleteCalc;

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

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

   388  show_pt pt;

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

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

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

   393 (*WN050225 intermed. outcommented

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

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

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

   397 	    ([3, 2], Res),

   398 	    ([3], Res),

   399 	    ([4], Res)]

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

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

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

   404 	    ([3, 2], Res),

   405 	    ([3], Res),

   406 	    ([4], Res)]

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

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

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

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

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

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

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

   416 	   ([3, 2], Res),

   417 	   ([3], Res),

   418 	   ([4], Res),

   419 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   430 	   ([3, 2], Res),

   431 	   ([3], Res),

   432 	   ([4], Res),

   433 	   ([], Res)]

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

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

   439 "-------------- cappend minisubpbl -------------------------------";

   440 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   450    *)

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

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

   453    *)

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

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

   456    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   475 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   487 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   506 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   520 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   537 WN050225 intermed. outcommented---*)

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

   540 "=====new ptree 3 ================================================";

   541 "=====new ptree 3 ================================================";

   543 (*========== inhibit exn AK110719 ==============================================

   544 (* ERROR: get_pos *)

   545 states:=[];

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

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

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

   549  Iterator 1; moveActiveRoot 1;

   550  autoCalculate 1 CompleteCalc;

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

   553  show_pt pt;

   554 ============ inhibit exn AK110719 ============================================*)

   556 "-------------- move_dn ------------------------------------------";

   557 "-------------- move_dn ------------------------------------------";

   558 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   568    term2str (get_obj g_form pt [4]);

   569    *)

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

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

   572 (*

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

   574                                   Exception PTREE end of calculation*)

   575 (*========== inhibit exn AK110719 ==============================================

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

   577 ============ inhibit exn AK110719 ============================================*)

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

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

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

   584  (*states := [];

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

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

   587        ("Test",

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

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

   590  Iterator 1; moveActiveRoot 1;

   591  autoCalculate 1 CompleteCalcHead;

   592  autoCalculate 1 (Step 1);

   593  refFormula 1 (get_pos 1 1);

   595  moveActiveRoot 1;

   596  moveActiveDown 1;

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

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

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

   601  autoCalculate 1 (Step 1);

   602  refFormula 1 (get_pos 1 1);

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

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

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

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

   610 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

   624                                   Exception PTREE begin of calculation*)

   625 (*========== inhibit exn AK110719 ==============================================

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

   627 ========== inhibit exn AK110719 ==============================================*)

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

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

   632 "------ move into detail -----------------------------------------";

   633  states:=[];

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

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

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

   637  Iterator 1; moveActiveRoot 1;

   638  autoCalculate 1 CompleteCalc;

   639  moveActiveRoot 1;

   640  moveActiveDown 1;

   641  moveActiveDown 1;

   642  moveActiveDown 1;

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

   645  interSteps 1 ([2],Res);

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

   648  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   662 "=====new ptree 3a ===============================================";

   663 "=====new ptree 3a ===============================================";

   664 "=====new ptree 3a ===============================================";

   665  states:=[];

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

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

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

   669  Iterator 1; moveActiveRoot 1;

   670  autoCalculate 1 CompleteCalcHead;

   671  autoCalculate 1 (Step 1);

   672  autoCalculate 1 (Step 1);

   673  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   684 (*

   685  get_obj g_ostate pt [1];

   686  show_pt pt;

   687 *)

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

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

   691 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   698 states:=[];

   699 CalcTree

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

   701 	   "solveFor x","solutions L"],

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

   703 Iterator 1; moveActiveRoot 1;

   704 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   730 writeln(pr_ptree pr_short pt);

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

   732  ###########################################################################*)

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

   734 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   743 (******************************************************************)

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

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

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

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

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

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

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

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

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

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

   754 www true [1,2];

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

   756 www true [1];

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

   759 local

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

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

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

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

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

   765 (*analoguous for tl*)

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

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

   769 (*see modspec.sml#pt_form

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

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

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

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

   774     in case cas of

   775 	   NONE => term2str (pblterm dI pI)

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

   777     end;

   778 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   813 in

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

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

   816 (1) the 'f' are given

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

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

   819 (2) the 't' ar given

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

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

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

   823 fun get_trace pt p q =

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

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

   826 end;

   828 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

   838 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

   844 ========== inhibit exn AK110719 ==============================================*)

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

   846     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   849 (*========== inhibit exn AK110719 ==============================================

   850 case get_trace pt [] [] of

   851     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

   857 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   863   development stopped in favour of move_dn, see get_interval

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

   865 *)

   866 (*

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

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

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

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

   871     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   874 *)

   876 (******************************************************************)

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

   878 (******************************************************************)

   881 "=====new ptree 4 ratequation ====================================";

   882 "=====new ptree 4 ratequation ====================================";

   883 "=====new ptree 4 ratequation ====================================";

   884 states:=[];

   885 CalcTree

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

   887 	   "solveFor x","solutions L"],

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

   889 Iterator 1; moveActiveRoot 1;

   890 autoCalculate 1 CompleteCalc;

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

   892 show_pt pt;

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

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

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

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

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

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

   901      Subproblem

   902          ("PolyEq",

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

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

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

   906 (*WN060717 unintentionally changed some rls/ord while

   907      completing knowl. for thes2file...

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

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

   911      *)Subproblem

   912          ("PolyEq",

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

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

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

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

   921 "=====new ptree 5 minisubpbl =====================================";

   922 "=====new ptree 5 minisubpbl =====================================";

   923 "=====new ptree 5 minisubpbl =====================================";

   924 states:=[];

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

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

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

   928 Iterator 1; moveActiveRoot 1;

   929 autoCalculate 1 CompleteCalc;

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

   931 show_pt pt;

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

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

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

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

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

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

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

   940      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   955     ("-1 + x = 0",

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

   957      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   978      []) => ()

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

   981 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

   989     ("[x = 1]",

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

   991      []) => ()

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

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

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

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

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

   998 ========== inhibit exn AK110719 ==============================================*)

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

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

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

  1003 states:=[];

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

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

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

  1007 Iterator 1; moveActiveRoot 1;

  1008 autoCalculate 1 CompleteCalc;

  1009 interSteps 1 ([2],Res);

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

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

  1012 show_pt pt;

  1014 (**##############################################################**)

  1015 "-------------- get_allpos' new ----------------------------------";

  1016 "-------------- get_allpos' new ----------------------------------";

  1017 "-------------- get_allpos' new ----------------------------------";

  1018 "--- whole ctree";

  1019 print_depth 99;

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

  1021 print_depth 3;

  1022 if cuts =

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

  1024     ([1], Frm),

  1025     ([1], Res),

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

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

  1028     ([2], Res),

  1029     ([3], Pbl),

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

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

  1032     ([3, 2], Res),

  1033     ([3], Res),

  1034     ([4], Res),

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

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

  1038 print_depth 99;

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

  1040 print_depth 3;

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

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

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

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

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

  1047 if cuts =

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

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

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

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

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

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

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

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

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

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

  1061 if cuts =

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

  1063     ([3, 1], Res),

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

  1065     ([3, 2], Res),

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

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

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

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

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

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

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

  1075 if cuts =

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

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

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

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

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

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

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

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

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

  1087 if cuts =

  1088    [] then () else

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

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

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

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

  1096 (**#################################################################**)

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

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

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

  1100 show_pt pt;

  1101 val b = get_obj g_branch pt [];

  1102 if b = TransitiveB then () else

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

  1104 val b = get_obj g_branch pt [3];

  1105 if b = TransitiveB then () else

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

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

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

  1110 print_depth 99;

  1111 cuts;

  1112 print_depth 3;

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

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

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

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

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

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

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

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

  1123 print_depth 99;

  1124 cuts;

  1125 print_depth 3;

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

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

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

  1129 	   ([2], Res),

  1130 	   ([3], Pbl),

  1131 	   ([3, 1], Frm),

  1132 	   ([3, 1], Res),

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

  1134 	   ([3, 2], Res),

  1135 	   ([3], Res),

  1136 	   ([4], Res),

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

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

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

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

  1142 print_depth 99;

  1143 cuts;

  1144 print_depth 3;

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

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

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

  1148 	   ([3, 2], Res),

  1149 	   ([3], Res),

  1150 	   ([4], Res),

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

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

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

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

  1156 print_depth 99;

  1157 cuts;

  1158 print_depth 1;

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

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

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

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

  1163 show_pt pt';

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

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

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

  1169 show_pt pt;

  1171 (*========== inhibit exn AK110719 ==============================================

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

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

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

  1177 print_depth 99;

  1178 cuts;

  1179 print_depth 3;

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

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

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

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

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

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

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

  1188 print_depth 99;

  1189 afterins;

  1190 print_depth 3;

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

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

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

  1194 show_pt pt';

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

  1197 show_pt pt;

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

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

  1200 print_depth 99;

  1201 cuts;

  1202 print_depth 3;

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

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

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

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

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

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

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

  1210 print_depth 99;

  1211 afterins;

  1212 print_depth 3;

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

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

  1215 then () else

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

  1217 show_pt pt';

  1218 (*

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

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

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

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

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

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

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

  1227  *)

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

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

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

  1232 print_depth 99;

  1233 cuts;

  1234 print_depth 3;

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

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

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

  1238 	   ([3, 2], Res),

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

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

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

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

  1243 print_depth 99;

  1244 afterins;

  1245 print_depth 3;

  1246 if afterins =

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

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

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

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

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

  1252    use"ctree.sml";

  1253    *)

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

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

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

  1258 print_depth 99;

  1259 cuts;

  1260 print_depth 3;

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

  1262 	   ([3, 2], Res),

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

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

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

  1267 print_depth 99;

  1268 afterins;

  1269 print_depth 3;

  1270 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1274 	       ([2], Res),

  1275 	       ([3], Pbl),

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

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

  1278 	       ([4], Res),

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

  1280 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] 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)] then () else

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

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

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

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

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

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

  1296 print_depth 99;

  1297 cuts;

  1298 print_depth 3;

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

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

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

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

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

  1304 print_depth 99;

  1305 afterins;

  1306 print_depth 3;

  1307 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1311 	       ([2], Res),

  1312 	       ([3], Pbl),

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

  1314 	       ([3], Res),

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

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

  1317 *)

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

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

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

  1321 	       ([2], Res),

  1322 	       ([3], Pbl),

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

  1324 then () else

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

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

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

  1330 "---(6++) on S(606)..S(608)--------";

  1331 (**)

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

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

  1334 print_depth 99;

  1335 cuts;

  1336 print_depth 1;

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

  1338 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1339 then () else

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

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

  1342 print_depth 99;

  1343 afterins;

  1344 print_depth 3;

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

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

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

  1348 	       ([2], Res),

  1349 	       ([3], Pbl),

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

  1351 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1352 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1355 (*

  1356 show_pt pt';

  1357 show_pt pt;

  1358 *)

  1359 ========== inhibit exn AK110719 ==============================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 19 Jul 2011 14:01:27 +0200
branch	decompose-isar
changeset 42124	ba52b628c40c
parent 42120	5b996050e25f
child 42185	332a0653d4c9
permissions	-rw-r--r--