1 (* Title: HOL/Tools/Ctr_Sugar/local_interpretation.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 |
|
4 Generic interpretation of local theory data -- ad hoc. Based on |
|
5 |
|
6 Title: Pure/interpretation.ML |
|
7 Author: Florian Haftmann and Makarius |
|
8 *) |
|
9 |
|
10 signature LOCAL_INTERPRETATION = |
|
11 sig |
|
12 type T |
|
13 val result: theory -> T list |
|
14 val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> |
|
15 theory -> theory |
|
16 val data: (string -> bool) -> T -> local_theory -> local_theory |
|
17 val data_global: (string -> bool) -> T -> theory -> theory |
|
18 val init: theory -> theory |
|
19 end; |
|
20 |
|
21 functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION = |
|
22 struct |
|
23 |
|
24 type T = T; |
|
25 |
|
26 structure Interp = Theory_Data |
|
27 ( |
|
28 type T = |
|
29 ((Name_Space.naming * (string -> bool)) * T) list |
|
30 * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp)) |
|
31 * ((Name_Space.naming * (string -> bool)) * T) list) list; |
|
32 val empty = ([], []); |
|
33 val extend = I; |
|
34 fun merge ((data1, interps1), (data2, interps2)) : T = |
|
35 (Library.merge (eq_snd eq) (data1, data2), |
|
36 AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2)); |
|
37 ); |
|
38 |
|
39 val result = map snd o fst o Interp.get; |
|
40 |
|
41 fun consolidate_common g_or_f lift_lthy thy thy_or_lthy = |
|
42 let |
|
43 val (data, interps) = Interp.get thy; |
|
44 |
|
45 fun unfinished_of ((gf, (name, _)), data') = |
|
46 (g_or_f gf, |
|
47 if eq_list (eq_snd eq) (data', data) then |
|
48 [] |
|
49 else |
|
50 subtract (eq_snd eq) data' data |
|
51 |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE)); |
|
52 |
|
53 val unfinished = map unfinished_of interps; |
|
54 val finished = map (apsnd (K data)) interps; |
|
55 in |
|
56 if forall (null o #2) unfinished then |
|
57 NONE |
|
58 else |
|
59 SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished |
|
60 |> lift_lthy (Interp.put (data, finished))) |
|
61 end; |
|
62 |
|
63 fun consolidate lthy = |
|
64 consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory |
|
65 (Proof_Context.theory_of lthy) lthy; |
|
66 |
|
67 fun consolidate_global thy = |
|
68 consolidate_common (fn (f, _) => fn (naming, x) => fn thy => |
|
69 thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy; |
|
70 |
|
71 fun interpretation name g f = |
|
72 Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global; |
|
73 |
|
74 fun data keep x = |
|
75 Local_Theory.background_theory |
|
76 (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy) |
|
77 #> perhaps consolidate; |
|
78 |
|
79 fun data_global keep x = |
|
80 (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy) |
|
81 #> perhaps consolidate_global; |
|
82 |
|
83 val init = Theory.at_begin consolidate_global; |
|
84 |
|
85 end; |
|