--- a/NEWS Tue Jun 23 15:32:34 2009 +0200
+++ b/NEWS Tue Jun 23 16:27:12 2009 +0200
@@ -52,10 +52,12 @@
INCOMPATIBILITY.
-
* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
If possible, use NewNumberTheory, not NumberTheory.
+* Simplified interfaces of datatype module. INCOMPATIBILITY.
+
+
*** ML ***
* Eliminated old Attrib.add_attributes, Method.add_methods and related
--- a/src/HOL/Inductive.thy Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Inductive.thy Tue Jun 23 16:27:12 2009 +0200
@@ -364,7 +364,7 @@
fun fun_tr ctxt [cs] =
let
val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
- val ft = DatatypeCase.case_tr true Datatype.datatype_of_constr
+ val ft = DatatypeCase.case_tr true Datatype.info_of_constr
ctxt [x, cs]
in lambda x ft end
in [("_lam_pats_syntax", fun_tr)] end
--- a/src/HOL/List.thy Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/List.thy Tue Jun 23 16:27:12 2009 +0200
@@ -363,7 +363,7 @@
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
$ NilC;
val cs = Syntax.const "_case2" $ case1 $ case2
- val ft = DatatypeCase.case_tr false Datatype.datatype_of_constr
+ val ft = DatatypeCase.case_tr false Datatype.info_of_constr
ctxt [x, cs]
in lambda x ft end;
--- a/src/HOL/Nominal/nominal.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML Tue Jun 23 16:27:12 2009 +0200
@@ -246,7 +246,7 @@
Datatype.add_datatype config new_type_names' dts'' thy;
val {descr, induction, ...} =
- Datatype.the_datatype thy1 (hd full_new_type_names');
+ Datatype.the_info thy1 (hd full_new_type_names');
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
val big_name = space_implode "_" new_type_names;
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jun 23 16:27:12 2009 +0200
@@ -104,7 +104,7 @@
val (dt_names, thy1) = Datatype.add_datatype
Datatype.default_config [ak] [dt] thy;
- val injects = maps (#inject o Datatype.the_datatype thy1) dt_names;
+ val injects = maps (#inject o Datatype.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/Statespace/state_fun.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML Tue Jun 23 16:27:12 2009 +0200
@@ -340,7 +340,7 @@
| mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
| mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
-fun is_datatype thy n = is_some (Symtab.lookup (Datatype.get_datatypes thy) n);
+fun is_datatype thy = is_some o Datatype.get_info thy;
fun mk_map "List.list" = Syntax.const "List.map"
| mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 16:27:12 2009 +0200
@@ -14,16 +14,16 @@
val rep_datatype : config -> (string list -> 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
+ val get_info : theory -> string -> info option
+ val the_info : theory -> string -> info
+ val the_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 the_spec : theory -> string -> (string * sort) list * (string * typ list) list
+ val get_constrs : theory -> string -> (string * typ) list option
+ val get_all : theory -> info Symtab.table
+ val info_of_constr : theory -> string -> info option
+ val info_of_case : theory -> string -> info option
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
val distinct_simproc : simproc
val make_case : Proof.context -> bool -> string list -> term ->
@@ -61,7 +61,7 @@
cases = Symtab.merge (K true) (cases1, cases2)};
);
-val get_datatypes = #types o DatatypesData.get;
+val get_all = #types o DatatypesData.get;
val map_datatypes = DatatypesData.map;
@@ -77,23 +77,23 @@
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
cases});
-val get_datatype = Symtab.lookup o get_datatypes;
+val get_info = Symtab.lookup o get_all;
-fun the_datatype thy name = (case get_datatype thy name of
+fun the_info thy name = (case get_info thy name of
SOME info => info
| NONE => error ("Unknown datatype " ^ quote name));
-val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
-val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
+val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
+val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-fun get_datatype_descr thy dtco =
- get_datatype thy dtco
+fun get_info_descr thy dtco =
+ get_info thy dtco
|> Option.map (fn info as { descr, index, ... } =>
(info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
-fun the_datatype_spec thy dtco =
+fun the_spec thy dtco =
let
- val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
+ val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
o DatatypeAux.dest_DtTFree) dtys;
@@ -101,9 +101,9 @@
(fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
in (sorts, cos) end;
-fun the_datatype_descr thy (raw_tycos as raw_tyco :: _) =
+fun the_descr thy (raw_tycos as raw_tyco :: _) =
let
- val info = the_datatype thy raw_tyco;
+ val info = the_info thy raw_tyco;
val descr = #descr info;
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
@@ -129,8 +129,8 @@
in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
-fun get_datatype_constrs thy dtco =
- case try (the_datatype_spec thy) dtco
+fun get_constrs thy dtco =
+ case try (the_spec thy) dtco
of SOME (sorts, cos) =>
let
fun subst (v, sort) = TVar ((v, 0), sort);
@@ -216,7 +216,7 @@
val distinctN = "constr_distinct";
-fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
+fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
(EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
atac 2, resolve_tac thms 1, etac FalseE 1]))
@@ -240,7 +240,7 @@
(case (stripT (0, T1), stripT (0, T2)) of
((i', Type (tname1, _)), (j', Type (tname2, _))) =>
if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
- (case (get_datatype_descr thy) tname1 of
+ (case (get_info_descr thy) tname1 of
SOME (_, (_, constrs)) => let val cnames = map fst constrs
in if cname1 mem cnames andalso cname2 mem cnames then
SOME (distinct_rule thy ss tname1
@@ -265,21 +265,21 @@
(**** translation rules for case ****)
fun make_case ctxt = DatatypeCase.make_case
- (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
+ (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
fun strip_case ctxt = DatatypeCase.strip_case
- (datatype_of_case (ProofContext.theory_of ctxt));
+ (info_of_case (ProofContext.theory_of ctxt));
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
let val case_name' = Sign.const_syntax_name thy case_name
- in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
+ in (case_name', DatatypeCase.case_tr' info_of_case case_name')
end) case_names, []) thy;
val trfun_setup =
Sign.add_advanced_trfuns ([],
- [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
+ [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
[], []);
@@ -395,7 +395,7 @@
| get_typ t = err t;
val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
- val dt_info = get_datatypes thy;
+ val dt_info = get_all thy;
val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val (case_names_induct, case_names_exhausts) =
@@ -466,7 +466,7 @@
val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
val _ = case map_filter (fn (tyco, _) =>
- if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
+ if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
of [] => ()
| tycos => error ("Type(s) " ^ commas (map quote tycos)
^ " already represented inductivly");
@@ -576,7 +576,7 @@
val (dts', constr_syntax, sorts', i) =
fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
- val dt_info = get_datatypes thy;
+ val dt_info = get_all thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
@@ -648,7 +648,7 @@
(fn {source = src, context = ctxt, ...} => fn dtco =>
let
val thy = ProofContext.theory_of ctxt;
- val (vs, cos) = the_datatype_spec thy dtco;
+ val (vs, cos) = the_spec thy dtco;
val ty = Type (dtco, map TFree vs);
fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jun 23 16:27:12 2009 +0200
@@ -276,12 +276,12 @@
fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
(c as Const (s, T), ts) =>
- (case Datatype.datatype_of_case thy s of
+ (case Datatype.info_of_case thy s of
SOME {index, descr, ...} =>
if is_some (get_assoc_code thy (s, T)) then NONE else
SOME (pretty_case thy defs dep module brack
(#3 (the (AList.lookup op = descr index))) c ts gr )
- | NONE => case (Datatype.datatype_of_constr thy s, strip_type T) of
+ | NONE => case (Datatype.info_of_constr thy s, strip_type T) of
(SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
if is_some (get_assoc_code thy (s, T)) then NONE else
let
@@ -296,7 +296,7 @@
| _ => NONE);
fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
NONE => NONE
| SOME {descr, sorts, ...} =>
if is_some (get_assoc_type thy s) then NONE else
@@ -331,7 +331,7 @@
fun mk_case_cert thy tyco =
let
val raw_thms =
- (#case_rewrites o Datatype.the_datatype thy) tyco;
+ (#case_rewrites o Datatype.the_info thy) tyco;
val thms as hd_thm :: _ = raw_thms
|> Conjunction.intr_balanced
|> Thm.unvarify
@@ -364,8 +364,8 @@
fun mk_eq_eqns thy dtco =
let
- val (vs, cos) = Datatype.the_datatype_spec thy dtco;
- val { descr, index, inject = inject_thms, ... } = Datatype.the_datatype thy dtco;
+ val (vs, cos) = Datatype.the_spec thy dtco;
+ val { descr, index, inject = inject_thms, ... } = Datatype.the_info thy dtco;
val ty = Type (dtco, map TFree vs);
fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
$ t1 $ t2;
@@ -428,11 +428,11 @@
fun add_all_code config dtcos thy =
let
- val (vs :: _, coss) = (split_list o map (Datatype.the_datatype_spec thy)) dtcos;
+ val (vs :: _, coss) = (split_list o map (Datatype.the_spec thy)) dtcos;
val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
val css = if exists is_none any_css then []
else map_filter I any_css;
- val case_rewrites = maps (#case_rewrites o Datatype.the_datatype thy) dtcos;
+ val case_rewrites = maps (#case_rewrites o Datatype.the_info thy) dtcos;
val certs = map (mk_case_cert thy) dtcos;
in
if null css then thy
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 23 16:27:12 2009 +0200
@@ -217,7 +217,7 @@
if ! Proofterm.proofs < 2 then thy
else let
val _ = message config "Adding realizers for induction and case analysis ..."
- val infos = map (Datatype.the_datatype thy) names;
+ val infos = map (Datatype.the_info thy) names;
val info :: _ = infos;
in
thy
--- a/src/HOL/Tools/Function/fundef.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML Tue Jun 23 16:27:12 2009 +0200
@@ -186,7 +186,7 @@
fun add_case_cong n thy =
Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
- (Datatype.get_datatype thy n |> the
+ (Datatype.the_info thy n
|> #case_cong
|> safe_mk_meta_eq)))
thy
--- a/src/HOL/Tools/Function/fundef_datatype.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML Tue Jun 23 16:27:12 2009 +0200
@@ -40,7 +40,7 @@
let
val (hd, args) = strip_comb t
in
- (((case Datatype.datatype_of_constr thy (fst (dest_Const hd)) of
+ (((case Datatype.info_of_constr thy (fst (dest_Const hd)) of
SOME _ => ()
| NONE => err "Non-constructor pattern")
handle TERM ("dest_Const", _) => err "Non-constructor patterns");
@@ -103,7 +103,7 @@
fun inst_constrs_of thy (T as Type (name, _)) =
map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
- (the (Datatype.get_datatype_constrs thy name))
+ (the (Datatype.get_constrs thy name))
| inst_constrs_of thy _ = raise Match
@@ -144,7 +144,7 @@
let
val T = fastype_of v
val (tname, _) = dest_Type T
- val {exhaustion=case_thm, ...} = Datatype.the_datatype thy tname
+ val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
val constrs = inst_constrs_of thy T
val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
in
--- a/src/HOL/Tools/Function/pattern_split.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Tue Jun 23 16:27:12 2009 +0200
@@ -40,7 +40,7 @@
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
- (the (Datatype.get_datatype_constrs thy name))
+ (the (Datatype.get_constrs thy name))
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
--- a/src/HOL/Tools/Function/size.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Tue Jun 23 16:27:12 2009 +0200
@@ -44,14 +44,14 @@
| SOME t => t);
fun is_poly thy (DtType (name, dts)) =
- (case Datatype.get_datatype thy name of
+ (case Datatype.get_info thy name of
NONE => false
| SOME _ => exists (is_poly thy) dts)
| is_poly _ _ = true;
fun constrs_of thy name =
let
- val {descr, index, ...} = Datatype.the_datatype thy name
+ val {descr, index, ...} = Datatype.the_info thy name
val SOME (_, _, constrs) = AList.lookup op = descr index
in constrs end;
@@ -220,7 +220,7 @@
fun add_size_thms config (new_type_names as name :: _) thy =
let
- val info as {descr, alt_names, ...} = Datatype.the_datatype thy name;
+ val info as {descr, alt_names, ...} = Datatype.the_info thy name;
val prefix = Long_Name.map_base_name (K (space_implode "_"
(the_default (map Long_Name.base_name new_type_names) alt_names))) name;
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
--- a/src/HOL/Tools/TFL/casesplit.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Tue Jun 23 16:27:12 2009 +0200
@@ -88,16 +88,13 @@
Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
(* get the case_thm (my version) from a type *)
-fun case_thm_of_ty sgn ty =
+fun case_thm_of_ty thy ty =
let
- val dtypestab = Datatype.get_datatypes sgn;
val ty_str = case ty of
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
| TVar((s,i),_) => error ("Free variable: " ^ s)
- val dt = case Symtab.lookup dtypestab ty_str
- of SOME dt => dt
- | NONE => error ("Not a Datatype: " ^ ty_str)
+ val dt = Datatype.the_info thy ty_str
in
cases_thm_of_induct_thm (#induction dt)
end;
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Jun 23 16:27:12 2009 +0200
@@ -446,7 +446,7 @@
slow.*)
val case_ss = Simplifier.theory_context theory
(HOL_basic_ss addcongs
- (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) theory addsimps case_rewrites)
+ (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
val corollaries' = map (Simplifier.simplify case_ss) corollaries
val extract = R.CONTEXT_REWRITE_RULE
(f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
--- a/src/HOL/Tools/TFL/thry.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Tue Jun 23 16:27:12 2009 +0200
@@ -60,20 +60,20 @@
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
- case (Datatype.get_datatype thy dtco,
- Datatype.get_datatype_constrs thy dtco) of
+ case (Datatype.get_info thy dtco,
+ Datatype.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_datatype thy dtco of
+fun induct_info thy dtco = case Datatype.get_info thy dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
- constructors = (map Const o the o Datatype.get_datatype_constrs thy) dtco};
+ constructors = (map Const o the o Datatype.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = (map snd o Symtab.dest o Datatype.get_datatypes) thy
+ let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
end;
--- a/src/HOL/Tools/inductive_codegen.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jun 23 16:27:12 2009 +0200
@@ -101,9 +101,9 @@
fun is_constrt thy =
let
- val cnstrs = List.concat (List.concat (map
+ val cnstrs = flat (maps
(map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd)
- (Symtab.dest (Datatype.get_datatypes thy))));
+ (Symtab.dest (Datatype.get_all thy)));
fun check t = (case strip_comb t of
(Var _, []) => true
| (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 16:27:12 2009 +0200
@@ -313,9 +313,9 @@
||> 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_datatype thy2) dt_names;
+ val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
val rec_thms = if null dt_names then []
- else (#rec_rewrites o Datatype.the_datatype thy2) (hd dt_names);
+ else (#rec_rewrites o Datatype.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) =>
--- a/src/HOL/Tools/old_primrec.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Tue Jun 23 16:27:12 2009 +0200
@@ -246,7 +246,7 @@
fun gen_primrec_i note def alt_name eqns_atts thy =
let
val (eqns, atts) = split_list eqns_atts;
- val dt_info = Datatype.get_datatypes thy;
+ val dt_info = Datatype.get_all thy;
val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
val dts = find_dts dt_info tnames tnames;
--- a/src/HOL/Tools/primrec.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Tue Jun 23 16:27:12 2009 +0200
@@ -220,7 +220,7 @@
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
- val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
+ val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
(index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
val {descr, rec_names, rec_rewrites, ...} =
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jun 23 16:27:12 2009 +0200
@@ -361,7 +361,7 @@
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
- Datatype.the_datatype_descr thy raw_tycos;
+ Datatype.the_descr thy raw_tycos;
val typrep_vs = (map o apsnd)
(curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
--- a/src/HOL/Tools/refute.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/refute.ML Tue Jun 23 16:27:12 2009 +0200
@@ -517,7 +517,7 @@
fun is_IDT_constructor thy (s, T) =
(case body_type T of
Type (s', _) =>
- (case Datatype.get_datatype_constrs thy s' of
+ (case Datatype.get_constrs thy s' of
SOME constrs =>
List.exists (fn (cname, cty) =>
cname = s andalso Sign.typ_instance thy (T, cty)) constrs
@@ -536,7 +536,7 @@
fun is_IDT_recursor thy (s, T) =
let
val rec_names = Symtab.fold (append o #rec_names o snd)
- (Datatype.get_datatypes thy) []
+ (Datatype.get_all thy) []
in
(* I'm not quite sure if checking the name 's' is sufficient, *)
(* or if we should also check the type 'T'. *)
@@ -825,7 +825,7 @@
(* axiomatic type classes *)
| Type ("itself", [T1]) => collect_type_axioms (axs, T1)
| Type (s, Ts) =>
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info => (* inductive datatype *)
(* only collect relevant type axioms for the argument types *)
Library.foldl collect_type_axioms (axs, Ts)
@@ -960,7 +960,7 @@
Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
| Type ("prop", []) => acc
| Type (s, Ts) =>
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1172,7 +1172,7 @@
(* TODO: no warning needed for /positive/ occurrences of IDTs *)
val maybe_spurious = Library.exists (fn
Type (s, _) =>
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1973,7 +1973,7 @@
val (typs, terms) = model
(* Term.typ -> (interpretation * model * arguments) option *)
fun interpret_term (Type (s, Ts)) =
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info => (* inductive datatype *)
let
(* int option -- only recursive IDTs have an associated depth *)
@@ -2107,7 +2107,7 @@
HOLogic_empty_set) pairss
end
| Type (s, Ts) =>
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info =>
(case AList.lookup (op =) typs T of
SOME 0 =>
@@ -2171,7 +2171,7 @@
Const (s, T) =>
(case body_type T of
Type (s', Ts') =>
- (case Datatype.get_datatype thy s' of
+ (case Datatype.get_info thy s' of
SOME info => (* body type is an inductive datatype *)
let
val index = #index info
@@ -2652,7 +2652,7 @@
end
else
NONE (* not a recursion operator of this datatype *)
- ) (Datatype.get_datatypes thy) NONE
+ ) (Datatype.get_all thy) NONE
| _ => (* head of term is not a constant *)
NONE;
@@ -3201,7 +3201,7 @@
fun IDT_printer thy model T intr assignment =
(case T of
Type (s, Ts) =>
- (case Datatype.get_datatype thy s of
+ (case Datatype.get_info thy s of
SOME info => (* inductive datatype *)
let
val (typs, _) = model
--- a/src/HOL/ex/predicate_compile.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Jun 23 16:27:12 2009 +0200
@@ -333,7 +333,7 @@
let
val cnstrs = flat (maps
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (Datatype.get_datatypes thy)));
+ (Symtab.dest (Datatype.get_all thy)));
fun check t = (case strip_comb t of
(Free _, []) => true
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
@@ -875,7 +875,7 @@
(* else false *)
fun is_constructor thy t =
if (is_Type (fastype_of t)) then
- (case Datatype.get_datatype thy ((fst o dest_Type o fastype_of) t) of
+ (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
NONE => false
| SOME info => (let
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
@@ -954,7 +954,7 @@
fun prove_match thy (out_ts : term list) = let
fun get_case_rewrite t =
if (is_constructor thy t) then let
- val case_rewrites = (#case_rewrites (Datatype.the_datatype thy
+ val case_rewrites = (#case_rewrites (Datatype.the_info thy
((fst o dest_Type o fastype_of) t)))
in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
else []
@@ -1093,7 +1093,7 @@
fun split_term_tac (Free _) = all_tac
| split_term_tac t =
if (is_constructor thy t) then let
- val info = Datatype.the_datatype thy ((fst o dest_Type o fastype_of) t)
+ val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
val num_of_constrs = length (#case_rewrites info)
(* special treatment of pairs -- because of fishing *)
val split_rules = case (fst o dest_Type o fastype_of) t of