--- 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;
--- 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 =
--- 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 [];
--- 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) =
--- 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;
--- 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))));
--- 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;
--- 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;