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