wneuper/isa: comparison test/Tools/isac/Interpret/ctree.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
 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;
 "-------------- get_allpos' (from ptree above)--------------------";
 ([3, 1], Res),
 ([3, 2], Res),
 ([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),
 ([1], Res),
 ([2], Res),
 ([3, 1], Frm),
 ([3, 1], Res),
 ([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),
 ([3], Frm),
 ([3, 1], Frm),
 ([3, 1], Res),
 ([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),
 ([3, 1], Frm),
 ([3, 1], Res),
 ([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),
 ([3, 1], Frm),
 ([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";
 (**##############################################################(**)
 "-------------- cut_level (from ptree above)----------------------";
 	   ([3, 1], Frm),
 	   ([3, 1], Res),
 	   ([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);
 if cuts = [([3], Frm),
 	   ([3, 1], Frm),
 	   ([3, 1], Res),
 	   ([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)-----------------------";
 "-------------- cut_tree (from ptree above)-----------------------";
 "-------------- cut_tree (from ptree above)-----------------------";
 	   ([3, 1], Res),
 	   ([3, 2], Res),
 	   ([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),
 	   ([3, 1], Frm),
 	   ([3, 1], Res),
 	   ([3, 2], Res),
 	   ([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),
 	   ([3, 2], Res),
 	   ([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 ===================";
 "=====new ptree 1a miniscript with mini-subpbl ===================";
 "=====new ptree 1a miniscript with mini-subpbl ===================";
 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
 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);
 val pt as Nd (b,_) = pt;
 if cuts = [([3, 2, 1], Res),
 	    ([3, 2, 2], Res),
 	    ([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)------------------------";
 "-------------- cappend (from ptree above)------------------------";
 "-------------- cappend (from ptree above)------------------------";
 	   ([3, 2, 2], Res),
 	   ([3, 2], Res),
 	   ([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;
 if cuts = [([3, 2, 1], Res), (*?????????????*)
 	   ([3, 2, 2], Res),
 	   ([3, 2], Res),
 	   ([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";
 "-------------- cappend minisubpbl -------------------------------";
 "-------------- cappend minisubpbl -------------------------------";
 val p = ([1], Frm);
 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
 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);
 val (pt,cuts) =
 cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
 		   Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
 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);
 val (pt,cuts) =
 cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
 		   Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
 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...*)
 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
 val p = ([3, 1], Frm);
 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
 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);
 val (pt,cuts) =
 cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
 		   Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
 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]*);
 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
 val p = move_dn [] pt p        (*-> ([4],Res)*);
 val p = move_dn [] pt p        (*-> ([],Res)*);
 (*
 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 ------------------------------";
 "-------------- move_dn: Frm -> Res ------------------------------";
 "-------------- move_dn: Frm -> Res ------------------------------";
 refFormula 1 (get_pos 1 1);
 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; (*<ERROR> pos does not exist </ERROR>*)
 autoCalculate 1 (Step 1);
 refFormula 1 (get_pos 1 1);
 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
 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; (*<ERROR> pos does not exist </ERROR>*)
 "-------------- move_up ------------------------------------------";
 "-------------- move_up ------------------------------------------";
 val p = move_up [] pt p;        (*-> ([1],Res)*)
 val p = move_up [] pt p;        (*-> ([1],Frm)*)
 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 -----------------------------------------";
 "------ move into detail -----------------------------------------";
 "------ move into detail -----------------------------------------";
 val p = move_dn [] pt p;     (*([2, 3], Res)*);
 val p = move_dn [] pt p;     (*([2, 4], Res)*);
 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 ===============================================";
 "=====new ptree 3a ===============================================";
 states:=[];
 end;
 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 ---------------------";
 "--- level 2: get pos' from start b to end p ---------------------";
 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
 actually used (inefficient) version with move_dn: see modspec.sml
 *)
 (*
 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";
 *)
 (******************************************************************)
 (**)            val get_trace = SAVE_get_trace;                 (**)
 (******************************************************************)
 ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
 Subproblem
 ("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...
 case (term2str form, tac, terms2strs asm) of
 ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
 *)Subproblem
 ("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*)
 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
 case (term2str form, tac, terms2strs asm) of
 ("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 ==========================";
 "=====new ptree 6 minisubpbl intersteps ==========================";
 states:=[];
 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
 ([3, 2], Res),
 ([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---------------------------------";
 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
 if cuts =
 [([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)--------";
 "--- nd [3] subproblem--------------------------------------";
 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
 [([3, 1], Frm),
 ([3, 1], Res),
 ([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]";
 (**#################################################################**)
 "-------------- cut_tree new (from ptree above)-------------------";
 "-------------- cut_tree new (from ptree above)-------------------";
 "-------------- cut_tree new (from ptree above)-------------------";
 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);
 print_depth 99;
 cuts;
 if cuts = [([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),
 ([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)--------";
 val (pt', cuts) = cut_tree pt ([2],Res);
 print_depth 99;
 	   ([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. 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);
 print_depth 99;
 cuts;
 	   ([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. 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);
 print_depth 99;
 cuts;
 print_depth 1;
 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';
 "-------------- cappend on complete ctree from above -------------";
 "-------------- cappend on complete ctree from above -------------";
 if cuts = [([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),
 ([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)--------";
 show_pt pt;
 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
 if cuts = [([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),
 ([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;
 print_depth 3;
 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)*);
 val p = move_dn [] pt' p        (*-> ([1],Res)*);
 val p = move_dn [] pt' p        (*-> ([2],Frm)*);
 	   ([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 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;
 print_depth 3;
 if afterins =
 [([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";
 *)
 "---(6-1) on S(606)..S(608)--------";
 cuts;
 print_depth 3;
 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;
 print_depth 3;
 (*WN060727 replaced after overwriting cutlevup by test_trans
 	       ([3], Pbl),
 	       ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
 	       ([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),
 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
 	       ([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]")
 (Tac "test") (str2term "Inres[3,2]",[]) Complete;
 print_depth 99;
 cuts;
 print_depth 3;
 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;
 print_depth 3;
 (*WN060727 replaced after overwriting cutlevup by test_trans
 	       ([2], Res),
 	       ([3], Pbl),
 	       ([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),
 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
 	       ([2], Res),
 	       ([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)--------";
 (**)
 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
 cuts;
 print_depth 1;
 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;
 print_depth 3;
 if afterins = [([1], Frm), ([1], Res),
 	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
 	       ([2], Res),
 	       ([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;
 *)

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37960	ec20007095f2
child 38058	ad0485155c0e