--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Aug 28 18:44:50 2013 +0200
@@ -14,8 +14,11 @@
type unfold_set
val empty_unfolds: unfold_set
+ exception BAD_DEAD of typ * typ
+
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
- ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
+ ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> typ ->
+ unfold_set * Proof.context ->
(BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
val default_comp_sort: (string * sort) list list -> (string * sort) list
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
@@ -645,10 +648,18 @@
((bnf', deads), lthy')
end;
-fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
- | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
- | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
+exception BAD_DEAD of typ * typ;
+
+fun bnf_of_typ _ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
+ | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+ | bnf_of_typ const_policy qualify' sort Xs (T as Type (C, Ts)) (unfold_set, lthy) =
let
+ fun check_bad_dead ((_, (deads, _)), _) =
+ let val Ds = fold Term.add_tfreesT deads [] in
+ (case Library.inter (op =) Ds Xs of [] => ()
+ | X :: _ => raise BAD_DEAD (TFree X, T))
+ end;
+
val tfrees = Term.add_tfreesT T [];
val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
in
@@ -679,11 +690,12 @@
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
apfst (apsnd split_list o split_list)
- (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
+ (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs)
(if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
in
compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
end)
+ |> tap check_bad_dead
end;
end;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 18:44:50 2013 +0200
@@ -97,6 +97,7 @@
open BNF_Util
open BNF_Ctr_Sugar
+open BNF_Comp
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
@@ -1103,12 +1104,14 @@
quote (Syntax.string_of_typ fake_lthy T)))
| eq_fpT_check _ _ = false;
- fun freeze_fp (T as Type (s, Us)) =
+ fun freeze_fp (T as Type (s, Ts)) =
(case find_index (eq_fpT_check T) fake_Ts of
- ~1 => Type (s, map freeze_fp Us)
+ ~1 => Type (s, map freeze_fp Ts)
| kk => nth Xs kk)
| freeze_fp T = T;
+ val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
+
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
@@ -1119,8 +1122,34 @@
xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
lthy)) =
- fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
- fake_Ts fp_eqs no_defs_lthy0;
+ fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
+ no_defs_lthy0
+ handle BAD_DEAD (X, X_backdrop) =>
+ (case X_backdrop of
+ Type (bad_tc, _) =>
+ let
+ val qsoty = quote o Syntax.string_of_typ fake_lthy;
+ val fake_T = qsoty (unfreeze_fp X);
+ val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
+ fun register_hint () =
+ "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^
+ quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
+ \it";
+ in
+ if is_some (bnf_of no_defs_lthy bad_tc) orelse
+ is_some (fp_sugar_of no_defs_lthy bad_tc) then
+ error ("Non-strictly-positive " ^ co_prefix fp ^ "recursive occurrence of type " ^
+ fake_T ^ " in type expression " ^ fake_T_backdrop)
+ else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+ bad_tc) then
+ error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+ " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^
+ fake_T_backdrop ^ register_hint ())
+ else
+ error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+ " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^
+ register_hint ())
+ end);
val time = time lthy;
val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 28 18:44:50 2013 +0200
@@ -575,12 +575,12 @@
let
val time = time lthy;
val timer = time (Timer.startRealTimer ());
- val (lhss, rhss) = split_list fp_eqs;
+ val (Xs, rhsXs) = split_list fp_eqs;
- (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
+ (* FIXME: because of "@ Xs", the output could contain type variables that are not in the
input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
fun fp_sort Ass =
- subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
+ subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
val common_name = mk_common_name (map Binding.name_of bs);
@@ -590,7 +590,7 @@
end;
val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
- (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss
+ (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
(empty_unfolds, lthy));
fun qualify i =
@@ -601,10 +601,6 @@
val resDs = fold (subtract (op =)) Ass resBs;
val Ds = fold (fold Term.add_tfreesT) deadss [];
- val _ = (case Library.inter (op =) Ds lhss of [] => ()
- | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
- \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
-
val timer = time (timer "Construction of BNFs");
val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =