1 (* Title: Pure/theory_data.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Type-safe interface for theory data. |
|
6 *) |
|
7 |
|
8 signature THEORY_DATA_ARGS = |
|
9 sig |
|
10 val name: string |
|
11 type T |
|
12 val empty: T |
|
13 val copy: T -> T |
|
14 val prep_ext: T -> T |
|
15 val merge: T * T -> T |
|
16 val print: Sign.sg -> T -> unit |
|
17 end; |
|
18 |
|
19 signature THEORY_DATA = |
|
20 sig |
|
21 type T |
|
22 val init: theory -> theory |
|
23 val print: theory -> unit |
|
24 val get_sg: Sign.sg -> T |
|
25 val get: theory -> T |
|
26 val put: T -> theory -> theory |
|
27 val map: (T -> T) -> theory -> theory |
|
28 end; |
|
29 |
|
30 functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA = |
|
31 struct |
|
32 |
|
33 (*object kind kept private!*) |
|
34 val kind = Object.kind Args.name; |
|
35 |
|
36 type T = Args.T; |
|
37 exception Data of T; |
|
38 |
|
39 val init = |
|
40 Theory.init_data kind |
|
41 (Data Args.empty, |
|
42 fn (Data x) => Data (Args.copy x), |
|
43 fn (Data x) => Data (Args.prep_ext x), |
|
44 fn (Data x1, Data x2) => Data (Args.merge (x1, x2)), |
|
45 fn sg => fn (Data x) => Args.print sg x); |
|
46 |
|
47 val print = Theory.print_data kind; |
|
48 val get_sg = Sign.get_data kind (fn Data x => x); |
|
49 val get = get_sg o Theory.sign_of; |
|
50 val put = Theory.put_data kind Data; |
|
51 fun map f thy = put (f (get thy)) thy; |
|
52 |
|
53 end; |
|
54 |
|
55 (*hide private data access functions*) |
|
56 structure Sign: SIGN = Sign; |
|
57 structure Theory: THEORY = Theory; |
|