# HG changeset patch # User wenzelm # Date 1686058183 -7200 # Node ID bb85bda12b8e23804ded14576416b573b1987c1a # Parent 0ea55458f867f4329ef56b18287eadafe0f4b469 proper exception positions; diff -r 0ea55458f867 -r bb85bda12b8e src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jun 06 15:12:40 2023 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 06 15:29:43 2023 +0200 @@ -600,8 +600,6 @@ exception BAD_THM of string; -fun bad_thm msg = raise BAD_THM msg; - datatype strictness = Silent | Liberal | Strict fun handle_strictness thm_of f strictness thy x = SOME (f x) @@ -622,7 +620,7 @@ let val ty_decl = const_typ thy c; in if typscheme_equiv (ty_decl, ty) then () - else bad_thm ("Type\n" ^ string_of_typ thy ty + else raise BAD_THM ("Type\n" ^ string_of_typ thy ty ^ "\nof constant " ^ quote c ^ "\nis too specific compared to declared type\n" ^ string_of_typ thy ty_decl) @@ -631,28 +629,28 @@ fun check_eqn thy {allow_nonlinear, allow_consts, allow_pats} thm (lhs, rhs) = let fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v - | Free _ => bad_thm "Illegal free variable" + | Free _ => raise BAD_THM "Illegal free variable" | _ => I) t []; fun tvars_of t = fold_term_types (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v - | TFree _ => bad_thm "Illegal free type variable")) t []; + | TFree _ => raise BAD_THM "Illegal free type variable")) t []; val lhs_vs = vars_of lhs; val rhs_vs = vars_of rhs; val lhs_tvs = tvars_of lhs; val rhs_tvs = tvars_of rhs; val _ = if null (subtract (op =) lhs_vs rhs_vs) then () - else bad_thm "Free variables on right hand side of equation"; + else raise BAD_THM "Free variables on right hand side of equation"; val _ = if null (subtract (op =) lhs_tvs rhs_tvs) then () - else bad_thm "Free type variables on right hand side of equation"; + else raise BAD_THM "Free type variables on right hand side of equation"; val (head, args) = strip_comb lhs; val (c, ty) = case head of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty) - | _ => bad_thm "Equation not headed by constant"; - fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" + | _ => raise BAD_THM "Equation not headed by constant"; + fun check _ (Abs _) = raise BAD_THM "Abstraction on left hand side of equation" | check 0 (Var _) = () - | check _ (Var _) = bad_thm "Variable with application on left hand side of equation" + | check _ (Var _) = raise BAD_THM "Variable with application on left hand side of equation" | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) | check n (Const (c_ty as (c, ty))) = if allow_pats then let @@ -660,25 +658,25 @@ in if n = (length o binder_types) ty then if allow_consts orelse is_constr thy c' then () - else bad_thm (quote c ^ " is not a constructor, on left hand side of equation") - else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation") - end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") + else raise BAD_THM (quote c ^ " is not a constructor, on left hand side of equation") + else raise BAD_THM ("Partially applied constant " ^ quote c ^ " on left hand side of equation") + end else raise BAD_THM ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") val _ = map (check 0) args; val _ = if allow_nonlinear orelse is_linear thm then () - else bad_thm "Duplicate variables on left hand side of equation"; + else raise BAD_THM "Duplicate variables on left hand side of equation"; val _ = if (is_none o Axclass.class_of_param thy) c then () - else bad_thm "Overloaded constant as head in equation"; + else raise BAD_THM "Overloaded constant as head in equation"; val _ = if not (is_constr thy c) then () - else bad_thm "Constructor as head in equation"; + else raise BAD_THM "Constructor as head in equation"; val _ = if not (is_abstr thy c) then () - else bad_thm "Abstractor as head in equation"; + else raise BAD_THM "Abstractor as head in equation"; val _ = check_decl_ty thy (c, ty); val _ = case strip_type ty of (Type (tyco, _) :: _, _) => (case lookup_vs_type_spec thy tyco of SOME (_, type_spec) => (case projection_of type_spec of SOME proj => if c = proj - then bad_thm "Projection as head in equation" + then raise BAD_THM "Projection as head in equation" else () | _ => ()) | _ => ()) @@ -690,8 +688,8 @@ fun raw_assert_eqn thy check_patterns (thm, proper) = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm - handle TERM _ => bad_thm "Not an equation" - | THM _ => bad_thm "Not a proper equation"; + handle TERM _ => raise BAD_THM "Not an equation" + | THM _ => raise BAD_THM "Not a proper equation"; val _ = check_eqn thy {allow_nonlinear = not proper, allow_consts = not (proper andalso check_patterns), allow_pats = true} thm (lhs, rhs); in (thm, proper) end; @@ -699,23 +697,23 @@ fun raw_assert_abs_eqn thy some_tyco thm = let val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm - handle TERM _ => bad_thm "Not an equation" - | THM _ => bad_thm "Not a proper equation"; + handle TERM _ => raise BAD_THM "Not an equation" + | THM _ => raise BAD_THM "Not a proper equation"; val (proj_t, lhs) = dest_comb full_lhs - handle TERM _ => bad_thm "Not an abstract equation"; + handle TERM _ => raise BAD_THM "Not an abstract equation"; val (proj, ty) = dest_Const proj_t - handle TERM _ => bad_thm "Not an abstract equation"; + handle TERM _ => raise BAD_THM "Not an abstract equation"; val (tyco, Ts) = (dest_Type o domain_type) ty - handle TERM _ => bad_thm "Not an abstract equation" - | TYPE _ => bad_thm "Not an abstract equation"; + handle TERM _ => raise BAD_THM "Not an abstract equation" + | TYPE _ => raise BAD_THM "Not an abstract equation"; val _ = case some_tyco of SOME tyco' => if tyco = tyco' then () - else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') + else raise BAD_THM ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') | NONE => (); val (vs, proj', (abs', _)) = case lookup_vs_type_spec thy tyco of SOME (vs, Abstractor spec) => (vs, #projection spec, #abstractor spec) - | _ => bad_thm ("Not an abstract type: " ^ tyco); + | _ => raise BAD_THM ("Not an abstract type: " ^ tyco); val _ = if proj = proj' then () - else bad_thm ("Projection mismatch: " ^ quote proj ^ " vs. " ^ quote proj'); + else raise BAD_THM ("Projection mismatch: " ^ quote proj ^ " vs. " ^ quote proj'); val _ = check_eqn thy {allow_nonlinear = false, allow_consts = false, allow_pats = false} thm (lhs, rhs); val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs) then () @@ -842,21 +840,21 @@ let val thm = (Axclass.unoverload (Proof_Context.init_global thy) o meta_rewrite thy) proto_thm; val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) - handle TERM _ => bad_thm "Not an equation" - | THM _ => bad_thm "Not a proper equation"; + handle TERM _ => raise BAD_THM "Not an equation" + | THM _ => raise BAD_THM "Not a proper equation"; val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) o apfst dest_Const o dest_comb) lhs - handle TERM _ => bad_thm "Not an abstype certificate"; + handle TERM _ => raise BAD_THM "Not an abstype certificate"; val _ = apply2 (fn c => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); val _ = check_decl_ty thy (abs, raw_ty); val _ = check_decl_ty thy (rep, rep_ty); val _ = if length (binder_types raw_ty) = 1 then () - else bad_thm "Bad type for abstract constructor"; + else raise BAD_THM "Bad type for abstract constructor"; val _ = (fst o dest_Var) param - handle TERM _ => bad_thm "Not an abstype certificate"; - val _ = if param = rhs then () else bad_thm "Not an abstype certificate"; + handle TERM _ => raise BAD_THM "Not an abstype certificate"; + val _ = if param = rhs then () else raise BAD_THM "Not an abstype certificate"; val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, devarify raw_ty); val ty = domain_type ty';