src/HOL/Tools/datatype_hooks.ML
author haftmann
Fri, 21 Jul 2006 14:47:22 +0200
changeset 20177 0af885e3dabf
parent 19935 604c203beb3a
child 21251 94e77628a47d
permissions -rw-r--r--
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Tools/datatype_hooks.ML
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     2
    ID:         $Id$
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     4
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     5
Hooks for datatype introduction.
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     6
*)
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     7
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     8
signature DATATYPE_HOOKS =
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
     9
sig
20177
0af885e3dabf hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
haftmann
parents: 19935
diff changeset
    10
  type hook = string list -> theory -> theory;
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    11
  val add: hook -> theory -> theory;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    12
  val invoke: hook;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    13
  val setup: theory -> theory;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    14
end;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    15
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    16
structure DatatypeHooks : DATATYPE_HOOKS =
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    17
struct
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    18
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    19
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    20
(* theory data *)
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    21
20177
0af885e3dabf hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
haftmann
parents: 19935
diff changeset
    22
type hook = string list -> theory -> theory;
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    23
datatype T = T of (serial * hook) list;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    24
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    25
fun map_T f (T hooks) = T (f hooks);
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    26
fun merge_T pp (T hooks1, T hooks2) =
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    27
  T (AList.merge (op =) (K true) (hooks1, hooks2));
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    28
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    29
structure DatatypeHooksData = TheoryDataFun
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    30
(struct
19935
604c203beb3a renamed thy data
haftmann
parents: 19599
diff changeset
    31
  val name = "HOL/datatype_hooks";
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    32
  type T = T;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    33
  val empty = T [];
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    34
  val copy = I;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    35
  val extend = I;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    36
  val merge = merge_T;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    37
  fun print _ _ = ();
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    38
end);
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    39
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    40
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    41
(* interface *)
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    42
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    43
fun add hook =
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    44
  DatatypeHooksData.map (map_T (cons (serial (), hook)));
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    45
20177
0af885e3dabf hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
haftmann
parents: 19935
diff changeset
    46
fun invoke dtcos thy =
0af885e3dabf hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
haftmann
parents: 19935
diff changeset
    47
  fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    48
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    49
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    50
(* theory setup *)
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    51
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    52
val setup = DatatypeHooksData.init;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    53
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    54
end;
a5c7eb37d14f added DatatypeHooks
haftmann
parents:
diff changeset
    55