1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Thu Jan 05 17:43:48 2012 +0100
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Sat Jan 07 10:06:06 2012 +0100
     1.3 @@ -46,6 +46,7 @@
     1.4  "=====new ptree 6 minisubpbl intersteps ==========================";
     1.5  "-------------- get_allpos' new ----------------------------------";
     1.6  "-------------- cut_tree new (from ptree above)-------------------";
     1.7 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -1373,3 +1374,42 @@
    1.12  show_pt pt;
    1.13  *)
    1.14  ========== inhibit exn AK110726 ==============================================*)
    1.15 +
    1.16 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
    1.17 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
    1.18 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
    1.19 +val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];
    1.20 +
    1.21 +if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()
    1.22 +else error "subte2sube broken";
    1.23 +
    1.24 +subst2subs : (term * term) list -> string list;
    1.25 +if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()
    1.26 +else error "subst2subs broken";
    1.27 +
    1.28 +subst2subs' : (term * term) list -> (string * string) list;
    1.29 +if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()
    1.30 +else error "subst2subs' broken";
    1.31 +
    1.32 +subs2subst : theory -> string list -> (term * term) list;
    1.33 +val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];
    1.34 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
    1.35 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
    1.36 +else error "subs2subst broken";
    1.37 +
    1.38 +sube2subst : theory -> string list -> (term * term) list;
    1.39 +val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];
    1.40 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
    1.41 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
    1.42 +else error "sube2subst broken";
    1.43 +
    1.44 +sube2subte : string list -> term list;
    1.45 +val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];
    1.46 +if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()
    1.47 +else error "sube2subte broken";
    1.48 +
    1.49 +val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];
    1.50 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
    1.51 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
    1.52 +else error "subte2subst broken";
    1.53 +