--- a/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 16:09:16 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 16:09:41 2009 +0100
@@ -96,6 +96,7 @@
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
+
(* complex queries *)
fun the_spec thy dtco =
@@ -157,6 +158,7 @@
| NONE => NONE;
+
(** various auxiliary **)
(* prepare datatype specifications *)
@@ -209,6 +211,7 @@
end;
+
(* translation rules for case *)
fun make_case ctxt = DatatypeCase.make_case
@@ -230,6 +233,7 @@
[], []);
+
(** document antiquotation **)
val _ = ThyOutput.antiquotation "datatype" Args.tyname
@@ -256,15 +260,17 @@
in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
+
(** abstract theory extensions relative to a datatype characterisation **)
-structure DatatypeInterpretation = InterpretationFun
+structure Datatype_Interpretation = InterpretationFun
(type T = config * string list val eq: T * T -> bool = eq_snd op =);
-fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
+fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
(index, (((((((((((_, (tname, _, _))), inject), distinct),
- exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
+ exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
+ (split, split_asm))) =
(tname,
{index = index,
alt_names = alt_names,
@@ -311,7 +317,8 @@
config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
- val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+ val dt_infos = map_index
+ (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
val dt_names = map fst dt_infos;
@@ -339,14 +346,16 @@
|> snd
|> add_case_tr' case_names
|> register dt_infos
- |> DatatypeInterpretation.data (config, dt_names)
+ |> Datatype_Interpretation.data (config, dt_names)
|> pair dt_names
end;
+
(** declare existing type as datatype **)
-fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names alt_names descr sorts
+ raw_inject half_distinct raw_induct thy1 =
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
@@ -419,7 +428,8 @@
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
+ (prove_rep_datatype config dt_names alt_names descr vs
+ raw_inject half_distinct raw_induct)
#-> after_qed
end;
in
@@ -432,6 +442,7 @@
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+
(** definitional introduction of datatypes **)
fun gen_add_datatype prep_typ config new_type_names dts thy =
@@ -447,16 +458,20 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
- in (case duplicates (op =) tvs of
- [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
- else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
- " : " ^ commas dups))
+ in
+ (case duplicates (op =) tvs of
+ [] =>
+ if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+ else error ("Mutually recursive datatypes must have same type parameters")
+ | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
+ " : " ^ commas dups))
end) dts);
val dt_names = map fst new_dts;
- val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
- [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
+ val _ =
+ (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
+ [] => ()
+ | dups => error ("Duplicate datatypes: " ^ commas dups));
fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
let
@@ -510,13 +525,15 @@
val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
+
(** package setup **)
(* setup theory *)
val setup =
trfun_setup #>
- DatatypeInterpretation.init;
+ Datatype_Interpretation.init;
+
(* outer syntax *)