src/HOL/Tools/datatype_hooks.ML
author paulson
Fri Nov 24 16:38:42 2006 +0100 (2006-11-24)
changeset 21513 9e9fff87dc6c
parent 21251 94e77628a47d
child 22846 fb79144af9a3
permissions -rw-r--r--
Conversion of "equal" to "=" for TSTP format; big tidy-up
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@20177
    10
  type hook = string list -> theory -> theory;
haftmann@19599
    11
  val add: hook -> theory -> theory;
haftmann@21251
    12
  val all: 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@20177
    22
type hook = string list -> 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@19935
    31
  val name = "HOL/datatype_hooks";
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@21251
    46
fun all dtcos thy =
haftmann@20177
    47
  fold (fn (_, f) => f dtcos) ((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