src/sml/systest/auto-inform.sml
changeset 2152 a863de293415
parent 2151 8df2ab3d17c9
child 2155 30bb491cf974
     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