author | haftmann |
Tue, 18 Sep 2007 07:36:13 +0200 | |
changeset 24622 | 8116eb022282 |
parent 24305 | b1df9e31cda1 |
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 |
|
22846 | 10 |
type hook = string list -> theory -> theory |
11 |
val add: hook -> theory -> theory |
|
12 |
val all: hook |
|
19599 | 13 |
end; |
14 |
||
15 |
structure DatatypeHooks : DATATYPE_HOOKS = |
|
16 |
struct |
|
17 |
||
20177
0af885e3dabf
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
haftmann
parents:
19935
diff
changeset
|
18 |
type hook = string list -> theory -> theory; |
19599 | 19 |
|
20 |
structure DatatypeHooksData = TheoryDataFun |
|
22846 | 21 |
( |
22 |
type T = (serial * hook) list; |
|
23 |
val empty = []; |
|
19599 | 24 |
val copy = I; |
25 |
val extend = I; |
|
22846 | 26 |
fun merge _ hooks : T = AList.merge (op =) (K true) hooks; |
27 |
); |
|
19599 | 28 |
|
29 |
fun add hook = |
|
22846 | 30 |
DatatypeHooksData.map (cons (serial (), hook)); |
19599 | 31 |
|
21251 | 32 |
fun all dtcos thy = |
24305 | 33 |
fold_rev (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy; |
19599 | 34 |
|
35 |
end; |