neuper@37906: (* tests for sml/ME/ctree.sml
neuper@37906: authors: Walther Neuper 060113
neuper@37906: (c) due to copyright terms
neuper@37906:
neuper@37906: use"../smltest/ME/ctree.sml";
neuper@37906: use"ctree.sml";
neuper@37906: *)
neuper@37906:
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@41990: "-------------- fun get_ctxt -------------------------------------";
neuper@41989: "-------------- fun update_ctxt, fun g_ctxt ----------------------";
neuper@41968: "-------------- check positions in miniscript --------------------";
wneuper@59279: "-------------- get_allpos' (from ctree above)--------------------";
wneuper@59279: "-------------- cut_level (from ctree above)----------------------";
wneuper@59279: "-------------- cut_tree (from ctree above)-----------------------";
wneuper@59279: "=====new ctree 1a miniscript with mini-subpbl ===================";
neuper@37906: "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
wneuper@59279: "=====new ctree 2 miniscript with mini-subpbl ====================";
wneuper@59279: "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
wneuper@59279: "-------------- cappend (from ctree above)------------------------";
neuper@37906: "-------------- cappend minisubpbl -------------------------------";
wneuper@59279: "=====new ctree 3 ================================================";
neuper@37906: "-------------- move_dn ------------------------------------------";
neuper@37906: "-------------- move_dn: Frm -> Res ------------------------------";
neuper@37906: "-------------- move_up ------------------------------------------";
neuper@37906: "------ move into detail -----------------------------------------";
wneuper@59279: "=====new ctree 3a ===============================================";
neuper@37906: "-------------- move_dn in Incomplete ctree ----------------------";
wneuper@59279: "=====new ctree 4: crooked by cut_level_'_ =======================";
neuper@37906: (*############## development stopped 0501 ########################*)
neuper@37906: (******************************************************************)
neuper@37906: (* val SAVE_get_trace = get_trace; *)
neuper@37906: (******************************************************************)
neuper@37906: "-------------- get_interval from ctree: incremental development--";
neuper@37906: (******************************************************************)
neuper@37906: (* val get_trace = SAVE_get_trace; *)
neuper@37906: (******************************************************************)
neuper@37906: (*############## development stopped 0501 ########################*)
wneuper@59279: "=====new ctree 4 ratequation ====================================";
neuper@37906: "-------------- pt_extract form, tac, asm<>[] --------------------";
wneuper@59279: "=====new ctree 5 minisubpbl =====================================";
neuper@37906: "-------------- pt_extract form, tac, asm ------------------------";
wneuper@59279: "=====new ctree 6 minisubpbl intersteps ==========================";
neuper@37906: "-------------- get_allpos' new ----------------------------------";
wneuper@59279: "-------------- cut_tree new (from ctree above)-------------------";
neuper@42360: "-------------- subst2subs subs2subst sube2subst subte2subst -----";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906:
neuper@37906:
neuper@41990: "-------------- fun get_ctxt -------------------------------------";
neuper@41990: "-------------- fun get_ctxt -------------------------------------";
neuper@41990: "-------------- fun get_ctxt -------------------------------------";
neuper@41990: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41990: val (dI',pI',mI') =
neuper@41990: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41990: ["Test","squ-equ-test-subpbl1"]);
neuper@41990: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41990: (get_ctxt pt p)
neuper@41992: handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: (get_ctxt pt p)
neuper@41992: handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
neuper@41990:
neuper@41989: "-------------- fun update_ctxt, fun g_ctxt ----------------------";
neuper@41989: "-------------- fun update_ctxt, fun g_ctxt ----------------------";
neuper@41989: "-------------- fun update_ctxt, fun g_ctxt ----------------------";
neuper@41992: val pt = EmptyPtree;
neuper@41992: val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
neuper@41992: val ctxt = get_obj g_ctxt pt [];
neuper@41992: if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
neuper@48761: val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac"});
neuper@48761: if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac"
neuper@41992: then () else error "--- fun update_ctxt, fun g_ctxt changed";
neuper@41989:
neuper@41968: "-------------- check positions in miniscript --------------------";
neuper@41968: "-------------- check positions in miniscript --------------------";
neuper@41968: "-------------- check positions in miniscript --------------------";
neuper@41972: val fmz = ["equality (x+1=(2::real))",
bonzai@41950: "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058: ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
bonzai@41951: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = Add_Given "equality (x + 1 = 2)"
neuper@37924: (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
bonzai@41950: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37924: (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37924: (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: "ctree.sml-------------- get_allpos' new ------------------------\"";
neuper@37906: val (PP, pp) = split_last [1];
neuper@37906: val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
neuper@37906:
neuper@37906: val cuts = get_allp [] ([], ([],Frm)) pt;
neuper@37906: val cuts2 = get_allps [] [1] (children pt);
wneuper@59279: "ctree.sml-------------- cut_tree new (from ctree above)----------";
neuper@37906: val (pt', cuts) = cut_tree pt ([1],Frm);
neuper@37906: "ctree.sml-------------- cappend on complete ctree from above ----";
bonzai@41949: val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
neuper@37906: "----------------------------------------------------------------/";
akargl@42108:
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
neuper@37906:
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
neuper@37906:
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
wneuper@59267: val FormKF res = f;
wneuper@59253: if res = "[x = 1]"
wneuper@59253: then case nxt of ("End_Proof'", End_Proof') => ()
wneuper@59253: | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
wneuper@59253: else error "new behaviour in test: miniscript with mini-subpbl 2"
neuper@37906:
neuper@37906: show_pt pt;
neuper@37906:
wneuper@59279: "-------------- get_allpos' (from ctree above)--------------------";
wneuper@59279: "-------------- get_allpos' (from ctree above)--------------------";
wneuper@59279: "-------------- get_allpos' (from ctree above)--------------------";
neuper@37906: if get_allpos' ([], 1) pt =
neuper@37906: [([], Frm),
neuper@37906: ([1], Frm),
neuper@37906: ([1], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 1";
neuper@37906:
neuper@37906: if get_allpos's ([], 1) (children pt) =
neuper@37906: [([1], Frm),
neuper@37906: ([1], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 2";
neuper@37906:
neuper@37906: if get_allpos's ([], 2) (takerest (1, children pt)) =
neuper@37906: [([2], Res),
neuper@37906: ([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 3";
neuper@37906:
neuper@37906: if get_allpos's ([], 3) (takerest (2, children pt)) =
neuper@37906: [([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 4";
neuper@37906:
neuper@37906: if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
neuper@37906: [([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 5";
neuper@37906:
neuper@37906: if get_allpos' ([3], 1) (nth 3 (children pt)) =
neuper@37906: [([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in get_allpos' 6";
neuper@37906:
neuper@37906:
akargl@42190:
akargl@42190:
akargl@42190:
akargl@42190:
wneuper@59279: "-------------- cut_level (from ctree above)----------------------";
wneuper@59279: "-------------- cut_level (from ctree above)----------------------";
wneuper@59279: "-------------- cut_level (from ctree above)----------------------";
neuper@37906: show_pt pt;
neuper@37906: show_pt pt';
wneuper@59111: default_print_depth 99; cuts; default_print_depth 3;
neuper@37906:
neuper@37906: (*if cuts = [([2], Res),
neuper@37906: ([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 1a";
neuper@37906: val (res,asm) = get_obj g_result pt' [2];
neuper@37906: if res = e_term andalso asm = [] then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
neuper@37906: if not (existpt [2] pt') then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
neuper@37906:
neuper@37906: val (res,asm) = get_obj g_result pt' [];
akargl@42193:
akargl@42193: (*============ inhibit exn AK110726 ==============================================
neuper@37906: if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_level 1ab";
akargl@42218: ============ inhibit exn AK110726 ==============================================*)
akargl@42218: (*============ inhibit exn AK110726 ==============================================
neuper@37906: if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
neuper@37906: [([], Frm),
neuper@37906: ([1], Frm),
neuper@37906: ([1], Res),
neuper@37906: ([2], Res),(*, e_term in cut_tree!!!*)
neuper@37906: ([], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_level 1b";
akargl@42193: ============ inhibit exn AK110726 ==============================================*)
neuper@37906:
neuper@37906: val (pt',cuts) = cut_level [] [] pt ([2],Res);
neuper@37906: if cuts = [([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 2a";
neuper@37906:
wneuper@59279: if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 2b";
neuper@37906:
neuper@37906: val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
neuper@37906: if cuts = [([3, 1], Res), ([3, 2], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 3a";
wneuper@59279: 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"
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 3b";
neuper@37906:
neuper@37906: val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
neuper@37906: if cuts = [([3, 2], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 4a";
wneuper@59279: 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"
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_level 4b";
neuper@37906:
neuper@37906:
wneuper@59279: "-------------- cut_tree (from ctree above)-----------------------";
wneuper@59279: "-------------- cut_tree (from ctree above)-----------------------";
wneuper@59279: "-------------- cut_tree (from ctree above)-----------------------";
neuper@37906: val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
akargl@42193:
akargl@42193: (*============ inhibit exn AK110726 ==============================================
neuper@37906: if cuts = [([2], Res),
neuper@37906: ([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 1a";
neuper@37906:
neuper@37906: val (res,asm) = get_obj g_result pt' [2];
akargl@42193: ============ inhibit exn AK110726 ==============================================*)
akargl@42193:
neuper@37906: if res = e_term (*WN050219 done by cut_level*) then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_tree 1aa";
neuper@37906:
akargl@42193: (*============ inhibit exn AK110726 ==============================================
neuper@37906: val form = get_obj g_form pt' [2];
neuper@37906: if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_tree 1ab";
akargl@42193: ============ inhibit exn AK110726 ==============================================*)
akargl@42218: (* AK110727 Debuging
akargl@42218: (* get_obj g_form pt' [2];
akargl@42218: (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"
akargl@42218: raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)
akargl@42218: "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)
neuper@37906:
neuper@37906: val (res,asm) = get_obj g_result pt' [];
neuper@37906: if res = e_term (*WN050219 done by cut_tree*) then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_tree 1ac";
neuper@37906:
neuper@37906: if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
neuper@37906: [([], Frm),
neuper@37906: ([1], Frm),
neuper@37906: ([1], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in cut_tree 1ad";
neuper@37906:
neuper@37906: val (pt', cuts) = cut_tree pt ([2],Res);
akargl@42193: (*============ inhibit exn AK110726 ==============================================
neuper@37906: if cuts = [([3], Frm),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 2";
akargl@42193: ============ inhibit exn AK110726 ==============================================*)
neuper@37906:
neuper@37906: val (pt', cuts) = cut_tree pt ([3,1],Frm);
akargl@42193: (*============ inhibit exn AK110726 ==============================================
neuper@37906: if cuts = [([3, 1], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 3";
akargl@42193: ============ inhibit exn AK110726 ==============================================*)
neuper@37906:
neuper@37906: val (pt', cuts) = cut_tree pt ([3,1],Res);
neuper@37906: if cuts = [([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 4";
neuper@37906:
wneuper@59279: "=====new ctree 1a miniscript with mini-subpbl ===================";
wneuper@59279: "=====new ctree 1a miniscript with mini-subpbl ===================";
wneuper@59279: "=====new ctree 1a miniscript with mini-subpbl ===================";
neuper@41970: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058: ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: show_pt pt;
neuper@37906:
neuper@37906: "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
neuper@37906: "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
neuper@37906: "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
neuper@37906:
neuper@37906: val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
neuper@37906: if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 4a";
neuper@37906:
neuper@37906: val (pt', cuts) = cut_tree pt ([1],Frm);
neuper@37906: if cuts = []
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 4a";
neuper@37906:
neuper@37906: (*WN050219
neuper@37906: val pos as ([p],_) = ([1],Frm);
neuper@37906: val pt as Nd (b,_) = pt;
neuper@37906:
neuper@37906:
neuper@37906: show_pt pt;
neuper@37906: show_pt pt';
wneuper@59111: default_print_depth 99;cuts;default_print_depth 3;
wneuper@59111: default_print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');default_print_depth 3;
akargl@42190: ####################################################################*)
akargl@42190:
akargl@42190:
akargl@42190:
wneuper@59279: "=====new ctree 2 miniscript with mini-subpbl ====================";
wneuper@59279: "=====new ctree 2 miniscript with mini-subpbl ====================";
wneuper@59279: "=====new ctree 2 miniscript with mini-subpbl ====================";
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906:
neuper@37906: interSteps 1 ([3,2],Res);
neuper@37906:
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: show_pt pt;
neuper@37906:
neuper@42185: if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
neuper@42185: else error "mini-subpbl interSteps broken";
neuper@42185:
wneuper@59279: "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
wneuper@59279: "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
wneuper@59279: "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
neuper@37906: (*WN050225 intermed. outcommented
neuper@37906: val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
neuper@37906: if cuts = [([3, 2, 1], Res),
neuper@37906: ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
neuper@37906:
neuper@37906: val (pt', cuts) = cut_tree pt ([3,2,1],Res);
neuper@37906: if cuts = [([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
neuper@37906:
neuper@37906:
wneuper@59279: "-------------- cappend (from ctree above)------------------------";
wneuper@59279: "-------------- cappend (from ctree above)------------------------";
wneuper@59279: "-------------- cappend (from ctree above)------------------------";
neuper@37906: val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
neuper@37906: if cuts = [([3, 2, 1], Res),
neuper@37906: ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cappend_form";
neuper@37906: if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
neuper@37906: get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
neuper@37906: term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
neuper@38031: then () else error "ctree.sml: diff:behav. in cappend 1";
neuper@37906:
neuper@37906: val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
neuper@37906: (Tac "test") (str2term "newresult",[]) Complete;
neuper@37906: if cuts = [([3, 2, 1], Res), (*?????????????*)
neuper@37906: ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)]
neuper@38031: then () else error "ctree.sml: diff:behav. in cappend_atomic";
neuper@37906:
neuper@37906:
neuper@37906:
neuper@37906: "-------------- cappend minisubpbl -------------------------------";
neuper@37906: "-------------- cappend minisubpbl -------------------------------";
neuper@37906: "-------------- cappend minisubpbl -------------------------------";
wneuper@59279: "=====new ctree 1 miniscript with mini-subpbl ====================";
neuper@41970: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058: ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = Add_Given "equality (x + 1 = 2)"
neuper@37924: (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37924: (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37924: (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
neuper@37906: *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
neuper@37906: val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
neuper@37906: val p = ([1], Frm);
neuper@37906: val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
neuper@37906: val form = get_obj g_form pt (fst p);
neuper@37906: val (res,_) = get_obj g_result pt (fst p);
neuper@37906: if term2str form = "x + 1 = 2" andalso res = e_term then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
neuper@37906: val p = ([1], Res);
neuper@37906: val (pt,cuts) =
neuper@37906: cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
neuper@37906: Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
neuper@37906: val form = get_obj g_form pt (fst p);
neuper@37906: val (res,_) = get_obj g_result pt (fst p);
neuper@37906: if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
neuper@38031: then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
neuper@37906: val p = ([2], Res);
neuper@37906: val (pt,cuts) =
neuper@37906: cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
neuper@37906: Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
neuper@37906: val form = get_obj g_form pt (fst p);
neuper@37906: val (res,_) = get_obj g_result pt (fst p);
neuper@37906: if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
neuper@38031: then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
neuper@37906:
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
neuper@37906: val p = ([3], Pbl);
neuper@37906: val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
neuper@37906: if is_pblobj (get_obj I pt (fst p)) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
neuper@37906:
neuper@37906: (* ...complete calchead skipped...*)
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
neuper@37906: val p = ([3, 1], Frm);
neuper@37906: val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
neuper@37906: val form = get_obj g_form pt (fst p);
neuper@37906: val (res,_) = get_obj g_result pt (fst p);
neuper@37906: if term2str form = "-1 + x = 0" andalso res = e_term then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
neuper@37906: val p = ([3, 1], Res);
neuper@37906: val (pt,cuts) =
neuper@37906: cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
neuper@37906: Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
neuper@37906: val form = get_obj g_form pt (fst p);
neuper@37906: val (res,_) = get_obj g_result pt (fst p);
neuper@37906: if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
neuper@38031: else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
neuper@37906: if not (existpt ((lev_on o fst) p) pt) then () else
neuper@38031: error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
neuper@37906:
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
neuper@37906:
neuper@37906: WN050225 intermed. outcommented---*)
neuper@37906:
wneuper@59279: "=====new ctree 3 ================================================";
wneuper@59279: "=====new ctree 3 ================================================";
wneuper@59279: "=====new ctree 3 ================================================";
akargl@42120:
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906:
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: show_pt pt;
neuper@37906:
neuper@37906: "-------------- move_dn ------------------------------------------";
neuper@37906: "-------------- move_dn ------------------------------------------";
neuper@37906: "-------------- move_dn ------------------------------------------";
neuper@37906: val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
neuper@37906: val p = move_dn [] pt p (*-> ([1],Res)*);
neuper@37906: val p = move_dn [] pt p (*-> ([2],Res)*);
neuper@37906: val p = move_dn [] pt p (*-> ([3],Pbl)*);
neuper@37906: val p = move_dn [] pt p (*-> ([3,1],Frm)*);
neuper@37906: val p = move_dn [] pt p (*-> ([3,1],Res)*);
neuper@37906: val p = move_dn [] pt p (*-> ([3,2],Res)*);
neuper@37906: val p = move_dn [] pt p (*-> ([3],Res)*);
neuper@37906: (* term2str (get_obj g_res pt [3]);
neuper@37906: term2str (get_obj g_form pt [4]);
neuper@37906: *)
neuper@37906: val p = move_dn [] pt p (*-> ([4],Res)*);
neuper@37906: val p = move_dn [] pt p (*-> ([],Res)*);
neuper@37906: (*
neuper@37906: val p = (move_dn [] pt p) handle e => print_exn_G e;
neuper@37906: Exception PTREE end of calculation*)
akargl@42193:
neuper@38031: if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
neuper@37906:
neuper@37906: "-------------- move_dn: Frm -> Res ------------------------------";
neuper@37906: "-------------- move_dn: Frm -> Res ------------------------------";
neuper@37906: "-------------- move_dn: Frm -> Res ------------------------------";
s1210629013@55445: reset_states ();
neuper@37906: CalcTree (*start of calculation, return No.1*)
neuper@42124: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
neuper@38058: ("Test",
neuper@55279: ["LINEAR","univariate","equation","test"],
neuper@37906: ["Test","solve_linear"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalcHead;
wneuper@59248: autoCalculate 1 (Step 1);
neuper@37906: refFormula 1 (get_pos 1 1);
neuper@37906:
neuper@37906: moveActiveRoot 1;
neuper@37906: moveActiveDown 1;
neuper@37906: if get_pos 1 1 = ([1], Frm) then ()
neuper@38031: else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
neuper@37906: moveActiveDown 1; (* pos does not exist *)
neuper@37906:
wneuper@59248: autoCalculate 1 (Step 1);
neuper@37906: refFormula 1 (get_pos 1 1);
neuper@37906:
neuper@37906: moveActiveDown 1; (* pos does not exist *)
neuper@37906: if get_pos 1 1 = ([1], Res) then ()
neuper@38031: else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
akargl@42202: moveActiveDown 1; (* pos does not exist *)
neuper@37906:
neuper@37906:
neuper@37906: "-------------- move_up ------------------------------------------";
neuper@37906: "-------------- move_up ------------------------------------------";
neuper@37906: "-------------- move_up ------------------------------------------";
neuper@37906: val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([3],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([3,2],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([3,1],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([3,1],Frm)*)
neuper@37906: val p = move_up [] pt p; (*-> ([3],Pbl)*)
neuper@37906: val p = move_up [] pt p; (*-> ([2],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([1],Res)*)
neuper@37906: val p = move_up [] pt p; (*-> ([1],Frm)*)
neuper@37906: val p = move_up [] pt p; (*-> ([],Pbl)*)
neuper@37906: (*val p = (move_up [] pt p) handle e => print_exn_G e;
neuper@37906: Exception PTREE begin of calculation*)
akargl@42193:
neuper@38031: if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
neuper@37906:
neuper@37906: "------ move into detail -----------------------------------------";
neuper@37906: "------ move into detail -----------------------------------------";
neuper@37906: "------ move into detail -----------------------------------------";
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906: moveActiveRoot 1;
neuper@37906: moveActiveDown 1;
neuper@37906: moveActiveDown 1;
neuper@37906: moveActiveDown 1;
neuper@37906: refFormula 1 (get_pos 1 1) (* 2 Res, -1 + x = 0 *);
neuper@37906:
neuper@37906: interSteps 1 ([2],Res);
neuper@37906:
neuper@37906: val ((pt,_),_) = get_calc 1; show_pt pt;
neuper@37906: val p = get_pos 1 1;
neuper@37906:
neuper@37906: val p = move_up [] pt p; (*([2, 6], Res)*);
neuper@37906: val p = movelevel_up [] pt p;(*([2], Frm)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 1], Frm)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 1], Res)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 2], Res)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 3], Res)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 4], Res)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 5], Res)*);
neuper@37906: val p = move_dn [] pt p; (*([2, 6], Res)*);
neuper@37906: if p = ([2, 6], Res) then()
neuper@38031: else error "ctree.sml: diff.behav. in move into detail";
neuper@37906:
wneuper@59279: "=====new ctree 3a ===============================================";
wneuper@59279: "=====new ctree 3a ===============================================";
wneuper@59279: "=====new ctree 3a ===============================================";
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalcHead;
wneuper@59248: autoCalculate 1 (Step 1);
wneuper@59248: autoCalculate 1 (Step 1);
wneuper@59248: autoCalculate 1 (Step 1);
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
neuper@37906: val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
neuper@37906: val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
neuper@37906: (*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
neuper@37906:
neuper@37906: moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
neuper@37906: moveDown 1 ([1],Frm) (*-> ([1],Res)*);
neuper@37906: moveDown 1 ([1],Res) (*-> ([2],Res)*);
neuper@37906: moveDown 1 ([2],Res) (*-> pos does not exist*);
neuper@37906: (*
neuper@37906: get_obj g_ostate pt [1];
neuper@37906: show_pt pt;
neuper@37906: *)
neuper@37906:
neuper@37906: "-------------- move_dn in Incomplete ctree ----------------------";
neuper@37906: "-------------- move_dn in Incomplete ctree ----------------------";
neuper@37906: "-------------- move_dn in Incomplete ctree ----------------------";
neuper@37906:
neuper@37906:
neuper@37906:
wneuper@59279: "=====new ctree 4: crooked by cut_level_'_ =======================";
wneuper@59279: "=====new ctree 4: crooked by cut_level_'_ =======================";
wneuper@59279: "=====new ctree 4: crooked by cut_level_'_ =======================";
s1210629013@55445: reset_states ();
neuper@37906: CalcTree
neuper@37906: [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
neuper@37906: "solveFor x","solutions L"],
neuper@38058: ("RatEq",["univariate","equation"],["no_met"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906:
neuper@37906: getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
neuper@37906: getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
neuper@37906: getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
neuper@37906: getTactic 1 ([4,1],Res);(*Rewrite all_left*)
neuper@37906: getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
neuper@37906: getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
neuper@37906:
neuper@37906: moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
neuper@37906: moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
neuper@37906: moveActiveFormula 1 ([3],Res)(*3.1.*);
neuper@37906: moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
neuper@37906: moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
neuper@37906:
neuper@37906: moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
neuper@37906: interSteps 1 ([1],Res)(*..is activeFormula !?!*);
neuper@37906:
neuper@37906: getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
neuper@37906: getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
neuper@37906: getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
neuper@37906: getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
neuper@37906:
neuper@37906: moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
neuper@37906: interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
neuper@37906: val ((pt,_),_) = get_calc 1;
wneuper@59279: writeln(pr_ctree pr_short pt);
neuper@37906: (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
neuper@37906: ###########################################################################*)
neuper@37906: val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
wneuper@59279: writeln(pr_ctree pr_short pt);
neuper@37906:
neuper@37906:
akargl@42190:
akargl@42190:
akargl@42190:
neuper@37906: "-------------- get_interval from ctree: incremental development--";
neuper@37906: "-------------- get_interval from ctree: incremental development--";
neuper@37906: "-------------- get_interval from ctree: incremental development--";
neuper@37906: "--- level 1: get pos from start b to end p ----------------------";
neuper@37906: "--- level 1: get pos from start b to end p ----------------------";
neuper@37906: "--- level 1: get pos from start b to end p ----------------------";
neuper@37906: (******************************************************************)
neuper@37906: (**) val SAVE_get_trace = get_trace; (**)
neuper@37906: (******************************************************************)
neuper@37906: (*'getnds' below is structured as such:*)
neuper@37906: fun www _ [x] = "l+r-margin"
neuper@37906: | www true [x1,x2] = "l-margin, r-margin"
neuper@37906: | www _ [x1,x2] = "intern, r-margin"
neuper@37906: | www true (x::(xs as _::_)) = "l-margin " ^ www false xs
neuper@37906: | www _ (x::(xs as _::_)) = "intern " ^ www false xs;
neuper@37906: www true [1,2,3,4,5];
neuper@37906: (*val it = "from intern intern intern to" : string*)
neuper@37906: www true [1,2];
neuper@37906: (*val it = "from to" : string*)
neuper@37906: www true [1];
neuper@37906: (*val it = "from+to" : string*)
neuper@37906:
neuper@37906: local
neuper@37906: (*specific values of hd of pos p,q for simple handling take_fromto,
neuper@37906: from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
neuper@37906: ... can be used even for positions _below_ p or q*)
neuper@37906: fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
neuper@37906: fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
neuper@37906: (*analoguous for tl*)
neuper@37906: fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
neuper@37906: fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
neuper@37906:
neuper@37906: (*see modspec.sml#pt_form
neuper@37906: fun pt_form (PrfObj {form,...}) = term2str form
neuper@37906: | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
neuper@37906: let val (dI, pI, _) = get_somespec' spec spec'
neuper@37906: val {cas,...} = get_pbt pI
neuper@37906: in case cas of
neuper@37926: NONE => term2str (pblterm dI pI)
neuper@37926: | SOME t => term2str (subst_atomic (mk_env probl) t)
neuper@37906: end;
neuper@37906: *)
wneuper@59279: (*.get an 'interval' from ctree down to a certain level
neuper@37906: by 'take_fromto children' of the nodes with specific 'from' and 'to';
neuper@37906: 'i > 0' suppresses output during recursive descent towards 'from'
neuper@37906: b: the 'from' incremented to the actual pos
neuper@37906: p,q: specific 'from','to' for simple use of 'take_fromto'*)
neuper@37906: fun getnd i (b,p) q (Nd (po, nds)) =
neuper@37906: (if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
neuper@37906:
neuper@37906: @ (writeln("getnd : b="^(ints2str' b)^", p="^
neuper@37906: (ints2str' p)^", q="^(ints2str' q));
neuper@37906:
neuper@37906: getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
neuper@37906: (take_fromto (hdp p) (hdq q) nds))
neuper@37906:
neuper@37906: and getnds _ _ _ _ [] = [] (*no children*)
neuper@37906: | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
neuper@37906: | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
neuper@37906: (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
neuper@37906: ", q="^ ints2str' q);
neuper@37906: (getnd i ( b, p ) [99999] n1) @
neuper@37906: (getnd ~99999 (lev_on b,[0]) q n2))
neuper@37906: | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
neuper@37906: (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
neuper@37906: ", q="^ ints2str' q);
neuper@37906: (getnd i ( b,[0]) [99999] n1) @
neuper@37906: (getnd ~99999 (lev_on b,[0]) q n2))
neuper@37906: | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
neuper@37906: (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
neuper@37906: ", q="^ ints2str' q);
neuper@37906: (getnd i ( b, p ) [99999] nd) @
neuper@37906: (getnds ~99999 false (lev_on b,[0]) q nds))
neuper@37906: | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
neuper@37906: (getnd i ( b,[0]) [99999] nd) @
neuper@37906: (getnds ~99999 false (lev_on b,[0]) q nds);
neuper@37906: in
wneuper@59279: (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
neuper@37906: where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
neuper@37906: (1) the 'f' are given
neuper@37906: (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
neuper@37906: (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
neuper@37906: (2) the 't' ar given
neuper@37906: (2a) by 'to' if 't' = the respective element of 'to' (right margin)
neuper@37906: (2b) inifinity, if 't' < the respective element of 'to (internal node)'
neuper@37906: the 'f' and 't' are set by hdp,... *)
neuper@37906: fun get_trace pt p q =
neuper@37906: (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
neuper@37906: (take_fromto (hdp p) (hdq q) (children pt));
neuper@37906: end;
neuper@37906:
wneuper@59279: writeln(pr_ctree pr_short pt);
akargl@42193:
neuper@37906: case get_trace pt [1,3] [4,1,1] of
neuper@37906: [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
neuper@37906: case get_trace pt [2] [4,3,2] of
neuper@37906: [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
neuper@37906: case get_trace pt [1,4] [4,3,1] of
neuper@37906: [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
akargl@42193:
akargl@42218:
akargl@42193: (*========== inhibit exn AK110719 ==============================================
neuper@37906: case get_trace pt [4,2] [5] of
neuper@37906: (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
neuper@37906: ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
neuper@37906: [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
akargl@42193: ========== inhibit exn AK110719 ==============================================*)
akargl@42193:
neuper@37906: case get_trace pt [] [4,4,2] of
neuper@37906: [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
neuper@37906: [4,3],[4,3,1],[4,3,2]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
akargl@42193:
akargl@42193: (*========== inhibit exn AK110719 ==============================================
neuper@37906: case get_trace pt [] [] of
neuper@37906: [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
neuper@37906: [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
neuper@37906: case get_trace pt [4,3] [4,3] of
neuper@37906: [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
akargl@42120: ========== inhibit exn AK110719 ==============================================*)
neuper@37906:
neuper@37906: "--- level 2: get pos' from start b to end p ---------------------";
neuper@37906: "--- level 2: get pos' from start b to end p ---------------------";
neuper@37906: "--- level 2: get pos' from start b to end p ---------------------";
neuper@37906: (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
neuper@37906: development stopped in favour of move_dn, see get_interval
neuper@37906: actually used (inefficient) version with move_dn: see modspec.sml
neuper@37906: *)
neuper@37906: (*
neuper@37906: case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
neuper@37906: [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
neuper@37906: case get_trace pt ([],Pbl) ([],Res) of
neuper@37906: [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
neuper@37906: [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
neuper@37906: *)
neuper@37906:
neuper@37906: (******************************************************************)
neuper@37906: (**) val get_trace = SAVE_get_trace; (**)
neuper@37906: (******************************************************************)
neuper@37906:
neuper@37906:
wneuper@59279: "=====new ctree 4 ratequation ====================================";
wneuper@59279: "=====new ctree 4 ratequation ====================================";
wneuper@59279: "=====new ctree 4 ratequation ====================================";
s1210629013@55445: reset_states ();
neuper@37906: CalcTree
neuper@37906: [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
neuper@37906: "solveFor x","solutions L"],
neuper@38058: ("RatEq",["univariate","equation"],["no_met"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@42394: val p = get_pos 1 1;
neuper@42394: val (Form f, tac, asms) = pt_extract (pt, p);
neuper@42394: (*============ inhibit exn WN120316 ==============================================
neuper@42394: if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
wneuper@59279: else error "after ===new ctree 4 ratequation ===";
neuper@42394: (*WN120317.TODO dropped rateq*)
neuper@42394: ============ inhibit exn WN120316 ==============================================*)
neuper@42394: if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
neuper@42394: andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
wneuper@59279: then () else error "after ===new ctree 4 ratequation ===";
neuper@37906:
neuper@37906:
neuper@37906: "-------------- pt_extract form, tac, asm<>[] --------------------";
neuper@37906: "-------------- pt_extract form, tac, asm<>[] --------------------";
neuper@37906: "-------------- pt_extract form, tac, asm<>[] --------------------";
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
neuper@37906: Subproblem
neuper@38058: ("PolyEq",
neuper@37906: ["normalize", "polynomial", "univariate", "equation"]),
neuper@37906: ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
neuper@37906: (*WN060717 unintentionally changed some rls/ord while
neuper@37906: completing knowl. for thes2file...
neuper@37906:
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
neuper@37906: *)Subproblem
neuper@38058: ("PolyEq",
neuper@37906: ["normalize", "polynomial", "univariate", "equation"]),
neuper@37906: ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
neuper@37906:
neuper@37906: .... but it became even better*)
neuper@37906:
neuper@37906:
neuper@37906:
wneuper@59279: "=====new ctree 5 minisubpbl =====================================";
wneuper@59279: "=====new ctree 5 minisubpbl =====================================";
wneuper@59279: "=====new ctree 5 minisubpbl =====================================";
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: show_pt pt;
neuper@37906:
neuper@37906: "-------------- pt_extract form, tac, asm ------------------------";
neuper@37906: "-------------- pt_extract form, tac, asm ------------------------";
neuper@37906: "-------------- pt_extract form, tac, asm ------------------------";
neuper@37926: val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("solve (x + 1 = 2, x)",
neuper@37906: Apply_Method ["Test", "squ-equ-test-subpbl1"],
neuper@37906: []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("-1 + x = 0",
neuper@55279: Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
neuper@37906: []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
neuper@37906:
neuper@37926: val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@55279: ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
neuper@37906: []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
neuper@37906:
akargl@42120: (*========== inhibit exn AK110719 ==============================================
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("[x = 1]", Check_elementwise "Assumptions", []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
neuper@37906:
neuper@37926: val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37906: ("[x = 1]",
neuper@37906: Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
neuper@37906: []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
neuper@37906:
neuper@37906: val (Form form, tac, asm) = pt_extract (pt, ([], Res));
neuper@37906: case (term2str form, tac, terms2strs asm) of
neuper@37926: ("[x = 1]", NONE, []) => ()
neuper@38031: | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
akargl@42120: ========== inhibit exn AK110719 ==============================================*)
neuper@37906:
wneuper@59279: "=====new ctree 6 minisubpbl intersteps ==========================";
wneuper@59279: "=====new ctree 6 minisubpbl intersteps ==========================";
wneuper@59279: "=====new ctree 6 minisubpbl intersteps ==========================";
s1210629013@55445: reset_states ();
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906: ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
neuper@37906: interSteps 1 ([2],Res);
neuper@37906: interSteps 1 ([3,2],Res);
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: show_pt pt;
neuper@37906:
neuper@37906: (**##############################################################**)
neuper@37906: "-------------- get_allpos' new ----------------------------------";
neuper@37906: "-------------- get_allpos' new ----------------------------------";
neuper@37906: "-------------- get_allpos' new ----------------------------------";
neuper@37906: "--- whole ctree";
wneuper@59111: default_print_depth 99;
neuper@37906: val cuts = get_allp [] ([], ([],Frm)) pt;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts =
neuper@37906: [(*never returns the first pos'*)
neuper@37906: ([1], Frm),
neuper@37906: ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allp new []";
neuper@37906:
wneuper@59111: default_print_depth 99;
neuper@37906: val cuts2 = get_allps [] [1] (children pt);
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = cuts2 @ [([], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allps new []";
neuper@37906:
neuper@37906: "---(3) on S(606)..S(608)--------";
neuper@37906: "--- nd [2] with 6 children---------------------------------";
neuper@37906: val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
neuper@37906: if cuts =
neuper@37906: [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allp new [2]";
neuper@37906:
neuper@37906: val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
neuper@37906: if cuts = cuts2 @ [([2], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allps new [2]";
neuper@37906:
neuper@37906:
neuper@37906: "---(4) on S(606)..S(608)--------";
neuper@37906: "--- nd [3] subproblem--------------------------------------";
neuper@37906: val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
neuper@37906: if cuts =
neuper@37906: [([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allp new [3]";
neuper@37906:
neuper@37906: val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
neuper@37906: if cuts = cuts2 @ [([3], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allps new [3]";
neuper@37906:
neuper@37906: "--- nd [3,2] with 2 children--------------------------------";
neuper@37906: val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
neuper@37906: if cuts =
neuper@37906: [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allp new [3,2]";
neuper@37906:
neuper@37906: val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
neuper@37906: if cuts = cuts2 @ [([3, 2], Res)] then () else
neuper@38031: error "ctree.sml diff.behav. get_allps new [3,2]";
neuper@37906:
neuper@37906: "---(5a) on S(606)..S(608)--------";
neuper@37906: "--- nd [3,2,1] with 0 children------------------------------";
neuper@37906: val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
neuper@37906: if cuts =
neuper@37906: [] then () else
neuper@38031: error "ctree.sml diff.behav. get_allp new [3,2,1]";
neuper@37906:
neuper@37906: val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
neuper@37906: if cuts = cuts2 @ [] then () else
neuper@38031: error "ctree.sml diff.behav. get_allps new [3,2,1]";
neuper@37906:
neuper@37906:
neuper@37906: (**#################################################################**)
wneuper@59279: "-------------- cut_tree new (from ctree above)-------------------";
wneuper@59279: "-------------- cut_tree new (from ctree above)-------------------";
wneuper@59279: "-------------- cut_tree new (from ctree above)-------------------";
neuper@37906: show_pt pt;
neuper@37906: val b = get_obj g_branch pt [];
neuper@37906: if b = TransitiveB then () else
neuper@38031: error ("ctree.sml diff.behav. in [] branch="^branch2str b);
neuper@37906: val b = get_obj g_branch pt [3];
neuper@37906: if b = TransitiveB then () else
neuper@38031: error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
neuper@37906:
neuper@37906: "---(2) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cut_tree pt ([1],Res);
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
neuper@37906: ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
neuper@37906: (*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
neuper@38031: error "ctree.sml: diff.behav. cut_tree ([1],Res)";
neuper@37906:
neuper@37906:
neuper@37906: "---(3) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cut_tree pt ([2],Res);
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [(*preceding step on WS was ([1]),Res*)
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm),
neuper@37906: ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
neuper@38031: else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
neuper@37906:
neuper@37906: "---(4) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cut_tree pt ([3],Pbl);
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
neuper@38031: then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
neuper@37906:
neuper@37906: "---(5a) on S(606)..S(608) cut_tree --------";
neuper@37906: val (pt', cuts) = cut_tree pt ([3,2,1],Res);
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 1;
neuper@37906: if cuts = [([3, 2, 2], Res), ([3, 2], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans:*)
neuper@37906: ([3], Res), ([4], Res),([],Res)] then ()
neuper@38031: else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
neuper@37906: show_pt pt';
neuper@37906:
neuper@37906:
neuper@37906: "-------------- cappend on complete ctree from above -------------";
neuper@37906: "-------------- cappend on complete ctree from above -------------";
neuper@37906: "-------------- cappend on complete ctree from above -------------";
neuper@37906: show_pt pt;
neuper@37906:
neuper@37906: "---(2) on S(606)..S(608)--------";
akargl@42193: (*========== inhibit exn AK110726 ==============================================
akargl@42193: (* ERROR: Can't unify istate to istate * Proof.context *)
neuper@37906: val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
neuper@37906: (Tac "test") (str2term "Inres[1]",[]) Complete;
akargl@42120:
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
neuper@37906: ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
neuper@38031: else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
akargl@42120:
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
neuper@37906: if afterins = [([1], Frm), ([1], Res)
neuper@37906: (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
neuper@38031: else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
neuper@37906: show_pt pt';
neuper@37906: "---(3) on S(606)..S(608)--------";
neuper@37906: show_pt pt;
neuper@37906: val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
neuper@37906: (Tac "test") (str2term "Inres[2]",[]) Complete;
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
akargl@42193:
neuper@37906: if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
neuper@37906: ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
neuper@37906: ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
neuper@38031: else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
akargl@42193:
akargl@42193:
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
akargl@42193:
neuper@37906: if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
neuper@37906: (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
neuper@37906: then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
neuper@37906: show_pt pt';
akargl@42193:
akargl@42193:
neuper@37906: (*
neuper@37906: val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
neuper@37906: val p = move_dn [] pt' p (*-> ([1],Res)*);
neuper@37906: val p = move_dn [] pt' p (*-> ([2],Frm)*);
neuper@37906: val p = move_dn [] pt' p (*-> ([2],Res)*);
neuper@37906:
neuper@37906: term2str (get_obj g_form pt' [2]);
neuper@37906: term2str (get_obj g_res pt' [2]);
neuper@37906: ostate2str (get_obj g_ostate pt' [2]);
neuper@37906: *)
neuper@37906:
neuper@37906: "---(4) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
neuper@37906: ([],e_spec, str2term "Inhead[3]");
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: ([3], Res), ([4], Res),
neuper@37906: (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
neuper@38031: error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
neuper@37906: if afterins =
neuper@37906: [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
neuper@37906: ([3], Pbl)] then () else
neuper@38031: error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
neuper@37906: (* use"systest/ctree.sml";
neuper@37906: use"ctree.sml";
neuper@37906: *)
neuper@37906:
neuper@37906: "---(6-1) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
neuper@37906: (Tac "test") (str2term "Inres[3,1]",[]) Complete;
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
neuper@37906: ([3, 2], Res),
neuper@37906: (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
akargl@42120:
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
neuper@37906: (*WN060727 replaced after overwriting cutlevup by test_trans
neuper@37906: if afterins = [([1], Frm), ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
neuper@37906: ([3], Res)(*cutlevup=false*),
neuper@37906: ([4], Res),
neuper@37906: ([], Res)(*cutlevup=false*)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
neuper@37906: *)
neuper@37906: if afterins = [([1], Frm), ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
neuper@37906:
neuper@37906: if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
neuper@37906:
neuper@37906: "---(6) on S(606)..S(608)--------";
neuper@37906: val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
neuper@37906: (Tac "test") (str2term "Inres[3,2]",[]) Complete;
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 3;
neuper@37906: if cuts = [(*just after is: cutlevup=false in [3]*)
neuper@37906: (*WN060727 after test_trans instead cutlevup added:*)
neuper@37906: ([3], Res), ([4], Res), ([], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
neuper@37906: (*WN060727 replaced after overwriting cutlevup by test_trans
neuper@37906: if afterins = [([1], Frm), ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
neuper@37906: ([3], Res),
neuper@37906: ([4], Res), ([], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
neuper@37906: *)
neuper@37906: if afterins = [([1], Frm), ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
neuper@37906: then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
neuper@37906:
neuper@37906: if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
neuper@37906:
neuper@37906: "---(6++) on S(606)..S(608)--------";
neuper@37906: (**)
neuper@37906: val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
neuper@37906: (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
wneuper@59111: default_print_depth 99;
neuper@37906: cuts;
wneuper@59111: default_print_depth 1;
neuper@37906: if cuts = [([3, 2, 2], Res), ([3, 2], Res),
neuper@37906: (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
neuper@37906: then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
neuper@37906: val afterins = get_allp [] ([], ([],Frm)) pt';
wneuper@59111: default_print_depth 99;
neuper@37906: afterins;
wneuper@59111: default_print_depth 3;
neuper@37906: if afterins = [([1], Frm), ([1], Res),
neuper@37906: ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
neuper@37906: ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
neuper@37906: ([2], Res),
neuper@37906: ([3], Pbl),
neuper@37906: ([3, 1], Frm), ([3, 1], Res),
neuper@37906: ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
neuper@38031: error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
neuper@37906: if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
neuper@38031: error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
neuper@37906: (*
neuper@37906: show_pt pt';
neuper@37906: show_pt pt;
neuper@37906: *)
akargl@42193: ========== inhibit exn AK110726 ==============================================*)
neuper@42360:
neuper@42360: "-------------- subst2subs subs2subst sube2subst subte2subst -----";
neuper@42360: "-------------- subst2subs subs2subst sube2subst subte2subst -----";
neuper@42360: "-------------- subst2subs subs2subst sube2subst subte2subst -----";
neuper@42360: val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];
neuper@42360:
neuper@42360: if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()
neuper@42360: else error "subte2sube broken";
neuper@42360:
neuper@42360: subst2subs : (term * term) list -> string list;
neuper@42360: if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()
neuper@42360: else error "subst2subs broken";
neuper@42360:
neuper@42360: subst2subs' : (term * term) list -> (string * string) list;
neuper@42360: if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()
neuper@42360: else error "subst2subs' broken";
neuper@42360:
neuper@42360: subs2subst : theory -> string list -> (term * term) list;
neuper@42360: val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];
neuper@42360: if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
neuper@42360: term2str i2 = "err" andalso term2str v2 = "0" then ()
neuper@42360: else error "subs2subst broken";
neuper@42360:
neuper@42360: sube2subst : theory -> string list -> (term * term) list;
neuper@42360: val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];
neuper@42360: if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
neuper@42360: term2str i2 = "err" andalso term2str v2 = "0" then ()
neuper@42360: else error "sube2subst broken";
neuper@42360:
neuper@42360: sube2subte : string list -> term list;
neuper@42360: val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];
neuper@42360: if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()
neuper@42360: else error "sube2subte broken";
neuper@42360:
neuper@42360: val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];
neuper@42360: if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
neuper@42360: term2str i2 = "err" andalso term2str v2 = "0" then ()
neuper@42360: else error "subte2subst broken";
neuper@42360: