1.1 --- a/test/Tools/isac/Interpret/ctree.sml Thu Dec 22 14:25:34 2016 +0100
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Dec 27 13:20:33 2016 +0100
1.3 @@ -46,7 +46,7 @@
1.4 "=====new ctree 6 minisubpbl intersteps ==========================";
1.5 "-------------- get_allpos' new ----------------------------------";
1.6 "-------------- cut_tree new (from ctree above)-------------------";
1.7 -"-------------- subst2subs subs2subst sube2subst subte2subst -----";
1.8 +"-------------- repl_app------------------------------------------";
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 "-----------------------------------------------------------------";
1.12 @@ -1137,7 +1137,7 @@
1.13 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.14 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.15 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.16 -(*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
1.17 + ([], Res)] then () else
1.18 error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1.19
1.20
1.21 @@ -1157,7 +1157,7 @@
1.22 ([3, 2], Res),
1.23 ([3], Res),
1.24 ([4], Res),
1.25 -(*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
1.26 + ([],Res)] then ()
1.27 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1.28
1.29 "---(4) on S(606)..S(608)--------";
1.30 @@ -1171,7 +1171,7 @@
1.31 ([3, 2], Res),
1.32 ([3], Res),
1.33 ([4], Res),
1.34 -(*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
1.35 + ([], Res)]
1.36 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1.37
1.38 "---(5a) on S(606)..S(608) cut_tree --------";
1.39 @@ -1179,9 +1179,7 @@
1.40 default_print_depth 99;
1.41 cuts;
1.42 default_print_depth 1;
1.43 -if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.44 -(*WN060727 added after replacing cutlevup by test_trans:*)
1.45 -([3], Res), ([4], Res),([],Res)] then ()
1.46 +if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then ()
1.47 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1.48 show_pt pt';
1.49
1.50 @@ -1204,15 +1202,14 @@
1.51 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.52 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.53 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.54 -(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.55 + ([], Res)] then ()
1.56 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1.57
1.58 val afterins = get_allp [] ([], ([],Frm)) pt';
1.59 default_print_depth 99;
1.60 afterins;
1.61 default_print_depth 3;
1.62 -if afterins = [([1], Frm), ([1], Res)
1.63 -(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1.64 +if afterins = [([1], Frm), ([1], Res)] then()
1.65 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1.66 show_pt pt';
1.67 "---(3) on S(606)..S(608)--------";
1.68 @@ -1227,7 +1224,7 @@
1.69 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1.70 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.71 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.72 -(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.73 + ([], Res)] then ()
1.74 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1.75
1.76
1.77 @@ -1236,8 +1233,7 @@
1.78 afterins;
1.79 default_print_depth 3;
1.80
1.81 -if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1.82 -(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1.83 +if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)]
1.84 then () else
1.85 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1.86 show_pt pt';
1.87 @@ -1265,7 +1261,7 @@
1.88 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.89 ([3, 2], Res),
1.90 ([3], Res), ([4], Res),
1.91 -(*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
1.92 + ([], Res)] then ()else
1.93 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1.94 val afterins = get_allp [] ([], ([],Frm)) pt';
1.95 default_print_depth 99;
1.96 @@ -1295,18 +1291,6 @@
1.97 default_print_depth 99;
1.98 afterins;
1.99 default_print_depth 3;
1.100 -(*WN060727 replaced after overwriting cutlevup by test_trans
1.101 -if afterins = [([1], Frm), ([1], Res),
1.102 - ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.103 - ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.104 - ([2], Res),
1.105 - ([3], Pbl),
1.106 - ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
1.107 - ([3], Res)(*cutlevup=false*),
1.108 - ([4], Res),
1.109 - ([], Res)(*cutlevup=false*)] then () else
1.110 -error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.111 -*)
1.112 if afterins = [([1], Frm), ([1], Res),
1.113 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.114 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.115 @@ -1324,25 +1308,12 @@
1.116 default_print_depth 99;
1.117 cuts;
1.118 default_print_depth 3;
1.119 -if cuts = [(*just after is: cutlevup=false in [3]*)
1.120 -(*WN060727 after test_trans instead cutlevup added:*)
1.121 - ([3], Res), ([4], Res), ([], Res)] then () else
1.122 +if cuts = [([3], Res), ([4], Res), ([], Res)] then () else
1.123 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1.124 val afterins = get_allp [] ([], ([],Frm)) pt';
1.125 default_print_depth 99;
1.126 afterins;
1.127 default_print_depth 3;
1.128 -(*WN060727 replaced after overwriting cutlevup by test_trans
1.129 -if afterins = [([1], Frm), ([1], Res),
1.130 - ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.131 - ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.132 - ([2], Res),
1.133 - ([3], Pbl),
1.134 - ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
1.135 - ([3], Res),
1.136 - ([4], Res), ([], Res)] then () else
1.137 -error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.138 -*)
1.139 if afterins = [([1], Frm), ([1], Res),
1.140 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.141 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.142 @@ -1362,8 +1333,7 @@
1.143 default_print_depth 99;
1.144 cuts;
1.145 default_print_depth 1;
1.146 -if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.147 -(*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
1.148 +if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)]
1.149 then () else
1.150 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1.151 val afterins = get_allp [] ([], ([],Frm)) pt';
1.152 @@ -1385,42 +1355,16 @@
1.153 show_pt pt;
1.154 *)
1.155 ========== inhibit exn AK110726 ==============================================*)
1.156 -
1.157 -"-------------- subst2subs subs2subst sube2subst subte2subst -----";
1.158 -"-------------- subst2subs subs2subst sube2subst subte2subst -----";
1.159 -"-------------- subst2subs subs2subst sube2subst subte2subst -----";
1.160 -val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];
1.161 -
1.162 -if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()
1.163 -else error "subte2sube broken";
1.164 -
1.165 -subst2subs : (term * term) list -> string list;
1.166 -if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()
1.167 -else error "subst2subs broken";
1.168 -
1.169 -subst2subs' : (term * term) list -> (string * string) list;
1.170 -if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()
1.171 -else error "subst2subs' broken";
1.172 -
1.173 -subs2subst : theory -> string list -> (term * term) list;
1.174 -val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];
1.175 -if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1.176 - term2str i2 = "err" andalso term2str v2 = "0" then ()
1.177 -else error "subs2subst broken";
1.178 -
1.179 -sube2subst : theory -> string list -> (term * term) list;
1.180 -val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];
1.181 -if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1.182 - term2str i2 = "err" andalso term2str v2 = "0" then ()
1.183 -else error "sube2subst broken";
1.184 -
1.185 -sube2subte : string list -> term list;
1.186 -val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];
1.187 -if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()
1.188 -else error "sube2subte broken";
1.189 -
1.190 -val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];
1.191 -if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1.192 - term2str i2 = "err" andalso term2str v2 = "0" then ()
1.193 -else error "subte2subst broken";
1.194 -
1.195 +"-------------- repl_app------------------------------------------";
1.196 +"-------------- repl_app------------------------------------------";
1.197 +"-------------- repl_app------------------------------------------";
1.198 +(*
1.199 +> repl [1,2,3] 2 22222;
1.200 +val it = [1,22222,3] : int list
1.201 +> repl_app [1,2,3,4] 5 5555;
1.202 +val it = [1,2,3,4,5555] : int list
1.203 +> repl_app [1,2,3] 2 22222;
1.204 +val it = [1,22222,3] : int list
1.205 +> repl_app [1] 2 22222 ;
1.206 +val it = [1,22222] : int list
1.207 +*)