src/HOL/Tools/datatype_hooks.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22846 fb79144af9a3
child 24305 b1df9e31cda1
permissions -rw-r--r--
Some hacks for SPASS format
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
wenzelm@22846
    10
  type hook = string list -> theory -> theory
wenzelm@22846
    11
  val add: hook -> theory -> theory
wenzelm@22846
    12
  val all: hook
haftmann@19599
    13
end;
haftmann@19599
    14
haftmann@19599
    15
structure DatatypeHooks : DATATYPE_HOOKS =
haftmann@19599
    16
struct
haftmann@19599
    17
haftmann@20177
    18
type hook = string list -> theory -> theory;
haftmann@19599
    19
haftmann@19599
    20
structure DatatypeHooksData = TheoryDataFun
wenzelm@22846
    21
(
wenzelm@22846
    22
  type T = (serial * hook) list;
wenzelm@22846
    23
  val empty = [];
haftmann@19599
    24
  val copy = I;
haftmann@19599
    25
  val extend = I;
wenzelm@22846
    26
  fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
wenzelm@22846
    27
);
haftmann@19599
    28
haftmann@19599
    29
fun add hook =
wenzelm@22846
    30
  DatatypeHooksData.map (cons (serial (), hook));
haftmann@19599
    31
haftmann@21251
    32
fun all dtcos thy =
wenzelm@22846
    33
  fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
haftmann@19599
    34
haftmann@19599
    35
end;