1.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -102,7 +102,7 @@
1.4 "----------- fun thy_containing_thm ------------------------------";
1.5 val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));
1.6 if thy_contains_thm str ("XXX",thy) then ()
1.7 -else raise error "rewtools.sml: NOT thy_contains_thm \
1.8 +else error "rewtools.sml: NOT thy_contains_thm \
1.9 \(real_diff_minus,(Root.thy,.";
1.10 (rev (!theory'));
1.11 dropuntil (curry op= thy');
1.12 @@ -111,15 +111,15 @@
1.13 (#1:theory' * theory -> theory'))
1.14 (rev (!theory'));
1.15 if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()
1.16 -else raise error "rewtools.sml: NOT thy_containin_thm \
1.17 +else error "rewtools.sml: NOT thy_containin_thm \
1.18 \(real_diff_minus,(Root.thy,.";
1.19
1.20 "----- search the same theorem somewhere further below in the list";
1.21 if thy_contains_thm str ("XXX",Poly.thy) then ()
1.22 -else raise error "rewtools.sml: NOT thy_contains_thm \
1.23 +else error "rewtools.sml: NOT thy_contains_thm \
1.24 \(real_diff_minus,(Poly.thy,.";
1.25 if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()
1.26 -else raise error "rewtools.sml: NOT thy_containing_thm \
1.27 +else error "rewtools.sml: NOT thy_containing_thm \
1.28 \(real_diff_minus,(Poly.thy,.";
1.29
1.30 "----- second test -------------------------------";
1.31 @@ -132,7 +132,7 @@
1.32 length (!theory');
1.33 length startsearch;
1.34 if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()
1.35 -else raise error "rewtools.sml: diff.behav. in \
1.36 +else error "rewtools.sml: diff.behav. in \
1.37 \thy_containing_thm Test radd_commute";
1.38
1.39
1.40 @@ -144,7 +144,7 @@
1.41 (#1:theory' * theory -> theory'))
1.42 (rev (!theory'));
1.43 if length (!theory') <> length dropthys then ()
1.44 -else raise error "rewtools.sml: diff.behav. in thy_containing_rls 1";
1.45 +else error "rewtools.sml: diff.behav. in thy_containing_rls 1";
1.46 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
1.47 dropthys;
1.48 print_depth 99; dropthy's; print_depth 3;
1.49 @@ -161,16 +161,16 @@
1.50 (rev (!ruleset'));
1.51 print_depth 99; map (#1 o #2) startsearch; print_depth 3;
1.52 if length (!ruleset') <> length startsearch then ()
1.53 -else raise error "rewtools.sml: diff.behav. in thy_containing_rls 2";
1.54 +else error "rewtools.sml: diff.behav. in thy_containing_rls 2";
1.55
1.56 val rls' = "norm_Poly";
1.57 case assoc (startsearch, rls') of
1.58 SOME (thy', _) => thyID2theory' thy'
1.59 - | _ => raise error ("thy_containing_rls : rls '"^str^
1.60 + | _ => error ("thy_containing_rls : rls '"^str^
1.61 "' not in !rulset' und thy '"^thy'^"'");
1.62
1.63 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()
1.64 -else raise error "rewtools.sml: diff.behav. in thy_containing_rls 3";
1.65 +else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
1.66
1.67
1.68 "----------- fun thy_containing_cal ------------------------------";
1.69 @@ -207,7 +207,7 @@
1.70 interSteps 1 ([1,1],Res);
1.71 val ((pt,p),_) = get_calc 1; show_pt pt;
1.72 if existpt' ([1,1,1], Frm) pt then ()
1.73 -else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
1.74 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
1.75
1.76 initContext 1 Thy_ ([1,1,1], Frm);
1.77 --------------------TODO.new_c: cvs before 071227, 11:50*)
1.78 @@ -241,7 +241,7 @@
1.79 val ContThm {thm,result,...} = context_thy (pt,p) tac;
1.80 if thm = "thy_isac_Test-thm-radd_left_commute"
1.81 andalso term2str result = "-2 + (1 + x) = 0" then ()
1.82 -else raise error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
1.83 +else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
1.84
1.85 val p = ([3,1,1], Frm);
1.86 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
1.87 @@ -251,7 +251,7 @@
1.88 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
1.89 if thm = "thy_isac_Test-thm-risolate_bdv_add"
1.90 andalso term2str result = "x = 0 + -1 * -1" then ()
1.91 -else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.92 +else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.93
1.94 initContext 1 Thy_ ([2,5], Res);
1.95 (*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
1.96 @@ -270,7 +270,7 @@
1.97 val ContRls {rls,result,...} = context_thy (pt,p) tac;
1.98 if rls = "thy_isac_Test-rls-Test_simplify"
1.99 andalso term2str result = "-1 + x = 0" then ()
1.100 -else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.101 +else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.102
1.103 val p = ([3,1], Frm);
1.104 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
1.105 @@ -280,7 +280,7 @@
1.106 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
1.107 if rls = "thy_isac_Test-rls-isolate_bdv"
1.108 andalso term2str result = "x = 0 + -1 * -1" then ()
1.109 -else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.110 +else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
1.111
1.112
1.113
1.114 @@ -297,7 +297,7 @@
1.115 val ContThm {thm,result,...} = context_thy (pt,p) tac;
1.116 if thm = "thy_isac_Test-thm-radd_left_commute"
1.117 andalso term2str result = "-2 + (1 + x) = 0" then ()
1.118 -else raise error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
1.119 +else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
1.120
1.121 val p = ([3,1,1], Frm);
1.122 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
1.123 @@ -307,7 +307,7 @@
1.124 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
1.125 if thm = "thy_isac_Test-thm-risolate_bdv_add"
1.126 andalso term2str result = "x = 0 + -1 * -1" then ()
1.127 -else raise error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
1.128 +else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
1.129
1.130 val p = ([2,5], Res);
1.131 val tac = Calculate "plus";
1.132 @@ -332,7 +332,7 @@
1.133 val ContRls {rls,result,...} = context_thy (pt,p) tac;
1.134 if rls = "thy_isac_Test-rls-Test_simplify"
1.135 andalso term2str result = "-1 + x = 0" then ()
1.136 -else raise error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
1.137 +else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
1.138
1.139 val p = ([3,1], Frm);
1.140 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
1.141 @@ -340,7 +340,7 @@
1.142 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
1.143 if rls = "thy_isac_Test-rls-isolate_bdv"
1.144 andalso term2str result = "x = 0 + -1 * -1" then ()
1.145 -else raise error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
1.146 +else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
1.147
1.148
1.149 "----------- checkContext..Thy_ on last formula ------------------";
1.150 @@ -387,7 +387,7 @@
1.151 val xstr = takerest (5, rest');
1.152
1.153 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
1.154 -else raise error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
1.155 +else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
1.156
1.157
1.158 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
1.159 @@ -405,13 +405,13 @@
1.160
1.161 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
1.162 if is_curr_endof_calc pt ([1],Frm) then ()
1.163 -else raise error "rewtools.sml is_curr_endof_calc ([1],Frm)";
1.164 +else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
1.165
1.166 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
1.167 if not (is_curr_endof_calc pt ([1],Frm)) then ()
1.168 -else raise error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
1.169 +else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
1.170 if is_curr_endof_calc pt ([1],Res) then ()
1.171 -else raise error "rewtools.sml is_curr_endof_calc ([1],Res)";
1.172 +else error "rewtools.sml is_curr_endof_calc ([1],Res)";
1.173
1.174 initContext 1 Thy_ ([1],Res);
1.175
1.176 @@ -473,7 +473,7 @@
1.177 "----- thus we repair the [.] in string_of_thmI...";
1.178 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
1.179 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
1.180 -else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
1.181 +else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
1.182 " = " ^ string_of_thmI thm);
1.183
1.184
1.185 @@ -496,7 +496,7 @@
1.186 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
1.187 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
1.188 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
1.189 -else raise error "rewtools.sml: string_of_thmI ?!?";
1.190 +else error "rewtools.sml: string_of_thmI ?!?";
1.191
1.192 getTactic 1 ([1],Frm);
1.193
1.194 @@ -514,7 +514,7 @@
1.195 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.196 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.197 Calculate "plus"] then ()
1.198 -else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
1.199 +else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
1.200
1.201
1.202 "----------- fun is_contained_in ---------------------------------";
1.203 @@ -522,12 +522,12 @@
1.204 "----------- fun is_contained_in ---------------------------------";
1.205 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
1.206 if contains_rule r1 Test_simplify then ()
1.207 -else raise error "rewtools.sml contains_rule Thm";
1.208 +else error "rewtools.sml contains_rule Thm";
1.209
1.210 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
1.211 if contains_rule r1 Test_simplify then ()
1.212 -else raise error "rewtools.sml contains_rule Calc";
1.213 +else error "rewtools.sml contains_rule Calc";
1.214
1.215 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
1.216 if not (contains_rule r1 Test_simplify) then ()
1.217 -else raise error "rewtools.sml contains_rule Calc";
1.218 +else error "rewtools.sml contains_rule Calc";