# HG changeset patch # User blanchet # Date 1483108835 -3600 # Node ID 7596b0736ab9a3eb38b4a9db94cc442040c78d69 # Parent 08c2d80428ff7922599e4f209f43a0989ab2e851 more uniform errors in '(prim)(co)rec(ursive)' variants diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Dec 30 15:40:35 2016 +0100 @@ -9,6 +9,44 @@ signature BNF_FP_REC_SUGAR_UTIL = sig val error_at: Proof.context -> term list -> string -> 'a + val warning_at: Proof.context -> term list -> string -> unit + + val excess_equations: Proof.context -> term list -> 'a + val extra_variable_in_rhs: Proof.context -> term list -> term -> 'a + val ill_formed_corec_call: Proof.context -> term -> 'a + val ill_formed_equation_head: Proof.context -> term list -> 'a + val ill_formed_equation_lhs_rhs: Proof.context -> term list -> 'a + val ill_formed_equation: Proof.context -> term -> 'a + val ill_formed_formula: Proof.context -> term -> 'a + val ill_formed_rec_call: Proof.context -> term -> 'a + val inconstant_pattern_pos_for_fun: Proof.context -> term list -> string -> 'a + val invalid_map: Proof.context -> term list -> term -> 'a + val missing_args_to_fun_on_lhs: Proof.context -> term list -> 'a + val missing_equations_for_const: string -> 'a + val missing_equations_for_fun: string -> 'a + val missing_pattern: Proof.context -> term list -> 'a + val more_than_one_nonvar_in_lhs: Proof.context -> term list -> 'a + val multiple_equations_for_ctr: Proof.context -> term list -> 'a + val nonprimitive_corec: Proof.context -> term list -> 'a + val nonprimitive_pattern_in_lhs: Proof.context -> term list -> 'a + val not_codatatype: Proof.context -> typ -> 'a + val not_datatype: Proof.context -> typ -> 'a + val not_constructor_in_pattern: Proof.context -> term list -> term -> 'a + val not_constructor_in_rhs: Proof.context -> term list -> term -> 'a + val rec_call_not_apply_to_ctr_arg: Proof.context -> term list -> term -> 'a + val partially_applied_ctr_in_pattern: Proof.context -> term list -> 'a + val partially_applied_ctr_in_rhs: Proof.context -> term list -> 'a + val too_few_args_in_rec_call: Proof.context -> term list -> term -> 'a + val unexpected_rec_call_in: Proof.context -> term list -> term -> 'a + val unexpected_corec_call_in: Proof.context -> term list -> term -> 'a + val unsupported_case_around_corec_call: Proof.context -> term list -> term -> 'a + + val no_equation_for_ctr_warning: Proof.context -> term list -> term -> unit + + val check_all_fun_arg_frees: Proof.context -> term list -> term list -> unit + val check_duplicate_const_names: binding list -> unit + val check_duplicate_variables_in_lhs: Proof.context -> term list -> term list -> unit + val check_top_sort: Proof.context -> binding -> typ -> unit datatype fp_kind = Least_FP | Greatest_FP @@ -63,9 +101,109 @@ structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = struct -fun error_at ctxt ts str = - error (str ^ (if null ts then "" - else " at\n " ^ space_implode "\n " (map (quote o Syntax.string_of_term ctxt) ts))); +fun error_at ctxt ats str = + error (str ^ (if null ats then "" + else " at\n" ^ cat_lines (map (prefix " " o Syntax.string_of_term ctxt) ats))); +fun warning_at ctxt ats str = + warning (str ^ (if null ats then "" + else " at\n" ^ cat_lines (map (prefix " " o Syntax.string_of_term ctxt) ats))); + +fun excess_equations ctxt ats = + error ("Excess equation(s):\n" ^ + cat_lines (map (prefix " " o Syntax.string_of_term ctxt) ats)); +fun extra_variable_in_rhs ctxt ats var = + error_at ctxt ats ("Extra variable " ^ quote (Syntax.string_of_term ctxt var) ^ + " in right-hand side"); +fun ill_formed_corec_call ctxt t = + error ("Ill-formed corecursive call " ^ quote (Syntax.string_of_term ctxt t)); +fun ill_formed_equation_head ctxt ats = + error_at ctxt ats "Ill-formed function equation (expected function name on left-hand side)"; +fun ill_formed_equation_lhs_rhs ctxt ats = + error_at ctxt ats "Ill-formed equation (expected \"lhs = rhs\")"; +fun ill_formed_equation ctxt t = + error_at ctxt [] ("Ill-formed equation:\n " ^ Syntax.string_of_term ctxt t); +fun ill_formed_formula ctxt t = + error_at ctxt [] ("Ill-formed formula:\n " ^ Syntax.string_of_term ctxt t); +fun ill_formed_rec_call ctxt t = + error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); +fun inconstant_pattern_pos_for_fun ctxt ats fun_name = + error_at ctxt ats ("Inconstant constructor pattern position for function " ^ quote fun_name); +fun invalid_map ctxt ats t = + error_at ctxt ats ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); +fun missing_args_to_fun_on_lhs ctxt ats = + error_at ctxt ats "Expected more arguments to function on left-hand side"; +fun missing_equations_for_const fun_name = + error ("Missing equations for constant " ^ quote fun_name); +fun missing_equations_for_fun fun_name = + error ("Missing equations for function " ^ quote fun_name); +fun missing_pattern ctxt ats = + error_at ctxt ats "Constructor pattern missing in left-hand side"; +fun more_than_one_nonvar_in_lhs ctxt ats = + error_at ctxt ats "More than one non-variable argument in left-hand side"; +fun multiple_equations_for_ctr ctxt ats = + error ("Multiple equations for constructor:\n" ^ + cat_lines (map (prefix " " o Syntax.string_of_term ctxt) ats)); +fun nonprimitive_corec ctxt ats = + error_at ctxt ats "Nonprimitive corecursive specification"; +fun nonprimitive_pattern_in_lhs ctxt ats = + error_at ctxt ats "Nonprimitive pattern in left-hand side"; +fun not_codatatype ctxt T = + error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); +fun not_datatype ctxt T = + error ("Not a datatype: " ^ Syntax.string_of_typ ctxt T); +fun not_constructor_in_pattern ctxt ats t = + error_at ctxt ats ("Not a constructor " ^ quote (Syntax.string_of_term ctxt t) ^ + " in pattern"); +fun not_constructor_in_rhs ctxt ats t = + error_at ctxt ats ("Not a constructor " ^ quote (Syntax.string_of_term ctxt t) ^ + " in right-hand side"); +fun rec_call_not_apply_to_ctr_arg ctxt ats t = + error_at ctxt ats ("Recursive call not directly applied to constructor argument in " ^ + quote (Syntax.string_of_term ctxt t)); +fun partially_applied_ctr_in_pattern ctxt ats = + error_at ctxt ats "Partially applied constructor in pattern"; +fun partially_applied_ctr_in_rhs ctxt ats = + error_at ctxt ats "Partially applied constructor in right-hand side"; +fun too_few_args_in_rec_call ctxt ats t = + error_at ctxt ats ("Too few arguments in recursive call " ^ quote (Syntax.string_of_term ctxt t)); +fun unexpected_rec_call_in ctxt ats t = + error_at ctxt ats ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); +fun unexpected_corec_call_in ctxt ats t = + error_at ctxt ats ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); +fun unsupported_case_around_corec_call ctxt ats t = + error_at ctxt ats ("Unsupported corecursive call under case expression " ^ + quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^ + quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^ + " with discriminators and selectors to circumvent this limitation)"); + +fun no_equation_for_ctr_warning ctxt ats ctr = + warning_at ctxt ats ("No equation for constructor " ^ quote (Syntax.string_of_term ctxt ctr)); + +fun check_all_fun_arg_frees ctxt ats fun_args = + (case find_first (not o is_Free) fun_args of + SOME t => error_at ctxt ats ("Non-variable function argument on left-hand side " ^ + quote (Syntax.string_of_term ctxt t)) + | NONE => + (case find_first (Variable.is_fixed ctxt o fst o dest_Free) fun_args of + SOME t => error_at ctxt ats ("Function argument " ^ + quote (Syntax.string_of_term ctxt t) ^ " is fixed in context") + | NONE => ())); + +fun check_duplicate_const_names bs = + let val dups = duplicates (op =) (map Binding.name_of bs) in + ignore (null dups orelse error ("Duplicate constant name " ^ quote (hd dups))) + end; + +fun check_duplicate_variables_in_lhs ctxt ats vars = + let val dups = duplicates (op aconv) vars in + ignore (null dups orelse + error_at ctxt ats ("Duplicable variable " ^ quote (Syntax.string_of_term ctxt (hd dups)) ^ + " in left-hand side")) + end; + +fun check_top_sort ctxt b T = + ignore (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort type}) orelse + error ("Type of " ^ Binding.print b ^ " contains top sort")); datatype fp_kind = Least_FP | Greatest_FP; diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Dec 30 15:40:35 2016 +0100 @@ -87,14 +87,6 @@ #> Raw_Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} [] end; -fun unexpected_corec_call ctxt eqns t = - error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); -fun unsupported_case_around_corec_call ctxt eqns t = - error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ - quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^ - quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^ - " with discriminators and selectors to circumvent this limitation.)"); - datatype corec_option = Plugins_Option of Proof.context -> Plugin_Name.filter | Friend_Option | @@ -754,43 +746,24 @@ fun check_fun_name () = null fun_frees orelse member (op aconv) fun_frees fun_t orelse - error (quote (Syntax.string_of_term ctxt fun_t) ^ - " is not the function currently being defined"); - - fun check_args_are_vars () = - let - fun is_ok_Free_or_Var (Free (s, _)) = not (String.isSuffix inner_fp_suffix s) - | is_ok_Free_or_Var (Var _) = true - | is_ok_Free_or_Var _ = false; - - fun is_valid arg = - (is_ok_Free_or_Var arg andalso not (member (op aconv) fun_frees arg)) orelse - error ("Argument " ^ quote (Syntax.string_of_term ctxt arg) ^ " is not free"); - in - forall is_valid arg_ts - end; - - fun check_no_duplicate_arg () = - (case duplicates (op =) arg_ts of - [] => () - | arg :: _ => error ("Repeated argument: " ^ quote (Syntax.string_of_term ctxt arg))); + ill_formed_equation_head ctxt [] fun_t; fun check_no_other_frees () = (case Term.add_frees rhs [] |> map Free |> subtract (op =) (fun_frees @ arg_ts) - |> filter_out (Variable.is_fixed ctxt o fst o dest_Free) of - [] => () - | Free (s, _) :: _ => error ("Extra variable on right-hand side: " ^ quote s)); + |> find_first (not o Variable.is_fixed ctxt o fst o dest_Free) of + NONE => () + | SOME t => extra_variable_in_rhs ctxt [] t); in - check_no_duplicate_arg (); + check_duplicate_variables_in_lhs ctxt [] arg_ts; check_fun_name (); - check_args_are_vars (); + check_all_fun_arg_frees ctxt [] (filter_out is_Var arg_ts); check_no_other_frees () end; fun parse_corec_equation ctxt fun_frees eq = let val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (drop_all eq)) - handle TERM _ => error "Expected HOL equation"; + handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eq]; val _ = check_corec_equation ctxt fun_frees (lhs, rhs); @@ -1536,10 +1509,7 @@ | NONE => explore params t) | _ => explore params t) and explore_cond params t = - if has_self_call t then - error ("Unallowed corecursive call in condition " ^ quote (Syntax.string_of_term lthy t)) - else - explore_inner params t + if has_self_call t then unexpected_rec_call_in lthy [] t else explore_inner params t and explore_inner params t = massage_rho explore_inner_general params t and explore_inner_general (params as {bound_Us, bound_Ts, T, ...}) t = @@ -1560,7 +1530,7 @@ disc' $ arg' else error ("Discriminator " ^ quote (Syntax.string_of_term lthy fun_t) ^ - " cannot be applied to non-lhs argument " ^ + " cannot be applied to non-variable " ^ quote (Syntax.string_of_term lthy (hd arg_ts))) end | _ => @@ -1576,7 +1546,7 @@ build_function_after_encapsulation fun_t sel' params arg_ts arg_ts' else error ("Selector " ^ quote (Syntax.string_of_term lthy fun_t) ^ - " cannot be applied to non-lhs argument " ^ + " cannot be applied to non-variable " ^ quote (Syntax.string_of_term lthy (hd arg_ts))) end | NONE => @@ -1615,8 +1585,7 @@ if is_some ctr_opt then rebuild_function_after_exploration fun_t (the ctr_opt) explore_inner params arg_ts else - error ("Constructor expected on right-hand side, " ^ - quote (Syntax.string_of_term lthy fun_t) ^ " found instead") + not_constructor_in_rhs lthy [] fun_t end; val rho_rhs = rhs @@ -1648,11 +1617,9 @@ HOLogic.mk_Trueprop (rho_rel $ rho_rhs $ rho_rhsZ) end; -fun extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T - ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy = +fun extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T + ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy = let - val Type (fpT_name, _) = body_type fun_T; - fun mk_rel T bnf = let val ZT = Tsubst Y Z T; @@ -1734,7 +1701,7 @@ fun massage_let_if_case_corec explore {bound_Ts, U, T, ...} t = massage_let_if_case ctxt has_self_call (fn bound_Ts => explore (build_params bound_Ts U T)) - (K (unexpected_corec_call ctxt [t])) (K (unsupported_case_around_corec_call ctxt [t])) + (K (unexpected_corec_call_in ctxt [t])) (K (unsupported_case_around_corec_call ctxt [t])) bound_Ts t; val massage_map_let_if_case = @@ -2004,8 +1971,7 @@ val ([((b, fun_T), mx)], [(_, eq)]) = fst (Specification.read_multi_specs raw_fixes [((Binding.empty_atts, raw_eq), [], [])] lthy); - val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse - error ("Type of " ^ Binding.print b ^ " contains top sort"); + val _ = check_top_sort lthy b fun_T; val (arg_Ts, res_T) = strip_type fun_T; val fpT_name = (case res_T of Type (s, _) => s | _ => not_codatatype lthy res_T); @@ -2030,8 +1996,8 @@ val parsed_eq' = parsed_eq ||> subst_atomic [(fun_free, fun_t)]; in lthy - |> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T - ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq' + |> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T + ssig_fp_sugar friend_parse_info fun_t parsed_eq' |>> pair prepared end; @@ -2277,7 +2243,7 @@ val fun_T = (case code_goal of @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _) => fastype_of (head_of t) - | _ => error "Expected HOL equation"); + | _ => ill_formed_equation_lhs_rhs lthy [code_goal]); val fun_t = Const (fun_name, fun_T); val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T; @@ -2294,8 +2260,8 @@ val parsed_eq = parse_corec_equation lthy [] code_goal; val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy) = - extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT fun_T k_T - ssig_T ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy; + extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T + ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy; fun register_friend_extra_and_note_thms code_goal code_thm const_transfers k_T friend_info lthy = diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Dec 30 15:40:35 2016 +0100 @@ -49,9 +49,6 @@ val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; -fun not_codatatype ctxt T = - error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); - fun generalize_types max_j T U = let val vars = Unsynchronized.ref []; diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Dec 30 15:40:35 2016 +0100 @@ -121,21 +121,6 @@ val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; -fun extra_variable ctxt ts var = - error_at ctxt ts ("Extra variable " ^ quote (Syntax.string_of_term ctxt var)); -fun not_codatatype ctxt T = - error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); -fun ill_formed_corec_call ctxt t = - error ("Ill-formed corecursive call " ^ quote (Syntax.string_of_term ctxt t)); -fun invalid_map ctxt t = - error_at ctxt [t] "Invalid map function"; -fun nonprimitive_corec ctxt eqns = - error_at ctxt eqns "Nonprimitive corecursive specification"; -fun unexpected_corec_call ctxt eqns t = - error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); -fun unsupported_case_around_corec_call ctxt eqns t = - error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ - quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors"); fun use_primcorecursive () = error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^ quote (#1 @{command_keyword primcorec}) ^ ")"); @@ -352,12 +337,12 @@ end; fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 = - massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) + massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call_in ctxt [t0])) (K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0; fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = let - fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else (); + fun check_no_call t = if has_call t then unexpected_corec_call_in ctxt [t0] t else (); fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2])) (Type (@{type_name fun}, [T1, T2])) t = @@ -658,23 +643,12 @@ fun check_extra_frees ctxt frees names t = let val bads = add_extra_frees ctxt frees names t [] in - null bads orelse extra_variable ctxt [t] (hd bads) + null bads orelse extra_variable_in_rhs ctxt [t] (hd bads) end; fun check_fun_args ctxt eqn fun_args = - let - val dups = duplicates (op =) fun_args; - val _ = null dups orelse error_at ctxt [eqn] - ("Duplicate variable " ^ quote (Syntax.string_of_term ctxt (hd dups))); - - val _ = forall is_Free fun_args orelse - error_at ctxt [eqn] ("Non-variable function argument on left-hand side " ^ - quote (Syntax.string_of_term ctxt (the (find_first (not o is_Free) fun_args)))); - - val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args; - val _ = null fixeds orelse error_at ctxt [eqn] ("Function argument " ^ - quote (Syntax.string_of_term ctxt (hd fixeds)) ^ " is fixed in context"); - in () end; + (check_duplicate_variables_in_lhs ctxt [eqn] fun_args; + check_all_fun_arg_frees ctxt [eqn] fun_args); fun dissect_coeqn_disc ctxt fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt prems0 @@ -695,7 +669,7 @@ val _ = check_fun_args ctxt concl fun_args; val bads = filter (Term.exists_subterm (is_free_in fun_names)) prems0; - val _ = null bads orelse error_at ctxt bads "Corecursive call(s) in condition(s)"; + val _ = null bads orelse unexpected_rec_call_in ctxt [] (hd bads); val (sequential, basic_ctr_specs) = the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name); @@ -752,7 +726,7 @@ ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn = let val (lhs, rhs) = HOLogic.dest_eq eqn - handle TERM _ => error_at ctxt [eqn] "Ill-formed equation (expected \"lhs = rhs\")"; + handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn]; val sel = head_of lhs; val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free @@ -787,7 +761,7 @@ val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs); val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs) - handle Option.Option => error_at ctxt [ctr] "Not a constructor"; + handle Option.Option => not_constructor_in_rhs ctxt [] ctr; val disc_concl = betapply (disc, lhs); val (eqn_data_disc_opt, matchedsss') = @@ -799,8 +773,7 @@ val sel_concls = sels ~~ ctr_args |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) - handle ListPair.UnequalLengths => - error_at ctxt [rhs] "Partially applied constructor in right-hand side"; + handle ListPair.UnequalLengths => partially_applied_ctr_in_rhs ctxt [rhs]; val eqns_data_sel = map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos @@ -822,7 +795,7 @@ val cond_ctrs = fold_rev_corec_code_rhs ctxt (fn cs => fn ctr => fn _ => if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs) - else error ("Not a constructor: " ^ quote (Syntax.string_of_term ctxt ctr))) [] rhs' [] + else not_constructor_in_rhs ctxt [] ctr) [] rhs' [] |> AList.group (op =); val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs); @@ -834,7 +807,7 @@ |> curry HOLogic.mk_eq lhs); val bads = maps (filter (Term.exists_subterm (is_free_in fun_names))) ctr_premss; - val _ = null bads orelse unexpected_corec_call ctxt [eqn0] rhs; + val _ = null bads orelse unexpected_corec_call_in ctxt [eqn0] rhs; val sequentials = replicate (length fun_names) false; in @@ -847,10 +820,10 @@ (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss = let val eqn = drop_all eqn0 - handle TERM _ => error_at ctxt [eqn0] "Ill-formed formula"; + handle TERM _ => ill_formed_formula ctxt eqn0; val (prems, concl) = Logic.strip_horn eqn |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop - handle TERM _ => error_at ctxt [eqn] "Ill-formed equation"; + handle TERM _ => ill_formed_equation ctxt eqn; val head = concl |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) @@ -860,7 +833,7 @@ fun check_num_args () = is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse - error_at ctxt [eqn] "Expected more arguments to function on left-hand side"; + missing_args_to_fun_on_lhs ctxt [eqn]; val discs = maps (map #disc) basic_ctr_specss; val sels = maps (maps #sels) basic_ctr_specss; @@ -940,8 +913,8 @@ let val U2 = (case try dest_sumT U of - SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt t0 - | NONE => invalid_map ctxt t0); + SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt [] t0 + | NONE => invalid_map ctxt [] t0); fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t') | rewrite bound_Ts (t as _ $ _) = @@ -1009,7 +982,7 @@ val bad = fold (add_extra_frees ctxt [] []) corec_args []; val _ = null bad orelse (if exists has_call corec_args then nonprimitive_corec ctxt [] - else extra_variable ctxt [] (hd bad)); + else extra_variable_in_rhs ctxt [] (hd bad)); val excludess' = disc_eqnss @@ -1084,14 +1057,11 @@ fun primcorec_ursive int auto opts fixes specs of_specs_opt lthy = let - val thy = Proof_Context.theory_of lthy; - val (bs, mxs) = map_split (apfst fst) fixes; val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list; - val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of - [] => () - | (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort")); + val _ = check_duplicate_const_names bs; + val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts); val actual_nn = length bs; @@ -1114,7 +1084,7 @@ val missing = fun_names |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data |> not oo member (op =)); - val _ = null missing orelse error ("Missing equations for " ^ commas missing); + val _ = null missing orelse missing_equations_for_const (hd missing); val callssss = map_filter (try (fn Sel x => x)) eqns_data @@ -1591,9 +1561,6 @@ fun primcorec_ursive_cmd int auto opts (raw_fixes, raw_specs_of) lthy = let - val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); - val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); - val (raw_specs, of_specs_opt) = split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy)); val (fixes, specs) = diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Dec 30 15:40:35 2016 +0100 @@ -208,15 +208,17 @@ let val thy = Proof_Context.theory_of lthy; - fun not_datatype s = error (quote s ^ " is not a datatype"); + fun not_datatype_name s = + error (quote s ^ " is not a datatype"); fun not_mutually_recursive ss = error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); fun checked_fp_sugar_of s = (case fp_sugar_of lthy s of SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) => - if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s - | _ => not_datatype s); + if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar + else not_datatype_name s + | _ => not_datatype_name s); val fpTs0 as Type (_, var_As) :: _ = map (#T o checked_fp_sugar_of o fst o dest_Type) @@ -317,7 +319,7 @@ |>> `(fn (inducts', induct', _, rec'_thmss) => SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) else - not_datatype fpT_name1; + not_datatype_name fpT_name1; val rec'_names = map (fst o dest_Const) recs'; val rec'_thms = flat rec'_thmss; diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_lfp_countable.ML --- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Dec 30 15:40:35 2016 +0100 @@ -27,7 +27,7 @@ HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN' REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE])); -fun meta_spec_mp_tac ctxt 0 = K all_tac +fun meta_spec_mp_tac _ 0 = K all_tac | meta_spec_mp_tac ctxt depth = dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' dtac ctxt meta_mp THEN' assume_tac ctxt; @@ -127,13 +127,14 @@ fun derive_encode_injectives_thms _ [] = [] | derive_encode_injectives_thms ctxt fpT_names0 = let - fun not_datatype s = error (quote s ^ " is not a datatype"); + fun not_datatype_name s = + error (quote s ^ " is not a datatype"); fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes"); fun lfp_sugar_of s = (case fp_sugar_of ctxt s of SOME (fp_sugar as {fp = Least_FP, fp_co_induct_sugar = SOME _, ...}) => fp_sugar - | _ => not_datatype s); + | _ => not_datatype_name s); val fpTs0 as Type (_, var_As) :: _ = map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0)))); diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Dec 30 15:40:35 2016 +0100 @@ -95,11 +95,6 @@ exception OLD_PRIMREC of unit; -fun malformed_eqn_lhs_rhs ctxt eqn = - error_at ctxt [eqn] "Malformed equation (expected \"lhs = rhs\")"; -fun malformed_eqn_head ctxt eqn = - error_at ctxt [eqn] "Malformed function equation (expected function name on left-hand side)"; - datatype rec_option = Plugins_Option of Proof.context -> Plugin_Name.filter | Nonexhaustive_Option | @@ -289,29 +284,25 @@ fun dissect_eqn ctxt fun_names eqn0 = let val eqn = drop_all eqn0 |> HOLogic.dest_Trueprop - handle TERM _ => malformed_eqn_lhs_rhs ctxt eqn0; + handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn0]; val (lhs, rhs) = HOLogic.dest_eq eqn - handle TERM _ => malformed_eqn_lhs_rhs ctxt eqn; + handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn]; val (fun_name, args) = strip_comb lhs - |>> (fn x => if is_Free x then fst (dest_Free x) else malformed_eqn_head ctxt eqn); + |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]); val (left_args, rest) = take_prefix is_Free args; val (nonfrees, right_args) = take_suffix is_Free rest; val num_nonfrees = length nonfrees; val _ = num_nonfrees = 1 orelse - error_at ctxt [eqn] (if num_nonfrees = 0 then "Constructor pattern missing in left-hand side" - else "More than one non-variable argument in left-hand side"); - val _ = member (op =) fun_names fun_name orelse raise malformed_eqn_head ctxt eqn; + (if num_nonfrees = 0 then missing_pattern ctxt [eqn] + else more_than_one_nonvar_in_lhs ctxt [eqn]); + val _ = member (op =) fun_names fun_name orelse raise ill_formed_equation_head ctxt [eqn]; val (ctr, ctr_args) = strip_comb (the_single nonfrees); val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse - error_at ctxt [eqn] "Partially applied constructor in pattern"; + partially_applied_ctr_in_pattern ctxt [eqn]; - val dups = duplicates (op =) (left_args @ ctr_args @ right_args) - val _ = null dups orelse - error_at ctxt [eqn] ("Duplicate variable \"" ^ Syntax.string_of_term ctxt (hd dups) ^ - "\" in left-hand side"); - val _ = forall is_Free ctr_args orelse - error_at ctxt [eqn] "Nonprimitive pattern in left-hand side"; + val _ = check_duplicate_variables_in_lhs ctxt [eqn] (left_args @ ctr_args @ right_args) + val _ = forall is_Free ctr_args orelse nonprimitive_pattern_in_lhs ctxt [eqn]; val _ = let val bads = @@ -323,8 +314,7 @@ I | _ => I) rhs []; in - null bads orelse - error_at ctxt [eqn] ("Extra variable " ^ quote (Syntax.string_of_term ctxt (hd bads))) + null bads orelse extra_variable_in_rhs ctxt [eqn] (hd bads) end; in {fun_name = fun_name, @@ -361,9 +351,7 @@ (case try (get_ctr_pos o fst o dest_Free) g of SOME ~1 => subst_comb t | SOME ctr_pos => - (length g_args >= ctr_pos orelse - error ("Too few arguments in recursive call " ^ - quote (Syntax.string_of_term ctxt t)); + (length g_args >= ctr_pos orelse too_few_args_in_rec_call ctxt [] t; (case AList.lookup (op =) mutual_calls y of SOME y' => list_comb (y', map (subst bound_Ts) g_args) | NONE => subst_comb t)) @@ -374,11 +362,8 @@ | subst _ t = t fun subst' t = - if has_call t then - error ("Recursive call not directly applied to constructor argument in " ^ - quote (Syntax.string_of_term ctxt t)) - else - try_nested_rec [] (head_of t) t |> the_default t; + if has_call t then rec_call_not_apply_to_ctr_arg ctxt [] t + else try_nested_rec [] (head_of t) t |> the_default t; in subst' o subst [] end; @@ -437,20 +422,20 @@ let val zs = replicate (length xs) z; val (b, c) = finds (fn ((x, _), y) => #ctr x = #ctr y) (xs ~~ zs) ys; - val _ = null c orelse error_at ctxt (map #rhs_term c) "Excess equation(s)"; + val _ = null c orelse excess_equations ctxt (map #rhs_term c); in b end) (map #ctr_specs (take n_funs rec_specs) ~~ funs_data ~~ nonexhaustives); val (_ : unit list) = ctr_spec_eqn_data_list' |> map (fn (({ctr, ...}, nonexhaustive), x) => if length x > 1 then - error_at ctxt (map #user_eqn x) "Multiple equations for constructor" + multiple_equations_for_ctr ctxt (map #user_eqn x) else if length x = 1 orelse nonexhaustive orelse not (Context_Position.is_visible ctxt) then () else - warning ("No equation for constructor " ^ Syntax.string_of_term ctxt ctr)); + no_equation_for_ctr_warning ctxt [] ctr); val ctr_spec_eqn_data_list = map (apfst fst) ctr_spec_eqn_data_list' @ - (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair [])); + (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair [])); val recs = take n_funs rec_specs |> map #recx; val rec_args = ctr_spec_eqn_data_list @@ -458,7 +443,7 @@ |> map (uncurry (build_rec_arg ctxt funs_data has_call) o apsnd (try the_single)); val ctr_poss = map (fn x => if length (distinct (op = o apply2 (length o #left_args)) x) <> 1 then - error ("Inconstant constructor pattern position for function " ^ quote (#fun_name (hd x))) + inconstant_pattern_pos_for_fun ctxt [] (#fun_name (hd x)) else hd x |> #left_args |> length) funs_data; in @@ -519,7 +504,7 @@ |> partition_eq (op = o apply2 #fun_name) |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst |> map (fn (x, y) => the_single y - handle List.Empty => error ("Missing equations for function " ^ quote x)); + handle List.Empty => missing_equations_for_fun x); val frees = map (fst #>> Binding.name_of #> Free) fixes; val has_call = exists_subterm (member (op =) frees); @@ -534,9 +519,7 @@ | is_only_old_datatype _ = false; val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else (); - val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of - [] => () - | (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort")); + val _ = List.app (uncurry (check_top_sort lthy0)) (bs ~~ res_Ts); val ((n2m, rec_specs, _, common_induct, inducts, induct_attrs, Ts), lthy) = rec_specs_of bs arg_Ts res_Ts frees callssss lthy0; @@ -544,10 +527,9 @@ val actual_nn = length funs_data; val ctrs = maps (map #ctr o #ctr_specs) rec_specs; - val _ = - map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse - error_at lthy0 [user_eqn] ("Argument " ^ quote (Syntax.string_of_term lthy ctr) ^ - " is not a constructor in left-hand side")) eqns_data; + val _ = List.app (fn {ctr, user_eqn, ...} => + ignore (member (op =) ctrs ctr orelse not_constructor_in_pattern lthy0 [user_eqn] ctr)) + eqns_data; val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call; @@ -608,6 +590,8 @@ fun primrec_simple0 int plugins nonexhaustive transfer fixes ts lthy = let + val _ = check_duplicate_const_names (map (fst o fst) fixes); + val actual_nn = length fixes; val nonexhaustives = replicate actual_nn nonexhaustive; @@ -634,9 +618,6 @@ fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy = let - val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes); - val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); - val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |> the_default Plugin_Name.default_filter; val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts; diff -r 08c2d80428ff -r 7596b0736ab9 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Dec 29 22:10:29 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Dec 30 15:40:35 2016 +0100 @@ -74,16 +74,9 @@ exception NO_MAP of term; -fun ill_formed_rec_call ctxt t = - error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); -fun invalid_map ctxt t = - error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); -fun unexpected_rec_call ctxt eqns t = - error_at ctxt eqns ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); - fun massage_nested_rec_call ctxt has_call massage_fun massage_nonfun bound_Ts y y' t0 = let - fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else (); + fun check_no_call t = if has_call t then unexpected_rec_call_in ctxt [t0] t else (); val typof = curry fastype_of1 bound_Ts; val massage_no_call = build_map ctxt [] [] massage_nonfun; @@ -133,11 +126,11 @@ if has_call t then if t2 = y then massage_map yU yT (elim_y t1) $ y' - handle NO_MAP t' => invalid_map ctxt t' + handle NO_MAP t' => invalid_map ctxt [t0] t' else let val (g, xs) = Term.strip_comb t2 in if g = y then - if exists has_call xs then unexpected_rec_call ctxt [t0] t2 + if exists has_call xs then unexpected_rec_call_in ctxt [t0] t2 else Term.list_comb (massage_outer_call (mk_compN (length xs) bound_Ts (t1, y)), xs) else ill_formed_rec_call ctxt t @@ -153,8 +146,8 @@ let val _ = (case try HOLogic.dest_prodT U of - SOME (U1, _) => U1 = T orelse invalid_map ctxt t - | NONE => invalid_map ctxt t); + SOME (U1, _) => U1 = T orelse invalid_map ctxt [] t + | NONE => invalid_map ctxt [] t); fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const U) | subst d (Abs (v, T, b)) = @@ -171,8 +164,7 @@ d = try (fn Bound n => n) (nth vs ctr_pos) then Term.list_comb (snd_const U $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) else - error ("Recursive call not directly applied to constructor argument in " ^ - quote (Syntax.string_of_term ctxt t)) + rec_call_not_apply_to_ctr_arg ctxt [] t else Term.list_comb (u, map (subst (if d = SOME ~1 then NONE else d)) vs) end;