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 |
TODO:
|
12063
|
12 |
- 'print_locales' command (also PG menu?);
|
|
13 |
- cert_elem (do *not* cert_def, yet) (!?);
|
|
14 |
- ensure unique defines;
|
|
15 |
- local syntax (mostly in ProofContext);
|
11896
|
16 |
*)
|
|
17 |
|
|
18 |
signature BASIC_LOCALE =
|
|
19 |
sig
|
|
20 |
val print_locales: theory -> unit
|
12063
|
21 |
val print_locale: theory -> xstring -> unit
|
11896
|
22 |
end;
|
|
23 |
|
|
24 |
signature LOCALE =
|
|
25 |
sig
|
|
26 |
include BASIC_LOCALE
|
12046
|
27 |
type context
|
12014
|
28 |
type expression
|
12046
|
29 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
30 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
31 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
32 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
|
33 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list |
|
|
34 |
Uses of expression
|
|
35 |
type 'att element
|
|
36 |
type 'att element_i
|
|
37 |
type locale
|
|
38 |
val intern: Sign.sg -> xstring -> string
|
12014
|
39 |
val cond_extern: Sign.sg -> string -> xstring
|
12063
|
40 |
val attribute: ('att -> context attribute) ->
|
12046
|
41 |
('typ, 'term, 'thm, 'att) elem -> ('typ, 'term, 'thm, context attribute) elem
|
|
42 |
val activate_elements: context attribute element list -> context -> context
|
|
43 |
val activate_elements_i: context attribute element_i list -> context -> context
|
|
44 |
val activate_locale: xstring -> context -> context
|
|
45 |
val activate_locale_i: string -> context -> context
|
12063
|
46 |
val add_locale: bstring -> xstring list -> context attribute element list -> theory -> theory
|
|
47 |
val add_locale_i: bstring -> xstring list -> context attribute element_i list -> theory -> theory
|
|
48 |
val store_thm: string -> (string * thm) * context attribute list -> theory -> theory
|
11896
|
49 |
val setup: (theory -> theory) list
|
|
50 |
end;
|
|
51 |
|
|
52 |
structure Locale: LOCALE =
|
|
53 |
struct
|
|
54 |
|
|
55 |
|
12014
|
56 |
(** locale elements and locales **)
|
11896
|
57 |
|
12014
|
58 |
type context = ProofContext.context;
|
11896
|
59 |
|
12014
|
60 |
type expression = unit; (* FIXME *)
|
11896
|
61 |
|
12046
|
62 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
63 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
64 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
65 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
|
66 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list |
|
12014
|
67 |
Uses of expression;
|
11896
|
68 |
|
12046
|
69 |
type 'att element = (string, string, string, 'att) elem;
|
|
70 |
type 'att element_i = (typ, term, thm list, 'att) elem;
|
12063
|
71 |
type locale = {imports: string list, elements: context attribute element_i list, closed: bool};
|
|
72 |
|
|
73 |
fun make_locale imports elements closed =
|
|
74 |
{imports = imports, elements = elements, closed = closed}: locale;
|
12046
|
75 |
|
|
76 |
|
12014
|
77 |
fun fixes_of_elem (Fixes fixes) = map #1 fixes
|
|
78 |
| fixes_of_elem _ = [];
|
11896
|
79 |
|
12014
|
80 |
fun frees_of_elem _ = []; (* FIXME *)
|
11896
|
81 |
|
12063
|
82 |
(*fun close_locale {imports, elements, closed = _} = make_locale imports elements true;*)
|
|
83 |
fun close_locale x = x; (* FIXME tmp *)
|
|
84 |
|
11896
|
85 |
|
|
86 |
|
|
87 |
(** theory data **)
|
|
88 |
|
|
89 |
(* data kind 'Pure/locales' *)
|
|
90 |
|
|
91 |
structure LocalesArgs =
|
|
92 |
struct
|
12014
|
93 |
val name = "Isar/locales";
|
12063
|
94 |
type T = NameSpace.T * locale Symtab.table;
|
11896
|
95 |
|
12063
|
96 |
val empty = (NameSpace.empty, Symtab.empty);
|
|
97 |
val copy = I;
|
|
98 |
fun prep_ext (space, locales) = (space, Symtab.map close_locale locales);
|
|
99 |
fun merge ((space1, locales1), (space2, locales2)) =
|
|
100 |
(NameSpace.merge (space1, space2), Symtab.merge (K true) (locales1, locales2));
|
11896
|
101 |
|
12063
|
102 |
fun print _ (space, locales) =
|
12014
|
103 |
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locales))
|
|
104 |
|> Pretty.writeln;
|
11896
|
105 |
end;
|
|
106 |
|
|
107 |
structure LocalesData = TheoryDataFun(LocalesArgs);
|
|
108 |
val print_locales = LocalesData.print;
|
|
109 |
|
12063
|
110 |
val intern = NameSpace.intern o #1 o LocalesData.get_sg;
|
|
111 |
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg;
|
12014
|
112 |
|
11896
|
113 |
|
|
114 |
(* access locales *)
|
|
115 |
|
12063
|
116 |
fun declare_locale name =
|
|
117 |
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name]))));
|
11896
|
118 |
|
12063
|
119 |
fun put_locale name locale =
|
|
120 |
LocalesData.map (apsnd (fn locales => Symtab.update ((name, locale), locales)));
|
|
121 |
|
|
122 |
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
|
11896
|
123 |
|
12014
|
124 |
fun the_locale thy name =
|
|
125 |
(case get_locale thy name of
|
|
126 |
Some loc => loc
|
|
127 |
| None => error ("Unknown locale " ^ quote name));
|
11896
|
128 |
|
|
129 |
|
12058
|
130 |
(* print locales *) (* FIXME activate local syntax *)
|
12014
|
131 |
|
|
132 |
fun pretty_locale thy xname =
|
|
133 |
let
|
|
134 |
val sg = Theory.sign_of thy;
|
|
135 |
val name = intern sg xname;
|
12063
|
136 |
val {imports, elements, closed = _} = the_locale thy name;
|
12014
|
137 |
|
|
138 |
val prt_typ = Pretty.quote o Sign.pretty_typ sg;
|
|
139 |
val prt_term = Pretty.quote o Sign.pretty_term sg;
|
|
140 |
|
|
141 |
fun prt_syn syn =
|
|
142 |
let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
|
|
143 |
in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
|
12058
|
144 |
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
|
|
145 |
prt_typ T :: Pretty.brk 1 :: prt_syn syn)
|
|
146 |
| prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
|
12014
|
147 |
|
|
148 |
fun prt_asm ((a, _), ts) = Pretty.block
|
|
149 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts));
|
|
150 |
fun prt_asms asms = Pretty.block
|
|
151 |
(flat (separate [Pretty.fbrk, Pretty.str "and"] (map (single o prt_asm) asms)));
|
|
152 |
|
|
153 |
fun prt_def ((a, _), (t, _)) = Pretty.block
|
|
154 |
[Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
|
|
155 |
|
|
156 |
fun prt_fact ((a, _), ths) = Pretty.block
|
|
157 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map Display.pretty_thm (flat (map fst ths))));
|
|
158 |
|
|
159 |
fun prt_elem (Fixes fixes) = Pretty.big_list "fixes" (map prt_fix fixes)
|
|
160 |
| prt_elem (Assumes asms) = Pretty.big_list "assumes" (map prt_asm asms)
|
|
161 |
| prt_elem (Defines defs) = Pretty.big_list "defines" (map prt_def defs)
|
|
162 |
| prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts)
|
|
163 |
| prt_elem (Uses _) = Pretty.str "FIXME";
|
|
164 |
|
|
165 |
val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
|
12063
|
166 |
(if null imports then [] else
|
|
167 |
(flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) imports)) @
|
12014
|
168 |
[Pretty.str "+"])));
|
|
169 |
in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
|
|
170 |
|
|
171 |
val print_locale = Pretty.writeln oo pretty_locale;
|
11896
|
172 |
|
|
173 |
|
12046
|
174 |
|
12063
|
175 |
(** internalize elements **)
|
|
176 |
|
|
177 |
(* read_elem *)
|
12046
|
178 |
|
12063
|
179 |
fun read_elem ctxt =
|
|
180 |
fn Fixes fixes =>
|
|
181 |
let val vars =
|
|
182 |
#2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
|
|
183 |
in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
|
|
184 |
| Assumes asms =>
|
|
185 |
Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
|
|
186 |
| Defines defs =>
|
|
187 |
let val propps =
|
|
188 |
#2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
|
|
189 |
in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
|
|
190 |
| Notes facts =>
|
|
191 |
Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts)
|
|
192 |
| Uses FIXME => Uses FIXME;
|
|
193 |
|
|
194 |
|
|
195 |
(* prepare attributes *)
|
|
196 |
|
|
197 |
local fun int_att attrib (x, srcs) = (x, map attrib srcs) in
|
|
198 |
|
|
199 |
fun attribute _ (Fixes fixes) = Fixes fixes
|
|
200 |
| attribute attrib (Assumes asms) = Assumes (map (apfst (int_att attrib)) asms)
|
|
201 |
| attribute attrib (Defines defs) = Defines (map (apfst (int_att attrib)) defs)
|
|
202 |
| attribute attrib (Notes facts) =
|
12046
|
203 |
Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts)
|
12063
|
204 |
| attribute _ (Uses FIXME) = Uses FIXME;
|
|
205 |
|
|
206 |
end;
|
12046
|
207 |
|
|
208 |
|
11896
|
209 |
|
12014
|
210 |
(** activate locales **)
|
11896
|
211 |
|
12063
|
212 |
(* activatation primitive *)
|
12046
|
213 |
|
|
214 |
fun activate (ctxt, Fixes fixes) =
|
12058
|
215 |
ProofContext.fix_direct (map (fn (x, T, FIXME) => ([x], T)) fixes) ctxt
|
|
216 |
| activate (ctxt, Assumes asms) =
|
|
217 |
ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
|
|
218 |
|> ProofContext.assume_i ProofContext.export_assume asms |> #1
|
12046
|
219 |
| activate (ctxt, Defines defs) = #1 (ProofContext.assume_i ProofContext.export_def
|
12058
|
220 |
(map (fn (a, (t, ps)) => (a, [(ProofContext.cert_def ctxt t, (ps, []))])) defs) ctxt)
|
12046
|
221 |
| activate (ctxt, Notes facts) = #1 (ProofContext.have_thmss facts ctxt)
|
|
222 |
| activate (ctxt, Uses FIXME) = ctxt;
|
11896
|
223 |
|
12063
|
224 |
|
|
225 |
(* activate operations *)
|
11896
|
226 |
|
12046
|
227 |
fun activate_elements_i elems ctxt = foldl activate (ctxt, elems);
|
12063
|
228 |
fun activate_elements elems ctxt =
|
|
229 |
foldl ((fn (ctxt, elem) => activate (ctxt, read_elem ctxt elem))) (ctxt, elems);
|
12046
|
230 |
|
12063
|
231 |
fun activate_locale_elements (ctxt, name) =
|
12014
|
232 |
let
|
|
233 |
val thy = ProofContext.theory_of ctxt;
|
12063
|
234 |
val {elements, ...} = the_locale thy name; (*exception ERROR*)
|
12014
|
235 |
in
|
12063
|
236 |
activate_elements_i elements ctxt handle ProofContext.CONTEXT (msg, c) =>
|
12014
|
237 |
raise ProofContext.CONTEXT (msg ^ "\nThe error(s) above occurred in locale " ^
|
|
238 |
quote (cond_extern (Theory.sign_of thy) name), c)
|
|
239 |
end;
|
|
240 |
|
12046
|
241 |
fun activate_locale_i name ctxt =
|
12063
|
242 |
activate_locale_elements (foldl activate_locale_elements
|
|
243 |
(ctxt, #imports (the_locale (ProofContext.theory_of ctxt) name)), name);
|
12046
|
244 |
|
|
245 |
fun activate_locale xname ctxt =
|
|
246 |
activate_locale_i (intern (ProofContext.sign_of ctxt) xname) ctxt;
|
11896
|
247 |
|
|
248 |
|
|
249 |
|
|
250 |
(** define locales **)
|
|
251 |
|
12063
|
252 |
(* closeup dangling frees *)
|
|
253 |
|
|
254 |
fun close_frees_wrt ctxt t =
|
|
255 |
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t)))
|
|
256 |
in curry Term.list_all_free frees end;
|
11896
|
257 |
|
12063
|
258 |
fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
|
|
259 |
(a, propps |> map (fn (t, (ps1, ps2)) =>
|
|
260 |
let val close = close_frees_wrt ctxt t in (close t, (map close ps1, map close ps2)) end))))
|
|
261 |
| closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
|
|
262 |
let
|
|
263 |
val t' = ProofContext.cert_def ctxt t;
|
|
264 |
val close = close_frees_wrt ctxt t';
|
|
265 |
in (a, (close t', map close ps)) end))
|
|
266 |
| closeup ctxt elem = elem;
|
11896
|
267 |
|
|
268 |
|
12063
|
269 |
(* add_locale(_i) *)
|
11896
|
270 |
|
12063
|
271 |
fun gen_add_locale prep_locale prep_elem bname raw_imports raw_elems thy =
|
|
272 |
let
|
|
273 |
val sign = Theory.sign_of thy;
|
11896
|
274 |
val name = Sign.full_name sign bname;
|
12063
|
275 |
val _ =
|
|
276 |
if is_none (get_locale thy name) then () else
|
|
277 |
error ("Duplicate definition of locale " ^ quote name);
|
11896
|
278 |
|
12063
|
279 |
val imports = map (prep_locale sign) raw_imports;
|
|
280 |
val imports_ctxt = foldl activate_locale_elements (ProofContext.init thy, imports);
|
|
281 |
fun prep (ctxt, raw_elem) =
|
|
282 |
let val elem = closeup ctxt (prep_elem ctxt raw_elem)
|
|
283 |
in (activate (ctxt, elem), elem) end;
|
|
284 |
val (locale_ctxt, elems) = foldl_map prep (imports_ctxt, raw_elems);
|
|
285 |
in
|
|
286 |
thy
|
|
287 |
|> declare_locale name
|
|
288 |
|> put_locale name (make_locale imports elems false)
|
|
289 |
end;
|
|
290 |
|
|
291 |
val add_locale = gen_add_locale intern read_elem;
|
|
292 |
val add_locale_i = gen_add_locale (K I) (K I);
|
|
293 |
|
11896
|
294 |
|
12063
|
295 |
|
|
296 |
(** store results **) (* FIXME test atts!? *)
|
11896
|
297 |
|
12063
|
298 |
fun store_thm name ((a, th), atts) thy =
|
|
299 |
let
|
|
300 |
val note = Notes [((a, atts), [([Thm.name_thm (a, th)], [])])];
|
|
301 |
val {imports, elements, closed} = the_locale thy name;
|
|
302 |
in
|
|
303 |
if closed then error ("Cannot store results in closed locale: " ^ quote name)
|
|
304 |
else thy |> put_locale name (make_locale imports (elements @ [note]) closed)
|
|
305 |
end;
|
11896
|
306 |
|
12063
|
307 |
|
|
308 |
(* FIXME old
|
|
309 |
|
11896
|
310 |
val mx = Syntax.fix_mixfix raw_c raw_mx;
|
|
311 |
val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
|
|
312 |
error ("The error(s) above occured in locale constant " ^ quote c);
|
|
313 |
val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
|
|
314 |
in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
|
|
315 |
|
12014
|
316 |
val (envS0, loc_fixes_syn) = foldl_map prep_const (envSb, raw_fixes);
|
|
317 |
val loc_fixes = map #1 loc_fixes_syn;
|
|
318 |
val loc_fixes = old_loc_fixes @ loc_fixes;
|
|
319 |
val loc_syn = map #2 loc_fixes_syn;
|
|
320 |
val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_fixes_syn));
|
|
321 |
val loc_trfuns = mapfilter #3 loc_fixes_syn;
|
11896
|
322 |
|
|
323 |
val syntax_thy =
|
|
324 |
thy
|
|
325 |
|> Theory.add_modesyntax_i ("", true) loc_syn
|
|
326 |
|> Theory.add_trfuns ([], loc_trfuns, [], []);
|
|
327 |
|
12014
|
328 |
(* check if definientes are locale constants
|
11896
|
329 |
(in the same locale, so no redefining!) *)
|
|
330 |
val err_def_head =
|
12014
|
331 |
let fun peal_appl t =
|
|
332 |
case t of
|
11896
|
333 |
t1 $ t2 => peal_appl t1
|
|
334 |
| Free(t) => t
|
|
335 |
| _ => locale_error ("Bad form of LHS in locale definition");
|
12014
|
336 |
fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
|
|
337 |
| lhs _ = locale_error ("Definitions must use the == relation");
|
11896
|
338 |
val defs = map lhs loc_defs;
|
12014
|
339 |
val check = defs subset loc_fixes
|
|
340 |
in if check then []
|
11896
|
341 |
else ["defined item not declared fixed in locale " ^ quote name]
|
12014
|
342 |
end;
|
11896
|
343 |
|
|
344 |
(* check that variables on rhs of definitions are either fixed or on lhs *)
|
12014
|
345 |
val err_var_rhs =
|
|
346 |
let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
|
|
347 |
let val varl1 = difflist d1 all_loc_fixes;
|
|
348 |
val varl2 = difflist d2 all_loc_fixes
|
|
349 |
in t andalso (varl2 subset varl1)
|
|
350 |
end
|
|
351 |
| compare_var_sides (_,_) =
|
|
352 |
locale_error ("Definitions must use the == relation")
|
11896
|
353 |
val check = foldl compare_var_sides (true, loc_defs)
|
|
354 |
in if check then []
|
|
355 |
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
|
|
356 |
end;
|
12014
|
357 |
*)
|
11896
|
358 |
|
|
359 |
|
|
360 |
(** locale theory setup **)
|
12063
|
361 |
|
11896
|
362 |
val setup =
|
|
363 |
[LocalesData.init];
|
|
364 |
|
|
365 |
end;
|
|
366 |
|
|
367 |
structure BasicLocale: BASIC_LOCALE = Locale;
|
|
368 |
open BasicLocale;
|