# HG changeset patch # User paulson # Date 1425577144 0 # Node ID 452458cf8506b408ffaee54b83c1c643c0fa3b47 # Parent 7103019278f03c7fbf6ec9c1dd786e7c7d4dfb90# Parent 7ea413656b64f07ae136bb4a7cf70f28406b4e92 Merge diff -r 7103019278f0 -r 452458cf8506 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 05 17:30:29 2015 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 05 17:39:04 2015 +0000 @@ -8,6 +8,7 @@ signature BNF_FP_REC_SUGAR_UTIL = sig + val error_at: Proof.context -> term list -> string -> 'a datatype fp_kind = Least_FP | Greatest_FP @@ -57,6 +58,10 @@ 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))); + datatype fp_kind = Least_FP | Greatest_FP; fun case_fp Least_FP l _ = l diff -r 7103019278f0 -r 452458cf8506 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 05 17:30:29 2015 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 05 17:39:04 2015 +0000 @@ -84,11 +84,20 @@ val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; -exception PRIMCOREC of string * term list; - -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 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 use_primcorecursive () = + error "\"auto\" failed (try \"primcorecursive\" instead of \"primcorec\")"; datatype corec_option = Plugins_Option of Proof.context -> Plugin_Name.filter | @@ -133,15 +142,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}; @@ -223,11 +223,11 @@ SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s' | _ => NONE); -fun massage_let_if_case ctxt has_call massage_leaf = +fun massage_let_if_case ctxt has_call massage_leaf bound_Ts t0 = 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 [t0] 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) @@ -240,9 +240,11 @@ (case Term.strip_comb t of (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t) | (Const (@{const_name If}, _), obj :: (branches as [_, _])) => - let val branches' = map (massage_rec bound_Ts) branches in - Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches') - end + (case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of + (dummy_branch' :: _, []) => dummy_branch' + | (_, [branch']) => branch' + | (_, branches') => + Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')) | (c as Const (@{const_name case_prod}, _), arg :: args) => massage_rec bound_Ts (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args))) @@ -277,24 +279,29 @@ | _ => massage_leaf bound_Ts t) end; in - massage_rec + massage_rec bound_Ts t0 + |> Term.map_aterms (fn t => + if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t) end; fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T; -fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t = +fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t0 = 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 [t0] t else (); val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd); - fun massage_mutual_call bound_Ts U T t = - if has_call t then - (case try dest_sumT U of - SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t - | NONE => invalid_map ctxt t) - else - build_map_Inl (T, U) $ t; + fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2])) + (Type (@{type_name fun}, [T1, T2])) t = + Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0)) + | massage_mutual_call bound_Ts U T t = + if has_call t then + (case try dest_sumT U of + SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t + | NONE => invalid_map ctxt t) + else + build_map_Inl (T, U) $ t; fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = (case try (dest_map ctxt s) t of @@ -321,8 +328,8 @@ mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2) | _ => let - val var = Var ((Name.uu, Term.maxidx_of_term t + 1), - domain_type (fastype_of1 (bound_Ts, t))); + val j = Term.maxidx_of_term t + 1; + val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t))); in Term.lambda var (Term.incr_boundvars 1 (massage_call bound_Ts U T (betapply (t, var)))) end) @@ -339,7 +346,8 @@ val f'_T = typof f'; val arg_Ts = map typof args; in - Term.list_comb (f', @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) + Term.list_comb (f', + @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) end | NONE => (case t of @@ -363,9 +371,9 @@ else build_map_Inl (T, U) $ t) bound_Ts; - val T = fastype_of1 (bound_Ts, t); + val T = fastype_of1 (bound_Ts, t0); in - if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t + if has_call t0 then massage_call bound_Ts U T t0 else build_map_Inl (T, U) $ t0 end; fun expand_to_ctr_term ctxt s Ts t = @@ -523,8 +531,8 @@ fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = - {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs, - sel_defs = sel_defs, + {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, + exhaust_discs = exhaust_discs, sel_defs = sel_defs, fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs, fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, @@ -577,24 +585,44 @@ eqn_pos: int, user_eqn: term}; +fun ctr_sel_of ({ctr, sel, ...} : coeqn_data_sel) = (ctr, sel); + datatype coeqn_data = Disc of coeqn_data_disc | Sel of coeqn_data_sel; -fun check_extra_variables lthy 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 [] - in - null b orelse - primcorec_error_eqn ("extra variable(s) in equation: " ^ - commas (map (Syntax.string_of_term lthy) b)) eqn +fun is_free_in frees (Free (v, _)) = member (op =) frees v + | is_free_in _ _ = false; + +fun add_extra_frees ctxt frees names = + fold_aterms (fn x as Free (v, _) => + (not (member (op =) frees x) andalso not (member (op =) names v) andalso + not (Variable.is_fixed ctxt v) andalso v <> Name.uu_) + ? cons x | _ => I); + +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) 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 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; + +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 +633,13 @@ 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 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 _ = check_fun_args ctxt concl fun_args; - 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 - - 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 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 (sequential, basic_ctr_specs) = the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name); @@ -632,25 +648,33 @@ 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); + |> (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_; + fun is_catch_all_prem (Free (s, _)) = s = Name.uu_ + | is_catch_all_prem _ = false; + + val catch_all = + (case prems0 of + [prem] => is_catch_all_prem prem + | _ => + if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises" + else false); 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 +687,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_frees 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,114 +695,118 @@ 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; - - 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; + handle TERM _ => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side"; + val _ = check_fun_args ctxt eqn fun_args; 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_frees 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_fun_args ctxt concl fun_args; + val _ = check_extra_frees 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; + handle ListPair.UnequalLengths => + 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_fun_args ctxt concl fun_args; + val _ = check_extra_frees 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 => - if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs') + |> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args => + if ctr' = ctr then nth args n else Term.dummy_pattern 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 formula"; 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 equation"; val head = concl |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) |> head_of; - val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (snd o HOLogic.dest_eq); + val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd); + + 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"; val discs = maps (map #disc) basic_ctr_specss; val sels = maps (maps #sels) basic_ctr_specss; @@ -788,29 +816,32 @@ (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 - matchedsss - |>> single + (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 - (if null prems then - SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0)))) - else - NONE) - prems concl matchedsss + (check_num_args (); + 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 - |>> flat + (check_num_args (); + 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 if is_some rhs_opt then + error_at ctxt [eqn] ("Ill-formed equation head: " ^ quote (Syntax.string_of_term ctxt head)) else - primcorec_error_eqn "malformed function equation" eqn + error_at ctxt [eqn] "Expected equation or discriminator formula" end; fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list) @@ -829,7 +860,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 +870,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 +905,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 +925,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 +942,12 @@ 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; + + 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)); fun currys [] t = t | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) @@ -931,7 +967,8 @@ 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 + |> (fn ts => Syntax.check_terms ctxt ts + handle ERROR _ => nonprimitive_corec ctxt []) |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) bs mxs |> rpair excludess' @@ -939,17 +976,21 @@ fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec) (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = - let val num_disc_eqns = length disc_eqns in - if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs - 1 then - disc_eqns + let + val fun_name = Binding.name_of fun_binding; + val num_disc_eqns = length disc_eqns; + val num_ctrs = length ctr_specs; + in + if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> num_ctrs - 1 then + (num_disc_eqns > 0 orelse error ("Missing discriminator formula for " ^ quote fun_name); + disc_eqns) else let - val n = 0 upto length ctr_specs + val ctr_no = 0 upto length ctr_specs |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns)); - val {ctr, disc, ...} = nth ctr_specs n; + val {ctr, disc, ...} = nth ctr_specs ctr_no; val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; - val fun_name = Binding.name_of fun_binding; val fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))); val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; @@ -959,11 +1000,11 @@ val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *) val extra_disc_eqn = - {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = n, + {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no, disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const}; in - chop n disc_eqns ||> cons extra_disc_eqn |> (op @) + chop ctr_no disc_eqns ||> cons extra_disc_eqn |> op @ end end; @@ -992,7 +1033,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 +1046,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 +1058,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 = @@ -1030,27 +1070,24 @@ |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} => (ctr, map (K []) sels))) basic_ctr_specss); - val (corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms, + val (corec_specs0, _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms, (coinduct_attrs, common_coinduct_attrs), n2m, lthy') = corec_specs_of bs arg_Ts res_Ts frees callssss lthy; - val corec_specs = take actual_nn corec_specs'; + val corec_specs = take actual_nn corec_specs0; val ctr_specss = map #ctr_specs corec_specs; - val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data + val disc_eqnss0 = map_filter (try (fn Disc x => x)) eqns_data |> partition_eq (op = o apply2 #fun_name) |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd); - 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)) + val _ = disc_eqnss0 |> map (fn x => + let val dups = duplicates (op = o apply2 #ctr_no) x in + null dups orelse + error_at lthy + (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) dups + |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn)) + "Overspecified case(s)" end); val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data @@ -1058,9 +1095,18 @@ |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> map (flat o snd); + val _ = sel_eqnss |> map (fn x => + let val dups = duplicates (op = o apply2 ctr_sel_of) x in + null dups orelse + error_at lthy + (maps (fn t => filter (curry (op =) (ctr_sel_of t) o ctr_sel_of) x) dups + |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn)) + "Overspecified case(s)" + end); + val arg_Tss = map (binder_types o snd o fst) fixes; val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss - disc_eqnss'; + disc_eqnss0; val (defs, excludess') = build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss; @@ -1075,9 +1121,10 @@ tac_opt; val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) => - (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation) - (exclude_tac tac_opt sequential j), goal)))) - tac_opts sequentials excludess'; + (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation) + (exclude_tac tac_opt sequential j), goal)))) + tac_opts sequentials excludess' + handle ERROR _ => use_primcorecursive (); val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess''; val (goal_idxss, exclude_goalss) = excludess'' @@ -1108,9 +1155,10 @@ val (_, _, arg_exhaust_discs, _, _) = case_thms_of_term lthy (the_default Term.dummy code_rhs_opt); in - [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => + [Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} => mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs)) |> Thm.close_derivation] + handle ERROR _ => use_primcorecursive () end | false => (case tac_opt of @@ -1468,19 +1516,15 @@ fun add_primcorec_ursive_cmd 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) = 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 @@ -1489,10 +1533,8 @@ |> Seq.hd) ooo add_primcorec_ursive_cmd false; val add_primcorec_cmd = (fn (goalss, after_qed, lthy) => - lthy - |> after_qed (map (fn [] => [] - | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"") - goalss)) ooo add_primcorec_ursive_cmd true; + lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo + add_primcorec_ursive_cmd true; val corec_option_parser = Parse.group (K "option") (Plugin_Name.parse_filter >> Plugins_Option diff -r 7103019278f0 -r 452458cf8506 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Mar 05 17:30:29 2015 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Mar 05 17:39:04 2015 +0000 @@ -119,7 +119,7 @@ REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI) else rtac FalseE THEN' - (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE' + (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE' cut_tac fun_disc') THEN' dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac) fun_discss) THEN' @@ -141,7 +141,8 @@ sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ mapsx @ map_ident0s @ map_comps))) ORELSE' fo_rtac @{thm cong} ctxt ORELSE' - rtac @{thm ext})); + rtac @{thm ext} ORELSE' + mk_primcorec_assumption_tac ctxt [])); fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' diff -r 7103019278f0 -r 452458cf8506 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Mar 05 17:30:29 2015 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Mar 05 17:39:04 2015 +0000 @@ -49,8 +49,6 @@ rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term -> term -> term -> term) option}; - exception PRIMREC of string * term list; - val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory val default_basic_lfp_sugars_of: binding list -> typ list -> term list -> (term * term list list) list list -> local_theory -> @@ -92,7 +90,11 @@ val nitpicksimp_simp_attrs = nitpicksimp_attrs @ simp_attrs; exception OLD_PRIMREC of unit; -exception PRIMREC of string * term list; + +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 | @@ -276,37 +278,35 @@ user_eqn: term }; -fun dissect_eqn ctxt fun_names eqn' = +fun dissect_eqn ctxt fun_names eqn0 = let - val eqn = drop_all eqn' |> HOLogic.dest_Trueprop - handle TERM _ => - raise PRIMREC ("malformed function equation (expected \"lhs = rhs\")", [eqn']); + val eqn = drop_all eqn0 |> HOLogic.dest_Trueprop + handle TERM _ => malformed_eqn_lhs_rhs ctxt eqn0; val (lhs, rhs) = HOLogic.dest_eq eqn - handle TERM _ => - raise PRIMREC ("malformed function equation (expected \"lhs = rhs\")", [eqn']); + handle TERM _ => malformed_eqn_lhs_rhs ctxt eqn; val (fun_name, args) = strip_comb lhs - |>> (fn x => if is_Free x then fst (dest_Free x) - else raise PRIMREC ("malformed function equation (does not start with free)", [eqn])); + |>> (fn x => if is_Free x then fst (dest_Free x) else malformed_eqn_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 if num_nonfrees = 0 then - raise PRIMREC ("constructor pattern missing in left-hand side", [eqn]) else - raise PRIMREC ("more than one non-variable argument in left-hand side", [eqn]); - val _ = member (op =) fun_names fun_name orelse - raise PRIMREC ("malformed function equation (does not start with function name)", [eqn]); + 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; val (ctr, ctr_args) = strip_comb (the_single nonfrees); val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse - raise PRIMREC ("partially applied constructor in pattern", [eqn]); - val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse - raise PRIMREC ("duplicate variable \"" ^ Syntax.string_of_term ctxt (hd d) ^ - "\" in left-hand side", [eqn]) end; + error_at ctxt [eqn] "Partially applied constructor in pattern"; + + 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 - raise PRIMREC ("non-primitive pattern in left-hand side", [eqn]); + error_at ctxt [eqn] "Nonprimitive pattern in left-hand side"; val _ = let - val b = + val bads = fold_aterms (fn x as Free (v, _) => if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso not (member (op =) fun_names v) andalso not (Variable.is_fixed ctxt v)) then @@ -315,9 +315,8 @@ I | _ => I) rhs []; in - null b orelse - raise PRIMREC ("extra variable(s) in right-hand side: " ^ - commas (map (Syntax.string_of_term ctxt) b), [eqn]) + null bads orelse + error_at ctxt [eqn] ("Extra variable " ^ quote (Syntax.string_of_term ctxt (hd bads))) end; in {fun_name = fun_name, @@ -328,7 +327,7 @@ right_args = right_args, res_type = map fastype_of (left_args @ right_args) ---> fastype_of rhs, rhs_term = rhs, - user_eqn = eqn'} + user_eqn = eqn0} end; fun subst_rec_calls ctxt get_ctr_pos has_call ctr_args mutual_calls nested_calls = @@ -355,7 +354,8 @@ SOME ~1 => subst_comb t | SOME ctr_pos => (length g_args >= ctr_pos orelse - raise PRIMREC ("too few arguments in recursive call", [t]); + error ("Too few arguments in recursive call " ^ + quote (Syntax.string_of_term 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)) @@ -367,7 +367,8 @@ fun subst' t = if has_call t then - raise PRIMREC ("recursive call not directly applied to constructor argument", [t]) + 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; in @@ -426,16 +427,18 @@ val ctr_spec_eqn_data_list' = maps (fn ((xs, ys), z) => let - val zs = replicate (length xs) z - val (b, c) = finds (fn ((x,_), y) => #ctr x = #ctr y) (xs ~~ zs) ys - val (_ : bool ) = (fn x => null x orelse - raise PRIMREC ("excess equations in definition", map #rhs_term x)) c + 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)"; 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 raise PRIMREC ("multiple equations for constructor", 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)); + if length x > 1 then + error_at ctxt (map #user_eqn x) "Multiple equations for constructor" + 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)); val ctr_spec_eqn_data_list = map (apfst fst) ctr_spec_eqn_data_list' @ @@ -447,8 +450,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 - raise PRIMREC ("inconstant constructor pattern position for function " ^ - quote (#fun_name (hd x)), []) + error ("Inconstant constructor pattern position for function " ^ quote (#fun_name (hd x))) else hd x |> #left_args |> length) funs_data; in @@ -505,7 +507,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 => raise PRIMREC ("missing equations for function " ^ quote x, [])); + handle List.Empty => error ("Missing equations for function " ^ quote x)); val frees = map (fst #>> Binding.name_of #> Free) fixes; val has_call = exists_subterm (member (op =) frees); @@ -522,7 +524,7 @@ 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, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", [])); + | (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort")); val ((n2m, rec_specs, _, common_induct, inducts, induct_attrs, Ts), lthy) = rec_specs_of bs arg_Ts res_Ts frees callssss lthy0; @@ -532,8 +534,8 @@ val ctrs = maps (map #ctr o #ctr_specs) rec_specs; val _ = map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse - raise PRIMREC ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^ - " is not a constructor in left-hand side", [user_eqn])) eqns_data; + error_at lthy0 [user_eqn] ("Argument " ^ quote (Syntax.string_of_term lthy ctr) ^ + " is not a constructor in left-hand side")) eqns_data; val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call; @@ -598,21 +600,14 @@ val transfers = replicate actual_nn transfer; val (((names, defs), prove), lthy') = - prepare_primrec plugins nonexhaustives transfers fixes ts lthy - handle ERROR str => raise PRIMREC (str, []); + prepare_primrec plugins nonexhaustives transfers fixes ts lthy; in lthy' |> fold_map Local_Theory.define defs |-> (fn defs => fn lthy => let val (thms, lthy) = prove lthy defs; in ((names, (map fst defs, thms)), lthy) end) - end - handle PRIMREC (str, eqns) => - if null eqns then - error ("primrec error:\n " ^ str) - else - error ("primrec error:\n " ^ str ^ "\nin\n " ^ - space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); + end; fun add_primrec_simple fixes ts lthy = add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy @@ -623,8 +618,8 @@ fun gen_primrec old_primrec prep_spec opts (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy = let - val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); - val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []); + val dups = duplicates (op =) (map (Binding.name_of o #1) 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; diff -r 7103019278f0 -r 452458cf8506 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Mar 05 17:30:29 2015 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Mar 05 17:39:04 2015 +0000 @@ -135,7 +135,7 @@ massage_call end; -fun rewrite_map_arg get_ctr_pos rec_type res_type = +fun rewrite_map_arg ctxt get_ctr_pos rec_type res_type = let val pT = HOLogic.mk_prodT (rec_type, res_type); @@ -154,7 +154,8 @@ d = try (fn Bound n => n) (nth vs ctr_pos) then Term.list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) else - raise PRIMREC ("recursive call not directly applied to constructor argument", [t]) + error ("Recursive call not directly applied to constructor argument in " ^ + quote (Syntax.string_of_term ctxt t)) else Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs) end @@ -163,7 +164,7 @@ end; fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = - massage_nested_rec_call ctxt has_call (rewrite_map_arg get_ctr_pos); + massage_nested_rec_call ctxt has_call (rewrite_map_arg ctxt get_ctr_pos); val _ = Theory.setup (register_lfp_rec_extension {nested_simps = nested_simps, is_new_datatype = is_new_datatype,