test/Tools/isac/Interpret/ctree.sml
branchdecompose-isar
changeset 41990 99e83a0bea44
parent 41989 235f3990c9b7
child 41992 1ada058e92bc
     1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri May 13 17:19:38 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  "table of contents -----------------------------------------------";
     1.5  "-----------------------------------------------------------------";
     1.6  "-----------------------------------------------------------------";
     1.7 +"-------------- fun get_ctxt -------------------------------------";
     1.8  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
     1.9  "-------------- check positions in miniscript --------------------";
    1.10  "-------------- get_allpos' (from ptree above)--------------------";
    1.11 @@ -59,6 +60,20 @@
    1.12  "-----------------------------------------------------------------";
    1.13  
    1.14  
    1.15 +"-------------- fun get_ctxt -------------------------------------";
    1.16 +"-------------- fun get_ctxt -------------------------------------";
    1.17 +"-------------- fun get_ctxt -------------------------------------";
    1.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.19 +val (dI',pI',mI') =
    1.20 +  ("Test", ["sqroot-test","univariate","equation","test"],
    1.21 +   ["Test","squ-equ-test-subpbl1"]);
    1.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.23 +(get_ctxt pt p)
    1.24 +  handle _ => error "ctree.sml: not even some ctxt found in PblObj";
    1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.26 +(get_ctxt pt p)
    1.27 +  handle _ => error "ctree.sml: not even some ctxt found in PrfObj";
    1.28 +
    1.29  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.30  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.31  "-------------- fun update_ctxt, fun g_ctxt ----------------------";