test/Tools/isac/Interpret/mstools.sml
branchdecompose-isar
changeset 41977 a3ce4017f41d
parent 41976 792c59bf54d4
child 41982 90f65f1b6351
     1.1 --- a/test/Tools/isac/Interpret/mstools.sml	Thu May 05 14:21:54 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Fri May 06 11:18:07 2011 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  "----------- fun declare_constraints --------------------";
     1.5  "----------- fun get_assumptions, fun get_environments --";
     1.6  "----------- fun transfer_from_subproblem ---------------";
     1.7 -"----------- all handling ctxt in minimsubpbl x+1=2  ----";
     1.8 +"----------- all handling ctxt in minimsubpbl x+1=2 -----";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11  "--------------------------------------------------------";
    1.12 @@ -63,5 +63,37 @@
    1.13  "----------- all handling ctxt in minimsubpbl x+1=2  ----";
    1.14  "----------- all handling ctxt in minimsubpbl x+1=2  ----";
    1.15  "----------- all handling ctxt in minimsubpbl x+1=2  ----";
    1.16 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.17 +val (dI',pI',mI') =
    1.18 +  ("Test", ["sqroot-test","univariate","equation","test"],
    1.19 +   ["Test","squ-equ-test-subpbl1"]);
    1.20 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.21 +print_depth 999; pt; (*see tmp/del.sml*)
    1.22 +(*GOON ---------------------------
    1.23 +val SOME (_, ctxt) = get_obj g_env pt (fst p);
    1.24 +if parseNEW ctxt "x+y+z" =  parseNEW ctxt "x+y+(z::real)" andalso
    1.25 +   parseNEW ctxt "a+b+c" <> parseNEW ctxt "a+b+(c::real)" then ()
    1.26 +else error "mstools.sml: ctxt initialisation broken in rootproblem";
    1.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    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 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.32 +(*nxt = Specify_Problem*)
    1.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.34 +(* check precond_root_1, precond_root_2 in root-ctxt TODO *)
    1.35 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.36 +(*nxt = Apply_Method*)
    1.37 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.38 +(* check precond_root_1, precond_root_2 in sub-ctxt TODO *)
    1.39 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.40 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.41 +(*nxt = Subproblem*)
    1.42 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.43 +(* check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a in subproblem*)
    1.44 +print_depth 999; pt; (*see tmp/del.sml*)
    1.45 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.46 +(*nxt = Tac..ERROR*)
    1.47 +---------------------------GOON *)
    1.48  
    1.49