1.1 --- a/src/sml/systest/script.sml	Thu Feb 17 15:35:04 2005 +0100
     1.2 +++ b/src/sml/systest/script.sml	Thu Feb 17 15:35:04 2005 +0100
     1.3 @@ -23,6 +23,8 @@
     1.4  "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
     1.5  "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
     1.6  
     1.7 +"--------- sel_rules ---------------------------------------------";
     1.8 +"-----------------------------------------------------------------";
     1.9  
    1.10  
    1.11  
    1.12 @@ -292,3 +294,48 @@
    1.13  \     (Repeat (Calculate power g_)) Or                        \n\
    1.14  \%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\
    1.15  \%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";
    1.16 +
    1.17 +
    1.18 +"--------- sel_rules ---------------------------------------------";
    1.19 +"--------- sel_rules ---------------------------------------------";
    1.20 +"--------- sel_rules ---------------------------------------------";
    1.21 + states:=[];
    1.22 + CalcTree
    1.23 + [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.24 +   ("Test.thy", 
    1.25 +    ["sqroot-test","univariate","equation","test"],
    1.26 +    ["Test","squ-equ-test-subpbl1"]))];
    1.27 + Iterator 1;
    1.28 + moveActiveRoot 1;
    1.29 + autoCalculate 1 CompleteCalc;
    1.30 + val ((pt,_),_) = get_calc 1;
    1.31 + show_pt pt;
    1.32 +
    1.33 + val tacs = sel_rules pt ([],Pbl);
    1.34 + if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
    1.35 + else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)";
    1.36 +
    1.37 + val tacs = sel_rules pt ([1],Res);
    1.38 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.39 +      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
    1.40 +      Check_elementwise "Assumptions"] then ()
    1.41 + else raise error "script.sml: diff.behav. in sel_rules ([1],Res)";
    1.42 +
    1.43 + val tacs = sel_rules pt ([3],Pbl);
    1.44 + if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
    1.45 + else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
    1.46 +
    1.47 + val tacs = sel_rules pt ([3,1],Res);
    1.48 + if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
    1.49 +      Rewrite_Set "Test_simplify"] then ()
    1.50 + else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
    1.51 +
    1.52 + val tacs = sel_rules pt ([3],Res);
    1.53 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.54 +      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
    1.55 +      Check_elementwise "Assumptions"] then ()
    1.56 + else raise error "script.sml: diff.behav. in sel_rules ([3],Res)";
    1.57 +
    1.58 + val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
    1.59 + if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
    1.60 + else raise error "script.sml: diff.behav. in sel_rules ([],Res)";