--- a/src/HOL/Nominal/nominal.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 19:09:31 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.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype.ML Sun Jun 21 19:09:31 2009 +0200
@@ -6,26 +6,7 @@
signature DATATYPE =
sig
- type datatype_config = DatatypeAux.datatype_config
- type datatype_info = DatatypeAux.datatype_info
- type descr = DatatypeAux.descr
- val get_datatypes : theory -> datatype_info Symtab.table
- val get_datatype : theory -> string -> datatype_info option
- val the_datatype : theory -> string -> datatype_info
- val datatype_of_constr : theory -> string -> datatype_info option
- val datatype_of_case : theory -> string -> datatype_info option
- val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
- val the_datatype_descr : theory -> string list
- -> descr * (string * sort) list * string list
- * (string list * string list) * (typ list * typ list)
- val get_datatype_constrs : theory -> string -> (string * typ) list option
- val distinct_simproc : simproc
- val make_case : Proof.context -> bool -> string list -> term ->
- (term * term) list -> term * (term * (int * bool)) list
- val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
- val read_typ: theory ->
- (typ list * (string * sort) list) * string -> typ list * (string * sort) list
- val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+ include DATATYPE_COMMON
type rules = {distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -34,15 +15,31 @@
split_thms : (thm * thm) list,
induction : thm,
simps : thm list}
- val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
- -> string list option -> term list -> theory -> Proof.state;
- val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
- val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+ val add_datatype : config -> string list -> (string list * binding * mixfix *
(binding * typ list * mixfix) list) list -> theory -> rules * theory
- val add_datatype_cmd : string list -> (string list * binding * mixfix *
- (binding * string list * mixfix) list) list -> theory -> rules * theory
+ val datatype_cmd : string list -> (string list * binding * mixfix *
+ (binding * string list * mixfix) list) list -> theory -> theory
+ val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
+ -> string list option -> term list -> theory -> Proof.state
+ val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+ val get_datatypes : theory -> info Symtab.table
+ val get_datatype : theory -> string -> info option
+ val the_datatype : theory -> string -> info
+ val datatype_of_constr : theory -> string -> info option
+ val datatype_of_case : theory -> string -> info option
+ val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
+ val the_datatype_descr : theory -> string list
+ -> descr * (string * sort) list * string list
+ * (string list * string list) * (typ list * typ list)
+ val get_datatype_constrs : theory -> string -> (string * typ) list option
+ val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
+ val distinct_simproc : simproc
+ val make_case : Proof.context -> bool -> string list -> term ->
+ (term * term) list -> term * (term * (int * bool)) list
+ val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
+ val read_typ: theory ->
+ (typ list * (string * sort) list) * string -> typ list * (string * sort) list
val setup: theory -> theory
- val print_datatypes : theory -> unit
end;
structure Datatype : DATATYPE =
@@ -56,9 +53,9 @@
structure DatatypesData = TheoryDataFun
(
type T =
- {types: datatype_info Symtab.table,
- constrs: datatype_info Symtab.table,
- cases: datatype_info Symtab.table};
+ {types: info Symtab.table,
+ constrs: info Symtab.table,
+ cases: info Symtab.table};
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
@@ -75,14 +72,10 @@
val get_datatypes = #types o DatatypesData.get;
val map_datatypes = DatatypesData.map;
-fun print_datatypes thy =
- Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
-
(** theory information about datatypes **)
-fun put_dt_infos (dt_infos : (string * datatype_info) list) =
+fun put_dt_infos (dt_infos : (string * info) list) =
map_datatypes (fn {types, constrs, cases} =>
{types = fold Symtab.update dt_infos types,
constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
@@ -207,7 +200,7 @@
let
val inducts = ProjectRule.projections (ProofContext.init thy) induction;
- fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
+ fun named_rules (name, {index, exhaustion, ...}: info) =
[((Binding.empty, nth inducts index), [Induct.induct_type name]),
((Binding.empty, exhaustion), [Induct.cases_type name])];
fun unnamed_rule i =
@@ -351,13 +344,13 @@
simps : thm list}
structure DatatypeInterpretation = InterpretationFun
- (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
+ (type T = config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
(******************* definitional introduction of datatypes *******************)
-fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
@@ -414,7 +407,7 @@
(*********************** declare existing type as datatype *********************)
-fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
let
val ((_, [induct']), _) =
Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -487,7 +480,7 @@
simps = simps}, thy11)
end;
-fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
let
fun constr_of_term (Const (c, T)) = (c, T)
| constr_of_term t =
@@ -553,13 +546,13 @@
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
(******************************** add datatype ********************************)
-fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
@@ -627,12 +620,12 @@
val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
in
add_datatype_def
- (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
+ (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy
end;
val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
+val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
@@ -649,23 +642,29 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
+local
-val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
+structure P = OuterParse and K = OuterKeyword
-fun mk_datatype args =
+fun prep_datatype_decls args =
let
val names = map
(fn ((((NONE, _), t), _), _) => Binding.name_of 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 snd o add_datatype_cmd names specs end;
+ in (names, specs) end;
+
+val parse_datatype_decl =
+ (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+ (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
+
+val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
+
+in
val _ =
OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
- (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
+ (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
val _ =
OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/function_package/size.ML Sun Jun 21 19:09:31 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/hologic.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Sun Jun 21 19:09:31 2009 +0200
@@ -603,8 +603,11 @@
val typerepT = Type ("Typerep.typerep", []);
-fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
- Term.itselfT T --> typerepT) $ Logic.mk_type T;
+fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
+ literalT --> listT typerepT --> typerepT) $ mk_literal tyco
+ $ mk_list typerepT (map mk_typerep Ts)
+ | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
+ Term.itselfT T --> typerepT) $ Logic.mk_type T;
val termT = Type ("Code_Eval.term", []);
--- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
+++ b/src/HOL/Tools/refute.ML Sun Jun 21 19:09:31 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 *)
--- a/src/HOL/Tools/typecopy.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/typecopy.ML Sun Jun 21 19:09:31 2009 +0200
@@ -6,21 +6,13 @@
signature TYPECOPY =
sig
- type info = {
- vs: (string * sort) list,
- constr: string,
- typ: typ,
- inject: thm,
- proj: string * typ,
- proj_def: thm
- }
+ type info = { vs: (string * sort) list, constr: string, typ: typ,
+ inject: thm, proj: string * typ, proj_def: thm }
val typecopy: binding * string list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
- val get_typecopies: theory -> string list
val get_info: theory -> string -> info option
val interpretation: (string -> theory -> theory) -> theory -> theory
val add_default_code: string -> theory -> theory
- val print_typecopies: theory -> unit
val setup: theory -> theory
end;
@@ -47,22 +39,6 @@
fun merge _ = Symtab.merge (K true);
);
-fun print_typecopies thy =
- let
- val tab = TypecopyData.get thy;
- fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
- (Pretty.block o Pretty.breaks) [
- Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
- Pretty.str "=",
- (Pretty.str o Sign.extern_const thy) constr,
- Syntax.pretty_typ_global thy typ,
- Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]];
- in
- (Pretty.writeln o Pretty.block o Pretty.fbreaks)
- (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
- end;
-
-val get_typecopies = Symtab.keys o TypecopyData.get;
val get_info = Symtab.lookup o TypecopyData.get;
@@ -72,7 +48,7 @@
val interpretation = TypecopyInterpretation.interpretation;
-(* declaring typecopies *)
+(* introducing typecopies *)
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
--- a/src/HOL/Tools/typedef.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOL/Tools/typedef.ML Sun Jun 21 19:09:31 2009 +0200
@@ -12,13 +12,13 @@
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
- val get_info: theory -> string -> info option
val add_typedef: bool -> binding option -> binding * string list * mixfix ->
term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
val typedef: (bool * binding) * (binding * string list * mixfix) * term
* (binding * binding) option -> theory -> Proof.state
val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
* (binding * binding) option -> theory -> Proof.state
+ val get_info: theory -> string -> info option
val interpretation: (string -> theory -> theory) -> theory -> theory
val setup: theory -> theory
end;
--- a/src/HOLCF/Fixrec.thy Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Fixrec.thy Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
theory Fixrec
imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec_package.ML")
+uses ("Tools/fixrec.ML")
begin
subsection {* Maybe monad type *}
@@ -599,12 +599,12 @@
subsection {* Initializing the fixrec package *}
-use "Tools/fixrec_package.ML"
+use "Tools/fixrec.ML"
-setup {* FixrecPackage.setup *}
+setup {* Fixrec.setup *}
setup {*
- FixrecPackage.add_matchers
+ Fixrec.add_matchers
[ (@{const_name up}, @{const_name match_up}),
(@{const_name sinl}, @{const_name match_sinl}),
(@{const_name sinr}, @{const_name match_sinr}),
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
theory Abstraction
imports LiveIOA
-uses ("ioa_package.ML")
+uses ("ioa.ML")
begin
defaultsort type
@@ -613,6 +613,6 @@
method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
-use "ioa_package.ML"
+use "ioa.ML"
end
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 19:09:31 2009 +0200
@@ -1,9 +1,8 @@
-(* Title: HOLCF/IOA/meta_theory/ioa_package.ML
- ID: $Id$
+(* Title: HOLCF/IOA/meta_theory/ioa.ML
Author: Tobias Hamberger, TU Muenchen
*)
-signature IOA_PACKAGE =
+signature IOA =
sig
val add_ioa: string -> string
-> (string) list -> (string) list -> (string) list
@@ -16,7 +15,7 @@
val add_rename : string -> string -> string -> theory -> theory
end;
-structure IoaPackage: IOA_PACKAGE =
+structure Ioa: IOA =
struct
val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
--- a/src/HOLCF/IsaMakefile Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/IsaMakefile Sun Jun 21 19:09:31 2009 +0200
@@ -67,8 +67,8 @@
Tools/domain/domain_library.ML \
Tools/domain/domain_syntax.ML \
Tools/domain/domain_theorems.ML \
- Tools/fixrec_package.ML \
- Tools/pcpodef_package.ML \
+ Tools/fixrec.ML \
+ Tools/pcpodef.ML \
holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
@@ -127,7 +127,7 @@
IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
- IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
+ IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
--- a/src/HOLCF/Pcpodef.thy Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Pcpodef.thy Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
theory Pcpodef
imports Adm
-uses ("Tools/pcpodef_package.ML")
+uses ("Tools/pcpodef.ML")
begin
subsection {* Proving a subtype is a partial order *}
@@ -303,6 +303,6 @@
subsection {* HOLCF type definition package *}
-use "Tools/pcpodef_package.ML"
+use "Tools/pcpodef.ML"
end
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 19:09:31 2009 +0200
@@ -6,7 +6,7 @@
signature DOMAIN_AXIOMS =
sig
- val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
+ val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
val calc_axioms :
string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
@@ -171,7 +171,7 @@
val mat_names = map mat_name con_names;
fun qualify n = Sign.full_name thy (Binding.name n);
val ms = map qualify con_names ~~ map qualify mat_names;
- in FixrecPackage.add_matchers ms thy end;
+ in Fixrec.add_matchers ms thy end;
fun add_axioms comp_dnam (eqs : eq list) thy' =
let
--- a/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 19:09:31 2009 +0200
@@ -135,10 +135,10 @@
eqtype arg;
type cons = string * arg list;
type eq = (string * typ list) * cons list;
- val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
+ val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
val is_lazy : arg -> bool;
val rec_of : arg -> int;
- val dtyp_of : arg -> DatatypeAux.dtyp;
+ val dtyp_of : arg -> Datatype.dtyp;
val sel_of : arg -> string option;
val vname : arg -> string;
val upd_vname : (string -> string) -> arg -> arg;
@@ -154,7 +154,7 @@
val idx_name : 'a list -> string -> int -> string;
val app_rec_arg : (int -> term) -> arg -> term;
val con_app : string -> arg list -> term;
- val dtyp_of_eq : eq -> DatatypeAux.dtyp;
+ val dtyp_of_eq : eq -> Datatype.dtyp;
(* Name mangling *)
@@ -215,7 +215,7 @@
(* ----- constructor list handling ----- *)
type arg =
- (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *)
+ (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
string option * (* selector name *)
string; (* argument name *)
--- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 19:09:31 2009 +0200
@@ -1,10 +1,10 @@
-(* Title: HOLCF/Tools/fixrec_package.ML
+(* Title: HOLCF/Tools/fixrec.ML
Author: Amber Telfer and Brian Huffman
Recursive function definition package for HOLCF.
*)
-signature FIXREC_PACKAGE =
+signature FIXREC =
sig
val add_fixrec: bool -> (binding * typ option * mixfix) list
-> (Attrib.binding * term) list -> local_theory -> local_theory
@@ -16,7 +16,7 @@
val setup: theory -> theory
end;
-structure FixrecPackage :> FIXREC_PACKAGE =
+structure Fixrec :> FIXREC =
struct
val def_cont_fix_eq = @{thm def_cont_fix_eq};
@@ -327,7 +327,7 @@
(*************************************************************************)
local
-(* code adapted from HOL/Tools/primrec_package.ML *)
+(* code adapted from HOL/Tools/primrec.ML *)
fun gen_fixrec
(set_group : bool)
--- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 15:47:41 2009 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 19:09:31 2009 +0200
@@ -1,11 +1,11 @@
-(* Title: HOLCF/Tools/pcpodef_package.ML
+(* Title: HOLCF/Tools/pcpodef.ML
Author: Brian Huffman
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
*)
-signature PCPODEF_PACKAGE =
+signature PCPODEF =
sig
val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
* (binding * binding) option -> theory -> Proof.state
@@ -17,7 +17,7 @@
* (binding * binding) option -> theory -> Proof.state
end;
-structure PcpodefPackage :> PCPODEF_PACKAGE =
+structure Pcpodef :> PCPODEF =
struct
(** type definitions **)