Added exception Datatype_Empty.
authorberghofe
Tue Jun 08 19:23:53 2004 +0200 (2004-06-08)
changeset 148874938ce4ef295
parent 14886 b792081d2399
child 14888 99ac3eb0f84e
Added exception Datatype_Empty.
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:22:37 2004 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Tue Jun 08 19:23:53 2004 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    type datatype_info
     1.5  
     1.6    exception Datatype
     1.7 +  exception Datatype_Empty of string
     1.8    val name_of_typ : typ -> string
     1.9    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
    1.10    val mk_Free : string -> typ -> int -> term
    1.11 @@ -203,6 +204,7 @@
    1.12    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    1.13  
    1.14  exception Datatype;
    1.15 +exception Datatype_Empty of string;
    1.16  
    1.17  fun dest_DtTFree (DtTFree a) = a
    1.18    | dest_DtTFree _ = raise Datatype;
    1.19 @@ -284,7 +286,7 @@
    1.20        in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
    1.21        end
    1.22    in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
    1.23 -    (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
    1.24 +    (fn (_, (s, _, _)) => raise Datatype_Empty s)
    1.25    end;
    1.26  
    1.27  (* unfold a list of mutually recursive datatype specifications *)
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 08 19:22:37 2004 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 08 19:23:53 2004 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4         induction : thm,
     2.5         size : thm list,
     2.6         simps : thm list}
     2.7 -  val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
     2.8 +  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
     2.9      (bstring * typ list * mixfix) list) list -> theory -> theory *
    2.10        {distinct : thm list list,
    2.11         inject : thm list list,
    2.12 @@ -904,7 +904,7 @@
    2.13  
    2.14  (******************************** add datatype ********************************)
    2.15  
    2.16 -fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
    2.17 +fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
    2.18    let
    2.19      val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
    2.20  
    2.21 @@ -963,7 +963,9 @@
    2.22      val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
    2.23      val dt_info = get_datatypes thy;
    2.24      val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
    2.25 -    val _ = check_nonempty descr;
    2.26 +    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    2.27 +      if err then error ("Nonemptiness check failed for datatype " ^ s)
    2.28 +      else raise exn;
    2.29  
    2.30      val descr' = flat descr;
    2.31      val case_names_induct = mk_case_names_induct descr';
    2.32 @@ -975,7 +977,7 @@
    2.33    end;
    2.34  
    2.35  val add_datatype_i = gen_add_datatype cert_typ;
    2.36 -val add_datatype = gen_add_datatype read_typ;
    2.37 +val add_datatype = gen_add_datatype read_typ true;
    2.38  
    2.39  
    2.40  (** package setup **)