src/HOL/thy_data.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 1726 cbea219f5e5a
child 2562 d571d6660240
permissions -rw-r--r--
added AxClasses test;
     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 fun claset_of tname =
    15   case get_thydata tname "claset" of
    16       None => empty_cs
    17     | Some (CS_DATA cs) => cs;
    18 
    19 
    20 (** Information about datatypes **)
    21 
    22 (* Retrieve information for a specific datatype *)
    23 fun datatype_info thy tname =
    24   case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    25       None => None
    26     | Some (DT_DATA ds) => assoc (ds, tname);
    27 
    28 fun match_info thy tname =
    29   case datatype_info thy tname of
    30       Some {case_const, constructors, ...} =>
    31         {case_const=case_const, constructors=constructors}
    32     | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    33 
    34 fun induct_info thy tname =
    35   case datatype_info thy tname of
    36       Some {constructors, nchotomy, ...} =>
    37         {constructors=constructors, nchotomy=nchotomy}
    38     | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    39 
    40 
    41 (* Retrieve information for all datatypes defined in a theory and its
    42    ancestors *)
    43 fun extract_info thy =
    44   let val (congs, rewrites) =
    45         case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    46             None => ([], [])
    47           | Some (DT_DATA ds) =>
    48               let val info = map snd ds
    49               in (map #case_cong info, flat (map #case_rewrites info)) end;
    50   in {case_congs = congs, case_rewrites = rewrites} end;