diff -r 95d956108461 -r 460c24a6a6ba test/Tools/isac/Interpret/ctree.sml
--- a/test/Tools/isac/Interpret/ctree.sml Tue Sep 28 08:58:06 2010 +0200
+++ b/test/Tools/isac/Interpret/ctree.sml Tue Sep 28 09:06:56 2010 +0200
@@ -116,7 +116,7 @@
val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
-else raise error "new behaviour in test: miniscript with mini-subpbl";
+else error "new behaviour in test: miniscript with mini-subpbl";
show_pt pt;
@@ -136,7 +136,7 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 1";
+then () else error "ctree.sml: diff:behav. in get_allpos' 1";
if get_allpos's ([], 1) (children pt) =
[([1], Frm),
@@ -148,7 +148,7 @@
([3, 2], Res),
([3], Res),
([4], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 2";
+then () else error "ctree.sml: diff:behav. in get_allpos' 2";
if get_allpos's ([], 2) (takerest (1, children pt)) =
[([2], Res),
@@ -158,7 +158,7 @@
([3, 2], Res),
([3], Res),
([4], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 3";
+then () else error "ctree.sml: diff:behav. in get_allpos' 3";
if get_allpos's ([], 3) (takerest (2, children pt)) =
[([3], Frm),
@@ -167,13 +167,13 @@
([3, 2], Res),
([3], Res),
([4], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 4";
+then () else error "ctree.sml: diff:behav. in get_allpos' 4";
if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
[([3, 1], Frm),
([3, 1], Res),
([3, 2], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 5";
+then () else error "ctree.sml: diff:behav. in get_allpos' 5";
if get_allpos' ([3], 1) (nth 3 (children pt)) =
[([3], Frm),
@@ -181,7 +181,7 @@
([3, 1], Res),
([3, 2], Res),
([3], Res)]
-then () else raise error "ctree.sml: diff:behav. in get_allpos' 6";
+then () else error "ctree.sml: diff:behav. in get_allpos' 6";
(**##############################################################(**)
@@ -200,23 +200,23 @@
([3, 2], Res),
([3], Res),
([4], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_level 1a";
+then () else error "ctree.sml: diff:behav. in cut_level 1a";
val (res,asm) = get_obj g_result pt' [2];
if res = e_term andalso asm = [] then () else
-raise error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
+error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
if not (existpt [2] pt') then () else
-raise error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
+error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
val (res,asm) = get_obj g_result pt' [];
if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
-raise error "ctree.sml: diff:behav. in cut_level 1ab";
+error "ctree.sml: diff:behav. in cut_level 1ab";
if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
[([], Frm),
([1], Frm),
([1], Res),
([2], Res),(*, e_term in cut_tree!!!*)
([], Res)] then () else
-raise error "ctree.sml: diff:behav. in cut_level 1b";
+error "ctree.sml: diff:behav. in cut_level 1b";
val (pt',cuts) = cut_level [] [] pt ([2],Res);
@@ -226,22 +226,22 @@
([3, 2], Res),
([3], Res),
([4], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_level 2a";
+then () else error "ctree.sml: diff:behav. in cut_level 2a";
if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
-then () else raise error "ctree.sml: diff:behav. in cut_level 2b";
+then () else error "ctree.sml: diff:behav. in cut_level 2b";
val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
if cuts = [([3, 1], Res), ([3, 2], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_level 3a";
+then () else error "ctree.sml: diff:behav. in cut_level 3a";
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"
-then () else raise error "ctree.sml: diff:behav. in cut_level 3b";
+then () else error "ctree.sml: diff:behav. in cut_level 3b";
val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
if cuts = [([3, 2], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_level 4a";
+then () else error "ctree.sml: diff:behav. in cut_level 4a";
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"
-then () else raise error "ctree.sml: diff:behav. in cut_level 4b";
+then () else error "ctree.sml: diff:behav. in cut_level 4b";
"-------------- cut_tree (from ptree above)-----------------------";
@@ -256,25 +256,25 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_tree 1a";
+then () else error "ctree.sml: diff:behav. in cut_tree 1a";
val (res,asm) = get_obj g_result pt' [2];
if res = e_term (*WN050219 done by cut_level*) then () else
-raise error "ctree.sml: diff:behav. in cut_tree 1aa";
+error "ctree.sml: diff:behav. in cut_tree 1aa";
val form = get_obj g_form pt' [2];
if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
-raise error "ctree.sml: diff:behav. in cut_tree 1ab";
+error "ctree.sml: diff:behav. in cut_tree 1ab";
val (res,asm) = get_obj g_result pt' [];
if res = e_term (*WN050219 done by cut_tree*) then () else
-raise error "ctree.sml: diff:behav. in cut_tree 1ac";
+error "ctree.sml: diff:behav. in cut_tree 1ac";
if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
[([], Frm),
([1], Frm),
([1], Res)] then () else
-raise error "ctree.sml: diff:behav. in cut_tree 1ad";
+error "ctree.sml: diff:behav. in cut_tree 1ad";
val (pt', cuts) = cut_tree pt ([2],Res);
if cuts = [([3], Frm),
@@ -284,7 +284,7 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_tree 2";
+then () else error "ctree.sml: diff:behav. in cut_tree 2";
val (pt', cuts) = cut_tree pt ([3,1],Frm);
if cuts = [([3, 1], Res),
@@ -292,14 +292,14 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_tree 3";
+then () else error "ctree.sml: diff:behav. in cut_tree 3";
val (pt', cuts) = cut_tree pt ([3,1],Res);
if cuts = [([3, 2], Res),
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cut_tree 4";
+then () else error "ctree.sml: diff:behav. in cut_tree 4";
"=====new ptree 1a miniscript with mini-subpbl ===================";
@@ -327,11 +327,11 @@
val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
-then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
+then () else error "ctree.sml: diff:behav. in cut_tree 4a";
val (pt', cuts) = cut_tree pt ([1],Frm);
if cuts = []
-then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
+then () else error "ctree.sml: diff:behav. in cut_tree 4a";
(*WN050219
val pos as ([p],_) = ([1],Frm);
@@ -371,14 +371,14 @@
([3, 2], Res),
([3], Res),
([4], Res)]
- then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
+ then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
val (pt', cuts) = cut_tree pt ([3,2,1],Res);
if cuts = [([3, 2, 2], Res),
([3, 2], Res),
([3], Res),
([4], Res)]
- then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
+ then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
"-------------- cappend (from ptree above)------------------------";
@@ -391,11 +391,11 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cappend_form";
+then () else error "ctree.sml: diff:behav. in cappend_form";
if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
- then () else raise error "ctree.sml: diff:behav. in cappend 1";
+ then () else error "ctree.sml: diff:behav. in cappend 1";
val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
(Tac "test") (str2term "newresult",[]) Complete;
@@ -405,7 +405,7 @@
([3], Res),
([4], Res),
([], Res)]
-then () else raise error "ctree.sml: diff:behav. in cappend_atomic";
+then () else error "ctree.sml: diff:behav. in cappend_atomic";
@@ -441,9 +441,9 @@
val form = get_obj g_form pt (fst p);
val (res,_) = get_obj g_result pt (fst p);
if term2str form = "x + 1 = 2" andalso res = e_term then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
+error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
val p = ([1], Res);
@@ -453,9 +453,9 @@
val form = get_obj g_form pt (fst p);
val (res,_) = get_obj g_result pt (fst p);
if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
-then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
+then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
val p = ([2], Res);
@@ -465,18 +465,18 @@
val form = get_obj g_form pt (fst p);
val (res,_) = get_obj g_result pt (fst p);
if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
-then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
+then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
val p = ([3], Pbl);
val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
if is_pblobj (get_obj I pt (fst p)) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
+error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
(* ...complete calchead skipped...*)
@@ -486,9 +486,9 @@
val form = get_obj g_form pt (fst p);
val (res,_) = get_obj g_result pt (fst p);
if term2str form = "-1 + x = 0" andalso res = e_term then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
+error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
val p = ([3, 1], Res);
@@ -498,9 +498,9 @@
val form = get_obj g_form pt (fst p);
val (res,_) = get_obj g_result pt (fst p);
if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
-else raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
+else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
if not (existpt ((lev_on o fst) p) pt) then () else
-raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
+error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
@@ -545,7 +545,7 @@
(*
val p = (move_dn [] pt p) handle e => print_exn_G e;
Exception PTREE end of calculation*)
-if p=([],Res) then () else raise error "ctree.sml: diff:behav. in move_dn";
+if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
"-------------- move_dn: Frm -> Res ------------------------------";
@@ -565,7 +565,7 @@
moveActiveRoot 1;
moveActiveDown 1;
if get_pos 1 1 = ([1], Frm) then ()
- else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
+ else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
moveActiveDown 1; (* pos does not exist *)
autoCalculate 1 (Step 1);
@@ -573,7 +573,7 @@
moveActiveDown 1; (* pos does not exist *)
if get_pos 1 1 = ([1], Res) then ()
- else raise error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
+ else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
moveActiveDown 1; (* pos does not exist *)
@@ -592,7 +592,7 @@
val p = move_up [] pt p; (*-> ([],Pbl)*)
(*val p = (move_up [] pt p) handle e => print_exn_G e;
Exception PTREE begin of calculation*)
-if p=([],Pbl) then () else raise error "ctree.sml: diff.behav. in move_up";
+if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
"------ move into detail -----------------------------------------";
@@ -627,7 +627,7 @@
val p = move_dn [] pt p; (*([2, 5], Res)*);
val p = move_dn [] pt p; (*([2, 6], Res)*);
if p = ([2, 6], Res) then()
- else raise error "ctree.sml: diff.behav. in move into detail";
+ else error "ctree.sml: diff.behav. in move into detail";
"=====new ptree 3a ===============================================";
"=====new ptree 3a ===============================================";
@@ -800,29 +800,29 @@
writeln(pr_ptree pr_short pt);
case get_trace pt [1,3] [4,1,1] of
[[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
case get_trace pt [2] [4,3,2] of
[[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
case get_trace pt [1,4] [4,3,1] of
[[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
case get_trace pt [4,2] [5] of
(*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
[[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
case get_trace pt [] [4,4,2] of
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
[4,3],[4,3,1],[4,3,2]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
case get_trace pt [] [] of
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
case get_trace pt [4,3] [4,3] of
[[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
"--- level 2: get pos' from start b to end p ---------------------";
"--- level 2: get pos' from start b to end p ---------------------";
@@ -834,11 +834,11 @@
(*
case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
[[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
case get_trace pt ([],Pbl) ([],Res) of
[[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
[4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
- | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
+ | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
*)
(******************************************************************)
@@ -870,7 +870,7 @@
("PolyEq.thy",
["normalize", "polynomial", "univariate", "equation"]),
["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
+ | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
(*WN060717 unintentionally changed some rls/ord while
completing knowl. for thes2file...
@@ -880,7 +880,7 @@
("PolyEq.thy",
["normalize", "polynomial", "univariate", "equation"]),
["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
+ | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
.... but it became even better*)
@@ -908,62 +908,62 @@
("solve (x + 1 = 2, x)",
Apply_Method ["Test", "squ-equ-test-subpbl1"],
[]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
case (term2str form, tac, terms2strs asm) of
("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
case (term2str form, tac, terms2strs asm) of
("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
case (term2str form, tac, terms2strs asm) of
("-1 + x = 0",
Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
[]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
case (term2str form, tac, terms2strs asm) of
("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
case (term2str form, tac, terms2strs asm) of
("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
case (term2str form, tac, terms2strs asm) of
("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
case (term2str form, tac, terms2strs asm) of
("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
[]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
case (term2str form, tac, terms2strs asm) of
("[x = 1]", Check_elementwise "Assumptions", []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
case (term2str form, tac, terms2strs asm) of
("[x = 1]",
Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
[]) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
val (Form form, tac, asm) = pt_extract (pt, ([], Res));
case (term2str form, tac, terms2strs asm) of
("[x = 1]", NONE, []) => ()
- | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Res)";
+ | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
"=====new ptree 6 minisubpbl intersteps ==========================";
"=====new ptree 6 minisubpbl intersteps ==========================";
@@ -1003,13 +1003,13 @@
([3], Res),
([4], Res),
([], Res)] then () else
-raise error "ctree.sml diff.behav. get_allp new []";
+error "ctree.sml diff.behav. get_allp new []";
print_depth 99;
val cuts2 = get_allps [] [1] (children pt);
print_depth 3;
if cuts = cuts2 @ [([], Res)] then () else
-raise error "ctree.sml diff.behav. get_allps new []";
+error "ctree.sml diff.behav. get_allps new []";
"---(3) on S(606)..S(608)--------";
"--- nd [2] with 6 children---------------------------------";
@@ -1018,11 +1018,11 @@
[([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
([2], Res)] then () else
-raise error "ctree.sml diff.behav. get_allp new [2]";
+error "ctree.sml diff.behav. get_allp new [2]";
val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
if cuts = cuts2 @ [([2], Res)] then () else
-raise error "ctree.sml diff.behav. get_allps new [2]";
+error "ctree.sml diff.behav. get_allps new [2]";
"---(4) on S(606)..S(608)--------";
@@ -1034,33 +1034,33 @@
([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
([3, 2], Res),
([3], Res)] then () else
-raise error "ctree.sml diff.behav. get_allp new [3]";
+error "ctree.sml diff.behav. get_allp new [3]";
val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
if cuts = cuts2 @ [([3], Res)] then () else
-raise error "ctree.sml diff.behav. get_allps new [3]";
+error "ctree.sml diff.behav. get_allps new [3]";
"--- nd [3,2] with 2 children--------------------------------";
val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
if cuts =
[([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
([3, 2], Res)] then () else
-raise error "ctree.sml diff.behav. get_allp new [3,2]";
+error "ctree.sml diff.behav. get_allp new [3,2]";
val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
if cuts = cuts2 @ [([3, 2], Res)] then () else
-raise error "ctree.sml diff.behav. get_allps new [3,2]";
+error "ctree.sml diff.behav. get_allps new [3,2]";
"---(5a) on S(606)..S(608)--------";
"--- nd [3,2,1] with 0 children------------------------------";
val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
if cuts =
[] then () else
-raise error "ctree.sml diff.behav. get_allp new [3,2,1]";
+error "ctree.sml diff.behav. get_allp new [3,2,1]";
val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
if cuts = cuts2 @ [] then () else
-raise error "ctree.sml diff.behav. get_allps new [3,2,1]";
+error "ctree.sml diff.behav. get_allps new [3,2,1]";
(**#################################################################**)
@@ -1070,10 +1070,10 @@
show_pt pt;
val b = get_obj g_branch pt [];
if b = TransitiveB then () else
-raise error ("ctree.sml diff.behav. in [] branch="^branch2str b);
+error ("ctree.sml diff.behav. in [] branch="^branch2str b);
val b = get_obj g_branch pt [3];
if b = TransitiveB then () else
-raise error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
+error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
"---(2) on S(606)..S(608)--------";
val (pt', cuts) = cut_tree pt ([1],Res);
@@ -1085,7 +1085,7 @@
([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
(*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
-raise error "ctree.sml: diff.behav. cut_tree ([1],Res)";
+error "ctree.sml: diff.behav. cut_tree ([1],Res)";
"---(3) on S(606)..S(608)--------";
@@ -1105,7 +1105,7 @@
([3], Res),
([4], Res),
(*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
-else raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
+else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
"---(4) on S(606)..S(608)--------";
val (pt', cuts) = cut_tree pt ([3],Pbl);
@@ -1119,7 +1119,7 @@
([3], Res),
([4], Res),
(*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
-then () else raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
+then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
"---(5a) on S(606)..S(608) cut_tree --------";
val (pt', cuts) = cut_tree pt ([3,2,1],Res);
@@ -1129,7 +1129,7 @@
if cuts = [([3, 2, 2], Res), ([3, 2], Res),
(*WN060727 added after replacing cutlevup by test_trans:*)
([3], Res), ([4], Res),([],Res)] then ()
-else raise error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
+else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
show_pt pt';
@@ -1149,14 +1149,14 @@
([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
-else raise error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
+else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
print_depth 3;
if afterins = [([1], Frm), ([1], Res)
(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
-else raise error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
+else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
show_pt pt';
"---(3) on S(606)..S(608)--------";
@@ -1171,7 +1171,7 @@
([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
(*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
-else raise error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
+else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
@@ -1179,7 +1179,7 @@
if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
(*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
show_pt pt';
(*
val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
@@ -1204,7 +1204,7 @@
([3, 2], Res),
([3], Res), ([4], Res),
(*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
-raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
+error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
@@ -1213,7 +1213,7 @@
[([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
([3], Pbl)] then () else
-raise error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
+error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
(* use"systest/ctree.sml";
use"ctree.sml";
*)
@@ -1227,7 +1227,7 @@
if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
([3, 2], Res),
(*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
@@ -1242,7 +1242,7 @@
([3], Res)(*cutlevup=false*),
([4], Res),
([], Res)(*cutlevup=false*)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
*)
if afterins = [([1], Frm), ([1], Res),
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
@@ -1250,10 +1250,10 @@
([2], Res),
([3], Pbl),
([3, 1], Frm), ([3, 1], Res)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
"---(6) on S(606)..S(608)--------";
val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
@@ -1264,7 +1264,7 @@
if cuts = [(*just after is: cutlevup=false in [3]*)
(*WN060727 after test_trans instead cutlevup added:*)
([3], Res), ([4], Res), ([], Res)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
@@ -1278,7 +1278,7 @@
([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
([3], Res),
([4], Res), ([], Res)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
*)
if afterins = [([1], Frm), ([1], Res),
([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
@@ -1287,10 +1287,10 @@
([3], Pbl),
([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
"---(6++) on S(606)..S(608)--------";
(**)
@@ -1302,7 +1302,7 @@
if cuts = [([3, 2, 2], Res), ([3, 2], Res),
(*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
+error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
val afterins = get_allp [] ([], ([],Frm)) pt';
print_depth 99;
afterins;
@@ -1314,9 +1314,9 @@
([3], Pbl),
([3, 1], Frm), ([3, 1], Res),
([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
-raise error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
+error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
-raise error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
+error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
(*
show_pt pt';
show_pt pt;