src/HOL/thy_data.ML
author clasohm
Fri Apr 19 11:33:24 1996 +0200 (1996-04-19)
changeset 1668 8ead1fe65aad
parent 1657 a7a6c3fb3cdd
child 1726 cbea219f5e5a
permissions -rw-r--r--
added Konrad's code for the datatype package
     1 (*  Title:      HOL/thy_data.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm
     4     Copyright   1995 TU Muenchen
     5 
     6 Definitions that have to be reread after init_thy_reader has been invoked
     7 *)
     8 
     9 fun simpset_of tname =
    10   case get_thydata tname "simpset" of
    11       None => empty_ss
    12     | Some (SS_DATA ss) => ss;
    13 
    14 
    15 (** Information about datatypes **)
    16 
    17 (* Retrieve information for a specific datatype *)
    18 fun datatype_info thy tname =
    19   case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    20       None => None
    21     | Some (DT_DATA ds) => assoc (ds, tname);
    22 
    23 fun match_info thy tname =
    24   case datatype_info thy tname of
    25       Some {case_const, constructors, ...} =>
    26         {case_const=case_const, constructors=constructors}
    27     | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    28 
    29 fun induct_info thy tname =
    30   case datatype_info thy tname of
    31       Some {constructors, nchotomy, ...} =>
    32         {constructors=constructors, nchotomy=nchotomy}
    33     | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    34 
    35 
    36 (* Retrieve information for all datatypes defined in a theory and its
    37    ancestors *)
    38 fun extract_info thy =
    39   let val (congs, rewrites) =
    40         case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    41             None => ([], [])
    42           | Some (DT_DATA ds) =>
    43               let val info = map snd ds
    44               in (map #case_cong info, flat (map #case_rewrites info)) end;
    45   in {case_congs = congs, case_rewrites = rewrites} end;