test/Tools/isac/Test_Isac.thy
branchdecompose-isar
changeset 41976 792c59bf54d4
parent 41975 61f358925792
child 41977 a3ce4017f41d
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu May 05 09:23:32 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu May 05 14:21:54 2011 +0200
     1.3 @@ -148,6 +148,44 @@
     1.4  Model_Problem';
     1.5  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
     1.6  *}
     1.7 +ML {*
     1.8 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
     1.9 +val (dI',pI',mI') =
    1.10 +  ("Test", ["sqroot-test","univariate","equation","test"],
    1.11 +   ["Test","squ-equ-test-subpbl1"]);
    1.12 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.13 +(*nxt = Model_Problem*)
    1.14 +print_depth 999; pt;
    1.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.16 +(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
    1.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.21 +(*nxt = Specify_Problem*)
    1.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.23 +(* check precond_root_1, precond_root_2 in root-ctxt *)
    1.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.25 +(*nxt = Apply_Method*)
    1.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.27 +(*check precond_root_1, precond_root_2 in sub-ctxt *)
    1.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.30 +*}
    1.31 +ML {*
    1.32 +(*nxt = Subproblem*)
    1.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.34 +*}
    1.35 +ML {*
    1.36 +(*nxt = Model_Problem*)
    1.37 +print_depth 999; pt;
    1.38 +*}
    1.39 +ML {*
    1.40 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.41 +(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
    1.42 +(*nxt = ERROR*)
    1.43 +*}
    1.44 +
    1.45    use "Interpret/mstools.sml"       (*new 2010*)
    1.46    use "Interpret/ctree.sml"         (*!...see(25)*)
    1.47    use "Interpret/ptyps.sml"         (*    *)