--- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 01 16:17:46 2014 +0200
@@ -6,8 +6,8 @@
signature NOMINAL_DATATYPE =
sig
- val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory
- val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
+ val nominal_datatype : Datatype_Aux.config -> Datatype.spec list -> theory -> theory
+ val nominal_datatype_cmd : Datatype_Aux.config -> Datatype.spec_cmd list -> theory -> theory
type descr
type nominal_datatype_info
val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -42,8 +42,8 @@
(* theory data *)
type descr =
- (int * (string * Datatype.dtyp list *
- (string * (Datatype.dtyp list * Datatype.dtyp) list) list)) list;
+ (int * (string * Datatype_Aux.dtyp list *
+ (string * (Datatype_Aux.dtyp list * Datatype_Aux.dtyp) list) list)) list;
type nominal_datatype_info =
{index : int,
@@ -201,8 +201,8 @@
val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
- val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
- fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i);
+ val {descr, induct, ...} = Datatype_Data.the_info thy1 (hd full_new_type_names');
+ fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype_Aux.DtRec i);
val big_name = space_implode "_" new_type_names;
@@ -467,13 +467,13 @@
| (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
- fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
+ fun strip_option (dtf as Datatype_Aux.DtType ("fun", [dt, Datatype_Aux.DtRec i])) =
(case AList.lookup op = descr i of
SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
apfst (cons dt) (strip_option dt')
| _ => ([], dtf))
- | strip_option (Datatype.DtType ("fun",
- [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
+ | strip_option (Datatype_Aux.DtType ("fun",
+ [dt, Datatype_Aux.DtType (@{type_name noption}, [dt'])])) =
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
@@ -499,7 +499,7 @@
end
in (j + 1, j' + length Ts,
case dt'' of
- Datatype.DtRec k => Logic.list_all (map (pair "x") Us,
+ Datatype_Aux.DtRec k => Logic.list_all (map (pair "x") Us,
HOLogic.mk_Trueprop (Free (nth rep_set_names k,
T --> HOLogic.boolT) $ free')) :: prems
| _ => prems,
@@ -680,8 +680,8 @@
(fn ((i, (@{type_name noption}, _, _)), p) => p
| ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
- fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
- | reindex (Datatype.DtRec i) = Datatype.DtRec (the (AList.lookup op = ty_idxs i))
+ fun reindex (Datatype_Aux.DtType (s, dts)) = Datatype_Aux.DtType (s, map reindex dts)
+ | reindex (Datatype_Aux.DtRec i) = Datatype_Aux.DtRec (the (AList.lookup op = ty_idxs i))
| reindex dt = dt;
fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *)
@@ -717,7 +717,7 @@
map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
(constrs ~~ idxss)))) (descr'' ~~ ndescr);
- fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype.DtRec i);
+ fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype_Aux.DtRec i);
val rep_names = map (fn s =>
Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
@@ -744,7 +744,7 @@
xs @ x :: l_args,
fold_rev mk_abs_fun xs
(case dt of
- Datatype.DtRec k => if k < length new_type_names then
+ Datatype_Aux.DtRec k => if k < length new_type_names then
Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt -->
Datatype_Aux.typ_of_dtyp descr dt) $ x
else error "nested recursion not (yet) supported"
@@ -1053,7 +1053,7 @@
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
(prems ~~ constr_defs))]);
- val case_names_induct = Datatype.mk_case_names_induct descr'';
+ val case_names_induct = Datatype_Data.mk_case_names_induct descr'';
(**** prove that new datatypes have finite support ****)
@@ -1446,7 +1446,7 @@
val binders = maps fst frees';
val atomTs = distinct op = (maps (map snd o fst) frees');
val recs = map_filter
- (fn ((_, Datatype.DtRec i), p) => SOME (i, p) | _ => NONE)
+ (fn ((_, Datatype_Aux.DtRec i), p) => SOME (i, p) | _ => NONE)
(partition_cargs idxs cargs ~~ frees');
val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
map (fn (i, _) => nth rec_result_Ts i) recs;
@@ -2053,6 +2053,6 @@
val _ =
Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
(Parse.and_list1 Datatype.spec_cmd >>
- (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
+ (Toplevel.theory o nominal_datatype_cmd Datatype_Aux.default_config));
end