test/Tools/isac/ME/me.sml
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37906 e2b23ba9df13
     1.1 --- a/test/Tools/isac/ME/me.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/test/Tools/isac/ME/me.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -344,23 +344,23 @@
     1.4   val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.5   val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.6   (*xt = Add_Given "solveFor x"*)
     1.7 - writeln (itms2str thy (get_obj g_pbl pt (fst p)));   
     1.8 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));   
     1.9  (*[
    1.10  (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
    1.11  (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
    1.12  (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
    1.13   val (pt,p) = complete_mod (pt, p);
    1.14 - if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
    1.15 + if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
    1.16   else raise error "completetest.sml: new behav. in complete_mod 1";
    1.17 - writeln (itms2str thy (get_obj g_pbl pt (fst p)));   
    1.18 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));   
    1.19  (*[
    1.20  (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
    1.21  (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
    1.22  (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
    1.23   val mits = get_obj g_met pt (fst p);
    1.24 - if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" 
    1.25 + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" 
    1.26   then () else raise error "completetest.sml: new behav. in complete_mod 2";
    1.27 - writeln (itms2str thy mits);   
    1.28 + writeln (itms2str_ ctxt mits);   
    1.29  (*[
    1.30  (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
    1.31  (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
    1.32 @@ -446,7 +446,7 @@
    1.33  (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
    1.34  (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
    1.35   val pits = get_obj g_pbl pt (fst p);
    1.36 - writeln (itms2str thy pits);
    1.37 + writeln (itms2str_ ctxt pits);
    1.38  (*[
    1.39  (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
    1.40  (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
    1.41 @@ -456,7 +456,7 @@
    1.42   val mits = get_obj g_met pt (fst p);
    1.43   val mits = complete_metitms oris pits [] 
    1.44  			((#ppc o get_met) ["DiffApp","max_by_calculus"]);
    1.45 - writeln (itms2str thy mits);
    1.46 + writeln (itms2str_ ctxt mits);
    1.47  (*[
    1.48  (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
    1.49  (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
    1.50 @@ -467,7 +467,7 @@
    1.51  (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
    1.52  0 <= x & x <= 2 * r}])),
    1.53  (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
    1.54 - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
    1.55 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
    1.56   else raise error "completetest.sml: new behav. in complete_metitms 1";
    1.57  
    1.58  
    1.59 @@ -494,7 +494,7 @@
    1.60   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.61   (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
    1.62   val pits = get_obj g_pbl pt (fst p);
    1.63 - writeln (itms2str thy pits);
    1.64 + writeln (itms2str_ ctxt pits);
    1.65  (*[
    1.66  (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
    1.67  (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
    1.68 @@ -502,9 +502,9 @@
    1.69  (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) 
    1.70   val (pt,p) = complete_mod (pt,p);
    1.71   val pits = get_obj g_pbl pt (fst p);
    1.72 - if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" 
    1.73 + if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" 
    1.74   then () else raise error "completetest.sml: new behav. in complete_mod 3";
    1.75 - writeln (itms2str thy pits);
    1.76 + writeln (itms2str_ ctxt pits);
    1.77  (*[
    1.78  (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
    1.79  (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
    1.80 @@ -512,9 +512,9 @@
    1.81  (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
    1.82  2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
    1.83   val mits = get_obj g_met pt (fst p);
    1.84 - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" 
    1.85 + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" 
    1.86   then () else raise error "completetest.sml: new behav. in complete_mod 3";
    1.87 - writeln (itms2str thy mits);
    1.88 + writeln (itms2str_ ctxt mits);
    1.89  (*[
    1.90  (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
    1.91  (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),