src/HOL/Tools/datatype_hooks.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 20177 0af885e3dabf
child 21251 94e77628a47d
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
     1 (*  Title:      HOL/Tools/datatype_hooks.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Hooks for datatype introduction.
     6 *)
     7 
     8 signature DATATYPE_HOOKS =
     9 sig
    10   type hook = string list -> theory -> theory;
    11   val add: hook -> theory -> theory;
    12   val invoke: hook;
    13   val setup: theory -> theory;
    14 end;
    15 
    16 structure DatatypeHooks : DATATYPE_HOOKS =
    17 struct
    18 
    19 
    20 (* theory data *)
    21 
    22 type hook = string list -> theory -> theory;
    23 datatype T = T of (serial * hook) list;
    24 
    25 fun map_T f (T hooks) = T (f hooks);
    26 fun merge_T pp (T hooks1, T hooks2) =
    27   T (AList.merge (op =) (K true) (hooks1, hooks2));
    28 
    29 structure DatatypeHooksData = TheoryDataFun
    30 (struct
    31   val name = "HOL/datatype_hooks";
    32   type T = T;
    33   val empty = T [];
    34   val copy = I;
    35   val extend = I;
    36   val merge = merge_T;
    37   fun print _ _ = ();
    38 end);
    39 
    40 
    41 (* interface *)
    42 
    43 fun add hook =
    44   DatatypeHooksData.map (map_T (cons (serial (), hook)));
    45 
    46 fun invoke dtcos thy =
    47   fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    48 
    49 
    50 (* theory setup *)
    51 
    52 val setup = DatatypeHooksData.init;
    53 
    54 end;
    55