12014
|
1 |
(* Title: Pure/Isar/locale.ML
|
11896
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
|
12058
|
6 |
Locales -- Isar proof contexts as meta-level predicates, with local
|
12063
|
7 |
syntax and implicit structures. Draws basic ideas from Florian
|
|
8 |
Kammueller's original version of locales, but uses the rich
|
|
9 |
infrastructure of Isar instead of the raw meta-logic.
|
11896
|
10 |
*)
|
|
11 |
|
|
12 |
signature BASIC_LOCALE =
|
|
13 |
sig
|
|
14 |
val print_locales: theory -> unit
|
12063
|
15 |
val print_locale: theory -> xstring -> unit
|
11896
|
16 |
end;
|
|
17 |
|
|
18 |
signature LOCALE =
|
|
19 |
sig
|
|
20 |
include BASIC_LOCALE
|
12046
|
21 |
type context
|
12014
|
22 |
type expression
|
12046
|
23 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
24 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
25 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
26 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
|
27 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list |
|
|
28 |
Uses of expression
|
|
29 |
type 'att element
|
|
30 |
type 'att element_i
|
|
31 |
type locale
|
|
32 |
val intern: Sign.sg -> xstring -> string
|
12014
|
33 |
val cond_extern: Sign.sg -> string -> xstring
|
12063
|
34 |
val attribute: ('att -> context attribute) ->
|
12046
|
35 |
('typ, 'term, 'thm, 'att) elem -> ('typ, 'term, 'thm, context attribute) elem
|
|
36 |
val activate_elements: context attribute element list -> context -> context
|
|
37 |
val activate_elements_i: context attribute element_i list -> context -> context
|
|
38 |
val activate_locale: xstring -> context -> context
|
|
39 |
val activate_locale_i: string -> context -> context
|
12063
|
40 |
val add_locale: bstring -> xstring list -> context attribute element list -> theory -> theory
|
|
41 |
val add_locale_i: bstring -> xstring list -> context attribute element_i list -> theory -> theory
|
|
42 |
val store_thm: string -> (string * thm) * context attribute list -> theory -> theory
|
11896
|
43 |
val setup: (theory -> theory) list
|
|
44 |
end;
|
|
45 |
|
|
46 |
structure Locale: LOCALE =
|
|
47 |
struct
|
|
48 |
|
|
49 |
|
12014
|
50 |
(** locale elements and locales **)
|
11896
|
51 |
|
12014
|
52 |
type context = ProofContext.context;
|
11896
|
53 |
|
12070
|
54 |
type expression = string;
|
11896
|
55 |
|
12046
|
56 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
57 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
58 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
59 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
|
60 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list |
|
12014
|
61 |
Uses of expression;
|
11896
|
62 |
|
12046
|
63 |
type 'att element = (string, string, string, 'att) elem;
|
|
64 |
type 'att element_i = (typ, term, thm list, 'att) elem;
|
12070
|
65 |
|
|
66 |
type locale =
|
|
67 |
{imports: expression list, elements: context attribute element_i list, closed: bool};
|
12063
|
68 |
|
|
69 |
fun make_locale imports elements closed =
|
|
70 |
{imports = imports, elements = elements, closed = closed}: locale;
|
12046
|
71 |
|
|
72 |
|
12063
|
73 |
(*fun close_locale {imports, elements, closed = _} = make_locale imports elements true;*)
|
|
74 |
fun close_locale x = x; (* FIXME tmp *)
|
|
75 |
|
11896
|
76 |
|
|
77 |
|
|
78 |
(** theory data **)
|
|
79 |
|
|
80 |
(* data kind 'Pure/locales' *)
|
|
81 |
|
|
82 |
structure LocalesArgs =
|
|
83 |
struct
|
12014
|
84 |
val name = "Isar/locales";
|
12063
|
85 |
type T = NameSpace.T * locale Symtab.table;
|
11896
|
86 |
|
12063
|
87 |
val empty = (NameSpace.empty, Symtab.empty);
|
|
88 |
val copy = I;
|
|
89 |
fun prep_ext (space, locales) = (space, Symtab.map close_locale locales);
|
|
90 |
fun merge ((space1, locales1), (space2, locales2)) =
|
|
91 |
(NameSpace.merge (space1, space2), Symtab.merge (K true) (locales1, locales2));
|
11896
|
92 |
|
12063
|
93 |
fun print _ (space, locales) =
|
12014
|
94 |
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locales))
|
|
95 |
|> Pretty.writeln;
|
11896
|
96 |
end;
|
|
97 |
|
|
98 |
structure LocalesData = TheoryDataFun(LocalesArgs);
|
|
99 |
val print_locales = LocalesData.print;
|
|
100 |
|
12063
|
101 |
val intern = NameSpace.intern o #1 o LocalesData.get_sg;
|
|
102 |
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg;
|
12014
|
103 |
|
11896
|
104 |
|
|
105 |
(* access locales *)
|
|
106 |
|
12063
|
107 |
fun declare_locale name =
|
|
108 |
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name]))));
|
11896
|
109 |
|
12063
|
110 |
fun put_locale name locale =
|
|
111 |
LocalesData.map (apsnd (fn locales => Symtab.update ((name, locale), locales)));
|
|
112 |
|
|
113 |
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
|
11896
|
114 |
|
12014
|
115 |
fun the_locale thy name =
|
|
116 |
(case get_locale thy name of
|
|
117 |
Some loc => loc
|
|
118 |
| None => error ("Unknown locale " ^ quote name));
|
11896
|
119 |
|
|
120 |
|
12046
|
121 |
|
12063
|
122 |
(** internalize elements **)
|
|
123 |
|
|
124 |
(* read_elem *)
|
12046
|
125 |
|
12063
|
126 |
fun read_elem ctxt =
|
|
127 |
fn Fixes fixes =>
|
|
128 |
let val vars =
|
|
129 |
#2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
|
|
130 |
in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
|
|
131 |
| Assumes asms =>
|
|
132 |
Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
|
|
133 |
| Defines defs =>
|
|
134 |
let val propps =
|
|
135 |
#2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
|
|
136 |
in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
|
|
137 |
| Notes facts =>
|
|
138 |
Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts)
|
12070
|
139 |
| Uses xname => Uses (intern (ProofContext.sign_of ctxt) xname);
|
12063
|
140 |
|
|
141 |
|
|
142 |
(* prepare attributes *)
|
|
143 |
|
|
144 |
local fun int_att attrib (x, srcs) = (x, map attrib srcs) in
|
|
145 |
|
|
146 |
fun attribute _ (Fixes fixes) = Fixes fixes
|
|
147 |
| attribute attrib (Assumes asms) = Assumes (map (apfst (int_att attrib)) asms)
|
|
148 |
| attribute attrib (Defines defs) = Defines (map (apfst (int_att attrib)) defs)
|
|
149 |
| attribute attrib (Notes facts) =
|
12046
|
150 |
Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts)
|
12070
|
151 |
| attribute _ (Uses name) = Uses name;
|
12063
|
152 |
|
|
153 |
end;
|
12046
|
154 |
|
|
155 |
|
11896
|
156 |
|
12014
|
157 |
(** activate locales **)
|
11896
|
158 |
|
12046
|
159 |
fun activate (ctxt, Fixes fixes) =
|
12070
|
160 |
ctxt |> ProofContext.fix_direct (map (fn (x, T, mx) => ([x], T)) fixes)
|
|
161 |
|> ProofContext.add_syntax fixes
|
12058
|
162 |
| activate (ctxt, Assumes asms) =
|
|
163 |
ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
|
|
164 |
|> ProofContext.assume_i ProofContext.export_assume asms |> #1
|
12046
|
165 |
| activate (ctxt, Defines defs) = #1 (ProofContext.assume_i ProofContext.export_def
|
12058
|
166 |
(map (fn (a, (t, ps)) => (a, [(ProofContext.cert_def ctxt t, (ps, []))])) defs) ctxt)
|
12046
|
167 |
| activate (ctxt, Notes facts) = #1 (ProofContext.have_thmss facts ctxt)
|
12070
|
168 |
| activate (ctxt, Uses name) = activate_locale_i name ctxt
|
11896
|
169 |
|
12070
|
170 |
and activate_elements_i elems ctxt = foldl activate (ctxt, elems)
|
12046
|
171 |
|
12070
|
172 |
and activate_locale_elements (ctxt, name) =
|
12014
|
173 |
let
|
|
174 |
val thy = ProofContext.theory_of ctxt;
|
12063
|
175 |
val {elements, ...} = the_locale thy name; (*exception ERROR*)
|
12014
|
176 |
in
|
12063
|
177 |
activate_elements_i elements ctxt handle ProofContext.CONTEXT (msg, c) =>
|
12014
|
178 |
raise ProofContext.CONTEXT (msg ^ "\nThe error(s) above occurred in locale " ^
|
|
179 |
quote (cond_extern (Theory.sign_of thy) name), c)
|
12070
|
180 |
end
|
12014
|
181 |
|
12070
|
182 |
and activate_locale_i name ctxt =
|
12063
|
183 |
activate_locale_elements (foldl activate_locale_elements
|
|
184 |
(ctxt, #imports (the_locale (ProofContext.theory_of ctxt) name)), name);
|
12046
|
185 |
|
12070
|
186 |
|
|
187 |
fun activate_elements elems ctxt =
|
|
188 |
foldl ((fn (ctxt, elem) => activate (ctxt, read_elem ctxt elem))) (ctxt, elems);
|
|
189 |
|
12046
|
190 |
fun activate_locale xname ctxt =
|
|
191 |
activate_locale_i (intern (ProofContext.sign_of ctxt) xname) ctxt;
|
11896
|
192 |
|
|
193 |
|
|
194 |
|
12070
|
195 |
(** print locale **)
|
|
196 |
|
|
197 |
fun pretty_locale thy xname =
|
|
198 |
let
|
|
199 |
val sg = Theory.sign_of thy;
|
|
200 |
val name = intern sg xname;
|
|
201 |
val {imports, elements, closed = _} = the_locale thy name;
|
|
202 |
val locale_ctxt = ProofContext.init thy |> activate_locale_i name;
|
|
203 |
|
|
204 |
val prt_typ = Pretty.quote o ProofContext.pretty_typ locale_ctxt;
|
|
205 |
val prt_term = Pretty.quote o ProofContext.pretty_term locale_ctxt;
|
|
206 |
val prt_thm = Pretty.quote o ProofContext.pretty_thm locale_ctxt;
|
|
207 |
|
|
208 |
fun prt_syn syn =
|
|
209 |
let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
|
|
210 |
in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
|
|
211 |
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
|
|
212 |
prt_typ T :: Pretty.brk 1 :: prt_syn syn)
|
|
213 |
| prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
|
|
214 |
|
|
215 |
fun prt_asm (("", _), ts) = Pretty.block (Pretty.breaks (map (prt_term o fst) ts))
|
|
216 |
| prt_asm ((a, _), ts) = Pretty.block
|
|
217 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts));
|
|
218 |
fun prt_asms asms = Pretty.block
|
|
219 |
(flat (separate [Pretty.fbrk, Pretty.str "and"] (map (single o prt_asm) asms)));
|
|
220 |
|
|
221 |
fun prt_def (("", _), (t, _)) = Pretty.block [Pretty.brk 1, prt_term t]
|
|
222 |
| prt_def ((a, _), (t, _)) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
|
|
223 |
|
|
224 |
fun prt_fact (("", _), ths) = Pretty.block (Pretty.breaks (map prt_thm (flat (map fst ths))))
|
|
225 |
| prt_fact ((a, _), ths) = Pretty.block
|
|
226 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map prt_thm (flat (map fst ths))));
|
|
227 |
|
|
228 |
fun prt_elem (Fixes fixes) = Pretty.big_list "fixes" (map prt_fix fixes)
|
|
229 |
| prt_elem (Assumes asms) = Pretty.big_list "assumes" (map prt_asm asms)
|
|
230 |
| prt_elem (Defines defs) = Pretty.big_list "defines" (map prt_def defs)
|
|
231 |
| prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts)
|
|
232 |
| prt_elem (Uses name) = Pretty.str ("uses " ^ cond_extern sg name);
|
|
233 |
|
|
234 |
val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
|
|
235 |
(if null imports then [] else
|
|
236 |
(flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) imports)) @
|
|
237 |
[Pretty.str "+"])));
|
|
238 |
in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
|
|
239 |
|
|
240 |
val print_locale = Pretty.writeln oo pretty_locale;
|
|
241 |
|
|
242 |
|
|
243 |
|
11896
|
244 |
(** define locales **)
|
|
245 |
|
12063
|
246 |
(* closeup dangling frees *)
|
|
247 |
|
|
248 |
fun close_frees_wrt ctxt t =
|
|
249 |
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t)))
|
|
250 |
in curry Term.list_all_free frees end;
|
11896
|
251 |
|
12063
|
252 |
fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
|
|
253 |
(a, propps |> map (fn (t, (ps1, ps2)) =>
|
|
254 |
let val close = close_frees_wrt ctxt t in (close t, (map close ps1, map close ps2)) end))))
|
|
255 |
| closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
|
|
256 |
let
|
|
257 |
val t' = ProofContext.cert_def ctxt t;
|
|
258 |
val close = close_frees_wrt ctxt t';
|
|
259 |
in (a, (close t', map close ps)) end))
|
|
260 |
| closeup ctxt elem = elem;
|
11896
|
261 |
|
|
262 |
|
12063
|
263 |
(* add_locale(_i) *)
|
11896
|
264 |
|
12063
|
265 |
fun gen_add_locale prep_locale prep_elem bname raw_imports raw_elems thy =
|
|
266 |
let
|
|
267 |
val sign = Theory.sign_of thy;
|
11896
|
268 |
val name = Sign.full_name sign bname;
|
12063
|
269 |
val _ =
|
|
270 |
if is_none (get_locale thy name) then () else
|
|
271 |
error ("Duplicate definition of locale " ^ quote name);
|
11896
|
272 |
|
12063
|
273 |
val imports = map (prep_locale sign) raw_imports;
|
|
274 |
val imports_ctxt = foldl activate_locale_elements (ProofContext.init thy, imports);
|
|
275 |
fun prep (ctxt, raw_elem) =
|
|
276 |
let val elem = closeup ctxt (prep_elem ctxt raw_elem)
|
|
277 |
in (activate (ctxt, elem), elem) end;
|
|
278 |
val (locale_ctxt, elems) = foldl_map prep (imports_ctxt, raw_elems);
|
|
279 |
in
|
|
280 |
thy
|
|
281 |
|> declare_locale name
|
|
282 |
|> put_locale name (make_locale imports elems false)
|
|
283 |
end;
|
|
284 |
|
|
285 |
val add_locale = gen_add_locale intern read_elem;
|
|
286 |
val add_locale_i = gen_add_locale (K I) (K I);
|
|
287 |
|
11896
|
288 |
|
12063
|
289 |
|
12070
|
290 |
(** store results **)
|
11896
|
291 |
|
12063
|
292 |
fun store_thm name ((a, th), atts) thy =
|
|
293 |
let
|
12070
|
294 |
val {imports, elements, closed} = the_locale thy name;
|
|
295 |
val _ = conditional closed
|
|
296 |
(fn () => error ("Cannot store results in closed locale: " ^ quote name));
|
12063
|
297 |
val note = Notes [((a, atts), [([Thm.name_thm (a, th)], [])])];
|
|
298 |
in
|
12070
|
299 |
activate (ProofContext.init thy |> activate_locale_i name, note); (*test attribute*)
|
|
300 |
thy |> put_locale name (make_locale imports (elements @ [note]) closed)
|
12063
|
301 |
end;
|
11896
|
302 |
|
12063
|
303 |
|
11896
|
304 |
|
|
305 |
(** locale theory setup **)
|
12063
|
306 |
|
11896
|
307 |
val setup =
|
|
308 |
[LocalesData.init];
|
|
309 |
|
|
310 |
end;
|
|
311 |
|
|
312 |
structure BasicLocale: BASIC_LOCALE = Locale;
|
|
313 |
open BasicLocale;
|