src/HOL/Tools/datatype_hooks.ML
changeset 19599 a5c7eb37d14f
child 19935 604c203beb3a
equal deleted inserted replaced
19598:d68dd20af31f 19599:a5c7eb37d14f
       
     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 -> 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 -> 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/DatatypeHooks";
       
    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 dtco thy =
       
    47   fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
       
    48 
       
    49 
       
    50 (* theory setup *)
       
    51 
       
    52 val setup = DatatypeHooksData.init;
       
    53 
       
    54 end;
       
    55