--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 19 09:39:11 2014 +0200
@@ -416,17 +416,6 @@
\in the problem.")
else
()
- val _ =
- if mode = Normal andalso
- exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
- all_Ts then
- print_nt (K ("Warning: The problem involves directly or indirectly the \
- \internal type " ^ quote @{type_name Datatype.node} ^
- ". This type is very Nitpick-unfriendly, and its presence \
- \usually indicates either a failure of abstraction or a \
- \quirk in Nitpick."))
- else
- ()
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
val _ =
if verbose andalso not unique_scope then
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Aug 19 09:39:11 2014 +0200
@@ -198,7 +198,7 @@
fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
- (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
+ (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
@@ -254,7 +254,7 @@
let
val cnstrs = flat (maps
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (Datatype.get_all (Proof_Context.theory_of ctxt))))
+ (Symtab.dest (Datatype_Data.get_all (Proof_Context.theory_of ctxt))))
fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
| _ => false)
@@ -537,19 +537,19 @@
Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
val setup_bounded_forall_datatype_interpretation =
- Datatype.interpretation (Quickcheck_Common.ensure_sort
+ Datatype_Data.interpretation (Quickcheck_Common.ensure_sort
(((@{sort type}, @{sort type}), @{sort bounded_forall}),
- (Datatype.the_descr, instantiate_bounded_forall_datatype)))
+ (Datatype_Data.the_descr, instantiate_bounded_forall_datatype)))
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =
Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
-(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+(* #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
- #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
- #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Aug 19 09:39:11 2014 +0200
@@ -175,7 +175,7 @@
fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
- (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
+ (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Aug 19 09:39:11 2014 +0200
@@ -23,15 +23,15 @@
val generator_test_goal_terms :
generator -> Proof.context -> bool -> (string * typ) list
-> (term * term list) list -> Quickcheck.result list
- type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+ type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
-> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
val ensure_sort :
(((sort * sort) * sort) *
((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
* string * (string list * string list) * (typ list * typ list)) * instantiation))
- -> Datatype.config -> string list -> theory -> theory
+ -> Datatype_Aux.config -> string list -> theory -> theory
val ensure_common_sort_datatype :
- (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
+ (sort * instantiation) -> Datatype_Aux.config -> string list -> theory -> theory
val datatype_interpretation : (sort * instantiation) -> theory -> theory
val gen_mk_parametric_generator_expr :
(((Proof.context -> term * term list -> term) * term) * typ)
@@ -387,7 +387,7 @@
(** ensuring sort constraints **)
-type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
-> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
fun perhaps_constrain thy insts raw_vs =
@@ -419,9 +419,9 @@
end;
fun ensure_common_sort_datatype (sort, instantiate) =
- ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
+ ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype_Data.the_descr, instantiate))
-val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
+val datatype_interpretation = Datatype_Data.interpretation o ensure_common_sort_datatype
(** generic parametric compilation **)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Aug 19 09:39:11 2014 +0200
@@ -158,7 +158,7 @@
| @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
| _ => raise CTERM ("no equation", [ct]))
- fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
+ fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
| get_constrs _ _ = []
fun is_constr thy (n, T) =
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Tue Aug 19 09:39:11 2014 +0200
@@ -144,7 +144,7 @@
| @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
| _ => raise CTERM ("no equation", [ct]))
- fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
+ fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
| get_constrs _ _ = []
fun is_constr thy (n, T) =