# HG changeset patch # User blanchet # Date 1425553054 -3600 # Node ID 43f0c669302da2de43065f7857eb78655036a9b6 # Parent 304ee0a475d193f3d68ff14192fbabe3111bf116 reworked primcorec error messages diff -r 304ee0a475d1 -r 43f0c669302d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 05 11:57:34 2015 +0100 @@ -84,11 +84,18 @@ val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; -exception PRIMCOREC of string * term list; +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 primcorec_error str = raise PRIMCOREC (str, []); -fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]); -fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns); +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 unexpected_corec_call ctxt eqns t = + error_at ctxt eqns ("Unexpected corecursive call " ^ quote (Syntax.string_of_term ctxt t)); datatype corec_option = Plugins_Option of Proof.context -> Plugin_Name.filter | @@ -133,15 +140,6 @@ exception NO_MAP of term; -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 ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); -fun unexpected_corec_call ctxt t = - error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); - fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; @@ -227,7 +225,7 @@ let val thy = Proof_Context.theory_of ctxt; - fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); + fun check_no_call t = if has_call t then unexpected_corec_call ctxt [] t else (); fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t) @@ -284,7 +282,7 @@ fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t = let - fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); + fun check_no_call t = if has_call t then unexpected_corec_call ctxt [] t else (); val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd); @@ -581,20 +579,23 @@ Disc of coeqn_data_disc | Sel of coeqn_data_sel; -fun check_extra_variables lthy vars names eqn = +fun is_free_in frees (Free (v, _)) = member (op =) frees v + | is_free_in _ _ = false; + +fun check_extra_variables ctxt vars names eqn = let val b = fold_aterms (fn x as Free (v, _) => if (not (member (op =) vars x) andalso not (member (op =) names v) andalso v <> Name.uu_ andalso - not (Variable.is_fixed lthy v)) then cons x else I | _ => I) eqn [] + not (Variable.is_fixed ctxt v)) then cons x else I | _ => I) eqn [] in - null b orelse - primcorec_error_eqn ("extra variable(s) in equation: " ^ - commas (map (Syntax.string_of_term lthy) b)) eqn + null b orelse error_at ctxt [eqn] + ("Extra variable " ^ quote (Syntax.string_of_term ctxt (hd b))) end; -fun dissect_coeqn_disc lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) - eqn_pos ctr_rhs_opt code_rhs_opt prems' concl matchedsss = +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 + concl matchedsss = let fun find_subterm p = let (* FIXME \? *) @@ -605,25 +606,25 @@ val applied_fun = concl |> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) |> the - handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl; + handle Option.Option => error_at ctxt [concl] "Ill-formed discriminator formula"; val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free; - val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args; - val _ = null fixeds orelse - primcorec_error_eqns "function argument(s) are fixed in context" fixeds; + val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args; + val _ = null fixeds orelse error_at ctxt fixeds "Function argument(s) are fixed in context"; - val bad = - filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v | _ => false)) prems'; - val _ = null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad; + 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 _ = forall is_Free fun_args orelse - primcorec_error_eqn ("non-variable function argument \"" ^ - Syntax.string_of_term lthy (find_first (not o is_Free) fun_args |> the) ^ - "\" (pattern matching is not supported by primcorec(ursive))") applied_fun + error_at ctxt [applied_fun] ("Non-variable function argument \"" ^ + Syntax.string_of_term ctxt (find_first (not o is_Free) fun_args |> the) ^ + "\" (pattern matching is not supported by primcorec(ursive))") - val _ = let val d = duplicates (op =) fun_args in null d orelse - primcorec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ "\"") - applied_fun end; + val dups = duplicates (op =) fun_args; + val _ = + null dups orelse + error_at ctxt [applied_fun] + ("Duplicate variable " ^ quote (Syntax.string_of_term ctxt (hd dups))); val (sequential, basic_ctr_specs) = the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name); @@ -632,25 +633,25 @@ val ctrs = map #ctr basic_ctr_specs; val not_disc = head_of concl = @{term Not}; val _ = not_disc andalso length ctrs <> 2 andalso - primcorec_error_eqn "negated discriminator for a type with \ 2 constructors" concl; + error_at ctxt [concl] "Negated discriminator for a type with \ 2 constructors"; val disc' = find_subterm (member (op =) discs o head_of) concl; val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd) |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in if n >= 0 then SOME n else NONE end | _ => NONE); - val _ = if is_some disc' andalso perhaps (try HOLogic.dest_not) concl <> the disc' - then primcorec_error_eqn "malformed discriminator formula" concl else (); + val _ = is_none disc' orelse perhaps (try HOLogic.dest_not) concl = the disc' orelse + error_at ctxt [concl] "Ill-formed discriminator formula"; + val _ = is_some disc' orelse is_some eq_ctr0 orelse + error_at ctxt [concl] "No discriminator in equation"; - val _ = is_some disc' orelse is_some eq_ctr0 orelse - primcorec_error_eqn "no discriminator in equation" concl; val ctr_no' = if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs; val ctr_no = if not_disc then 1 - ctr_no' else ctr_no'; val {ctr, disc, ...} = nth basic_ctr_specs ctr_no; - val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; + val catch_all = (try (fst o dest_Free o the_single) prems0 = SOME Name.uu_); val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; - val prems = map (abstract (List.rev fun_args)) prems'; + val prems = map (abstract (List.rev fun_args)) prems0; val actual_prems = (if catch_all orelse sequential then maps s_not_conj matchedss else []) @ (if catch_all then [] else prems); @@ -663,7 +664,7 @@ |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args) |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies; - val _ = check_extra_variables lthy fun_args fun_names user_eqn; + val _ = check_extra_variables ctxt fun_args fun_names user_eqn; in (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt, @@ -671,108 +672,109 @@ matchedsss') end; -fun dissect_coeqn_sel lthy fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos +fun dissect_coeqn_sel ctxt fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn = let val (lhs, rhs) = HOLogic.dest_eq eqn - handle TERM _ => - primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn; + handle TERM _ => error_at ctxt [eqn] "Ill-formed equation (expected \"lhs = rhs\")"; val sel = head_of lhs; val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free - handle TERM _ => - primcorec_error_eqn "malformed selector argument in left-hand side" eqn; + handle TERM _ => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side"; - val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in - null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds - end; + val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args; + val _ = + null fixeds orelse error ("Function argument " ^ + quote (Syntax.string_of_term ctxt (hd fixeds)) ^ " is fixed in context"); val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name) - handle Option.Option => - primcorec_error_eqn "malformed selector argument in left-hand side" eqn; + handle Option.Option => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side"; val {ctr, ...} = (case of_spec_opt of SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs) | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single - handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn); + handle List.Empty => error_at ctxt [eqn] "Ambiguous selector (without \"of\")"); val user_eqn = drop_all eqn0; - val _ = check_extra_variables lthy fun_args fun_names user_eqn; + val _ = check_extra_variables ctxt fun_args fun_names user_eqn; in Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel, rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn} end; -fun dissect_coeqn_ctr lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) +fun dissect_coeqn_ctr ctxt fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos eqn0 code_rhs_opt prems concl matchedsss = let val (lhs, rhs) = HOLogic.dest_eq concl; val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; - val _ = check_extra_variables lthy fun_args fun_names (drop_all eqn0); + val _ = check_extra_variables ctxt fun_args fun_names (drop_all eqn0); 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 => primcorec_error_eqn "not a constructor" ctr; + handle Option.Option => error_at ctxt [ctr] "Not a constructor"; val disc_concl = betapply (disc, lhs); val (eqn_data_disc_opt, matchedsss') = if null (tl basic_ctr_specs) andalso not (null sels) then (NONE, matchedsss) else - apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos + apfst SOME (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss); val sel_concls = sels ~~ ctr_args |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) handle ListPair.UnequalLengths => - primcorec_error_eqn "partially applied constructor in right-hand side" rhs; + error_at ctxt [rhs] "Partially applied constructor in right-hand side"; val eqns_data_sel = - map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos + map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls; in (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss') end; -fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = +fun dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss = let - val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []); + val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs ctxt has_call []); val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; - val _ = check_extra_variables lthy fun_args fun_names concl; + val _ = check_extra_variables ctxt fun_args fun_names concl; val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); - val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ => + 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 primcorec_error_eqn "not a constructor" ctr) [] rhs' [] + else error ("Not a constructor: " ^ quote (Syntax.string_of_term ctxt ctr))) [] rhs' [] |> AList.group (op =); val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs); val ctr_concls = cond_ctrs |> map (fn (ctr, _) => binder_types (fastype_of ctr) - |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args => + |> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args => if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs') |> curry Term.list_comb ctr |> 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 sequentials = replicate (length fun_names) false; in - @{fold_map 2} (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 + @{fold_map 2} (dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 (SOME (abstract (List.rev fun_args) rhs))) ctr_premss ctr_concls matchedsss end; -fun dissect_coeqn lthy has_call fun_names sequentials +fun dissect_coeqn ctxt has_call fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss = let val eqn = drop_all eqn0 - handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0; + handle TERM _ => error_at ctxt [eqn0] "Ill-formed function equation"; val (prems, concl) = Logic.strip_horn eqn |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop - handle TERM _ => primcorec_error_eqn "malformed function equation" eqn; + handle TERM _ => error_at ctxt [eqn] "Ill-formed function equation"; val head = concl |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) @@ -788,29 +790,28 @@ (is_some rhs_opt andalso member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then - dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl + dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl matchedsss |>> single else if member (op =) sels head then - (null prems orelse primcorec_error_eqn "premise(s) in selector formula" eqn; - ([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt + (null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula"; + ([dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl], matchedsss)) - else if is_some rhs_opt andalso - is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then + else if is_some rhs_opt andalso is_Free head andalso is_free_in fun_names head then if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then - dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0 + dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0 (if null prems then SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0)))) else NONE) prems concl matchedsss else if null prems then - dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss + dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss |>> flat else - primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn + error_at ctxt [eqn] "Cannot mix constructor and code views" else - primcorec_error_eqn "malformed function equation" eqn + error_at ctxt [eqn] "Ill-formed function equation" end; fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) @@ -829,7 +830,7 @@ |> the_default undef_const |> K; -fun build_corec_args_mutual_call lthy has_call (sel_eqns : coeqn_data_sel list) sel = +fun build_corec_args_mutual_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = (case find_first (curry (op =) sel o #sel) sel_eqns of NONE => (I, I, I) | SOME {fun_args, rhs_term, ... } => @@ -839,13 +840,13 @@ fun rewrite_end _ t = if has_call t then undef_const else t; fun rewrite_cont bound_Ts t = if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const; - fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term + fun massage f _ = massage_let_if_case ctxt has_call f bound_Ts rhs_term |> abs_tuple_balanced fun_args; in (massage rewrite_stop, massage rewrite_end, massage rewrite_cont) end); -fun build_corec_arg_nested_call lthy has_call (sel_eqns : coeqn_data_sel list) sel = +fun build_corec_arg_nested_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel = (case find_first (curry (op =) sel o #sel) sel_eqns of NONE => I | SOME {fun_args, rhs_term, ...} => @@ -874,13 +875,13 @@ fun build t = rhs_term - |> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t)) + |> massage_nested_corec_call ctxt has_call massage bound_Ts (range_type (fastype_of t)) |> abs_tuple_balanced fun_args; in build end); -fun build_corec_args_sel lthy has_call (all_sel_eqns : coeqn_data_sel list) +fun build_corec_args_sel ctxt has_call (all_sel_eqns : coeqn_data_sel list) (ctr_spec : corec_ctr_spec) = (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of [] => I @@ -894,13 +895,13 @@ I #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls' #> fold (fn (sel, (q, g, h)) => - let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in + let val (fq, fg, fh) = build_corec_args_mutual_call ctxt has_call sel_eqns sel in nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls' #> fold (fn (sel, n) => nth_map n - (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls' + (build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls' end); -fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list) +fun build_codefs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list) (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = let val corecs = map #corec corec_specs; @@ -911,7 +912,7 @@ if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False}) else Const (@{const_name undefined}, T)) |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss - |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; + |> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss; fun currys [] t = t | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) @@ -931,7 +932,7 @@ map (Term.list_comb o rpair corec_args) corecs |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss |> map2 currys arg_Tss - |> Syntax.check_terms lthy + |> Syntax.check_terms ctxt |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) bs mxs |> rpair excludess' @@ -992,7 +993,7 @@ val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of [] => () - | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort")); + | (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort")); val actual_nn = length bs; @@ -1005,7 +1006,7 @@ val fun_names = map Binding.name_of bs; val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; val frees = map (fst #>> Binding.name_of #> Free) fixes; - val has_call = exists_subterm (member (op =) frees); + val has_call = Term.exists_subterm (member (op =) frees); val eqns_data = @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs)) of_specs_opt [] @@ -1017,8 +1018,7 @@ |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data |> not oo member (op =)); in - null missing - orelse primcorec_error_eqns ("missing equations for function(s): " ^ commas missing) [] + null missing orelse error ("Missing equations for " ^ commas missing) end; val callssss = @@ -1044,13 +1044,15 @@ val _ = disc_eqnss' |> map (fn x => let val d = duplicates (op = o apply2 #ctr_no) x in null d orelse - (if forall (is_some o #ctr_rhs_opt) x then - primcorec_error_eqns "multiple equations for constructor(s)" - (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d - |> map (the o #ctr_rhs_opt)) - else - primcorec_error_eqns "excess discriminator formula in definition" - (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) + (if forall (is_some o #ctr_rhs_opt) x then + error_at lthy + (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d + |> map (the o #ctr_rhs_opt)) + "Multiple equations for same constructor" + else + error_at lthy + (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) + "Excess discriminator formula in definition") end); val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data @@ -1473,14 +1475,7 @@ val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); in add_primcorec_ursive auto opts fixes specs of_specs_opt lthy - handle ERROR str => primcorec_error str - end - handle PRIMCOREC (str, eqns) => - if null eqns then - error ("primcorec error:\n " ^ str) - else - error ("primcorec error:\n " ^ str ^ "\nin\n " ^ - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); + end; val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) => lthy