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

     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 "-------------- subst2subs subs2subst sube2subst subte2subst -----";

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

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

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

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

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

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

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

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

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

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

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

    63 (get_ctxt pt p)

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

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

    66 (get_ctxt pt p)

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

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

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

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

    72 val pt = EmptyPtree;

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

    74 val ctxt = get_obj g_ctxt pt [];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    92    *)

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

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

    95    *)

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

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

    98    *)

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

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

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

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

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

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

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

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

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

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

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

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

   112 "----------------------------------------------------------------/";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   134 val FormKF res = f;

   135 if res = "[x = 1]"

   136 then case nxt of ("End_Proof'", End_Proof') => ()

   137   | _ => error "new behaviour in test: miniscript with mini-subpbl 1"

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

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

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

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

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

   212 show_pt pt;

   213 show_pt pt';

   214 default_print_depth 99; cuts; default_print_depth 3;

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

   217 	   ([3], Frm),

   218 	   ([3, 1], Frm),

   219 	   ([3, 1], Res),

   220 	   ([3, 2], Res),

   221 	   ([3], Res),

   222 	   ([4], Res)]

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

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

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

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

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

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

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

   232 (*============ inhibit exn AK110726 ==============================================

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

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

   235 ============ inhibit exn AK110726 ==============================================*)

   236 (*============ inhibit exn AK110726 ==============================================

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

   238    [([], Frm),

   239     ([1], Frm),

   240     ([1], Res),

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

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

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

   244 ============ inhibit exn AK110726 ==============================================*)

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

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

   248 	   ([3, 1], Frm),

   249 	   ([3, 1], Res),

   250 	   ([3, 2], Res),

   251 	   ([3], Res),

   252 	   ([4], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   276 (*============ inhibit exn AK110726 ==============================================

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

   278 	   ([3], Frm),

   279 	   ([3, 1], Frm),

   280 	   ([3, 1], Res),

   281 	   ([3, 2], Res),

   282 	   ([3], Res),

   283 	   ([4], Res),

   284 	   ([], Res)]

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

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

   288 ============ inhibit exn AK110726 ==============================================*)

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

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

   293 (*============ inhibit exn AK110726 ==============================================

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

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

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

   297 ============ inhibit exn AK110726 ==============================================*)

   298 (* AK110727 Debuging

   299   (* get_obj g_form pt' [2];

   300     (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"

   301           raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)

   302 "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)

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

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

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

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

   309    [([], Frm),

   310     ([1], Frm),

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

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

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

   315 (*============ inhibit exn AK110726 ==============================================

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

   317 	   ([3, 1], Frm),

   318 	   ([3, 1], Res),

   319 	   ([3, 2], Res),

   320 	   ([3], Res),

   321 	   ([4], Res),

   322 	   ([], Res)]

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

   324 ============ inhibit exn AK110726 ==============================================*)

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

   327 (*============ inhibit exn AK110726 ==============================================

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

   329 	   ([3, 2], Res),

   330 	   ([3], Res),

   331 	   ([4], Res),

   332 	   ([], Res)]

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

   334 ============ inhibit exn AK110726 ==============================================*)

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

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

   338 	   ([3], Res),

   339 	   ([4], Res),

   340 	   ([], Res)]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   359 show_pt pt;

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

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

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

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

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

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

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

   370 if cuts = []

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

   373 (*WN050219

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

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

   378 show_pt pt;

   379 show_pt pt';

   380 default_print_depth 99;cuts;default_print_depth 3;

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

   382 ####################################################################*)

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

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

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

   389 reset_states ();

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

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

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

   393  Iterator 1; moveActiveRoot 1;

   394  autoCalculate 1 CompleteCalc;

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

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

   399  show_pt pt;

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

   402 else error "mini-subpbl interSteps broken";

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

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

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

   407 (*WN050225 intermed. outcommented

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

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

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

   411 	    ([3, 2], Res),

   412 	    ([3], Res),

   413 	    ([4], Res)]

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

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

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

   418 	    ([3, 2], Res),

   419 	    ([3], Res),

   420 	    ([4], Res)]

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

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

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

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

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

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

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

   430 	   ([3, 2], Res),

   431 	   ([3], Res),

   432 	   ([4], Res),

   433 	   ([], Res)]

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

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

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

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

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

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

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

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

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

   444 	   ([3, 2], Res),

   445 	   ([3], Res),

   446 	   ([4], Res),

   447 	   ([], Res)]

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

   452 "-------------- cappend minisubpbl -------------------------------";

   453 "-------------- cappend minisubpbl -------------------------------";

   454 "-------------- cappend minisubpbl -------------------------------";

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

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

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

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

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

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

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

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

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

   464    *)

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

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

   467    *)

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

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

   470    *)

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

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

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

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

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

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

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

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

   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 = 2" andalso res = e_term then () else

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

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

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

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

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

   489 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

   501 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   520 (* ...complete calchead skipped...*)

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

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

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

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

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

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

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

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

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

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

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

   534 val (pt,cuts) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   551 WN050225 intermed. outcommented---*)

   553 "=====new ptree 3 ================================================";

   554 "=====new ptree 3 ================================================";

   555 "=====new ptree 3 ================================================";

   557 reset_states ();

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

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

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

   561  Iterator 1; moveActiveRoot 1;

   562  autoCalculate 1 CompleteCalc;

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

   565  show_pt pt;

   567 "-------------- move_dn ------------------------------------------";

   568 "-------------- move_dn ------------------------------------------";

   569 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

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

   579    term2str (get_obj g_form pt [4]);

   580    *)

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

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

   583 (*

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

   585                                   Exception PTREE end of calculation*)

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

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

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

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

   592  reset_states ();

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

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

   595        ("Test",

   596 	["LINEAR","univariate","equation","test"],

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

   598  Iterator 1; moveActiveRoot 1;

   599  autoCalculate 1 CompleteCalcHead;

   600  autoCalculate 1 (Step 1);

   601  refFormula 1 (get_pos 1 1);

   603  moveActiveRoot 1;

   604  moveActiveDown 1;

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

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

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

   609  autoCalculate 1 (Step 1);

   610  refFormula 1 (get_pos 1 1);

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

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

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

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

   618 "-------------- move_up ------------------------------------------";

   619 "-------------- move_up ------------------------------------------";

   620 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

   632                                   Exception PTREE begin of calculation*)

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

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

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

   638 "------ move into detail -----------------------------------------";

   639  reset_states ();

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

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

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

   643  Iterator 1; moveActiveRoot 1;

   644  autoCalculate 1 CompleteCalc;

   645  moveActiveRoot 1;

   646  moveActiveDown 1;

   647  moveActiveDown 1;

   648  moveActiveDown 1;

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

   651  interSteps 1 ([2],Res);

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

   654  val p = get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

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

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

   670 "=====new ptree 3a ===============================================";

   671  reset_states ();

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

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

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

   675  Iterator 1; moveActiveRoot 1;

   676  autoCalculate 1 CompleteCalcHead;

   677  autoCalculate 1 (Step 1);

   678  autoCalculate 1 (Step 1);

   679  autoCalculate 1 (Step 1);

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

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

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

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

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

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

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

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

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

   690 (*

   691  get_obj g_ostate pt [1];

   692  show_pt pt;

   693 *)

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

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

   697 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

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

   704 reset_states ();

   705 CalcTree

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

   707 	   "solveFor x","solutions L"],

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

   709 Iterator 1; moveActiveRoot 1;

   710 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   736 writeln(pr_ptree pr_short pt);

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

   738  ###########################################################################*)

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

   740 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

   752 (******************************************************************)

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

   754 (******************************************************************)

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

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

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

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

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

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

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

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

   763 www true [1,2];

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

   765 www true [1];

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

   768 local

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

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

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

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

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

   774 (*analoguous for tl*)

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

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

   778 (*see modspec.sml#pt_form

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

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

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

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

   783     in case cas of

   784 	   NONE => term2str (pblterm dI pI)

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

   786     end;

   787 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   822 in

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

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

   825 (1) the 'f' are given

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

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

   828 (2) the 't' ar given

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

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

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

   832 fun get_trace pt p q =

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

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

   835 end;

   837 writeln(pr_ptree pr_short pt);

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

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

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

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

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

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

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

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

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

   850 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

   856 ========== inhibit exn AK110719 ==============================================*)

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

   859     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

   863 (*========== inhibit exn AK110719 ==============================================

   864 case get_trace pt [] [] of

   865     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

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

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

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

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

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

   871 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   877   development stopped in favour of move_dn, see get_interval

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

   879 *)

   880 (*

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

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

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

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

   885     [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

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

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

   888 *)

   890 (******************************************************************)

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

   892 (******************************************************************)

   895 "=====new ptree 4 ratequation ====================================";

   896 "=====new ptree 4 ratequation ====================================";

   897 "=====new ptree 4 ratequation ====================================";

   898 reset_states ();

   899 CalcTree

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

   901 	   "solveFor x","solutions L"],

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

   903 Iterator 1; moveActiveRoot 1;

   904 autoCalculate 1 CompleteCalc;

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

   906 val p = get_pos 1 1;

   907 val (Form f, tac, asms) = pt_extract (pt, p);

   908 (*============ inhibit exn WN120316 ==============================================

   909 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()

   910   else error "after ===new ptree 4 ratequation ===";

   911 (*WN120317.TODO dropped rateq*)

   912 ============ inhibit exn WN120316 ==============================================*)

   913 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)

   914 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)

   915 then () else error "after ===new ptree 4 ratequation ===";

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

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

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

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

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

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

   924      Subproblem

   925          ("PolyEq",

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

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

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

   929 (*WN060717 unintentionally changed some rls/ord while

   930      completing knowl. for thes2file...

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

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

   934      *)Subproblem

   935          ("PolyEq",

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

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

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

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

   944 "=====new ptree 5 minisubpbl =====================================";

   945 "=====new ptree 5 minisubpbl =====================================";

   946 "=====new ptree 5 minisubpbl =====================================";

   947 reset_states ();

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

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

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

   951 Iterator 1; moveActiveRoot 1;

   952 autoCalculate 1 CompleteCalc;

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

   954 show_pt pt;

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

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

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

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

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

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

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

   963      []) => ()

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

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

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

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

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

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

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

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

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

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

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

   978     ("-1 + x = 0",

   979      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

   980      []) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1000     ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],

  1001      []) => ()

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

  1004 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

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

  1012     ("[x = 1]",

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

  1014      []) => ()

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

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

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

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

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

  1021 ========== inhibit exn AK110719 ==============================================*)

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

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

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

  1026 reset_states ();

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

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

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

  1030 Iterator 1; moveActiveRoot 1;

  1031 autoCalculate 1 CompleteCalc;

  1032 interSteps 1 ([2],Res);

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

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

  1035 show_pt pt;

  1037 (**##############################################################**)

  1038 "-------------- get_allpos' new ----------------------------------";

  1039 "-------------- get_allpos' new ----------------------------------";

  1040 "-------------- get_allpos' new ----------------------------------";

  1041 "--- whole ctree";

  1042 default_print_depth 99;

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

  1044 default_print_depth 3;

  1045 if cuts =

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

  1047     ([1], Frm),

  1048     ([1], Res),

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

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

  1051     ([2], Res),

  1052     ([3], Pbl),

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

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

  1055     ([3, 2], Res),

  1056     ([3], Res),

  1057     ([4], Res),

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

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

  1061 default_print_depth 99;

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

  1063 default_print_depth 3;

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

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

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

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

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

  1070 if cuts =

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

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

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

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

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

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

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

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

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

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

  1084 if cuts =

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

  1086     ([3, 1], Res),

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

  1088     ([3, 2], Res),

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

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

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

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

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

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

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

  1098 if cuts =

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

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

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

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

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

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

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

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

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

  1110 if cuts =

  1111    [] then () else

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

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

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

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

  1119 (**#################################################################**)

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

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

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

  1123 show_pt pt;

  1124 val b = get_obj g_branch pt [];

  1125 if b = TransitiveB then () else

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

  1127 val b = get_obj g_branch pt [3];

  1128 if b = TransitiveB then () else

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

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

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

  1133 default_print_depth 99;

  1134 cuts;

  1135 default_print_depth 3;

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

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

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

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

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

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

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

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

  1146 default_print_depth 99;

  1147 cuts;

  1148 default_print_depth 3;

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

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

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

  1152 	   ([2], Res),

  1153 	   ([3], Pbl),

  1154 	   ([3, 1], Frm),

  1155 	   ([3, 1], Res),

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

  1157 	   ([3, 2], Res),

  1158 	   ([3], Res),

  1159 	   ([4], Res),

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

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

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

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

  1165 default_print_depth 99;

  1166 cuts;

  1167 default_print_depth 3;

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

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

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

  1171 	   ([3, 2], Res),

  1172 	   ([3], Res),

  1173 	   ([4], Res),

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

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

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

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

  1179 default_print_depth 99;

  1180 cuts;

  1181 default_print_depth 1;

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

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

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

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

  1186 show_pt pt';

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

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

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

  1192 show_pt pt;

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

  1195 (*========== inhibit exn AK110726 ==============================================

  1196 (* ERROR: Can't unify istate to istate * Proof.context *)

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

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

  1200 default_print_depth 99;

  1201 cuts;

  1202 default_print_depth 3;

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

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

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

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

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

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

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

  1211 default_print_depth 99;

  1212 afterins;

  1213 default_print_depth 3;

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

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

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

  1217 show_pt pt';

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

  1219 show_pt pt;

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

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

  1222 default_print_depth 99;

  1223 cuts;

  1224 default_print_depth 3;

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

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

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

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

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

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

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

  1235 default_print_depth 99;

  1236 afterins;

  1237 default_print_depth 3;

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

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

  1241 then () else

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

  1243 show_pt pt';

  1246 (*

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

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

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

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

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

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

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

  1255  *)

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

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

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

  1260 default_print_depth 99;

  1261 cuts;

  1262 default_print_depth 3;

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

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

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

  1266 	   ([3, 2], Res),

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

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

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

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

  1271 default_print_depth 99;

  1272 afterins;

  1273 default_print_depth 3;

  1274 if afterins =

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

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

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

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

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

  1280    use"ctree.sml";

  1281    *)

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

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

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

  1286 default_print_depth 99;

  1287 cuts;

  1288 default_print_depth 3;

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

  1290 	   ([3, 2], Res),

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

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

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

  1295 default_print_depth 99;

  1296 afterins;

  1297 default_print_depth 3;

  1298 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1302 	       ([2], Res),

  1303 	       ([3], Pbl),

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

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

  1306 	       ([4], Res),

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

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

  1309 *)

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

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

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

  1313 	       ([2], Res),

  1314 	       ([3], Pbl),

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

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

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

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

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

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

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

  1324 default_print_depth 99;

  1325 cuts;

  1326 default_print_depth 3;

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

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

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

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

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

  1332 default_print_depth 99;

  1333 afterins;

  1334 default_print_depth 3;

  1335 (*WN060727 replaced after overwriting cutlevup by test_trans

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

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

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

  1339 	       ([2], Res),

  1340 	       ([3], Pbl),

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

  1342 	       ([3], Res),

  1343 	       ([4], Res), ([], Res)] then () else

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

  1345 *)

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

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

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

  1349 	       ([2], Res),

  1350 	       ([3], Pbl),

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

  1352 then () else

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

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

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

  1358 "---(6++) on S(606)..S(608)--------";

  1359 (**)

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

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

  1362 default_print_depth 99;

  1363 cuts;

  1364 default_print_depth 1;

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

  1366 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]

  1367 then () else

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

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

  1370 default_print_depth 99;

  1371 afterins;

  1372 default_print_depth 3;

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

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

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

  1376 	       ([2], Res),

  1377 	       ([3], Pbl),

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

  1379 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1380 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

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

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

  1383 (*

  1384 show_pt pt';

  1385 show_pt pt;

  1386 *)

  1387 ========== inhibit exn AK110726 ==============================================*)

  1389 "-------------- subst2subs subs2subst sube2subst subte2subst -----";

  1390 "-------------- subst2subs subs2subst sube2subst subte2subst -----";

  1391 "-------------- subst2subs subs2subst sube2subst subte2subst -----";

  1392 val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];

  1394 if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()

  1395 else error "subte2sube broken";

  1397 subst2subs : (term * term) list -> string list;

  1398 if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()

  1399 else error "subst2subs broken";

  1401 subst2subs' : (term * term) list -> (string * string) list;

  1402 if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()

  1403 else error "subst2subs' broken";

  1405 subs2subst : theory -> string list -> (term * term) list;

  1406 val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];

  1407 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso

  1408   term2str i2 = "err" andalso term2str v2 = "0" then ()

  1409 else error "subs2subst broken";

  1411 sube2subst : theory -> string list -> (term * term) list;

  1412 val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];

  1413 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso

  1414   term2str i2 = "err" andalso term2str v2 = "0" then ()

  1415 else error "sube2subst broken";

  1417 sube2subte : string list -> term list;

  1418 val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];

  1419 if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()

  1420 else error "sube2subte broken";

  1422 val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];

  1423 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso

  1424   term2str i2 = "err" andalso term2str v2 = "0" then ()

  1425 else error "subte2subst broken";

author	Walther Neuper <wneuper@ist.tugraz.at>
	Wed, 14 Dec 2016 10:45:41 +0100
changeset 59267	aab874fdd910
parent 59253	f0bb15a046ae
child 59279	255c853ea2f0
permissions	-rw-r--r--