1.1 --- a/src/sml/ME/ctree.sml Sat Mar 05 14:36:49 2005 +0100
1.2 +++ b/src/sml/ME/ctree.sml Sat Mar 05 17:26:21 2005 +0100
1.3 @@ -1231,6 +1231,8 @@
1.4 | update_loc pt (p,_) x =
1.5 let val (_,lres) = get_obj g_loc pt p
1.6 in appl_obj (repl_loc (Some x,lres)) pt p end;
1.7 +(*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1.8 +fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
1.9
1.10 (*13.8.02---------------------------
1.11 fun get_loc EmptyPtree _ = None
1.12 @@ -1824,7 +1826,7 @@
1.13 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1.14 end
1.15 end;
1.16 -
1.17 +
1.18
1.19 fun cut_tree pt (pos,_) =
1.20 if not (existpt pos pt)
1.21 @@ -1870,14 +1872,39 @@
1.22 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.23 );
1.24 fun cappend_atomic pt p loc f r f' s =
1.25 -let val _= writeln("##@cappend_atomic: pos ="^pos2str p)
1.26 - val _= writeln("##@cappend_atomic before cut_tree: loc ="^istate2str loc)
1.27 - val (pt', cs) = cut_tree pt (p,Frm)
1.28 +let val _= writeln("##@cappend_atomic: pos ="^pos2str p);
1.29 + val _= writeln("##@cappend_atomic arg loc ="^istate2str loc);
1.30 + val _= if existpt p pt
1.31 + then writeln("##@cappend_atomic before cut_ loc ="^
1.32 + istates2str (get_obj g_loc pt p))
1.33 + else writeln("##@cappend_atomic pos not existent before cut_");
1.34 + val (pt', cs) = cut_tree pt (p,Frm);
1.35 + val _= if existpt p pt'
1.36 + then writeln("##@cappend_atomic after cut_ loc ="^
1.37 + istates2str (get_obj g_loc pt' p))
1.38 + else writeln("##@cappend_atomic pos not existent after cut_");
1.39 + val pt'' = append_atomic p loc f r f' s pt';
1.40 + val _= writeln("##@cappend_atomic after append: loc ="^
1.41 + istates2str (get_obj g_loc pt'' p));
1.42 +in (pt'', cs) end;
1.43 +
1.44 +fun cappend_atomic pt p loc f r f' s =
1.45 +let val (pt', cs) = cut_tree pt (p,Frm)
1.46 val pt'' = append_atomic p loc f r f' s pt'
1.47 - val _= writeln("##@cappend_atomic after append: loc ="^
1.48 - istates2str (get_obj g_loc pt'' p))
1.49 in (pt'', cs) end;
1.50
1.51 +fun cappend_atomic pt p ist_res f r f' s =
1.52 + if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.53 + then (*after Take: transfer Frm and respective istate*)
1.54 + let val (ist_form, f) = (get_loc pt (p,Frm),
1.55 + get_obj g_form pt p)
1.56 + val (pt, cs) = cut_tree pt (p,Frm)
1.57 + val pt = append_atomic p e_istate f r f' s pt
1.58 + val pt = update_loc' pt p (Some ist_form, Some ist_res)
1.59 + in (pt, cs) end
1.60 + else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
1.61 +
1.62 +
1.63 (* called by Take *)
1.64 fun append_form p l f pt =
1.65 (writeln("##@append_form: pos ="^pos2str p);
2.1 --- a/src/sml/systest/auto-inform.sml Sat Mar 05 14:36:49 2005 +0100
2.2 +++ b/src/sml/systest/auto-inform.sml Sat Mar 05 17:26:21 2005 +0100
2.3 @@ -9,15 +9,15 @@
2.4 "--------- maximum-example: complete_mod -------------------------";
2.5 "appendForm with miniscript with mini-subpbl:";
2.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
2.7 -"--------- appendFormula: on Frm + equ_nrls ----------------------X";
2.8 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
2.9 "--------- appendFormula: on Res + NO deriv ----------------------";
2.10 "--------- appendFormula: on Res + late deriv --------------------";
2.11 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
2.12 "replaceForm with miniscript with mini-subpbl:";
2.13 "--------- replaceFormula: on Res + = ----------------------------";
2.14 -"--------- replaceFormula: on Res + = 1st Nd ---------------------X";
2.15 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
2.16 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
2.17 -"--------- replaceFormula: cut calculation -----------------------X";
2.18 +"--------- replaceFormula: cut calculation -----------------------";
2.19
2.20
2.21
2.22 @@ -309,49 +309,8 @@
2.23 Iterator 1; moveActiveRoot 1;
2.24 autoCalculate 1 CompleteCalcHead;
2.25 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
2.26 - (*> ###generate1 Apply_Method': pos = ([1], Frm)
2.27 -###generate1 Apply_Method': topt= Some x + 1 = 2
2.28 -###generate1 Apply_Method': is = ScrState (["
2.29 -(e_, x + 1 = 2)","
2.30 -(v_, x)"],
2.31 - [], None,
2.32 - ??.empty, Safe, true)
2.33 -##@cappend_form: pos =[1]
2.34 -##@cappend_form before cut_tree: loc =ScrState (["
2.35 -(e_, x + 1 = 2)","
2.36 -(v_, x)"],
2.37 - [], None,
2.38 - ??.empty, Safe, true)
2.39 -##@append_form: pos =[1]
2.40 -##@cappend_form after append: loc =(#Some ScrState (["
2.41 -(e_, x + 1 = 2)","
2.42 -(v_, x)"],
2.43 - [], None,
2.44 - ??.empty, Safe, true),
2.45 - #None)
2.46 -###generate1 Apply_Method: after cappend
2.47 -*)
2.48 +
2.49 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
2.50 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@;(**)
2.51 -(*
2.52 -> appendFormula 1 "2+ -1 + x = 2";
2.53 -###generate1 Rewrite_Set': pos= ([1], Frm)
2.54 -##@cappend_atomic: pos =[1]
2.55 -##@cappend_atomic before cut_tree: loc =ScrState (["
2.56 -(e_, x + 1 = 2)","
2.57 -(v_, x)"],
2.58 - [R,L,R,L,L,R,R], Some e_,
2.59 - x + 1 + -1 * 2 = 0, Sundef, false)
2.60 -#@append_atomic: pos =[1]
2.61 -##@cappend_atomic after append: loc =(#None,
2.62 -#Some ScrState (["
2.63 -(e_, x + 1 = 2)","
2.64 -(v_, x)"],
2.65 - [R,L,R,L,L,R,R], Some e_,
2.66 - x + 1 + -1 * 2 = 0, Sundef, false))
2.67 -Exception- Bind raised
2.68 -*)
2.69 -
2.70
2.71 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
2.72 >>>>>>> 1.8
2.73 @@ -375,8 +334,6 @@
2.74 val ((pt,_),_) = get_calc 1;
2.75 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
2.76 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
2.77 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
2.78 -
2.79
2.80
2.81 "--------- appendFormula: on Res + NO deriv ----------------------";
2.82 @@ -486,7 +443,7 @@
2.83 val str = pr_ptree pr_short pt;
2.84 writeln str;
2.85 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
2.86 - else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 1";
2.87 + else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";
2.88 autoCalculate 1 CompleteCalc;
2.89 val ((pt,pos as(p,_)),_) = get_calc 1;
2.90 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
2.91 @@ -496,7 +453,6 @@
2.92 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
2.93 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
2.94 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
2.95 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**)
2.96 states:=[];
2.97 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
2.98 ("Test.thy",
2.99 @@ -517,7 +473,6 @@
2.100 val ((pt,pos as(p,_)),_) = get_calc 1;
2.101 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
2.102 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
2.103 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
2.104
2.105
2.106 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
2.107 @@ -547,7 +502,6 @@
2.108 "--------- replaceFormula: cut calculation -----------------------";
2.109 "--------- replaceFormula: cut calculation -----------------------";
2.110 "--------- replaceFormula: cut calculation -----------------------";
2.111 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**)
2.112 states:=[];
2.113 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
2.114 ("Test.thy",
2.115 @@ -565,7 +519,6 @@
2.116 writeln str;
2.117 if p = ([1], Res) then ()
2.118 else raise error "auto-inform.sml: diff.behav. cut calculation 2";
2.119 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
2.120
2.121
2.122