1 (* Title: Pure/interpretation.ML |
|
2 Author: Florian Haftmann and Makarius |
|
3 |
|
4 Generic interpretation of theory data. |
|
5 *) |
|
6 |
|
7 signature INTERPRETATION = |
|
8 sig |
|
9 type T |
|
10 val result: theory -> T list |
|
11 val interpretation: (T -> theory -> theory) -> theory -> theory |
|
12 val data: T -> theory -> theory |
|
13 val init: theory -> theory |
|
14 end; |
|
15 |
|
16 functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION = |
|
17 struct |
|
18 |
|
19 type T = T; |
|
20 |
|
21 structure Interp = Theory_Data |
|
22 ( |
|
23 type T = T list * (((T -> theory -> theory) * stamp) * T list) list; |
|
24 val empty = ([], []); |
|
25 val extend = I; |
|
26 fun merge ((data1, interps1), (data2, interps2)) : T = |
|
27 (Library.merge eq (data1, data2), |
|
28 AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2)); |
|
29 ); |
|
30 |
|
31 val result = #1 o Interp.get; |
|
32 |
|
33 fun consolidate thy = |
|
34 let |
|
35 val (data, interps) = Interp.get thy; |
|
36 val unfinished = interps |> map (fn ((f, _), xs) => |
|
37 (f, if eq_list eq (xs, data) then [] else subtract eq xs data)); |
|
38 val finished = interps |> map (fn (interp, _) => (interp, data)); |
|
39 in |
|
40 if forall (null o #2) unfinished then NONE |
|
41 else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished)) |
|
42 end; |
|
43 |
|
44 fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate; |
|
45 fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate; |
|
46 |
|
47 val init = Theory.at_begin consolidate; |
|
48 |
|
49 end; |
|