1.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -116,7 +116,7 @@
1.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
1.5 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.6 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
1.7 -else raise error "new behaviour in test: miniscript with mini-subpbl";
1.8 +else error "new behaviour in test: miniscript with mini-subpbl";
1.9
1.10 show_pt pt;
1.11
1.12 @@ -136,7 +136,7 @@
1.13 ([3], Res),
1.14 ([4], Res),
1.15 ([], Res)]
1.16 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 1";
1.17 +then () else error "ctree.sml: diff:behav. in get_allpos' 1";
1.18
1.19 if get_allpos's ([], 1) (children pt) =
1.20 [([1], Frm),
1.21 @@ -148,7 +148,7 @@
1.22 ([3, 2], Res),
1.23 ([3], Res),
1.24 ([4], Res)]
1.25 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 2";
1.26 +then () else error "ctree.sml: diff:behav. in get_allpos' 2";
1.27
1.28 if get_allpos's ([], 2) (takerest (1, children pt)) =
1.29 [([2], Res),
1.30 @@ -158,7 +158,7 @@
1.31 ([3, 2], Res),
1.32 ([3], Res),
1.33 ([4], Res)]
1.34 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 3";
1.35 +then () else error "ctree.sml: diff:behav. in get_allpos' 3";
1.36
1.37 if get_allpos's ([], 3) (takerest (2, children pt)) =
1.38 [([3], Frm),
1.39 @@ -167,13 +167,13 @@
1.40 ([3, 2], Res),
1.41 ([3], Res),
1.42 ([4], Res)]
1.43 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 4";
1.44 +then () else error "ctree.sml: diff:behav. in get_allpos' 4";
1.45
1.46 if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
1.47 [([3, 1], Frm),
1.48 ([3, 1], Res),
1.49 ([3, 2], Res)]
1.50 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 5";
1.51 +then () else error "ctree.sml: diff:behav. in get_allpos' 5";
1.52
1.53 if get_allpos' ([3], 1) (nth 3 (children pt)) =
1.54 [([3], Frm),
1.55 @@ -181,7 +181,7 @@
1.56 ([3, 1], Res),
1.57 ([3, 2], Res),
1.58 ([3], Res)]
1.59 -then () else raise error "ctree.sml: diff:behav. in get_allpos' 6";
1.60 +then () else error "ctree.sml: diff:behav. in get_allpos' 6";
1.61
1.62
1.63 (**##############################################################(**)
1.64 @@ -200,23 +200,23 @@
1.65 ([3, 2], Res),
1.66 ([3], Res),
1.67 ([4], Res)]
1.68 -then () else raise error "ctree.sml: diff:behav. in cut_level 1a";
1.69 +then () else error "ctree.sml: diff:behav. in cut_level 1a";
1.70 val (res,asm) = get_obj g_result pt' [2];
1.71 if res = e_term andalso asm = [] then () else
1.72 -raise error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
1.73 +error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
1.74 if not (existpt [2] pt') then () else
1.75 -raise error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
1.76 +error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
1.77
1.78 val (res,asm) = get_obj g_result pt' [];
1.79 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
1.80 -raise error "ctree.sml: diff:behav. in cut_level 1ab";
1.81 +error "ctree.sml: diff:behav. in cut_level 1ab";
1.82 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.83 [([], Frm),
1.84 ([1], Frm),
1.85 ([1], Res),
1.86 ([2], Res),(*, e_term in cut_tree!!!*)
1.87 ([], Res)] then () else
1.88 -raise error "ctree.sml: diff:behav. in cut_level 1b";
1.89 +error "ctree.sml: diff:behav. in cut_level 1b";
1.90
1.91
1.92 val (pt',cuts) = cut_level [] [] pt ([2],Res);
1.93 @@ -226,22 +226,22 @@
1.94 ([3, 2], Res),
1.95 ([3], Res),
1.96 ([4], Res)]
1.97 -then () else raise error "ctree.sml: diff:behav. in cut_level 2a";
1.98 +then () else error "ctree.sml: diff:behav. in cut_level 2a";
1.99
1.100 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
1.101 -then () else raise error "ctree.sml: diff:behav. in cut_level 2b";
1.102 +then () else error "ctree.sml: diff:behav. in cut_level 2b";
1.103
1.104 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
1.105 if cuts = [([3, 1], Res), ([3, 2], Res)]
1.106 -then () else raise error "ctree.sml: diff:behav. in cut_level 3a";
1.107 +then () else error "ctree.sml: diff:behav. in cut_level 3a";
1.108 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
1.109 -then () else raise error "ctree.sml: diff:behav. in cut_level 3b";
1.110 +then () else error "ctree.sml: diff:behav. in cut_level 3b";
1.111
1.112 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
1.113 if cuts = [([3, 2], Res)]
1.114 -then () else raise error "ctree.sml: diff:behav. in cut_level 4a";
1.115 +then () else error "ctree.sml: diff:behav. in cut_level 4a";
1.116 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
1.117 -then () else raise error "ctree.sml: diff:behav. in cut_level 4b";
1.118 +then () else error "ctree.sml: diff:behav. in cut_level 4b";
1.119
1.120
1.121 "-------------- cut_tree (from ptree above)-----------------------";
1.122 @@ -256,25 +256,25 @@
1.123 ([3], Res),
1.124 ([4], Res),
1.125 ([], Res)]
1.126 -then () else raise error "ctree.sml: diff:behav. in cut_tree 1a";
1.127 +then () else error "ctree.sml: diff:behav. in cut_tree 1a";
1.128
1.129 val (res,asm) = get_obj g_result pt' [2];
1.130 if res = e_term (*WN050219 done by cut_level*) then () else
1.131 -raise error "ctree.sml: diff:behav. in cut_tree 1aa";
1.132 +error "ctree.sml: diff:behav. in cut_tree 1aa";
1.133
1.134 val form = get_obj g_form pt' [2];
1.135 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
1.136 -raise error "ctree.sml: diff:behav. in cut_tree 1ab";
1.137 +error "ctree.sml: diff:behav. in cut_tree 1ab";
1.138
1.139 val (res,asm) = get_obj g_result pt' [];
1.140 if res = e_term (*WN050219 done by cut_tree*) then () else
1.141 -raise error "ctree.sml: diff:behav. in cut_tree 1ac";
1.142 +error "ctree.sml: diff:behav. in cut_tree 1ac";
1.143
1.144 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
1.145 [([], Frm),
1.146 ([1], Frm),
1.147 ([1], Res)] then () else
1.148 -raise error "ctree.sml: diff:behav. in cut_tree 1ad";
1.149 +error "ctree.sml: diff:behav. in cut_tree 1ad";
1.150
1.151 val (pt', cuts) = cut_tree pt ([2],Res);
1.152 if cuts = [([3], Frm),
1.153 @@ -284,7 +284,7 @@
1.154 ([3], Res),
1.155 ([4], Res),
1.156 ([], Res)]
1.157 -then () else raise error "ctree.sml: diff:behav. in cut_tree 2";
1.158 +then () else error "ctree.sml: diff:behav. in cut_tree 2";
1.159
1.160 val (pt', cuts) = cut_tree pt ([3,1],Frm);
1.161 if cuts = [([3, 1], Res),
1.162 @@ -292,14 +292,14 @@
1.163 ([3], Res),
1.164 ([4], Res),
1.165 ([], Res)]
1.166 -then () else raise error "ctree.sml: diff:behav. in cut_tree 3";
1.167 +then () else error "ctree.sml: diff:behav. in cut_tree 3";
1.168
1.169 val (pt', cuts) = cut_tree pt ([3,1],Res);
1.170 if cuts = [([3, 2], Res),
1.171 ([3], Res),
1.172 ([4], Res),
1.173 ([], Res)]
1.174 -then () else raise error "ctree.sml: diff:behav. in cut_tree 4";
1.175 +then () else error "ctree.sml: diff:behav. in cut_tree 4";
1.176
1.177
1.178 "=====new ptree 1a miniscript with mini-subpbl ===================";
1.179 @@ -327,11 +327,11 @@
1.180
1.181 val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
1.182 if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
1.183 -then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
1.184 +then () else error "ctree.sml: diff:behav. in cut_tree 4a";
1.185
1.186 val (pt', cuts) = cut_tree pt ([1],Frm);
1.187 if cuts = []
1.188 -then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
1.189 +then () else error "ctree.sml: diff:behav. in cut_tree 4a";
1.190
1.191 (*WN050219
1.192 val pos as ([p],_) = ([1],Frm);
1.193 @@ -371,14 +371,14 @@
1.194 ([3, 2], Res),
1.195 ([3], Res),
1.196 ([4], Res)]
1.197 - then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
1.198 + then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
1.199
1.200 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1.201 if cuts = [([3, 2, 2], Res),
1.202 ([3, 2], Res),
1.203 ([3], Res),
1.204 ([4], Res)]
1.205 - then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
1.206 + then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
1.207
1.208
1.209 "-------------- cappend (from ptree above)------------------------";
1.210 @@ -391,11 +391,11 @@
1.211 ([3], Res),
1.212 ([4], Res),
1.213 ([], Res)]
1.214 -then () else raise error "ctree.sml: diff:behav. in cappend_form";
1.215 +then () else error "ctree.sml: diff:behav. in cappend_form";
1.216 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
1.217 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
1.218 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
1.219 - then () else raise error "ctree.sml: diff:behav. in cappend 1";
1.220 + then () else error "ctree.sml: diff:behav. in cappend 1";
1.221
1.222 val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
1.223 (Tac "test") (str2term "newresult",[]) Complete;
1.224 @@ -405,7 +405,7 @@
1.225 ([3], Res),
1.226 ([4], Res),
1.227 ([], Res)]
1.228 -then () else raise error "ctree.sml: diff:behav. in cappend_atomic";
1.229 +then () else error "ctree.sml: diff:behav. in cappend_atomic";
1.230
1.231
1.232
1.233 @@ -441,9 +441,9 @@
1.234 val form = get_obj g_form pt (fst p);
1.235 val (res,_) = get_obj g_result pt (fst p);
1.236 if term2str form = "x + 1 = 2" andalso res = e_term then () else
1.237 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
1.238 +error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
1.239 if not (existpt ((lev_on o fst) p) pt) then () else
1.240 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
1.241 +error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
1.242
1.243 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
1.244 val p = ([1], Res);
1.245 @@ -453,9 +453,9 @@
1.246 val form = get_obj g_form pt (fst p);
1.247 val (res,_) = get_obj g_result pt (fst p);
1.248 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
1.249 -then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
1.250 +then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
1.251 if not (existpt ((lev_on o fst) p) pt) then () else
1.252 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
1.253 +error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
1.254
1.255 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
1.256 val p = ([2], Res);
1.257 @@ -465,18 +465,18 @@
1.258 val form = get_obj g_form pt (fst p);
1.259 val (res,_) = get_obj g_result pt (fst p);
1.260 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
1.261 -then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
1.262 +then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
1.263 if not (existpt ((lev_on o fst) p) pt) then () else
1.264 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
1.265 +error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
1.266
1.267
1.268 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
1.269 val p = ([3], Pbl);
1.270 val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
1.271 if is_pblobj (get_obj I pt (fst p)) then () else
1.272 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
1.273 +error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
1.274 if not (existpt ((lev_on o fst) p) pt) then () else
1.275 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
1.276 +error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
1.277
1.278 (* ...complete calchead skipped...*)
1.279
1.280 @@ -486,9 +486,9 @@
1.281 val form = get_obj g_form pt (fst p);
1.282 val (res,_) = get_obj g_result pt (fst p);
1.283 if term2str form = "-1 + x = 0" andalso res = e_term then () else
1.284 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
1.285 +error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
1.286 if not (existpt ((lev_on o fst) p) pt) then () else
1.287 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
1.288 +error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
1.289
1.290 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
1.291 val p = ([3, 1], Res);
1.292 @@ -498,9 +498,9 @@
1.293 val form = get_obj g_form pt (fst p);
1.294 val (res,_) = get_obj g_result pt (fst p);
1.295 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
1.296 -else raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
1.297 +else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
1.298 if not (existpt ((lev_on o fst) p) pt) then () else
1.299 -raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
1.300 +error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
1.301
1.302 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
1.303 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
1.304 @@ -545,7 +545,7 @@
1.305 (*
1.306 val p = (move_dn [] pt p) handle e => print_exn_G e;
1.307 Exception PTREE end of calculation*)
1.308 -if p=([],Res) then () else raise error "ctree.sml: diff:behav. in move_dn";
1.309 +if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
1.310
1.311
1.312 "-------------- move_dn: Frm -> Res ------------------------------";
1.313 @@ -565,7 +565,7 @@
1.314 moveActiveRoot 1;
1.315 moveActiveDown 1;
1.316 if get_pos 1 1 = ([1], Frm) then ()
1.317 - else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.318 + else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.319 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.320
1.321 autoCalculate 1 (Step 1);
1.322 @@ -573,7 +573,7 @@
1.323
1.324 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.325 if get_pos 1 1 = ([1], Res) then ()
1.326 - else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.327 + else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
1.328 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
1.329
1.330
1.331 @@ -592,7 +592,7 @@
1.332 val p = move_up [] pt p; (*-> ([],Pbl)*)
1.333 (*val p = (move_up [] pt p) handle e => print_exn_G e;
1.334 Exception PTREE begin of calculation*)
1.335 -if p=([],Pbl) then () else raise error "ctree.sml: diff.behav. in move_up";
1.336 +if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
1.337
1.338
1.339 "------ move into detail -----------------------------------------";
1.340 @@ -627,7 +627,7 @@
1.341 val p = move_dn [] pt p; (*([2, 5], Res)*);
1.342 val p = move_dn [] pt p; (*([2, 6], Res)*);
1.343 if p = ([2, 6], Res) then()
1.344 - else raise error "ctree.sml: diff.behav. in move into detail";
1.345 + else error "ctree.sml: diff.behav. in move into detail";
1.346
1.347 "=====new ptree 3a ===============================================";
1.348 "=====new ptree 3a ===============================================";
1.349 @@ -800,29 +800,29 @@
1.350 writeln(pr_ptree pr_short pt);
1.351 case get_trace pt [1,3] [4,1,1] of
1.352 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
1.353 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
1.354 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
1.355 case get_trace pt [2] [4,3,2] of
1.356 [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
1.357 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
1.358 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
1.359 case get_trace pt [1,4] [4,3,1] of
1.360 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
1.361 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
1.362 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
1.363 case get_trace pt [4,2] [5] of
1.364 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
1.365 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
1.366 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
1.367 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
1.368 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
1.369 case get_trace pt [] [4,4,2] of
1.370 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.371 [4,3],[4,3,1],[4,3,2]] => ()
1.372 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
1.373 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
1.374 case get_trace pt [] [] of
1.375 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
1.376 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
1.377 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
1.378 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
1.379 case get_trace pt [4,3] [4,3] of
1.380 [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
1.381 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
1.382 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
1.383
1.384 "--- level 2: get pos' from start b to end p ---------------------";
1.385 "--- level 2: get pos' from start b to end p ---------------------";
1.386 @@ -834,11 +834,11 @@
1.387 (*
1.388 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
1.389 [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
1.390 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
1.391 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
1.392 case get_trace pt ([],Pbl) ([],Res) of
1.393 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
1.394 [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
1.395 - | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
1.396 + | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
1.397 *)
1.398
1.399 (******************************************************************)
1.400 @@ -870,7 +870,7 @@
1.401 ("PolyEq.thy",
1.402 ["normalize", "polynomial", "univariate", "equation"]),
1.403 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
1.404 - | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.405 + | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.406 (*WN060717 unintentionally changed some rls/ord while
1.407 completing knowl. for thes2file...
1.408
1.409 @@ -880,7 +880,7 @@
1.410 ("PolyEq.thy",
1.411 ["normalize", "polynomial", "univariate", "equation"]),
1.412 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
1.413 - | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.414 + | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
1.415
1.416 .... but it became even better*)
1.417
1.418 @@ -908,62 +908,62 @@
1.419 ("solve (x + 1 = 2, x)",
1.420 Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.421 []) => ()
1.422 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
1.423 + | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
1.424
1.425 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
1.426 case (term2str form, tac, terms2strs asm) of
1.427 ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
1.428 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
1.429 + | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
1.430
1.431 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
1.432 case (term2str form, tac, terms2strs asm) of
1.433 ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
1.434 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
1.435 + | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
1.436
1.437 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
1.438 case (term2str form, tac, terms2strs asm) of
1.439 ("-1 + x = 0",
1.440 Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
1.441 []) => ()
1.442 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
1.443 + | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
1.444
1.445 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
1.446 case (term2str form, tac, terms2strs asm) of
1.447 ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
1.448 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
1.449 + | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
1.450
1.451 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
1.452 case (term2str form, tac, terms2strs asm) of
1.453 ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
1.454 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
1.455 + | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
1.456
1.457 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
1.458 case (term2str form, tac, terms2strs asm) of
1.459 ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
1.460 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
1.461 + | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
1.462
1.463 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
1.464 case (term2str form, tac, terms2strs asm) of
1.465 ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
1.466 []) => ()
1.467 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
1.468 + | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
1.469
1.470 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
1.471 case (term2str form, tac, terms2strs asm) of
1.472 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
1.473 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
1.474 + | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
1.475
1.476 val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
1.477 case (term2str form, tac, terms2strs asm) of
1.478 ("[x = 1]",
1.479 Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
1.480 []) => ()
1.481 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
1.482 + | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
1.483
1.484 val (Form form, tac, asm) = pt_extract (pt, ([], Res));
1.485 case (term2str form, tac, terms2strs asm) of
1.486 ("[x = 1]", NONE, []) => ()
1.487 - | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Res)";
1.488 + | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
1.489
1.490 "=====new ptree 6 minisubpbl intersteps ==========================";
1.491 "=====new ptree 6 minisubpbl intersteps ==========================";
1.492 @@ -1003,13 +1003,13 @@
1.493 ([3], Res),
1.494 ([4], Res),
1.495 ([], Res)] then () else
1.496 -raise error "ctree.sml diff.behav. get_allp new []";
1.497 +error "ctree.sml diff.behav. get_allp new []";
1.498
1.499 print_depth 99;
1.500 val cuts2 = get_allps [] [1] (children pt);
1.501 print_depth 3;
1.502 if cuts = cuts2 @ [([], Res)] then () else
1.503 -raise error "ctree.sml diff.behav. get_allps new []";
1.504 +error "ctree.sml diff.behav. get_allps new []";
1.505
1.506 "---(3) on S(606)..S(608)--------";
1.507 "--- nd [2] with 6 children---------------------------------";
1.508 @@ -1018,11 +1018,11 @@
1.509 [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.510 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1.511 ([2], Res)] then () else
1.512 -raise error "ctree.sml diff.behav. get_allp new [2]";
1.513 +error "ctree.sml diff.behav. get_allp new [2]";
1.514
1.515 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
1.516 if cuts = cuts2 @ [([2], Res)] then () else
1.517 -raise error "ctree.sml diff.behav. get_allps new [2]";
1.518 +error "ctree.sml diff.behav. get_allps new [2]";
1.519
1.520
1.521 "---(4) on S(606)..S(608)--------";
1.522 @@ -1034,33 +1034,33 @@
1.523 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.524 ([3, 2], Res),
1.525 ([3], Res)] then () else
1.526 -raise error "ctree.sml diff.behav. get_allp new [3]";
1.527 +error "ctree.sml diff.behav. get_allp new [3]";
1.528
1.529 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
1.530 if cuts = cuts2 @ [([3], Res)] then () else
1.531 -raise error "ctree.sml diff.behav. get_allps new [3]";
1.532 +error "ctree.sml diff.behav. get_allps new [3]";
1.533
1.534 "--- nd [3,2] with 2 children--------------------------------";
1.535 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
1.536 if cuts =
1.537 [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.538 ([3, 2], Res)] then () else
1.539 -raise error "ctree.sml diff.behav. get_allp new [3,2]";
1.540 +error "ctree.sml diff.behav. get_allp new [3,2]";
1.541
1.542 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
1.543 if cuts = cuts2 @ [([3, 2], Res)] then () else
1.544 -raise error "ctree.sml diff.behav. get_allps new [3,2]";
1.545 +error "ctree.sml diff.behav. get_allps new [3,2]";
1.546
1.547 "---(5a) on S(606)..S(608)--------";
1.548 "--- nd [3,2,1] with 0 children------------------------------";
1.549 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
1.550 if cuts =
1.551 [] then () else
1.552 -raise error "ctree.sml diff.behav. get_allp new [3,2,1]";
1.553 +error "ctree.sml diff.behav. get_allp new [3,2,1]";
1.554
1.555 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
1.556 if cuts = cuts2 @ [] then () else
1.557 -raise error "ctree.sml diff.behav. get_allps new [3,2,1]";
1.558 +error "ctree.sml diff.behav. get_allps new [3,2,1]";
1.559
1.560
1.561 (**#################################################################**)
1.562 @@ -1070,10 +1070,10 @@
1.563 show_pt pt;
1.564 val b = get_obj g_branch pt [];
1.565 if b = TransitiveB then () else
1.566 -raise error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1.567 +error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1.568 val b = get_obj g_branch pt [3];
1.569 if b = TransitiveB then () else
1.570 -raise error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1.571 +error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1.572
1.573 "---(2) on S(606)..S(608)--------";
1.574 val (pt', cuts) = cut_tree pt ([1],Res);
1.575 @@ -1085,7 +1085,7 @@
1.576 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.577 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.578 (*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
1.579 -raise error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1.580 +error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1.581
1.582
1.583 "---(3) on S(606)..S(608)--------";
1.584 @@ -1105,7 +1105,7 @@
1.585 ([3], Res),
1.586 ([4], Res),
1.587 (*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
1.588 -else raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1.589 +else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1.590
1.591 "---(4) on S(606)..S(608)--------";
1.592 val (pt', cuts) = cut_tree pt ([3],Pbl);
1.593 @@ -1119,7 +1119,7 @@
1.594 ([3], Res),
1.595 ([4], Res),
1.596 (*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
1.597 -then () else raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1.598 +then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1.599
1.600 "---(5a) on S(606)..S(608) cut_tree --------";
1.601 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1.602 @@ -1129,7 +1129,7 @@
1.603 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.604 (*WN060727 added after replacing cutlevup by test_trans:*)
1.605 ([3], Res), ([4], Res),([],Res)] then ()
1.606 -else raise error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1.607 +else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1.608 show_pt pt';
1.609
1.610
1.611 @@ -1149,14 +1149,14 @@
1.612 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.613 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.614 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.615 -else raise error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1.616 +else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1.617 val afterins = get_allp [] ([], ([],Frm)) pt';
1.618 print_depth 99;
1.619 afterins;
1.620 print_depth 3;
1.621 if afterins = [([1], Frm), ([1], Res)
1.622 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1.623 -else raise error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1.624 +else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1.625 show_pt pt';
1.626
1.627 "---(3) on S(606)..S(608)--------";
1.628 @@ -1171,7 +1171,7 @@
1.629 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1.630 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1.631 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1.632 -else raise error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1.633 +else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1.634 val afterins = get_allp [] ([], ([],Frm)) pt';
1.635 print_depth 99;
1.636 afterins;
1.637 @@ -1179,7 +1179,7 @@
1.638 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1.639 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1.640 then () else
1.641 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1.642 +error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1.643 show_pt pt';
1.644 (*
1.645 val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1.646 @@ -1204,7 +1204,7 @@
1.647 ([3, 2], Res),
1.648 ([3], Res), ([4], Res),
1.649 (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
1.650 -raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1.651 +error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1.652 val afterins = get_allp [] ([], ([],Frm)) pt';
1.653 print_depth 99;
1.654 afterins;
1.655 @@ -1213,7 +1213,7 @@
1.656 [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.657 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
1.658 ([3], Pbl)] then () else
1.659 -raise error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1.660 +error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1.661 (* use"systest/ctree.sml";
1.662 use"ctree.sml";
1.663 *)
1.664 @@ -1227,7 +1227,7 @@
1.665 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.666 ([3, 2], Res),
1.667 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
1.668 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1.669 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1.670 val afterins = get_allp [] ([], ([],Frm)) pt';
1.671 print_depth 99;
1.672 afterins;
1.673 @@ -1242,7 +1242,7 @@
1.674 ([3], Res)(*cutlevup=false*),
1.675 ([4], Res),
1.676 ([], Res)(*cutlevup=false*)] then () else
1.677 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.678 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.679 *)
1.680 if afterins = [([1], Frm), ([1], Res),
1.681 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.682 @@ -1250,10 +1250,10 @@
1.683 ([2], Res),
1.684 ([3], Pbl),
1.685 ([3, 1], Frm), ([3, 1], Res)] then () else
1.686 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.687 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1.688
1.689 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
1.690 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1.691 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1.692
1.693 "---(6) on S(606)..S(608)--------";
1.694 val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
1.695 @@ -1264,7 +1264,7 @@
1.696 if cuts = [(*just after is: cutlevup=false in [3]*)
1.697 (*WN060727 after test_trans instead cutlevup added:*)
1.698 ([3], Res), ([4], Res), ([], Res)] then () else
1.699 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1.700 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1.701 val afterins = get_allp [] ([], ([],Frm)) pt';
1.702 print_depth 99;
1.703 afterins;
1.704 @@ -1278,7 +1278,7 @@
1.705 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
1.706 ([3], Res),
1.707 ([4], Res), ([], Res)] then () else
1.708 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.709 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.710 *)
1.711 if afterins = [([1], Frm), ([1], Res),
1.712 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1.713 @@ -1287,10 +1287,10 @@
1.714 ([3], Pbl),
1.715 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
1.716 then () else
1.717 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.718 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1.719
1.720 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
1.721 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1.722 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1.723
1.724 "---(6++) on S(606)..S(608)--------";
1.725 (**)
1.726 @@ -1302,7 +1302,7 @@
1.727 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1.728 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
1.729 then () else
1.730 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1.731 +error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1.732 val afterins = get_allp [] ([], ([],Frm)) pt';
1.733 print_depth 99;
1.734 afterins;
1.735 @@ -1314,9 +1314,9 @@
1.736 ([3], Pbl),
1.737 ([3, 1], Frm), ([3, 1], Res),
1.738 ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
1.739 -raise error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1.740 +error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1.741 if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
1.742 -raise error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1.743 +error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1.744 (*
1.745 show_pt pt';
1.746 show_pt pt;