reduced dependency on 'Datatype' theory and ML module
authorblanchet
Tue Aug 19 09:39:11 2014 +0200 (2014-08-19)
changeset 57996ca917ea6969c
parent 57995 08aa1e2cbec0
child 57997 4f93afabcdd2
reduced dependency on 'Datatype' theory and ML module
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:36:57 2014 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:39:11 2014 +0200
     1.3 @@ -416,17 +416,6 @@
     1.4                     \in the problem.")
     1.5        else
     1.6          ()
     1.7 -    val _ =
     1.8 -      if mode = Normal andalso
     1.9 -         exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
    1.10 -                all_Ts then
    1.11 -        print_nt (K ("Warning: The problem involves directly or indirectly the \
    1.12 -                     \internal type " ^ quote @{type_name Datatype.node} ^
    1.13 -                     ". This type is very Nitpick-unfriendly, and its presence \
    1.14 -                     \usually indicates either a failure of abstraction or a \
    1.15 -                     \quirk in Nitpick."))
    1.16 -      else
    1.17 -        ()
    1.18      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
    1.19      val _ =
    1.20        if verbose andalso not unique_scope then
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Aug 19 09:36:57 2014 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Aug 19 09:39:11 2014 +0200
     2.3 @@ -198,7 +198,7 @@
     2.4    
     2.5  fun contains_recursive_type_under_function_types xs =
     2.6    exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
     2.7 -    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
     2.8 +    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
     2.9      
    2.10  fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
    2.11      config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.12 @@ -254,7 +254,7 @@
    2.13    let
    2.14      val cnstrs = flat (maps
    2.15        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    2.16 -      (Symtab.dest (Datatype.get_all (Proof_Context.theory_of ctxt))))
    2.17 +      (Symtab.dest (Datatype_Data.get_all (Proof_Context.theory_of ctxt))))
    2.18      fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
    2.19          (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
    2.20        | _ => false)
    2.21 @@ -537,19 +537,19 @@
    2.22    Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
    2.23  
    2.24  val setup_bounded_forall_datatype_interpretation =
    2.25 -  Datatype.interpretation (Quickcheck_Common.ensure_sort
    2.26 +  Datatype_Data.interpretation (Quickcheck_Common.ensure_sort
    2.27      (((@{sort type}, @{sort type}), @{sort bounded_forall}),
    2.28 -    (Datatype.the_descr, instantiate_bounded_forall_datatype)))
    2.29 +    (Datatype_Data.the_descr, instantiate_bounded_forall_datatype)))
    2.30  
    2.31  val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
    2.32  
    2.33  val setup =
    2.34    Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
    2.35 -(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.36 +(* #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.37        (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
    2.38 -  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.39 +  #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.40        (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
    2.41 -  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.42 +  #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.43        (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
    2.44    #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
    2.45    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Aug 19 09:36:57 2014 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Aug 19 09:39:11 2014 +0200
     3.3 @@ -175,7 +175,7 @@
     3.4      
     3.5  fun contains_recursive_type_under_function_types xs =
     3.6    exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
     3.7 -    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
     3.8 +    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
     3.9  
    3.10  fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    3.11    let
     4.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Aug 19 09:36:57 2014 +0200
     4.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Aug 19 09:39:11 2014 +0200
     4.3 @@ -23,15 +23,15 @@
     4.4    val generator_test_goal_terms :
     4.5      generator -> Proof.context -> bool -> (string * typ) list
     4.6        -> (term * term list) list -> Quickcheck.result list
     4.7 -  type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
     4.8 +  type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
     4.9       -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    4.10    val ensure_sort :
    4.11      (((sort * sort) * sort) *
    4.12        ((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
    4.13          * string * (string list * string list) * (typ list * typ list)) * instantiation))
    4.14 -    -> Datatype.config -> string list -> theory -> theory
    4.15 +    -> Datatype_Aux.config -> string list -> theory -> theory
    4.16    val ensure_common_sort_datatype :
    4.17 -    (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
    4.18 +    (sort * instantiation) -> Datatype_Aux.config -> string list -> theory -> theory
    4.19    val datatype_interpretation : (sort * instantiation) -> theory -> theory
    4.20    val gen_mk_parametric_generator_expr :
    4.21     (((Proof.context -> term * term list -> term) * term) * typ)
    4.22 @@ -387,7 +387,7 @@
    4.23  
    4.24  (** ensuring sort constraints **)
    4.25  
    4.26 -type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
    4.27 +type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
    4.28    -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    4.29  
    4.30  fun perhaps_constrain thy insts raw_vs =
    4.31 @@ -419,9 +419,9 @@
    4.32    end;
    4.33  
    4.34  fun ensure_common_sort_datatype (sort, instantiate) =
    4.35 -  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
    4.36 +  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype_Data.the_descr, instantiate))
    4.37  
    4.38 -val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
    4.39 +val datatype_interpretation = Datatype_Data.interpretation o ensure_common_sort_datatype
    4.40    
    4.41  (** generic parametric compilation **)
    4.42  
     5.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:36:57 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:39:11 2014 +0200
     5.3 @@ -158,7 +158,7 @@
     5.4      | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     5.5      | _ => raise CTERM ("no equation", [ct]))
     5.6  
     5.7 -  fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
     5.8 +  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
     5.9      | get_constrs _ _ = []
    5.10  
    5.11    fun is_constr thy (n, T) =
     6.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Aug 19 09:36:57 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Aug 19 09:39:11 2014 +0200
     6.3 @@ -144,7 +144,7 @@
     6.4      | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     6.5      | _ => raise CTERM ("no equation", [ct]))
     6.6  
     6.7 -  fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
     6.8 +  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
     6.9      | get_constrs _ _ = []
    6.10  
    6.11    fun is_constr thy (n, T) =