--- a/NEWS Wed Nov 03 07:02:09 2010 -0700
+++ b/NEWS Wed Nov 03 15:56:15 2010 +0100
@@ -349,6 +349,10 @@
*** ML ***
+* Discontinued obsolete function sys_error and exception SYS_ERROR.
+See implementation manual for further details on exceptions in
+Isabelle/ML.
+
* Antiquotation @{assert} inlines a function bool -> unit that raises
Fail if the argument is false. Due to inlining the source position of
failed assertions is included in the error output.
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Nov 03 15:56:15 2010 +0100
@@ -138,7 +138,7 @@
else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
else if member (op =) [Gt, Ge] c then Thm.dest_arg1
else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
- else sys_error "decomp_mpinf: Impossible case!!") fm
+ else raise Fail "decomp_mpinf: Impossible case!!") fm
val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
if c = Nox then map (instantiate' [] [SOME fm])
[minf_P, pinf_P, nmi_P, npi_P, ld_P]
--- a/src/HOL/Library/Eval_Witness.thy Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Library/Eval_Witness.thy Wed Nov 03 15:56:15 2010 +0100
@@ -63,7 +63,7 @@
fun dest_exs 0 t = t
| dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
- | dest_exs _ _ = sys_error "dest_exs";
+ | dest_exs _ _ = raise Fail "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Wed Nov 03 15:56:15 2010 +0100
@@ -115,7 +115,7 @@
fun type_of (Free (_, ty)) = ty
| type_of (Const (_, ty)) = ty
| type_of (Var (_, ty)) = ty
- | type_of _ = sys_error "infer_types: type_of error"
+ | type_of _ = raise Fail "infer_types: type_of error"
in
fun infer_types naming encoding =
let
@@ -132,7 +132,7 @@
val (adom, arange) =
case aty of
Type ("fun", [dom, range]) => (dom, range)
- | _ => sys_error "infer_types: function type expected"
+ | _ => raise Fail "infer_types: function type expected"
val (b, bty) = infer_types level bounds (SOME adom) b
in
(a $ b, arange)
@@ -143,7 +143,8 @@
in
(Abs (naming level, dom, m), ty)
end
- | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
+ | infer_types _ _ NONE (AbstractMachine.Abs m) =
+ raise Fail "infer_types: cannot infer type of abstraction"
fun infer ty term =
let
--- a/src/HOL/Tools/Function/context_tree.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/context_tree.ML Wed Nov 03 15:56:15 2010 +0100
@@ -125,7 +125,7 @@
(cterm_instantiate inst r, dep, branches)
end
handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
- | find_cong_rule _ _ _ [] _ = sys_error "Function/context_tree.ML: No cong rule found!"
+ | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
fun mk_tree fvar h ctxt t =
--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Nov 03 15:56:15 2010 +0100
@@ -117,7 +117,7 @@
rtac @{thm "mlex_leq"} 1
THEN PRIMITIVE (Thm.elim_implies thm)
THEN prove_row cs
- | _ => sys_error "lexicographic_order")
+ | _ => raise General.Fail "lexicographic_order")
| prove_row [] = no_tac;
--- a/src/HOL/Tools/Function/mutual.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/mutual.ML Wed Nov 03 15:56:15 2010 +0100
@@ -185,7 +185,7 @@
case cprems_of psimp of
[] => (psimp, I)
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
- | _ => sys_error "Too many conditions"
+ | _ => raise General.Fail "Too many conditions"
in
Goal.prove ctxt [] []
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Nov 03 15:56:15 2010 +0100
@@ -171,8 +171,8 @@
else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
| SOME (Termination.LessEq (thm, _)) =>
if not bStrict then thm
- else sys_error "get_desc_thm"
- | _ => sys_error "get_desc_thm"
+ else raise Fail "get_desc_thm"
+ | _ => raise Fail "get_desc_thm"
val (label, lev, sl, covering) = certificate
--- a/src/HOL/Tools/TFL/tfl.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Nov 03 15:56:15 2010 +0100
@@ -607,8 +607,7 @@
val vlist = #2(S.strip_comb (S.rhs body))
val plist = ListPair.zip (vlist, xlist)
val args = map (the o AList.lookup (op aconv) plist) qvars
- handle Option => sys_error
- "TFL fault [alpha_ex_unroll]: no correspondence"
+ handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
fun build ex [] = []
| build (_$rex) (v::rst) =
let val ex1 = Term.betapply(rex, v)
--- a/src/HOL/Tools/inductive.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/inductive.ML Wed Nov 03 15:56:15 2010 +0100
@@ -229,7 +229,7 @@
fun arg_types_of k c = drop k (binder_types (fastype_of c));
-fun find_arg T x [] = sys_error "find_arg"
+fun find_arg T x [] = raise Fail "find_arg"
| find_arg T x ((p as (_, (SOME _, _))) :: ps) =
apsnd (cons p) (find_arg T x ps)
| find_arg T x ((p as (U, (NONE, y))) :: ps) =
--- a/src/HOL/Tools/record.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/record.ML Wed Nov 03 15:56:15 2010 +0100
@@ -1578,7 +1578,7 @@
(case rev params of
[] =>
(case AList.lookup (op =) (Term.add_frees g []) s of
- NONE => sys_error "try_param_tac: no such variable"
+ NONE => error "try_param_tac: no such variable"
| SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
| (_, T) :: _ =>
[(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
--- a/src/HOL/Tools/sat_solver.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOL/Tools/sat_solver.ML Wed Nov 03 15:56:15 2010 +0100
@@ -321,7 +321,7 @@
[] => [xs1]
| (0::[]) => [xs1]
| (0::tl) => xs1 :: clauses tl
- | _ => sys_error "this cannot happen"
+ | _ => raise Fail "SatSolver.clauses"
end
(* int -> PropLogic.prop_formula *)
fun literal_from_int i =
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Nov 03 15:56:15 2010 +0100
@@ -327,8 +327,8 @@
fun multiply_ineq n (i as Lineq(k,ty,l,just)) =
if n = 1 then i
- else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
- else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
+ else if n = 0 andalso ty = Lt then raise Fail "multiply_ineq"
+ else if n < 0 andalso (ty=Le orelse ty=Lt) then raise Fail "multiply_ineq"
else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));
(* ------------------------------------------------------------------------- *)
@@ -352,7 +352,7 @@
if (c1 >= 0) = (c2 >= 0)
then if ty1 = Eq then (~m1,m2)
else if ty2 = Eq then (m1,~m2)
- else sys_error "elim_var"
+ else raise Fail "elim_var"
else (m1,m2)
val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1)
then (~n1,~n2) else (n1,n2)
@@ -497,7 +497,7 @@
(the (try_add ([thm2] RL inj_thms) thm1)
handle Option =>
(trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
- sys_error "Linear arithmetic: failed to add thms"))
+ raise Fail "Linear arithmetic: failed to add thms"))
| SOME thm => thm)
| SOME thm => thm);
@@ -598,7 +598,7 @@
else lineq(c,Lt,diff,just)
| "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just))
| "=" => lineq(c,Eq,diff,just)
- | _ => sys_error("mklineq" ^ rel)
+ | _ => raise Fail ("mklineq" ^ rel)
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Pure/Isar/code.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/Isar/code.ML Wed Nov 03 15:56:15 2010 +0100
@@ -222,7 +222,7 @@
fun invoke f k = case Datatab.lookup (! kinds) k
of SOME kind => f kind
- | NONE => sys_error "Invalid code data identifier";
+ | NONE => raise Fail "Invalid code data identifier";
in
--- a/src/Pure/Isar/runtime.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/Isar/runtime.ML Wed Nov 03 15:56:15 2010 +0100
@@ -68,7 +68,6 @@
| TERMINATE => ["Exit"]
| TimeLimit.TimeOut => ["Timeout"]
| TOPLEVEL_ERROR => ["Error"]
- | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
| ERROR msg => [msg]
| Fail msg => [raised exn "Fail" [msg]]
| THEORY (msg, thys) =>
--- a/src/Pure/ML/ml_lex.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/ML/ml_lex.ML Wed Nov 03 15:56:15 2010 +0100
@@ -73,7 +73,14 @@
fun check_content_of tok =
(case kind_of tok of
Error msg => error msg
- | _ => content_of tok);
+ | _ =>
+ (case tok of
+ Token (_, (Keyword, ":>")) =>
+ warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
+ \prefer non-opaque matching (:) possibly with abstype" ^
+ Position.str_of (pos_of tok))
+ | _ => ();
+ content_of tok));
val flatten = implode o map (Symbol.escape o check_content_of);
--- a/src/Pure/codegen.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/codegen.ML Wed Nov 03 15:56:15 2010 +0100
@@ -354,10 +354,11 @@
fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
-fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
+fun dest_sym s =
+ (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
("<" :: "^" :: xs, ">") => (true, implode xs)
| ("<" :: xs, ">") => (false, implode xs)
- | _ => sys_error "dest_sym");
+ | _ => raise Fail "dest_sym");
fun mk_id s = if s = "" then "" else
let
@@ -378,7 +379,7 @@
fun mk_long_id (p as (tab, used)) module s =
let
- fun find_name [] = sys_error "mk_long_id"
+ fun find_name [] = raise Fail "mk_long_id"
| find_name (ys :: yss) =
let
val s' = Long_Name.implode ys
--- a/src/Pure/library.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/Pure/library.ML Wed Nov 03 15:56:15 2010 +0100
@@ -29,8 +29,6 @@
val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
(*errors*)
- exception SYS_ERROR of string
- val sys_error: string -> 'a
exception ERROR of string
val error: string -> 'a
val cat_error: string -> string -> 'a
@@ -256,11 +254,9 @@
fun funpow_yield (0 : int) _ x = ([], x)
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
+
(* errors *)
-exception SYS_ERROR of string;
-fun sys_error msg = raise SYS_ERROR msg;
-
exception ERROR of string;
fun error msg = raise ERROR msg;
--- a/src/ZF/Tools/numeral_syntax.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/ZF/Tools/numeral_syntax.ML Wed Nov 03 15:56:15 2010 +0100
@@ -21,7 +21,7 @@
fun mk_bit 0 = Syntax.const @{const_syntax "0"}
| mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
- | mk_bit _ = sys_error "mk_bit";
+ | mk_bit _ = raise Fail "mk_bit";
fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
| dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
--- a/src/ZF/int_arith.ML Wed Nov 03 07:02:09 2010 -0700
+++ b/src/ZF/int_arith.ML Wed Nov 03 15:56:15 2010 +0100
@@ -4,18 +4,25 @@
Simprocs for linear arithmetic.
*)
-structure Int_Numeral_Simprocs =
+signature INT_NUMERAL_SIMPROCS =
+sig
+ val cancel_numerals: simproc list
+ val combine_numerals: simproc
+ val combine_numerals_prod: simproc
+end
+
+structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
struct
(* abstract syntax operations *)
fun mk_bit 0 = @{term "0"}
| mk_bit 1 = @{term "succ(0)"}
- | mk_bit _ = sys_error "mk_bit";
+ | mk_bit _ = raise TERM ("mk_bit", []);
fun dest_bit @{term "0"} = 0
| dest_bit @{term "succ(0)"} = 1
- | dest_bit _ = raise Match;
+ | dest_bit t = raise TERM ("dest_bit", [t]);
fun mk_bin i =
let
@@ -29,7 +36,7 @@
fun bin_of @{term Pls} = []
| bin_of @{term Min} = [~1]
| bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of _ = sys_error "dest_bin";
+ | bin_of _ = raise TERM ("dest_bin", [tm]);
in Numeral_Syntax.dest_binary (bin_of tm) end;
@@ -37,10 +44,8 @@
fun mk_numeral i = @{const integ_of} $ mk_bin i;
-(*Decodes a binary INTEGER*)
-fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
- (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_numeral (Const(@{const_name integ_of}, _) $ w) = dest_bin w
+ | dest_numeral t = raise TERM ("dest_numeral", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)
@@ -59,8 +64,6 @@
fun long_mk_sum [] = zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
-
(*decompose additions AND subtractions as a sum*)
fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
@@ -71,9 +74,6 @@
fun dest_sum t = dest_summing (true, t, []);
-val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
-val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
-
val one = mk_numeral 1;
val mk_times = FOLogic.mk_binop @{const_name "zmult"};