# HG changeset patch # User blanchet # Date 1377708290 -7200 # Node ID 8b159677efb519846543b8c4da421926ad2f86de # Parent 67e122cedbba88b9d0bcb2f38c955b8799d9a309 better error message diff -r 67e122cedbba -r 8b159677efb5 src/HOL/BNF/Tools/bnf_comp.ML --- 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; diff -r 67e122cedbba -r 8b159677efb5 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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 ()); diff -r 67e122cedbba -r 8b159677efb5 src/HOL/BNF/Tools/bnf_fp_util.ML --- 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'))) =