wneuper/isa: test/Tools/isac/MathEngBasic/ctree.sml@f92963a33fe3

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

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

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

    16 "-------------- cut_level (from ctree above)----------------------";

    17 "-------------- cut_tree (from ctree above)-----------------------";

    18 "=====new ctree 1a miniscript with mini-subpbl ===================";

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

    20 "=====new ctree 2 miniscript with mini-subpbl ====================";

    21 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

    22 "-------------- cappend (from ctree above)------------------------";

    23 "-------------- cappend minisubpbl -------------------------------";

    24 "=====new ctree 3 ================================================";

    25 "-------------- move_dn ------------------------------------------";

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

    27 "-------------- move_up ------------------------------------------";

    28 "------ move into detail -----------------------------------------";

    29 "=====new ctree 3a ===============================================";

    30 "-------------- move_dn in Incomplete ctree ----------------------";

    31 "=====new ctree 4: crooked by cut_level_'_ =======================";

    32 (*//############## development stopped 0501 ########################\\*)

    33 (******************************************************************)

    34 (*              val SAVE_get_trace = get_trace;                   *)

    35 (******************************************************************)

    36 "-------------- ME_Misc.get_interval from ctree: incremental development--";

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

    38 (*              val get_trace = SAVE_get_trace;                   *)

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

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

    41 "=====new ctree 4 ratequation ====================================";

    42 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";

    43 "=====new ctree 5 minisubpbl =====================================";

    44 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";

    45 "=====new ctree 6 minisubpbl intersteps ==========================";

    46 "-------------- get_allpos' new ----------------------------------";

    47 "-------------- cut_tree new (from ctree above)-------------------";

    48 "-------------- repl_app------------------------------------------";

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

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

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

    54 "-------------- fun get_ctxt, g_ctxt -----------------------------";

    55 "-------------- fun get_ctxt, g_ctxt -----------------------------";

    56 "-------------- fun get_ctxt, g_ctxt -----------------------------";

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

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

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

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

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

    62 case \<^try>\<open> (get_ctxt pt p)\<close> of

    63   SOME x => x

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

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

    66 case \<^try>\<open> (get_ctxt pt p)\<close> of

    67   SOME x => x

    68 | NONE => error "--- fun get_ctxt not even some ctxt found in PrfObj";

    70 val pt = EmptyPtree;

    71 val pt = append_problem [] (Istate.empty, ContextC.empty) Formalise.empty ([(*oris*)], References.empty, TermC.empty, ContextC.empty) pt;

    72 val ctxt = get_obj g_ctxt pt [];

    73 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";

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

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

    77 "-------------- check positions in miniscript --------------------";

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

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

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

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

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

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

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

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

    86    (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

    87    *)

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

    89 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

    90    *)

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

    92 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

    93    *)

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

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

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

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

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

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

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

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

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

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

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

   106 val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.parse_test @{context} "Inform[1]");

   107 "----------------------------------------------------------------/";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   129 val Test_Out.FormKF res = f;

   130 if res = "[x = 1]"

   131 then case nxt of End_Proof' => ()

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

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

   135  Test_Tool.show_pt pt;

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

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

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

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

   141    [([], Frm),

   142     ([1], Frm),

   143     ([1], Res),

   144     ([2], Res),

   145     ([3], Frm),

   146     ([3, 1], Frm),

   147     ([3, 1], Res),

   148     ([3, 2], Res),

   149     ([3], Res),

   150     ([4], Res),

   151     ([], Res)]

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

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

   155    [([1], Frm),

   156     ([1], Res),

   157     ([2], Res),

   158     ([3], Frm),

   159     ([3, 1], Frm),

   160     ([3, 1], Res),

   161     ([3, 2], Res),

   162     ([3], Res),

   163     ([4], Res)]

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

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

   167    [([2], Res),

   168     ([3], Frm),

   169     ([3, 1], Frm),

   170     ([3, 1], Res),

   171     ([3, 2], Res),

   172     ([3], Res),

   173     ([4], Res)]

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

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

   177    [([3], Frm),

   178     ([3, 1], Frm),

   179     ([3, 1], Res),

   180     ([3, 2], Res),

   181     ([3], Res),

   182     ([4], Res)]

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

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

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

   187     ([3, 1], Res),

   188     ([3, 2], Res)]

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

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

   192    [([3], Frm),

   193     ([3, 1], Frm),

   194     ([3, 1], Res),

   195     ([3, 2], Res),

   196     ([3], Res)]

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

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

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

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

   207 Test_Tool.show_pt pt;

   208 Test_Tool.show_pt pt';

   209 (*default_print_depth 99*) cuts; (*default_print_depth 3*)

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

   212 	   ([3], Frm),

   213 	   ([3, 1], Frm),

   214 	   ([3, 1], Res),

   215 	   ([3, 2], Res),

   216 	   ([3], Res),

   217 	   ([4], Res)]

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

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

   220 if res = TermC.empty andalso asm = [] then () else

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

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

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

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

   227 (*============ inhibit exn AK110726 ==============================================

   228 if UnparseC.term res = "[x = 1]" (*WN050219 TermC.empty in cut_tree!!!*) then () else

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

   230 ============ inhibit exn AK110726 ==============================================*)

   231 (*============ inhibit exn AK110726 ==============================================

   232 if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =

   233    [([], Frm),

   234     ([1], Frm),

   235     ([1], Res),

   236     ([2], Res),(*, TermC.empty in cut_tree!!!*)

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

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

   239 ============ inhibit exn AK110726 ==============================================*)

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

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

   243 	   ([3, 1], Frm),

   244 	   ([3, 1], Res),

   245 	   ([3, 2], Res),

   246 	   ([3], Res),

   247 	   ([4], Res)]

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

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

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

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

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

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

   256 if pr_ctree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + - 1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   - 1 + x = 0\n4.   [x = 1]\n"

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

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

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

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

   262 if pr_ctree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + - 1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   - 1 + x = 0\n4.   [x = 1]\n"

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

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

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

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

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

   271 (*============ inhibit exn AK110726 ==============================================

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

   273 	   ([3], Frm),

   274 	   ([3, 1], Frm),

   275 	   ([3, 1], Res),

   276 	   ([3, 2], Res),

   277 	   ([3], Res),

   278 	   ([4], Res),

   279 	   ([], Res)]

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

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

   283 ============ inhibit exn AK110726 ==============================================*)

   285 if res = TermC.empty (*WN050219 done by cut_level*) then () else

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

   288 (*============ inhibit exn AK110726 ==============================================

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

   290 if UnparseC.term form = "x + 1 + - 1 * 2 = 0" (*remained !!!*) then () else

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

   292 ============ inhibit exn AK110726 ==============================================*)

   293 (* AK110727 Debuging

   294   (* get_obj g_form pt' [2];

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

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

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

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

   300 if res = TermC.empty (*WN050219 done by cut_tree*) then () else

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

   303 if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =

   304    [([], Frm),

   305     ([1], Frm),

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

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

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

   310 (*============ inhibit exn AK110726 ==============================================

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

   312 	   ([3, 1], Frm),

   313 	   ([3, 1], Res),

   314 	   ([3, 2], Res),

   315 	   ([3], Res),

   316 	   ([4], Res),

   317 	   ([], Res)]

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

   319 ============ inhibit exn AK110726 ==============================================*)

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

   322 (*============ inhibit exn AK110726 ==============================================

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

   324 	   ([3, 2], Res),

   325 	   ([3], Res),

   326 	   ([4], Res),

   327 	   ([], Res)]

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

   329 ============ inhibit exn AK110726 ==============================================*)

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

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

   333 	   ([3], Res),

   334 	   ([4], Res),

   335 	   ([], Res)]

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

   338 "=====new ctree 1a miniscript with mini-subpbl ===================";

   339 "=====new ctree 1a miniscript with mini-subpbl ===================";

   340 "=====new ctree 1a miniscript with mini-subpbl ===================";

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

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

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

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

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

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

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

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

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

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

   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 Test_Tool.show_pt pt;

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

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

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

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

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

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

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

   365 if cuts = []

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

   368 (*WN050219

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

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

   373 Test_Tool.show_pt pt;

   374 Test_Tool.show_pt pt';

   375 (*default_print_depth 99;*)cuts;(*default_print_depth 3;*)

   376 (*default_print_depth 99;*)map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)

   377 ####################################################################*)

   381 "=====new ctree 2 miniscript with mini-subpbl ====================";

   382 "=====new ctree 2 miniscript with mini-subpbl ====================";

   383 "=====new ctree 2 miniscript with mini-subpbl ====================";

   384 States.reset ();

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

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

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

   388  Iterator 1; moveActiveRoot 1;

   389  autoCalculate 1 CompleteCalc;

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

   393  val ((pt,_),_) = States.get_calc 1;

   394  Test_Tool.show_pt pt;

   396 if (UnparseC.term o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()

   397 else error "mini-subpbl interSteps broken";

   399 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   400 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   401 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";

   402 (*WN050225 intermed. outcommented

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

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

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

   406 	    ([3, 2], Res),

   407 	    ([3], Res),

   408 	    ([4], Res)]

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

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

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

   413 	    ([3, 2], Res),

   414 	    ([3], Res),

   415 	    ([4], Res)]

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

   419 "-------------- cappend (from ctree above)------------------------";

   420 "-------------- cappend (from ctree above)------------------------";

   421 "-------------- cappend (from ctree above)------------------------";

   422 val (pt',cuts) = cappend_form pt [3,2,1] Istate.empty (TermC.parse_test @{context} "newnew");

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

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

   425 	   ([3, 2], Res),

   426 	   ([3], Res),

   427 	   ([4], Res),

   428 	   ([], Res)]

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

   430 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "newnew" andalso

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

   432    UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty"

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

   435 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "newform")

   436     (Tac "test") (TermC.parse_test @{context} "newresult",[]) Complete;

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

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

   439 	   ([3, 2], Res),

   440 	   ([3], Res),

   441 	   ([4], Res),

   442 	   ([], Res)]

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

   447 "-------------- cappend minisubpbl -------------------------------";

   448 "-------------- cappend minisubpbl -------------------------------";

   449 "-------------- cappend minisubpbl -------------------------------";

   450 "=====new ctree 1 miniscript with mini-subpbl ====================";

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

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

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

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

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

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

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

   458    (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

   459    *)

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

   461 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

   462    *)

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

   464 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));

   465    *)

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

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

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

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

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

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

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

   474 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2");

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

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

   477 if UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty then () else

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

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

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

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

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

   484 val (pt,cuts) =

   485     cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2")

   486 		   Empty_Tac (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0",[]) Incomplete;

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

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

   489 if UnparseC.term form = "x + 1 = 2" andalso UnparseC.term res = "x + 1 + - 1 * 2 = 0"

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

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

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

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

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

   496 val (pt,cuts) =

   497     cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0")

   498 		   Empty_Tac (TermC.parse_test @{context} "- 1 + x = 0",[]) Incomplete;

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

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

   501 if UnparseC.term form = "x + 1 + - 1 * 2 = 0" andalso UnparseC.term res = "- 1 + x = 0"

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

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

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

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

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

   509 val (pt,cuts) = cappend_problem pt (fst p) Istate.empty Formalise.empty ([],References.empty,TermC.empty, ContextC.empty);

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

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

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

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

   515 (* ...complete calchead skipped...*)

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

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

   519 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0");

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

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

   522 if UnparseC.term form = "- 1 + x = 0" andalso res = TermC.empty then () else

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

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

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

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

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

   529 val (pt,cuts) =

   530     cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0")

   531 		   Empty_Tac (TermC.parse_test @{context} "x = 0 + - 1 * - 1",[]) Incomplete;

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

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

   534 if UnparseC.term form = "- 1 + x = 0" andalso UnparseC.term res = "x = 0 + - 1 * - 1" then()

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

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

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

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

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

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

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

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

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

   546 WN050225 intermed. outcommented---*)

   548 "=====new ctree 3 ================================================";

   549 "=====new ctree 3 ================================================";

   550 "=====new ctree 3 ================================================";

   552 States.reset ();

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

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

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

   556  Iterator 1; moveActiveRoot 1;

   557  autoCalculate 1 CompleteCalc;

   559  val ((pt,_),_) = States.get_calc 1;

   560  Test_Tool.show_pt pt;

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

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

   564 "-------------- move_dn ------------------------------------------";

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

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

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

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

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

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

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

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

   573 (* UnparseC.term (get_obj g_res pt [3]);

   574    UnparseC.term (get_obj g_form pt [4]);

   575    *)

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

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

   578 (*

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

   580                                   Exception PTREE end of calculation*)

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

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

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

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

   587  States.reset ();

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

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

   590        ("Test",

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

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

   593  Iterator 1; moveActiveRoot 1;

   594  autoCalculate 1 CompleteCalcHead;

   595  autoCalculate 1 (Steps 1);

   596  refFormula 1 (States.get_pos 1 1);

   598  moveActiveRoot 1;

   599  moveActiveDown 1;

   600  if States.get_pos 1 1 = ([1], Frm) then ()

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

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

   604  autoCalculate 1 (Steps 1);

   605  refFormula 1 (States.get_pos 1 1);

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

   608  if States.get_pos 1 1 = ([1], Res) then ()

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

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

   613 "-------------- move_up ------------------------------------------";

   614 "-------------- move_up ------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

   627                                   Exception PTREE begin of calculation*)

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

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

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

   633 "------ move into detail -----------------------------------------";

   634  States.reset ();

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

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

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

   638  Iterator 1; moveActiveRoot 1;

   639  autoCalculate 1 CompleteCalc;

   640  moveActiveRoot 1;

   641  moveActiveDown 1;

   642  moveActiveDown 1;

   643  moveActiveDown 1;

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

   646  interSteps 1 ([2],Res);

   648  val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt;

   649  val p = States.get_pos 1 1;

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

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

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

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

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

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

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

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

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

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

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

   663 "=====new ctree 3a ===============================================";

   664 "=====new ctree 3a ===============================================";

   665 "=====new ctree 3a ===============================================";

   666  States.reset ();

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

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

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

   670  Iterator 1; moveActiveRoot 1;

   671  autoCalculate 1 CompleteCalcHead;

   672  autoCalculate 1 (Steps 1);

   673  autoCalculate 1 (Steps 1);

   674  autoCalculate 1 (Steps 1);

   675  val ((pt,_),_) = States.get_calc 1;

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

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

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

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

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

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

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

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

   685 (*

   686  get_obj g_ostate pt [1];

   687  Test_Tool.show_pt pt;

   688 *)

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

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

   692 "-------------- move_dn in Incomplete ctree ----------------------";

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

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

   698 "=====new ctree 4: crooked by cut_level_'_ =======================";

   699 States.reset ();

   700 CalcTree

   701 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",

   702 	   "solveFor x", "solutions L"],

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

   704 Iterator 1; moveActiveRoot 1;

   705 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   730 val ((pt,_),_) = States.get_calc 1;

   731 writeln(pr_ctree pr_short pt);

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

   733  ###########################################################################*)

   734 val (pt, ppp) = cut_level__ [] [] pt ([4,1],Frm);

   735 writeln(pr_ctree pr_short pt);

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

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

   740 "-------------- ME_Misc.get_interval from ctree: incremental development--";

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

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

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

   744 (******************************************************************)

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

   746 (******************************************************************)

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

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

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

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

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

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

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

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

   755 www true [1,2];

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

   757 www true [1];

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

   760 local

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

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

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

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

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

   766 (*analoguous for tl*)

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

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

   770 (*see modspec.sml#pt_form

   771 fun pt_form (PrfObj {form,...}) = UnparseC.term form

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

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

   774 	val {cas,...} = Problem.from_store pI

   775     in case cas of

   776 	   NONE => UnparseC.term (pblterm dI pI)

   777 	 | SOME t => UnparseC.term (subst_atomic (I_Model.environment probl) t)

   778     end;

   779 *)

   780 (*.get an 'interval' from ctree down to a certain level

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   814 in

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

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

   817 (1) the 'f' are given

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

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

   820 (2) the 't' ar given

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

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

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

   824 fun get_trace pt p q =

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

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

   827 end;

   829 writeln(pr_ctree pr_short pt);

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

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

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

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

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

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

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

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

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

   842 (*========== inhibit exn AK110719 ==============================================

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

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

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

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

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

   848 ========== inhibit exn AK110719 ==============================================*)

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

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

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

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

   855 (*========== inhibit exn AK110719 ==============================================

   856 case get_trace pt [] [] of

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

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

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

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

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

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

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

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

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

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

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

   869   development stopped in favour of move_dn, see ME_Misc.get_interval

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

   871 *)

   872 (*

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

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

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

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

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

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

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

   880 *)

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

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

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

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

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

   888 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";

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

   890 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

   891     ("(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)",

   892      Subproblem

   893          ("PolyEq",

   894           ["normalise", "polynomial", "univariate", "equation"]),

   895 	 ["x \<noteq> 0", "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]) => ()

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

   897 (*WN060717 unintentionally changed some rls/ord while

   898      completing knowl. for thes2file...

   900   case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

   901     ((*"(3 + (- 1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))",

   902      *)Subproblem

   903          ("PolyEq",

   904           ["normalise", "polynomial", "univariate", "equation"]),

   905 	 ["9 * x + (x \<up> 3 + -6 * x \<up> 2) ~= 0"]) => ()

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

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

   912 "=====new ctree 5 minisubpbl =====================================";

   913 "=====new ctree 5 minisubpbl =====================================";

   914 "=====new ctree 5 minisubpbl =====================================";

   915 States.reset ();

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

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

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

   919 Iterator 1; moveActiveRoot 1;

   920 autoCalculate 1 CompleteCalc;

   921 val ((pt,_),_) = States.get_calc 1;

   922 Test_Tool.show_pt pt;

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

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

   926 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";

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

   928 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

   931      []) => ()

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

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

   935 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   940 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   945 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

   946     ("- 1 + x = 0",

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

   948      []) => ()

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

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

   952 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   957 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   962 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   967 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

   969      []) => ()

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

   972 (*========== inhibit exn AK110719 ==============================================

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

   974 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

   979 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

   980     ("[x = 1]",

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

   982      []) => ()

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

   985 val (Form form, tac, asm) = ME_Misc.pt_extract (pt, ([], Res));

   986 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

   989 ========== inhibit exn AK110719 ==============================================*)

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

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

   993 "=====new ctree 6 minisubpbl intersteps ==========================";

   994 States.reset ();

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

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

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

   998 Iterator 1; moveActiveRoot 1;

   999 autoCalculate 1 CompleteCalc;

  1000 interSteps 1 ([2],Res);

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

  1002 val ((pt,_),_) = States.get_calc 1;

  1003 Test_Tool.show_pt pt;

  1005 (**##############################################################**)

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

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

  1008 "-------------- get_allpos' new ----------------------------------";

  1009 "--- whole ctree";

  1010 (*default_print_depth 99;*)

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

  1012 (*default_print_depth 3;*)

  1013 if cuts =

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

  1015     ([1], Frm),

  1016     ([1], Res),

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

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

  1019     ([2], Res),

  1020     ([3], Pbl),

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

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

  1023     ([3, 2], Res),

  1024     ([3], Res),

  1025     ([4], Res),

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

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

  1029 (*default_print_depth 99;*)

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

  1031 (*default_print_depth 3;*)

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

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

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

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

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

  1038 if cuts =

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

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

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

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

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

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

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

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

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

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

  1052 if cuts =

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

  1054     ([3, 1], Res),

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

  1056     ([3, 2], Res),

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

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

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

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

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

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

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

  1066 if cuts =

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

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

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

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

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

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

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

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

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

  1078 if cuts =

  1079    [] then () else

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

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

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

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

  1087 (**#################################################################**)

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

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

  1090 "-------------- cut_tree new (from ctree above)-------------------";

  1091 Test_Tool.show_pt pt;

  1092 val b = get_obj g_branch pt [];

  1093 if b = TransitiveB then () else

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

  1095 val b = get_obj g_branch pt [3];

  1096 if b = TransitiveB then () else

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

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

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

  1101 (*default_print_depth 99;*)

  1102 cuts;

  1103 (*default_print_depth 3;*)

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

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

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

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

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

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

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

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

  1114 (*default_print_depth 99;*)

  1115 cuts;

  1116 (*default_print_depth 3;*)

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

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

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

  1120 	   ([2], Res),

  1121 	   ([3], Pbl),

  1122 	   ([3, 1], Frm),

  1123 	   ([3, 1], Res),

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

  1125 	   ([3, 2], Res),

  1126 	   ([3], Res),

  1127 	   ([4], Res),

  1128 	   ([],Res)] then ()

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

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

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

  1133 (*default_print_depth 99;*)

  1134 cuts;

  1135 (*default_print_depth 3;*)

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

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

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

  1139 	   ([3, 2], Res),

  1140 	   ([3], Res),

  1141 	   ([4], Res),

  1142 	   ([], Res)]

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

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

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

  1147 (*default_print_depth 99;*)

  1148 cuts;

  1149 (*default_print_depth 1;*)

  1150 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then ()

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

  1152 Test_Tool.show_pt pt';

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

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

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

  1158 Test_Tool.show_pt pt;

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

  1161 (*========== inhibit exn AK110726 ==============================================

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

  1163 val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.parse_test @{context} "Inform[1]")

  1164     (Tac "test") (TermC.parse_test @{context} "Inres[1]",[]) Complete;

  1166 (*default_print_depth 99;*)

  1167 cuts;

  1168 (*default_print_depth 3;*)

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

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

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

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

  1173 	    ([], Res)] then ()

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

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

  1177 (*default_print_depth 99;*)

  1178 afterins;

  1179 (*default_print_depth 3;*)

  1180 if afterins = [([1], Frm), ([1], Res)] then()

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

  1182 Test_Tool.show_pt pt';

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

  1184 Test_Tool.show_pt pt;

  1185 val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.parse_test @{context} "Inform[2]")

  1186     (Tac "test") (TermC.parse_test @{context} "Inres[2]",[]) Complete;

  1187 (*default_print_depth 99;*)

  1188 cuts;

  1189 (*default_print_depth 3;*)

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

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

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

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

  1195 	    ([], Res)] then ()

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

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

  1200 (*default_print_depth 99;*)

  1201 afterins;

  1202 (*default_print_depth 3;*)

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

  1205 then () else

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

  1207 Test_Tool.show_pt pt';

  1210 (*

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

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

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

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

  1216  UnparseC.term (get_obj g_form pt' [2]);

  1217  UnparseC.term (get_obj g_res pt' [2]);

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

  1219  *)

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

  1222 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],References.empty)

  1223 				  ([],References.empty, TermC.parse_test @{context} "Inhead[3]", ContextC.empty);

  1224 (*default_print_depth 99;*)

  1225 cuts;

  1226 (*default_print_depth 3;*)

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

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

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

  1230 	   ([3, 2], Res),

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

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

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

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

  1235 (*default_print_depth 99;*)

  1236 afterins;

  1237 (*default_print_depth 3;*)

  1238 if afterins =

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

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

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

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

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

  1244    use"ctree.sml";

  1245    *)

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

  1248 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.parse_test @{context} "Inform[3,1]")

  1249     (Tac "test") (TermC.parse_test @{context} "Inres[3,1]",[]) Complete;

  1250 (*default_print_depth 99;*)

  1251 cuts;

  1252 (*default_print_depth 3;*)

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

  1254 	   ([3, 2], Res),

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

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

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

  1259 (*default_print_depth 99;*)

  1260 afterins;

  1261 (*default_print_depth 3;*)

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

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

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

  1265 	       ([2], Res),

  1266 	       ([3], Pbl),

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

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

  1270 if UnparseC.term (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else

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

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

  1274 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.parse_test @{context} "Inform[3,2]")

  1275     (Tac "test") (TermC.parse_test @{context} "Inres[3,2]",[]) Complete;

  1276 (*default_print_depth 99;*)

  1277 cuts;

  1278 (*default_print_depth 3;*)

  1279 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else

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

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

  1282 (*default_print_depth 99;*)

  1283 afterins;

  1284 (*default_print_depth 3;*)

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

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

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

  1288 	       ([2], Res),

  1289 	       ([3], Pbl),

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

  1291 then () else

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

  1294 if UnparseC.term (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else

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

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

  1298 (**)

  1299 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "Inform[3,2,1]")

  1300     (Tac "test") (TermC.parse_test @{context} "Inres[3,2,1]",[]) Complete;

  1301 (*default_print_depth 99;*)

  1302 cuts;

  1303 (*default_print_depth 1;*)

  1304 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)]

  1305 then () else

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

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

  1308 (*default_print_depth 99;*)

  1309 afterins;

  1310 (*default_print_depth 3;*)

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

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

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

  1314 	       ([2], Res),

  1315 	       ([3], Pbl),

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

  1317 	       ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else

  1318 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";

  1319 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else

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

  1321 (*

  1322 Test_Tool.show_pt pt';

  1323 Test_Tool.show_pt pt;

  1324 *)

  1325 ========== inhibit exn AK110726 ==============================================*)

  1326 "-------------- repl_app------------------------------------------";

  1327 "-------------- repl_app------------------------------------------";

  1328 "-------------- repl_app------------------------------------------";

  1329 (*

  1330 > repl [1,2,3] 2 22222;

  1331 val it = [1,22222,3] : int list

  1332 > repl_app [1,2,3,4] 5 5555;

  1333 val it = [1,2,3,4,5555] : int list

  1334 > repl_app [1,2,3] 2 22222;

  1335 val it = [1,22222,3] : int list

  1336 > repl_app [1] 2 22222 ;

  1337 val it = [1,22222] : int list

  1338 *)

author	wneuper <Walther.Neuper@jku.at>
	Sun, 09 Oct 2022 07:44:22 +0200
changeset 60565	f92963a33fe3
parent 60549	c0a775618258
child 60571	19a172de0bb5
permissions	-rw-r--r--