author | wenzelm |
Fri, 08 Dec 2006 23:25:52 +0100 | |
changeset 21713 | 85722dc0fc81 |
parent 21251 | 94e77628a47d |
child 22846 | fb79144af9a3 |
permissions | -rw-r--r-- |
19599 | 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 |
|
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 | 11 |
val add: hook -> theory -> theory; |
21251 | 12 |
val all: hook; |
19599 | 13 |
val setup: theory -> theory; |
14 |
end; |
|
15 |
||
16 |
structure DatatypeHooks : DATATYPE_HOOKS = |
|
17 |
struct |
|
18 |
||
19 |
||
20 |
(* theory data *) |
|
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 | 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 |
|
19935 | 31 |
val name = "HOL/datatype_hooks"; |
19599 | 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 |
||
21251 | 46 |
fun all dtcos thy = |
20177
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 | 48 |
|
49 |
||
50 |
(* theory setup *) |
|
51 |
||
52 |
val setup = DatatypeHooksData.init; |
|
53 |
||
54 |
end; |
|
55 |