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

     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 "-------------- cut_level (from ptree above)----------------------";

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

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

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

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

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

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

    27 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

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

    38 (*              val SAVE_get_trace = get_trace;                   *)

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

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

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

    42 (*              val get_trace = SAVE_get_trace;                   *)

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

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

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

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

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

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

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

    50 "-------------- get_allpos' new ----------------------------------";

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

    52 "-----------------------------------------------------------------";

    53 "-----------------------------------------------------------------";

    54 "-----------------------------------------------------------------";

    57 "-------------- fun get_ctxt -------------------------------------";

    58 "-------------- fun get_ctxt -------------------------------------";

    59 "-------------- fun get_ctxt -------------------------------------";

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

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

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

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

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

    65 (get_ctxt pt p)

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

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

    68 (get_ctxt pt p)

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

    71 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    72 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    73 "-------------- fun update_ctxt, fun g_ctxt ----------------------";

    74 val pt = EmptyPtree;

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

    76 val ctxt = get_obj g_ctxt pt [];

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

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

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

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

    82 "-------------- check positions in miniscript --------------------";

    83 "-------------- check positions in miniscript --------------------";

    84 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

    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;

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

   100    *)

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

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

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

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

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

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

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

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

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

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

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

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

   114 "----------------------------------------------------------------/";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   140  show_pt pt;

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

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

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

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

   146    [([], Frm),

   147     ([1], Frm),

   148     ([1], Res),

   149     ([2], Res),

   150     ([3], Frm),

   151     ([3, 1], Frm),

   152     ([3, 1], Res),

   153     ([3, 2], Res),

   154     ([3], Res),

   155     ([4], Res),

   156     ([], Res)]

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

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

   160    [([1], Frm),

   161     ([1], Res),

   162     ([2], Res),

   163     ([3], Frm),

   164     ([3, 1], Frm),

   165     ([3, 1], Res),

   166     ([3, 2], Res),

   167     ([3], Res),

   168     ([4], Res)]

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

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

   172    [([2], Res),

   173     ([3], Frm),

   174     ([3, 1], Frm),

   175     ([3, 1], Res),

   176     ([3, 2], Res),

   177     ([3], Res),

   178     ([4], Res)]

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

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

   182    [([3], Frm),

   183     ([3, 1], Frm),

   184     ([3, 1], Res),

   185     ([3, 2], Res),

   186     ([3], Res),

   187     ([4], Res)]

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

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

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

   192     ([3, 1], Res),

   193     ([3, 2], Res)]

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

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

   197    [([3], Frm),

   198     ([3, 1], Frm),

   199     ([3, 1], Res),

   200     ([3, 2], Res),

   201     ([3], Res)]

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

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

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

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

   208 show_pt pt;

   209 show_pt pt';

   210 print_depth 99; cuts; print_depth 3;

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

   213 	   ([3], Frm),

   214 	   ([3, 1], Frm),

   215 	   ([3, 1], Res),

   216 	   ([3, 2], Res),

   217 	   ([3], Res),

   218 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

   230    [([], Frm),

   231     ([1], Frm),

   232     ([1], Res),

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

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

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

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

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

   240 	   ([3, 1], Frm),

   241 	   ([3, 1], Res),

   242 	   ([3, 2], Res),

   243 	   ([3], Res),

   244 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   268 	   ([3], Frm),

   269 	   ([3, 1], Frm),

   270 	   ([3, 1], Res),

   271 	   ([3, 2], Res),

   272 	   ([3], Res),

   273 	   ([4], Res),

   274 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

   290    [([], Frm),

   291     ([1], Frm),

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

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

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

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

   297 	   ([3, 1], Frm),

   298 	   ([3, 1], Res),

   299 	   ([3, 2], Res),

   300 	   ([3], Res),

   301 	   ([4], Res),

   302 	   ([], Res)]

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

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

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

   307 	   ([3, 2], Res),

   308 	   ([3], Res),

   309 	   ([4], Res),

   310 	   ([], Res)]

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

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

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

   315 	   ([3], Res),

   316 	   ([4], Res),

   317 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   337 show_pt pt;

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

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

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

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

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

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

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

   348 if cuts = []

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

   351 (*WN050219

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

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

   356 show_pt pt;

   357 show_pt pt';

   358 print_depth 99;cuts;print_depth 3;

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

   360 ####################################################################*)*)

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

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

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

   365  states:=[];

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

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

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

   369  Iterator 1; moveActiveRoot 1;

   370  autoCalculate 1 CompleteCalc;

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

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

   375  show_pt pt;

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

   378 else error "mini-subpbl interSteps broken";

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

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

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

   383 (*WN050225 intermed. outcommented

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

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

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

   387 	    ([3, 2], Res),

   388 	    ([3], Res),

   389 	    ([4], Res)]

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

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

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

   394 	    ([3, 2], Res),

   395 	    ([3], Res),

   396 	    ([4], Res)]

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

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

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

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

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

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

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

   406 	   ([3, 2], Res),

   407 	   ([3], Res),

   408 	   ([4], Res),

   409 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   420 	   ([3, 2], Res),

   421 	   ([3], Res),

   422 	   ([4], Res),

   423 	   ([], Res)]

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

   428 "-------------- cappend minisubpbl -------------------------------";

   429 "-------------- cappend minisubpbl -------------------------------";

   430 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   440    *)

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

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

   443    *)

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

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

   446    *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   465 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   477 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   496 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   510 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   527 WN050225 intermed. outcommented---*)

   529 "=====new ptree 3 ================================================";

   530 "=====new ptree 3 ================================================";

   531 "=====new ptree 3 ================================================";

   533 (*========== inhibit exn AK110719 ==============================================

   534 (* ERROR: get_pos *)

   535 states:=[];

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

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

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

   539  Iterator 1; moveActiveRoot 1;

   540  autoCalculate 1 CompleteCalc;

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

   543  show_pt pt;

   544 ============ inhibit exn AK110719 ============================================*)

   546 "-------------- move_dn ------------------------------------------";

   547 "-------------- move_dn ------------------------------------------";

   548 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   558    term2str (get_obj g_form pt [4]);

   559    *)

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

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

   562 (*

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

   564                                   Exception PTREE end of calculation*)

   565 (*========== inhibit exn AK110719 ==============================================

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

   567 ============ inhibit exn AK110719 ============================================*)

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

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

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

   574  (*states := [];

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

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

   577        ("Test",

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

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

   580  Iterator 1; moveActiveRoot 1;

   581  autoCalculate 1 CompleteCalcHead;

   582  autoCalculate 1 (Step 1);

   583  refFormula 1 (get_pos 1 1);

   585  moveActiveRoot 1;

   586  moveActiveDown 1;

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

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

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

   591  autoCalculate 1 (Step 1);

   592  refFormula 1 (get_pos 1 1);

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

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

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

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

   600 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

   614                                   Exception PTREE begin of calculation*)

   615 (*========== inhibit exn AK110719 ==============================================

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

   617 ========== inhibit exn AK110719 ==============================================*)

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

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

   622 "------ move into detail -----------------------------------------";

   623  states:=[];

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

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

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

   627  Iterator 1; moveActiveRoot 1;

   628  autoCalculate 1 CompleteCalc;

   629  moveActiveRoot 1;

   630  moveActiveDown 1;

   631  moveActiveDown 1;

   632  moveActiveDown 1;

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

   635  interSteps 1 ([2],Res);

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

   638  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

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

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

   654 "=====new ptree 3a ===============================================";

   655  states:=[];

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

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

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

   659  Iterator 1; moveActiveRoot 1;

   660  autoCalculate 1 CompleteCalcHead;

   661  autoCalculate 1 (Step 1);

   662  autoCalculate 1 (Step 1);

   663  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   674 (*

   675  get_obj g_ostate pt [1];

   676  show_pt pt;

   677 *)

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

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

   681 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   688 states:=[];

   689 CalcTree

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

   691 	   "solveFor x","solutions L"],

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

   693 Iterator 1; moveActiveRoot 1;

   694 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   720 writeln(pr_ptree pr_short pt);

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

   722  ###########################################################################*)

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

   724 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   733 (******************************************************************)

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

   735 (******************************************************************)

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

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

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

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

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

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

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

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

   744 www true [1,2];

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

   746 www true [1];

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

   749 local

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

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

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

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

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

   755 (*analoguous for tl*)

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

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

   759 (*see modspec.sml#pt_form

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

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

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

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

   764     in case cas of

   765 	   NONE => term2str (pblterm dI pI)

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

   767     end;

   768 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   803 in

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

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

   806 (1) the 'f' are given

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

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

   809 (2) the 't' ar given

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

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

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

   813 fun get_trace pt p q =

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

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

   816 end;

   818 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

   828 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

   834 ========== inhibit exn AK110719 ==============================================*)

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

   836     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   839 (*========== inhibit exn AK110719 ==============================================

   840 case get_trace pt [] [] of

   841     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

   842      [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 1f";

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

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

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

   847 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   853   development stopped in favour of move_dn, see get_interval

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

   855 *)

   856 (*

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

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

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

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

   861     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   864 *)

   866 (******************************************************************)

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

   868 (******************************************************************)

   871 "=====new ptree 4 ratequation ====================================";

   872 "=====new ptree 4 ratequation ====================================";

   873 "=====new ptree 4 ratequation ====================================";

   874 states:=[];

   875 CalcTree

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

   877 	   "solveFor x","solutions L"],

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

   879 Iterator 1; moveActiveRoot 1;

   880 autoCalculate 1 CompleteCalc;

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

   882 show_pt pt;

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

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

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

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

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

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

   891      Subproblem

   892          ("PolyEq",

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

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

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

   896 (*WN060717 unintentionally changed some rls/ord while

   897      completing knowl. for thes2file...

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

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

   901      *)Subproblem

   902          ("PolyEq",

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

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

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

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

   911 "=====new ptree 5 minisubpbl =====================================";

   912 "=====new ptree 5 minisubpbl =====================================";

   913 "=====new ptree 5 minisubpbl =====================================";

   914 states:=[];

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

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

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

   918 Iterator 1; moveActiveRoot 1;

   919 autoCalculate 1 CompleteCalc;

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

   921 show_pt pt;

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

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

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

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

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

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

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

   930      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   945     ("-1 + x = 0",

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

   947      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   968      []) => ()

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

   971 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

   979     ("[x = 1]",

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

   981      []) => ()

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

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

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

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

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

   988 ========== inhibit exn AK110719 ==============================================*)

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

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

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

   993 states:=[];

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

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

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

   997 Iterator 1; moveActiveRoot 1;

   998 autoCalculate 1 CompleteCalc;

   999 interSteps 1 ([2],Res);

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

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

  1002 show_pt pt;

  1004 (**##############################################################**)

  1005 "-------------- get_allpos' new ----------------------------------";

  1006 "-------------- get_allpos' new ----------------------------------";

  1007 "-------------- get_allpos' new ----------------------------------";

  1008 "--- whole ctree";

  1009 print_depth 99;

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

  1011 print_depth 3;

  1012 if cuts =

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

  1014     ([1], Frm),

  1015     ([1], Res),

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

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

  1018     ([2], Res),

  1019     ([3], Pbl),

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

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

  1022     ([3, 2], Res),

  1023     ([3], Res),

  1024     ([4], Res),

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

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

  1028 print_depth 99;

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

  1030 print_depth 3;

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

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

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

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

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

  1037 if cuts =

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

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

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

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

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

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

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

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

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

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

  1051 if cuts =

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

  1053     ([3, 1], Res),

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

  1055     ([3, 2], Res),

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

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

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

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

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

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

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

  1065 if cuts =

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

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

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

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

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

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

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

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

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

  1077 if cuts =

  1078    [] then () else

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

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

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

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

  1086 (**#################################################################**)

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

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

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

  1090 show_pt pt;

  1091 val b = get_obj g_branch pt [];

  1092 if b = TransitiveB then () else

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

  1094 val b = get_obj g_branch pt [3];

  1095 if b = TransitiveB then () else

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

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

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

  1100 print_depth 99;

  1101 cuts;

  1102 print_depth 3;

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

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

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

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

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

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

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

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

  1113 print_depth 99;

  1114 cuts;

  1115 print_depth 3;

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

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

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

  1119 	   ([2], Res),

  1120 	   ([3], Pbl),

  1121 	   ([3, 1], Frm),

  1122 	   ([3, 1], Res),

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

  1124 	   ([3, 2], Res),

  1125 	   ([3], Res),

  1126 	   ([4], Res),

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

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

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

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

  1132 print_depth 99;

  1133 cuts;

  1134 print_depth 3;

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

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

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

  1138 	   ([3, 2], Res),

  1139 	   ([3], Res),

  1140 	   ([4], Res),

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

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

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

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

  1146 print_depth 99;

  1147 cuts;

  1148 print_depth 1;

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

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

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

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

  1153 show_pt pt';

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

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

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

  1159 show_pt pt;

  1161 (*========== inhibit exn AK110719 ==============================================

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

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

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

  1167 print_depth 99;

  1168 cuts;

  1169 print_depth 3;

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

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

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

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

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

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

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

  1178 print_depth 99;

  1179 afterins;

  1180 print_depth 3;

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

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

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

  1184 show_pt pt';

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

  1187 show_pt pt;

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

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

  1190 print_depth 99;

  1191 cuts;

  1192 print_depth 3;

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

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

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

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

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

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

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

  1200 print_depth 99;

  1201 afterins;

  1202 print_depth 3;

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

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

  1205 then () else

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

  1207 show_pt pt';

  1208 (*

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

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

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

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

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

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

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

  1217  *)

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

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

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

  1222 print_depth 99;

  1223 cuts;

  1224 print_depth 3;

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

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

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

  1228 	   ([3, 2], Res),

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

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

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

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

  1233 print_depth 99;

  1234 afterins;

  1235 print_depth 3;

  1236 if afterins =

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

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

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

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

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

  1242    use"ctree.sml";

  1243    *)

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

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

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

  1248 print_depth 99;

  1249 cuts;

  1250 print_depth 3;

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

  1252 	   ([3, 2], Res),

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

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

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

  1257 print_depth 99;

  1258 afterins;

  1259 print_depth 3;

  1260 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1264 	       ([2], Res),

  1265 	       ([3], Pbl),

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

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

  1268 	       ([4], Res),

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

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

  1271 *)

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

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

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

  1275 	       ([2], Res),

  1276 	       ([3], Pbl),

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

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

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

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

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

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

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

  1286 print_depth 99;

  1287 cuts;

  1288 print_depth 3;

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

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

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

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

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

  1294 print_depth 99;

  1295 afterins;

  1296 print_depth 3;

  1297 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1301 	       ([2], Res),

  1302 	       ([3], Pbl),

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

  1304 	       ([3], Res),

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

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

  1307 *)

  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 then () else

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

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

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

  1320 "---(6++) on S(606)..S(608)--------";

  1321 (**)

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

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

  1324 print_depth 99;

  1325 cuts;

  1326 print_depth 1;

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

  1328 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1329 then () else

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

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

  1332 print_depth 99;

  1333 afterins;

  1334 print_depth 3;

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

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

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

  1338 	       ([2], Res),

  1339 	       ([3], Pbl),

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

  1341 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1342 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1345 (*

  1346 show_pt pt';

  1347 show_pt pt;

  1348 *)

  1349 ========== inhibit exn AK110719 ==============================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 25 Jul 2011 17:44:19 +0200
branch	decompose-isar
changeset 42185	332a0653d4c9
parent 42124	ba52b628c40c
child 42190	a48e6fdc934c
permissions	-rw-r--r--