--- a/src/HOL/Fun.thy Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Fun.thy Mon Sep 01 16:17:46 2014 +0200
@@ -585,7 +585,7 @@
"f(x:=y)" == "CONST fun_upd f x y"
(* Hint: to define the sum of two functions (or maps), use case_sum.
- A nice infix syntax could be defined (in Datatype.thy or below) by
+ A nice infix syntax could be defined by
notation
case_sum (infixr "'(+')"80)
*)
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 01 16:17:46 2014 +0200
@@ -233,8 +233,7 @@
["finite_intvl_succ_class",
"nibble"]
-val forbidden_consts =
- [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
+val forbidden_consts = [@{const_name Pure.type}]
fun is_forbidden_theorem (s, th) =
let val consts = Term.add_const_names (prop_of th) [] in
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Sep 01 16:17:46 2014 +0200
@@ -100,9 +100,9 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
- val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
+ val (dt_names, thy1) = Datatype.add_datatype Datatype_Aux.default_config [dt] thy;
- val injects = maps (#inject o Datatype.the_info thy1) dt_names;
+ val injects = maps (#inject o Datatype_Data.the_info thy1) dt_names;
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak
--- 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
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 16:17:46 2014 +0200
@@ -173,8 +173,8 @@
fun add_enum_type tyname tyname' thy =
let
- val {case_name, ...} = the (Datatype.get_info thy tyname');
- val cs = map Const (the (Datatype.get_constrs thy tyname'));
+ val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
+ val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
val k = length cs;
val T = Type (tyname', []);
val p = Const (@{const_name pos}, T --> HOLogic.intT);
@@ -209,7 +209,7 @@
(fn _ =>
rtac @{thm subset_antisym} 1 THEN
rtac @{thm subsetI} 1 THEN
- Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
+ Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
(Proof_Context.theory_of lthy) tyname'))) 1 THEN
ALLGOALS (asm_full_simp_tac lthy));
@@ -327,7 +327,7 @@
tyname)
end
| SOME (T as Type (tyname, []), cmap) =>
- (case Datatype.get_constrs thy tyname of
+ (case Datatype_Data.get_constrs thy tyname of
NONE => assoc_ty_err thy T s "is not a datatype"
| SOME cs =>
let val (prfx', _) = strip_prfx s
@@ -338,7 +338,7 @@
| SOME msg => assoc_ty_err thy T s msg
end)
| SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
- val cs = map Const (the (Datatype.get_constrs thy' tyname));
+ val cs = map Const (the (Datatype_Data.get_constrs thy' tyname));
in
((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
fold Name.declare els ctxt),
@@ -888,7 +888,7 @@
handle Symtab.DUP _ => error ("SPARK type " ^ s ^
" already associated with type")) |>
(fn thy' =>
- case Datatype.get_constrs thy' tyname of
+ case Datatype_Data.get_constrs thy' tyname of
NONE => (case get_record_info thy' T of
NONE => thy'
| SOME {fields, ...} =>
--- a/src/HOL/Statespace/state_fun.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Sep 01 16:17:46 2014 +0200
@@ -339,7 +339,7 @@
| mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
| mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
-fun is_datatype thy = is_some o Datatype.get_info thy;
+fun is_datatype thy = is_some o Datatype_Data.get_info thy;
fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
| mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 01 16:17:46 2014 +0200
@@ -9,7 +9,6 @@
signature DATATYPE =
sig
- include DATATYPE_DATA
val distinct_lemma: thm
type spec =
(binding * (string * sort) list * mixfix) *
@@ -19,8 +18,8 @@
(binding * string list * mixfix) list
val read_specs: spec_cmd list -> theory -> spec list * Proof.context
val check_specs: spec list -> theory -> spec list * Proof.context
- val add_datatype: config -> spec list -> theory -> string list * theory
- val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
+ val add_datatype: Datatype_Aux.config -> spec list -> theory -> string list * theory
+ val add_datatype_cmd: Datatype_Aux.config -> spec_cmd list -> theory -> string list * theory
val spec_cmd: spec_cmd parser
end;
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 01 16:17:46 2014 +0200
@@ -7,6 +7,7 @@
signature DATATYPE_DATA =
sig
include DATATYPE_COMMON
+
val get_all : theory -> info Symtab.table
val get_info : theory -> string -> info option
val the_info : theory -> string -> info
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 01 16:17:46 2014 +0200
@@ -7,7 +7,7 @@
signature DATATYPE_REALIZER =
sig
- val add_dt_realizers: Datatype.config -> string list -> theory -> theory
+ val add_dt_realizers: Datatype_Aux.config -> string list -> theory -> theory
val setup: theory -> theory
end;
@@ -25,7 +25,7 @@
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
-fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
+fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
@@ -84,7 +84,7 @@
in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
constrs) (descr ~~ recTs) 1)));
- fun mk_proj j [] t = t
+ fun mk_proj _ [] t = t
| mk_proj j (i :: is) t =
if null is then t
else if (j: int) = i then HOLogic.mk_fst t
@@ -159,7 +159,8 @@
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
-fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype.info) thy =
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info)
+ thy =
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
@@ -232,7 +233,7 @@
else
let
val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
- val infos = map (Datatype.the_info thy) names;
+ val infos = map (Datatype_Data.the_info thy) names;
val info :: _ = infos;
in
thy
@@ -240,6 +241,6 @@
|> fold_rev make_casedists infos
end;
-val setup = Datatype.interpretation add_dt_realizers;
+val setup = Datatype_Data.interpretation add_dt_realizers;
end;
--- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 01 16:17:46 2014 +0200
@@ -24,7 +24,7 @@
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
| TVar((s,i),_) => error ("Free variable: " ^ s)
- val {induct, ...} = Datatype.the_info thy ty_str
+ val {induct, ...} = Datatype_Data.the_info thy ty_str
in
cases_thm_of_induct_thm induct
end;
--- a/src/HOL/Tools/TFL/tfl.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Sep 01 16:17:46 2014 +0200
@@ -435,7 +435,7 @@
put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
|> fold (Simplifier.add_cong o #case_cong_weak o snd)
- (Symtab.dest (Datatype.get_all theory))
+ (Symtab.dest (Datatype_Data.get_all theory))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
val extract = Rules.CONTEXT_REWRITE_RULE
(f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
--- a/src/HOL/Tools/TFL/thry.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Mon Sep 01 16:17:46 2014 +0200
@@ -58,20 +58,20 @@
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
- case (Datatype.get_info thy dtco,
- Datatype.get_constrs thy dtco) of
+ case (Datatype_Data.get_info thy dtco,
+ Datatype_Data.get_constrs thy dtco) of
(SOME { case_name, ... }, SOME constructors) =>
SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
| _ => NONE;
-fun induct_info thy dtco = case Datatype.get_info thy dtco of
+fun induct_info thy dtco = case Datatype_Data.get_info thy dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
- constructors = (map Const o the o Datatype.get_constrs thy) dtco};
+ constructors = (map Const o the o Datatype_Data.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = map snd (Symtab.dest (Datatype.get_all thy))
+ let val infos = map snd (Symtab.dest (Datatype_Data.get_all thy))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;
--- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 01 16:17:46 2014 +0200
@@ -313,10 +313,10 @@
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
val dt_names = these some_dt_names;
- val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
+ val case_thms = map (#case_rewrites o Datatype_Data.the_info thy2) dt_names;
val rec_thms =
if null dt_names then []
- else #rec_rewrites (Datatype.the_info thy2 (hd dt_names));
+ else #rec_rewrites (Datatype_Data.the_info thy2 (hd dt_names));
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>