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

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

     2    authors: Walther Neuper 060113

     3    (c) due to copyright terms

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

     6 use"ctree.sml";

     7 *)

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

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

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

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

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

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

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

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

    17 "-------------- 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 "=====new ptree 2 miniscript with mini-subpbl ====================";

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

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

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

    25 "=====new ptree 3 ================================================";

    26 "-------------- move_dn ------------------------------------------";

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

    28 "-------------- move_up ------------------------------------------";

    29 "------ move into detail -----------------------------------------";

    30 "=====new ptree 3a ===============================================";

    31 "-------------- move_dn in Incomplete ctree ----------------------";

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

    33 (*############## development stopped 0501 ########################*)

    34 (******************************************************************)

    35 (*              val SAVE_get_trace = get_trace;                   *)

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

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

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

    39 (*              val get_trace = SAVE_get_trace;                   *)

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

    41 (*############## development stopped 0501 ########################*)

    42 "=====new ptree 4 ratequation ====================================";

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

    44 "=====new ptree 5 minisubpbl =====================================";

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

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

    47 "-------------- get_allpos' new ----------------------------------";

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

    49 "-----------------------------------------------------------------";

    50 "-----------------------------------------------------------------";

    51 "-----------------------------------------------------------------";

    54 "-------------- fun get_ctxt -------------------------------------";

    55 "-------------- fun get_ctxt -------------------------------------";

    56 "-------------- fun get_ctxt -------------------------------------";

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

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

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

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

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

    62 (get_ctxt pt p)

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

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

    65 (get_ctxt pt p)

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

    68 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    69 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    70 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    71 val pt = EmptyPtree;

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

    73 val ctxt = get_obj g_ctxt pt [];

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

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

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

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

    79 "-------------- check positions in miniscript --------------------";

    80 "-------------- check positions in miniscript --------------------";

    81 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

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

    91    *)

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

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

    94    *)

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

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

    97    *)

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

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

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

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

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

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

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

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

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

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

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

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

   111 "----------------------------------------------------------------/";

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

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

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

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

   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 = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   137  show_pt pt;

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

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

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

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

   143    [([], Frm),

   144     ([1], Frm),

   145     ([1], Res),

   146     ([2], Res),

   147     ([3], Frm),

   148     ([3, 1], Frm),

   149     ([3, 1], Res),

   150     ([3, 2], Res),

   151     ([3], Res),

   152     ([4], Res),

   153     ([], Res)]

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

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

   157    [([1], Frm),

   158     ([1], Res),

   159     ([2], Res),

   160     ([3], Frm),

   161     ([3, 1], Frm),

   162     ([3, 1], Res),

   163     ([3, 2], Res),

   164     ([3], Res),

   165     ([4], Res)]

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

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

   169    [([2], Res),

   170     ([3], Frm),

   171     ([3, 1], Frm),

   172     ([3, 1], Res),

   173     ([3, 2], Res),

   174     ([3], Res),

   175     ([4], Res)]

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

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

   179    [([3], Frm),

   180     ([3, 1], Frm),

   181     ([3, 1], Res),

   182     ([3, 2], Res),

   183     ([3], Res),

   184     ([4], Res)]

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

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

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

   189     ([3, 1], Res),

   190     ([3, 2], Res)]

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

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

   194    [([3], Frm),

   195     ([3, 1], Frm),

   196     ([3, 1], Res),

   197     ([3, 2], Res),

   198     ([3], Res)]

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

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

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

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

   209 show_pt pt;

   210 show_pt pt';

   211 print_depth 99; cuts; print_depth 3;

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

   214 	   ([3], Frm),

   215 	   ([3, 1], Frm),

   216 	   ([3, 1], Res),

   217 	   ([3, 2], Res),

   218 	   ([3], Res),

   219 	   ([4], Res)]

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

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

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

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

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

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

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

   228 (*============ inhibit exn AK110725 ==============================================

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

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

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

   232    [([], Frm),

   233     ([1], Frm),

   234     ([1], Res),

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

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

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

   238 ============ inhibit exn AK110725 ==============================================*)

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

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

   243 	   ([3, 1], Frm),

   244 	   ([3, 1], Res),

   245 	   ([3, 2], Res),

   246 	   ([3], Res),

   247 	   ([4], Res)]

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

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

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

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

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

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

   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 3b";

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

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

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

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

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

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

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

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

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

   270 (*============ inhibit exn AK110725 ==============================================

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

   272 	   ([3], Frm),

   273 	   ([3, 1], Frm),

   274 	   ([3, 1], Res),

   275 	   ([3, 2], Res),

   276 	   ([3], Res),

   277 	   ([4], Res),

   278 	   ([], Res)]

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

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

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

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

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

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

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

   288 ============ inhibit exn AK110725 ==============================================*)

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

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

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

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

   295    [([], Frm),

   296     ([1], Frm),

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

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

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

   301 (*============ inhibit exn AK110725 ==============================================

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

   303 	   ([3, 1], Frm),

   304 	   ([3, 1], Res),

   305 	   ([3, 2], Res),

   306 	   ([3], Res),

   307 	   ([4], Res),

   308 	   ([], Res)]

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

   310 ============ inhibit exn AK110725 ==============================================*)

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

   313 (*============ inhibit exn AK110725 ==============================================

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

   315 	   ([3, 2], Res),

   316 	   ([3], Res),

   317 	   ([4], Res),

   318 	   ([], Res)]

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

   320 ============ inhibit exn AK110725 ==============================================*)

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

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

   324 	   ([3], Res),

   325 	   ([4], Res),

   326 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   345 show_pt pt;

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

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

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

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

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

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

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

   356 if cuts = []

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

   359 (*WN050219

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

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

   364 show_pt pt;

   365 show_pt pt';

   366 print_depth 99;cuts;print_depth 3;

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

   368 ####################################################################*)

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

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

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

   380  states:=[];

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

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

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

   384  Iterator 1; moveActiveRoot 1;

   385  autoCalculate 1 CompleteCalc;

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

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

   390  show_pt pt;

   392 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()

   393 else error "mini-subpbl interSteps broken";

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

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

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

   398 (*WN050225 intermed. outcommented

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

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

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

   402 	    ([3, 2], Res),

   403 	    ([3], Res),

   404 	    ([4], Res)]

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

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

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

   409 	    ([3, 2], Res),

   410 	    ([3], Res),

   411 	    ([4], Res)]

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

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

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

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

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

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

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

   421 	   ([3, 2], Res),

   422 	   ([3], Res),

   423 	   ([4], Res),

   424 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   435 	   ([3, 2], Res),

   436 	   ([3], Res),

   437 	   ([4], Res),

   438 	   ([], Res)]

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

   443 "-------------- cappend minisubpbl -------------------------------";

   444 "-------------- cappend minisubpbl -------------------------------";

   445 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   455    *)

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

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

   458    *)

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

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

   461    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   480 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   492 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   511 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   525 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   542 WN050225 intermed. outcommented---*)

   544 "=====new ptree 3 ================================================";

   545 "=====new ptree 3 ================================================";

   546 "=====new ptree 3 ================================================";

   548 (*========== inhibit exn AK110719 ==============================================

   549 (* ERROR: get_pos *)

   550 states:=[];

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

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

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

   554  Iterator 1; moveActiveRoot 1;

   555  autoCalculate 1 CompleteCalc;

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

   558  show_pt pt;

   559 ============ inhibit exn AK110719 ============================================*)

   561 "-------------- move_dn ------------------------------------------";

   562 "-------------- move_dn ------------------------------------------";

   563 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   573    term2str (get_obj g_form pt [4]);

   574    *)

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

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

   577 (*

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

   579                                   Exception PTREE end of calculation*)

   580 (*========== inhibit exn AK110719 ==============================================

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

   582 ============ inhibit exn AK110719 ============================================*)

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

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

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

   589  (*states := [];

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

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

   592        ("Test",

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

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

   595  Iterator 1; moveActiveRoot 1;

   596  autoCalculate 1 CompleteCalcHead;

   597  autoCalculate 1 (Step 1);

   598  refFormula 1 (get_pos 1 1);

   600  moveActiveRoot 1;

   601  moveActiveDown 1;

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

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

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

   606  autoCalculate 1 (Step 1);

   607  refFormula 1 (get_pos 1 1);

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

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

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

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

   615 "-------------- move_up ------------------------------------------";

   616 "-------------- move_up ------------------------------------------";

   617 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   629                                   Exception PTREE begin of calculation*)

   630 (*========== inhibit exn AK110719 ==============================================

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

   632 ========== inhibit exn AK110719 ==============================================*)

   635 "------ move into detail -----------------------------------------";

   636 "------ move into detail -----------------------------------------";

   637 "------ move into detail -----------------------------------------";

   638  states:=[];

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

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

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

   642  Iterator 1; moveActiveRoot 1;

   643  autoCalculate 1 CompleteCalc;

   644  moveActiveRoot 1;

   645  moveActiveDown 1;

   646  moveActiveDown 1;

   647  moveActiveDown 1;

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

   650  interSteps 1 ([2],Res);

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

   653  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   667 "=====new ptree 3a ===============================================";

   668 "=====new ptree 3a ===============================================";

   669 "=====new ptree 3a ===============================================";

   670  states:=[];

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

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

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

   674  Iterator 1; moveActiveRoot 1;

   675  autoCalculate 1 CompleteCalcHead;

   676  autoCalculate 1 (Step 1);

   677  autoCalculate 1 (Step 1);

   678  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   689 (*

   690  get_obj g_ostate pt [1];

   691  show_pt pt;

   692 *)

   694 "-------------- move_dn in Incomplete ctree ----------------------";

   695 "-------------- move_dn in Incomplete ctree ----------------------";

   696 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   703 states:=[];

   704 CalcTree

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

   706 	   "solveFor x","solutions L"],

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

   708 Iterator 1; moveActiveRoot 1;

   709 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   735 writeln(pr_ptree pr_short pt);

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

   737  ###########################################################################*)

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

   739 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   751 (******************************************************************)

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

   753 (******************************************************************)

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

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

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

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

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

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

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

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

   762 www true [1,2];

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

   764 www true [1];

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

   767 local

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

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

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

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

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

   773 (*analoguous for tl*)

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

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

   777 (*see modspec.sml#pt_form

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

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

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

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

   782     in case cas of

   783 	   NONE => term2str (pblterm dI pI)

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

   785     end;

   786 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   821 in

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

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

   824 (1) the 'f' are given

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

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

   827 (2) the 't' ar given

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

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

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

   831 fun get_trace pt p q =

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

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

   834 end;

   836 writeln(pr_ptree pr_short pt);

   837 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   853     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   856 case get_trace pt [] [] of

   857     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

   863 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   869   development stopped in favour of move_dn, see get_interval

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

   871 *)

   872 (*

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

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

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

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

   877     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   880 *)

   882 (******************************************************************)

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

   884 (******************************************************************)

   887 "=====new ptree 4 ratequation ====================================";

   888 "=====new ptree 4 ratequation ====================================";

   889 "=====new ptree 4 ratequation ====================================";

   890 states:=[];

   891 CalcTree

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

   893 	   "solveFor x","solutions L"],

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

   895 Iterator 1; moveActiveRoot 1;

   896 autoCalculate 1 CompleteCalc;

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

   898 show_pt pt;

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

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

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

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

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

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

   907      Subproblem

   908          ("PolyEq",

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

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

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

   912 (*WN060717 unintentionally changed some rls/ord while

   913      completing knowl. for thes2file...

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

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

   917      *)Subproblem

   918          ("PolyEq",

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

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

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

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

   927 "=====new ptree 5 minisubpbl =====================================";

   928 "=====new ptree 5 minisubpbl =====================================";

   929 "=====new ptree 5 minisubpbl =====================================";

   930 states:=[];

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

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

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

   934 Iterator 1; moveActiveRoot 1;

   935 autoCalculate 1 CompleteCalc;

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

   937 show_pt pt;

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

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

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

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

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

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

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

   946      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   961     ("-1 + x = 0",

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

   963      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   984      []) => ()

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

   987 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

   995     ("[x = 1]",

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

   997      []) => ()

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

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

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

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

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

  1004 ========== inhibit exn AK110719 ==============================================*)

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

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

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

  1009 states:=[];

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

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

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

  1013 Iterator 1; moveActiveRoot 1;

  1014 autoCalculate 1 CompleteCalc;

  1015 interSteps 1 ([2],Res);

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

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

  1018 show_pt pt;

  1020 (**##############################################################**)

  1021 "-------------- get_allpos' new ----------------------------------";

  1022 "-------------- get_allpos' new ----------------------------------";

  1023 "-------------- get_allpos' new ----------------------------------";

  1024 "--- whole ctree";

  1025 print_depth 99;

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

  1027 print_depth 3;

  1028 if cuts =

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

  1030     ([1], Frm),

  1031     ([1], Res),

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

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

  1034     ([2], Res),

  1035     ([3], Pbl),

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

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

  1038     ([3, 2], Res),

  1039     ([3], Res),

  1040     ([4], Res),

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

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

  1044 print_depth 99;

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

  1046 print_depth 3;

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

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

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

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

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

  1053 if cuts =

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

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

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

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

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

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

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

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

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

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

  1067 if cuts =

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

  1069     ([3, 1], Res),

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

  1071     ([3, 2], Res),

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

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

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

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

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

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

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

  1081 if cuts =

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

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

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

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

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

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

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

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

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

  1093 if cuts =

  1094    [] then () else

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

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

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

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

  1102 (**#################################################################**)

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

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

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

  1106 show_pt pt;

  1107 val b = get_obj g_branch pt [];

  1108 if b = TransitiveB then () else

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

  1110 val b = get_obj g_branch pt [3];

  1111 if b = TransitiveB then () else

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

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

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

  1116 print_depth 99;

  1117 cuts;

  1118 print_depth 3;

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

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

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

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

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

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

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

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

  1129 print_depth 99;

  1130 cuts;

  1131 print_depth 3;

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

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

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

  1135 	   ([2], Res),

  1136 	   ([3], Pbl),

  1137 	   ([3, 1], Frm),

  1138 	   ([3, 1], Res),

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

  1140 	   ([3, 2], Res),

  1141 	   ([3], Res),

  1142 	   ([4], Res),

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

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

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

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

  1148 print_depth 99;

  1149 cuts;

  1150 print_depth 3;

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

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

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

  1154 	   ([3, 2], Res),

  1155 	   ([3], Res),

  1156 	   ([4], Res),

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

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

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

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

  1162 print_depth 99;

  1163 cuts;

  1164 print_depth 1;

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

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

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

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

  1169 show_pt pt';

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

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

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

  1175 show_pt pt;

  1177 (*========== inhibit exn AK110719 ==============================================

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

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

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

  1183 print_depth 99;

  1184 cuts;

  1185 print_depth 3;

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

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

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

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

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

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

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

  1194 print_depth 99;

  1195 afterins;

  1196 print_depth 3;

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

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

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

  1200 show_pt pt';

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

  1203 show_pt pt;

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

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

  1206 print_depth 99;

  1207 cuts;

  1208 print_depth 3;

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

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

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

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

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

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

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

  1216 print_depth 99;

  1217 afterins;

  1218 print_depth 3;

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

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

  1221 then () else

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

  1223 show_pt pt';

  1224 (*

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

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

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

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

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

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

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

  1233  *)

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

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

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

  1238 print_depth 99;

  1239 cuts;

  1240 print_depth 3;

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

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

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

  1244 	   ([3, 2], Res),

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

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

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

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

  1249 print_depth 99;

  1250 afterins;

  1251 print_depth 3;

  1252 if afterins =

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

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

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

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

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

  1258    use"ctree.sml";

  1259    *)

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

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

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

  1264 print_depth 99;

  1265 cuts;

  1266 print_depth 3;

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

  1268 	   ([3, 2], Res),

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

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

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

  1273 print_depth 99;

  1274 afterins;

  1275 print_depth 3;

  1276 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1280 	       ([2], Res),

  1281 	       ([3], Pbl),

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

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

  1284 	       ([4], Res),

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

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

  1287 *)

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

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

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

  1291 	       ([2], Res),

  1292 	       ([3], Pbl),

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

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

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

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

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

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

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

  1302 print_depth 99;

  1303 cuts;

  1304 print_depth 3;

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

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

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

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

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

  1310 print_depth 99;

  1311 afterins;

  1312 print_depth 3;

  1313 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1317 	       ([2], Res),

  1318 	       ([3], Pbl),

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

  1320 	       ([3], Res),

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

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

  1323 *)

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

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

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

  1327 	       ([2], Res),

  1328 	       ([3], Pbl),

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

  1330 then () else

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

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

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

  1336 "---(6++) on S(606)..S(608)--------";

  1337 (**)

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

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

  1340 print_depth 99;

  1341 cuts;

  1342 print_depth 1;

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

  1344 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1345 then () else

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

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

  1348 print_depth 99;

  1349 afterins;

  1350 print_depth 3;

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

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

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

  1354 	       ([2], Res),

  1355 	       ([3], Pbl),

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

  1357 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1358 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1361 (*

  1362 show_pt pt';

  1363 show_pt pt;

  1364 *)

  1365 ========== inhibit exn AK110719 ==============================================*)

author	Alexander Kargl <akargl@brgkepler.net>
	Tue, 26 Jul 2011 09:38:07 +0200
branch	decompose-isar
changeset 42190	a48e6fdc934c
parent 42185	332a0653d4c9
child 42193	06de2f62f744
permissions	-rw-r--r--