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