--- a/src/HOL/Nominal/nominal.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
signature NOMINAL =
sig
- val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
+ val add_nominal_datatype : Datatype.config -> string list ->
(string list * bstring * mixfix *
(bstring * string list * mixfix) list) list -> theory -> theory
type descr
@@ -2084,7 +2084,7 @@
val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
- in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
+ in add_nominal_datatype Datatype.default_config names specs end;
val _ =
OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
--- a/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 08:38:58 2009 +0200
@@ -102,7 +102,7 @@
fold_map (fn ak => fn thy =>
let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
val ({inject,case_thms,...},thy1) = Datatype.add_datatype
- DatatypeAux.default_datatype_config [ak] [dt] thy
+ Datatype.default_config [ak] [dt] thy
val inject_flat = flat inject
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 08:38:58 2009 +0200
@@ -14,24 +14,22 @@
signature DATATYPE_ABS_PROOFS =
sig
- type datatype_config = DatatypeAux.datatype_config
- type descr = DatatypeAux.descr
- type datatype_info = DatatypeAux.datatype_info
- val prove_casedist_thms : datatype_config -> string list ->
+ include DATATYPE_COMMON
+ val prove_casedist_thms : config -> string list ->
descr list -> (string * sort) list -> thm ->
attribute list -> theory -> thm list * theory
- val prove_primrec_thms : datatype_config -> string list ->
+ val prove_primrec_thms : config -> string list ->
descr list -> (string * sort) list ->
- datatype_info Symtab.table -> thm list list -> thm list list ->
+ info Symtab.table -> thm list list -> thm list list ->
simpset -> thm -> theory -> (string list * thm list) * theory
- val prove_case_thms : datatype_config -> string list ->
+ val prove_case_thms : config -> string list ->
descr list -> (string * sort) list ->
string list -> thm list -> theory -> (thm list list * string list) * theory
- val prove_split_thms : datatype_config -> string list ->
+ val prove_split_thms : config -> string list ->
descr list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
(thm * thm) list * theory
- val prove_nchotomys : datatype_config -> string list -> descr list ->
+ val prove_nchotomys : config -> string list -> descr list ->
(string * sort) list -> thm list -> theory -> thm list * theory
val prove_weak_case_congs : string list -> descr list ->
(string * sort) list -> theory -> thm list * theory
@@ -47,7 +45,7 @@
(************************ case distinction theorems ***************************)
-fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
let
val _ = message config "Proving case distinction theorems ...";
@@ -89,8 +87,8 @@
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
- (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
+fun prove_primrec_thms (config : config) new_type_names descr sorts
+ (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
let
val _ = message config "Constructing primrec combinators ...";
@@ -275,7 +273,7 @@
(***************************** case combinators *******************************)
-fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
let
val _ = message config "Proving characteristic theorems for case combinators ...";
@@ -349,7 +347,7 @@
(******************************* case splitting *******************************)
-fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
casedist_thms case_thms thy =
let
val _ = message config "Proving equations for case splitting ...";
@@ -398,7 +396,7 @@
(************************* additional theorems for TFL ************************)
-fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
let
val _ = message config "Proving additional theorems for TFL ...";
--- a/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 08:38:58 2009 +0200
@@ -4,11 +4,23 @@
Auxiliary functions for defining datatypes.
*)
+signature DATATYPE_COMMON =
+sig
+ type config
+ val default_config : config
+ datatype dtyp =
+ DtTFree of string
+ | DtType of string * (dtyp list)
+ | DtRec of int;
+ type descr
+ type info
+end
+
signature DATATYPE_AUX =
sig
- type datatype_config
- val default_datatype_config : datatype_config
- val message : datatype_config -> string -> unit
+ include DATATYPE_COMMON
+
+ val message : config -> string -> unit
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
@@ -33,12 +45,6 @@
datatype simproc_dist = FewConstrs of thm list
| ManyConstrs of thm * simpset;
- datatype dtyp =
- DtTFree of string
- | DtType of string * (dtyp list)
- | DtRec of int;
- type descr
- type datatype_info
exception Datatype
exception Datatype_Empty of string
@@ -61,7 +67,7 @@
-> ((string * Term.typ list) * (string * 'a list) list) list
val check_nonempty : descr list -> unit
val unfold_datatypes :
- theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
+ theory -> descr -> (string * sort) list -> info Symtab.table ->
descr -> int -> descr list * int
end;
@@ -70,10 +76,10 @@
(* datatype option flags *)
-type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
-val default_datatype_config : datatype_config =
+type config = { strict: bool, flat_names: bool, quiet: bool };
+val default_config : config =
{ strict = true, flat_names = false, quiet = false };
-fun message ({ quiet, ...} : datatype_config) s =
+fun message ({ quiet, ...} : config) s =
if quiet then () else writeln s;
fun add_path flat_names s = if flat_names then I else Sign.add_path s;
@@ -186,7 +192,7 @@
(* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
-type datatype_info =
+type info =
{index : int,
alt_names : string list option,
descr : descr,
@@ -317,7 +323,7 @@
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
(* need to be unfolded *)
-fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
+fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
let
fun typ_error T msg = error ("Non-admissible type expression\n" ^
Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
--- a/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 08:38:58 2009 +0200
@@ -7,16 +7,16 @@
signature DATATYPE_CASE =
sig
- val make_case: (string -> DatatypeAux.datatype_info option) ->
+ val make_case: (string -> DatatypeAux.info option) ->
Proof.context -> bool -> string list -> term -> (term * term) list ->
term * (term * (int * bool)) list
- val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
+ val dest_case: (string -> DatatypeAux.info option) -> bool ->
string list -> term -> (term * (term * term) list) option
- val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
+ val strip_case: (string -> DatatypeAux.info option) -> bool ->
term -> (term * (term * term) list) option
- val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
+ val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
-> Proof.context -> term list -> term
- val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
+ val case_tr': (theory -> string -> DatatypeAux.info option) ->
string -> Proof.context -> term list -> term
end;
@@ -31,7 +31,7 @@
* Get information about datatypes
*---------------------------------------------------------------------------*)
-fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
+fun ty_info (tab : string -> DatatypeAux.info option) s =
case tab s of
SOME {descr, case_name, index, sorts, ...} =>
let
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
signature DATATYPE_CODEGEN =
sig
- val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
+ val find_shortest_path: Datatype.descr -> int -> (string * int) option
val mk_eq_eqns: theory -> string -> (thm * bool) list
val mk_case_cert: theory -> string -> thm
val setup: theory -> theory
@@ -17,7 +17,7 @@
(** find shortest path to constructor with no recursive arguments **)
-fun find_nonempty (descr: DatatypeAux.descr) is i =
+fun find_nonempty (descr: Datatype.descr) is i =
let
val (_, _, constrs) = the (AList.lookup (op =) descr i);
fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
@@ -42,7 +42,7 @@
(* datatype definition *)
-fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
+fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
let
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 08:38:58 2009 +0200
@@ -7,7 +7,7 @@
signature DATATYPE_REALIZER =
sig
- val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
+ val add_dt_realizers: Datatype.config -> string list -> theory -> theory
val setup: theory -> theory
end;
@@ -38,7 +38,7 @@
fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
let
val recTs = get_rec_types descr sorts;
val pnames = if length descr = 1 then ["P"]
@@ -157,7 +157,7 @@
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
-fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
+fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
let
val cert = cterm_of thy;
val rT = TFree ("'P", HOLogic.typeS);
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 08:38:58 2009 +0200
@@ -11,12 +11,10 @@
signature DATATYPE_REP_PROOFS =
sig
- type datatype_config = DatatypeAux.datatype_config
- type descr = DatatypeAux.descr
- type datatype_info = DatatypeAux.datatype_info
+ include DATATYPE_COMMON
val distinctness_limit : int Config.T
val distinctness_limit_setup : theory -> theory
- val representation_proofs : datatype_config -> datatype_info Symtab.table ->
+ val representation_proofs : config -> info Symtab.table ->
string list -> descr list -> (string * sort) list ->
(binding * mixfix) list -> (binding * mixfix) list list -> attribute
-> theory -> (thm list list * thm list list * thm list list *
@@ -43,12 +41,12 @@
val myinv_f_f = thm "myinv_f_f";
-fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
+fun exh_thm_of (dt_info : info Symtab.table) tname =
#exhaustion (the (Symtab.lookup dt_info tname));
(******************************************************************************)
-fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
+fun representation_proofs (config : config) (dt_info : info Symtab.table)
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
let
val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
--- a/src/HOL/Tools/function_package/size.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/function_package/size.ML Sun Jun 21 08:38:58 2009 +0200
@@ -57,7 +57,7 @@
val app = curry (list_comb o swap);
-fun prove_size_thms (info : datatype_info) new_type_names thy =
+fun prove_size_thms (info : info) new_type_names thy =
let
val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
val l = length new_type_names;
--- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:58 2009 +0200
@@ -221,7 +221,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname::tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a datatype")
@@ -230,7 +230,7 @@
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
-fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
+fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
let
fun constrs_of (_, (_, _, cs)) =
map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
--- a/src/HOL/Tools/primrec.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Sun Jun 21 08:38:58 2009 +0200
@@ -203,7 +203,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname::tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_error (quote tname ^ " is not a datatype")
--- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 08:38:58 2009 +0200
@@ -12,10 +12,10 @@
-> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
val ensure_random_typecopy: string -> theory -> theory
val random_aux_specification: string -> term list -> local_theory -> local_theory
- val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
+ val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
-> string list -> string list * string list -> typ list * typ list
-> string * (term list * (term * term) list)
- val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
+ val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
end;
--- a/src/HOL/Tools/refute.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/refute.ML Sun Jun 21 08:38:58 2009 +0200
@@ -73,7 +73,7 @@
val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
val string_of_typ : Term.typ -> string
val typ_of_dtyp :
- DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp
+ Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
-> Term.typ
end; (* signature REFUTE *)
@@ -411,15 +411,6 @@
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *)
-(* ('Term.typ'), given type parameters for the data type's type *)
-(* arguments *)
-(* ------------------------------------------------------------------------- *)
-
- (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->
- DatatypeAux.dtyp -> Term.typ *)
-
fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
(* replace a 'DtTFree' variable by the associated type *)
the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
@@ -1660,10 +1651,6 @@
(* their arguments) of the size of the argument types *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->
- (DatatypeAux.dtyp * Term.typ) list ->
- (string * DatatypeAux.dtyp list) list -> int *)
-
fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
sum (map (fn (_, dtyps) =>
product (map (size_of_type thy (typ_sizes, []) o
@@ -2144,7 +2131,6 @@
(* decrement depth for the IDT 'T' *)
val typs' = (case AList.lookup (op =) typs T of NONE => typs
| SOME n => AList.update (op =) (T, n-1) typs)
- (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *)
fun constructor_terms terms [] = terms
| constructor_terms terms (d::ds) =
let
@@ -2241,7 +2227,6 @@
else ()
(* returns an interpretation where everything is mapped to *)
(* an "undefined" element of the datatype *)
- (* DatatypeAux.dtyp list -> interpretation *)
fun make_undef [] =
Leaf (replicate total False)
| make_undef (d::ds) =
@@ -2253,7 +2238,6 @@
Node (replicate size (make_undef ds))
end
(* returns the interpretation for a constructor *)
- (* int * DatatypeAux.dtyp list -> int * interpretation *)
fun make_constr (offset, []) =
if offset<total then
(offset+1, Leaf ((replicate offset False) @ True ::
@@ -2421,9 +2405,6 @@
(* mutually recursive types must have the same type *)
(* parameters, unless the mutual recursion comes from *)
(* indirect recursion *)
- (* (DatatypeAux.dtyp * Term.typ) list ->
- (DatatypeAux.dtyp * Term.typ) list ->
- (DatatypeAux.dtyp * Term.typ) list *)
fun rec_typ_assoc acc [] =
acc
| rec_typ_assoc acc ((d, T)::xs) =
@@ -2458,7 +2439,6 @@
else
raise REFUTE ("IDT_recursion_interpreter",
"different type associations for the same dtyp"))
- (* (DatatypeAux.dtyp * Term.typ) list *)
val typ_assoc = filter
(fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
(rec_typ_assoc []
@@ -2613,7 +2593,6 @@
val rec_dtyps_args = List.filter
(DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
(* map those indices to interpretations *)
- (* (DatatypeAux.dtyp * interpretation) list *)
val rec_dtyps_intrs = map (fn (dtyp, arg) =>
let
val dT = typ_of_dtyp descr typ_assoc dtyp
@@ -2625,8 +2604,6 @@
(* takes the dtyp and interpretation of an element, *)
(* and computes the interpretation for the *)
(* corresponding recursive argument *)
- (* DatatypeAux.dtyp -> interpretation ->
- interpretation *)
fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
(* recursive argument is "rec_i params elem" *)
compute_array_entry i (find_index_eq True xs)
@@ -3252,8 +3229,6 @@
(* constructor generates the datatype's element that is given by *)
(* 'element', returns the constructor (as a term) as well as the *)
(* indices of the arguments *)
- (* string * DatatypeAux.dtyp list ->
- (Term.term * int list) option *)
fun get_constr_args (cname, cargs) =
let
val cTerm = Const (cname,
@@ -3281,7 +3256,6 @@
in
Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
end
- (* Term.term * DatatypeAux.dtyp list * int list *)
val (cTerm, cargs, args) =
(* we could speed things up by computing the correct *)
(* constructor directly (rather than testing all *)