test/Tools/isac/Interpret/ctree.sml
branchdecompose-isar
changeset 41970 25957ffe68e8
parent 41968 3228aa46fd30
child 41972 22c5483e9bfb
     1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Tue May 03 15:58:04 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Tue May 03 16:20:55 2011 +0200
     1.3 @@ -323,8 +323,7 @@
     1.4  "=====new ptree 1a miniscript with mini-subpbl ===================";
     1.5  "=====new ptree 1a miniscript with mini-subpbl ===================";
     1.6  "=====new ptree 1a miniscript with mini-subpbl ===================";
     1.7 -val fmz = ["equality (x+1=2)",
     1.8 -	   "solveFor x","solutions L"];
     1.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.10  val (dI',pI',mI') =
    1.11    ("Test",["sqroot-test","univariate","equation","test"],
    1.12     ["Test","squ-equ-test-subpbl1"]);
    1.13 @@ -366,10 +365,8 @@
    1.14  "=====new ptree 2 miniscript with mini-subpbl ====================";
    1.15  "=====new ptree 2 miniscript with mini-subpbl ====================";
    1.16   states:=[];
    1.17 - CalcTree
    1.18 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.19 -   ("Test", 
    1.20 -    ["sqroot-test","univariate","equation","test"],
    1.21 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.22 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.23      ["Test","squ-equ-test-subpbl1"]))];
    1.24   Iterator 1; moveActiveRoot 1;
    1.25   autoCalculate 1 CompleteCalc; 
    1.26 @@ -431,8 +428,7 @@
    1.27  "-------------- cappend minisubpbl -------------------------------";
    1.28  "-------------- cappend minisubpbl -------------------------------";
    1.29  "=====new ptree 1 miniscript with mini-subpbl ====================";
    1.30 -val fmz = ["equality (x+1=2)",
    1.31 -	   "solveFor x","solutions L"];
    1.32 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.33  val (dI',pI',mI') =
    1.34    ("Test",["sqroot-test","univariate","equation","test"],
    1.35     ["Test","squ-equ-test-subpbl1"]);
    1.36 @@ -533,10 +529,8 @@
    1.37  "=====new ptree 3 ================================================";
    1.38  "=====new ptree 3 ================================================";
    1.39   states:=[];
    1.40 - CalcTree
    1.41 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.42 -   ("Test", 
    1.43 -    ["sqroot-test","univariate","equation","test"],
    1.44 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.45 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.46      ["Test","squ-equ-test-subpbl1"]))];
    1.47   Iterator 1; moveActiveRoot 1;
    1.48   autoCalculate 1 CompleteCalc; 
    1.49 @@ -617,10 +611,8 @@
    1.50  "------ move into detail -----------------------------------------";
    1.51  "------ move into detail -----------------------------------------";
    1.52   states:=[];
    1.53 - CalcTree
    1.54 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.55 -   ("Test", 
    1.56 -    ["sqroot-test","univariate","equation","test"],
    1.57 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.58 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.59      ["Test","squ-equ-test-subpbl1"]))];
    1.60   Iterator 1; moveActiveRoot 1;
    1.61   autoCalculate 1 CompleteCalc; 
    1.62 @@ -651,10 +643,8 @@
    1.63  "=====new ptree 3a ===============================================";
    1.64  "=====new ptree 3a ===============================================";
    1.65   states:=[];
    1.66 - CalcTree
    1.67 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.68 -   ("Test", 
    1.69 -    ["sqroot-test","univariate","equation","test"],
    1.70 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.71 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.72      ["Test","squ-equ-test-subpbl1"]))];
    1.73   Iterator 1; moveActiveRoot 1;
    1.74   autoCalculate 1 CompleteCalcHead; 
    1.75 @@ -908,10 +898,8 @@
    1.76  "=====new ptree 5 minisubpbl =====================================";
    1.77  "=====new ptree 5 minisubpbl =====================================";
    1.78  states:=[];
    1.79 -CalcTree
    1.80 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.81 -   ("Test", 
    1.82 -    ["sqroot-test","univariate","equation","test"],
    1.83 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.84 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.85      ["Test","squ-equ-test-subpbl1"]))];
    1.86  Iterator 1; moveActiveRoot 1;
    1.87  autoCalculate 1 CompleteCalc; 
    1.88 @@ -987,10 +975,8 @@
    1.89  "=====new ptree 6 minisubpbl intersteps ==========================";
    1.90  "=====new ptree 6 minisubpbl intersteps ==========================";
    1.91  states:=[];
    1.92 -CalcTree
    1.93 - [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.94 -   ("Test", 
    1.95 -    ["sqroot-test","univariate","equation","test"],
    1.96 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.97 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.98      ["Test","squ-equ-test-subpbl1"]))];
    1.99  Iterator 1; moveActiveRoot 1;
   1.100  autoCalculate 1 CompleteCalc;