--- 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 \<exists>? *)
@@ -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 \<noteq> 2 constructors" concl;
+ error_at ctxt [concl] "Negated discriminator for a type with \<noteq> 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
--- 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;