src/HOL/Tools/datatype_hooks.ML
changeset 19599 a5c7eb37d14f
child 19935 604c203beb3a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Tue May 09 10:09:37 2006 +0200
     1.3 @@ -0,0 +1,55 @@
     1.4 +(*  Title:      HOL/Tools/datatype_hooks.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Hooks for datatype introduction.
     1.9 +*)
    1.10 +
    1.11 +signature DATATYPE_HOOKS =
    1.12 +sig
    1.13 +  type hook = string -> theory -> theory;
    1.14 +  val add: hook -> theory -> theory;
    1.15 +  val invoke: hook;
    1.16 +  val setup: theory -> theory;
    1.17 +end;
    1.18 +
    1.19 +structure DatatypeHooks : DATATYPE_HOOKS =
    1.20 +struct
    1.21 +
    1.22 +
    1.23 +(* theory data *)
    1.24 +
    1.25 +type hook = string -> theory -> theory;
    1.26 +datatype T = T of (serial * hook) list;
    1.27 +
    1.28 +fun map_T f (T hooks) = T (f hooks);
    1.29 +fun merge_T pp (T hooks1, T hooks2) =
    1.30 +  T (AList.merge (op =) (K true) (hooks1, hooks2));
    1.31 +
    1.32 +structure DatatypeHooksData = TheoryDataFun
    1.33 +(struct
    1.34 +  val name = "HOL/DatatypeHooks";
    1.35 +  type T = T;
    1.36 +  val empty = T [];
    1.37 +  val copy = I;
    1.38 +  val extend = I;
    1.39 +  val merge = merge_T;
    1.40 +  fun print _ _ = ();
    1.41 +end);
    1.42 +
    1.43 +
    1.44 +(* interface *)
    1.45 +
    1.46 +fun add hook =
    1.47 +  DatatypeHooksData.map (map_T (cons (serial (), hook)));
    1.48 +
    1.49 +fun invoke dtco thy =
    1.50 +  fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    1.51 +
    1.52 +
    1.53 +(* theory setup *)
    1.54 +
    1.55 +val setup = DatatypeHooksData.init;
    1.56 +
    1.57 +end;
    1.58 +