1.1 --- a/src/sml/systest/auto-inform.sml Sat Mar 05 14:36:49 2005 +0100
1.2 +++ b/src/sml/systest/auto-inform.sml Sat Mar 05 17:26:21 2005 +0100
1.3 @@ -9,15 +9,15 @@
1.4 "--------- maximum-example: complete_mod -------------------------";
1.5 "appendForm with miniscript with mini-subpbl:";
1.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.7 -"--------- appendFormula: on Frm + equ_nrls ----------------------X";
1.8 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
1.9 "--------- appendFormula: on Res + NO deriv ----------------------";
1.10 "--------- appendFormula: on Res + late deriv --------------------";
1.11 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.12 "replaceForm with miniscript with mini-subpbl:";
1.13 "--------- replaceFormula: on Res + = ----------------------------";
1.14 -"--------- replaceFormula: on Res + = 1st Nd ---------------------X";
1.15 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.16 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.17 -"--------- replaceFormula: cut calculation -----------------------X";
1.18 +"--------- replaceFormula: cut calculation -----------------------";
1.19
1.20
1.21
1.22 @@ -309,49 +309,8 @@
1.23 Iterator 1; moveActiveRoot 1;
1.24 autoCalculate 1 CompleteCalcHead;
1.25 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.26 - (*> ###generate1 Apply_Method': pos = ([1], Frm)
1.27 -###generate1 Apply_Method': topt= Some x + 1 = 2
1.28 -###generate1 Apply_Method': is = ScrState (["
1.29 -(e_, x + 1 = 2)","
1.30 -(v_, x)"],
1.31 - [], None,
1.32 - ??.empty, Safe, true)
1.33 -##@cappend_form: pos =[1]
1.34 -##@cappend_form before cut_tree: loc =ScrState (["
1.35 -(e_, x + 1 = 2)","
1.36 -(v_, x)"],
1.37 - [], None,
1.38 - ??.empty, Safe, true)
1.39 -##@append_form: pos =[1]
1.40 -##@cappend_form after append: loc =(#Some ScrState (["
1.41 -(e_, x + 1 = 2)","
1.42 -(v_, x)"],
1.43 - [], None,
1.44 - ??.empty, Safe, true),
1.45 - #None)
1.46 -###generate1 Apply_Method: after cappend
1.47 -*)
1.48 +
1.49 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
1.50 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@;(**)
1.51 -(*
1.52 -> appendFormula 1 "2+ -1 + x = 2";
1.53 -###generate1 Rewrite_Set': pos= ([1], Frm)
1.54 -##@cappend_atomic: pos =[1]
1.55 -##@cappend_atomic before cut_tree: loc =ScrState (["
1.56 -(e_, x + 1 = 2)","
1.57 -(v_, x)"],
1.58 - [R,L,R,L,L,R,R], Some e_,
1.59 - x + 1 + -1 * 2 = 0, Sundef, false)
1.60 -#@append_atomic: pos =[1]
1.61 -##@cappend_atomic after append: loc =(#None,
1.62 -#Some ScrState (["
1.63 -(e_, x + 1 = 2)","
1.64 -(v_, x)"],
1.65 - [R,L,R,L,L,R,R], Some e_,
1.66 - x + 1 + -1 * 2 = 0, Sundef, false))
1.67 -Exception- Bind raised
1.68 -*)
1.69 -
1.70
1.71 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.72 >>>>>>> 1.8
1.73 @@ -375,8 +334,6 @@
1.74 val ((pt,_),_) = get_calc 1;
1.75 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.76 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.77 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
1.78 -
1.79
1.80
1.81 "--------- appendFormula: on Res + NO deriv ----------------------";
1.82 @@ -486,7 +443,7 @@
1.83 val str = pr_ptree pr_short pt;
1.84 writeln str;
1.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()
1.86 - else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 1";
1.87 + else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";
1.88 autoCalculate 1 CompleteCalc;
1.89 val ((pt,pos as(p,_)),_) = get_calc 1;
1.90 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.91 @@ -496,7 +453,6 @@
1.92 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.93 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.94 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.95 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**)
1.96 states:=[];
1.97 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.98 ("Test.thy",
1.99 @@ -517,7 +473,6 @@
1.100 val ((pt,pos as(p,_)),_) = get_calc 1;
1.101 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.102 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.103 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
1.104
1.105
1.106 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.107 @@ -547,7 +502,6 @@
1.108 "--------- replaceFormula: cut calculation -----------------------";
1.109 "--------- replaceFormula: cut calculation -----------------------";
1.110 "--------- replaceFormula: cut calculation -----------------------";
1.111 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**)
1.112 states:=[];
1.113 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.114 ("Test.thy",
1.115 @@ -565,7 +519,6 @@
1.116 writeln str;
1.117 if p = ([1], Res) then ()
1.118 else raise error "auto-inform.sml: diff.behav. cut calculation 2";
1.119 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
1.120
1.121
1.122