--- a/src/HOL/thy_data.ML Fri Apr 19 11:18:59 1996 +0200
+++ b/src/HOL/thy_data.ML Fri Apr 19 11:33:24 1996 +0200
@@ -11,7 +11,35 @@
None => empty_ss
| Some (SS_DATA ss) => ss;
-fun datatypes_of tname =
- case get_thydata tname "datatypes" of
- None => []
- | Some (DT_DATA ds) => ds;
+
+(** Information about datatypes **)
+
+(* Retrieve information for a specific datatype *)
+fun datatype_info thy tname =
+ case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+ None => None
+ | Some (DT_DATA ds) => assoc (ds, tname);
+
+fun match_info thy tname =
+ case datatype_info thy tname of
+ Some {case_const, constructors, ...} =>
+ {case_const=case_const, constructors=constructors}
+ | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+fun induct_info thy tname =
+ case datatype_info thy tname of
+ Some {constructors, nchotomy, ...} =>
+ {constructors=constructors, nchotomy=nchotomy}
+ | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+
+
+(* Retrieve information for all datatypes defined in a theory and its
+ ancestors *)
+fun extract_info thy =
+ let val (congs, rewrites) =
+ case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
+ None => ([], [])
+ | Some (DT_DATA ds) =>
+ let val info = map snd ds
+ in (map #case_cong info, flat (map #case_rewrites info)) end;
+ in {case_congs = congs, case_rewrites = rewrites} end;