12014
|
1 |
(* Title: Pure/Isar/locale.ML
|
11896
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
4 |
Author: Markus Wenzel, TU Muenchen
|
|
5 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
6 |
|
12014
|
7 |
Locales. The theory section 'locale' declarings constants, assumptions
|
|
8 |
and definitions that have local scope.
|
11896
|
9 |
|
|
10 |
TODO:
|
12014
|
11 |
- reset scope context on qed of legacy goal (!??);
|
12046
|
12 |
- implicit closure of ``loose'' free vars;
|
|
13 |
- avoid dynamic scoping of facts/atts
|
|
14 |
(use thms_closure for globals, even within att expressions);
|
|
15 |
- scope of implicit fixed in elementents vs. locales (!??);
|
|
16 |
- Fixes: optional type (!?);
|
11896
|
17 |
*)
|
|
18 |
|
|
19 |
signature BASIC_LOCALE =
|
|
20 |
sig
|
|
21 |
val print_locales: theory -> unit
|
|
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 =
|
|
30 |
Fixes of (string * 'typ * mixfix option) list |
|
|
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
|
12046
|
40 |
val intern_att: ('att -> context attribute) ->
|
|
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
|
12014
|
46 |
(*
|
|
47 |
val add_locale: bstring -> xstring option -> (string * string * mixfix) list ->
|
12046
|
48 |
((string * context attribute list) * string) list ->
|
|
49 |
((string * context attribute list) * string) list -> theory -> theory
|
12014
|
50 |
val add_locale_i: bstring -> xstring option -> (string * typ * mixfix) list ->
|
12046
|
51 |
((string * context attribute list) * term) list ->
|
|
52 |
((string * context attribute list) * term) list -> theory -> theory
|
12014
|
53 |
val read_prop_schematic: Sign.sg -> string -> cterm
|
|
54 |
*)
|
11896
|
55 |
val setup: (theory -> theory) list
|
|
56 |
end;
|
|
57 |
|
|
58 |
structure Locale: LOCALE =
|
|
59 |
struct
|
|
60 |
|
|
61 |
|
12014
|
62 |
(** locale elements and locales **)
|
11896
|
63 |
|
12014
|
64 |
type context = ProofContext.context;
|
11896
|
65 |
|
12014
|
66 |
type expression = unit; (* FIXME *)
|
11896
|
67 |
|
12046
|
68 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12014
|
69 |
Fixes of (string * 'typ * mixfix option) list |
|
12046
|
70 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
71 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
|
72 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list |
|
12014
|
73 |
Uses of expression;
|
11896
|
74 |
|
12046
|
75 |
type 'att element = (string, string, string, 'att) elem;
|
|
76 |
type 'att element_i = (typ, term, thm list, 'att) elem;
|
|
77 |
type locale = (thm -> string) * string list * context attribute element_i list;
|
|
78 |
|
|
79 |
|
12014
|
80 |
fun fixes_of_elem (Fixes fixes) = map #1 fixes
|
|
81 |
| fixes_of_elem _ = [];
|
11896
|
82 |
|
12014
|
83 |
fun frees_of_elem _ = []; (* FIXME *)
|
11896
|
84 |
|
|
85 |
|
|
86 |
|
|
87 |
(** theory data **)
|
|
88 |
|
|
89 |
(* data kind 'Pure/locales' *)
|
|
90 |
|
|
91 |
type locale_data =
|
|
92 |
{space: NameSpace.T,
|
|
93 |
locales: locale Symtab.table,
|
12046
|
94 |
scope: ((string * locale) list * context option) ref};
|
11896
|
95 |
|
|
96 |
fun make_locale_data space locales scope =
|
|
97 |
{space = space, locales = locales, scope = scope}: locale_data;
|
|
98 |
|
12014
|
99 |
val empty_scope = ([], None);
|
|
100 |
|
11896
|
101 |
structure LocalesArgs =
|
|
102 |
struct
|
12014
|
103 |
val name = "Isar/locales";
|
11896
|
104 |
type T = locale_data;
|
|
105 |
|
12014
|
106 |
val empty = make_locale_data NameSpace.empty Symtab.empty (ref empty_scope);
|
|
107 |
fun copy {space, locales, scope = ref r} = make_locale_data space locales (ref r);
|
|
108 |
fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref empty_scope);
|
11896
|
109 |
fun merge ({space = space1, locales = locales1, scope = _},
|
|
110 |
{space = space2, locales = locales2, scope = _}) =
|
|
111 |
make_locale_data (NameSpace.merge (space1, space2))
|
12014
|
112 |
(Symtab.merge (K true) (locales1, locales2)) (ref empty_scope);
|
11896
|
113 |
|
12014
|
114 |
fun print _ {space, locales, scope = _} =
|
|
115 |
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locales))
|
|
116 |
|> Pretty.writeln;
|
11896
|
117 |
end;
|
|
118 |
|
|
119 |
structure LocalesData = TheoryDataFun(LocalesArgs);
|
|
120 |
val print_locales = LocalesData.print;
|
|
121 |
|
12014
|
122 |
val intern = NameSpace.intern o #space o LocalesData.get_sg;
|
|
123 |
val cond_extern = NameSpace.cond_extern o #space o LocalesData.get_sg;
|
|
124 |
|
11896
|
125 |
|
|
126 |
(* access locales *)
|
|
127 |
|
|
128 |
fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
|
|
129 |
val get_locale = get_locale_sg o Theory.sign_of;
|
|
130 |
|
12014
|
131 |
fun put_locale (name, locale) = LocalesData.map (fn {space, locales, scope} =>
|
|
132 |
make_locale_data (NameSpace.extend (space, [name]))
|
|
133 |
(Symtab.update ((name, locale), locales)) scope);
|
11896
|
134 |
|
12014
|
135 |
fun the_locale thy name =
|
|
136 |
(case get_locale thy name of
|
|
137 |
Some loc => loc
|
|
138 |
| None => error ("Unknown locale " ^ quote name));
|
11896
|
139 |
|
|
140 |
|
|
141 |
(* access scope *)
|
|
142 |
|
|
143 |
fun get_scope_sg sg =
|
12014
|
144 |
if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then empty_scope
|
11896
|
145 |
else ! (#scope (LocalesData.get_sg sg));
|
|
146 |
|
|
147 |
val get_scope = get_scope_sg o Theory.sign_of;
|
12014
|
148 |
val nonempty_scope_sg = not o null o #1 o get_scope_sg;
|
11896
|
149 |
|
|
150 |
fun change_scope f thy =
|
|
151 |
let val {scope, ...} = LocalesData.get thy
|
12014
|
152 |
in scope := f (! scope); thy end;
|
|
153 |
|
|
154 |
fun print_scope thy =
|
|
155 |
Pretty.writeln (Pretty.strs ("current scope:" ::
|
|
156 |
rev (map (cond_extern (Theory.sign_of thy) o #1) (#1 (get_scope thy)))));
|
|
157 |
|
|
158 |
|
|
159 |
(* print locales *)
|
|
160 |
|
|
161 |
fun pretty_locale thy xname =
|
|
162 |
let
|
|
163 |
val sg = Theory.sign_of thy;
|
|
164 |
val name = intern sg xname;
|
12046
|
165 |
val (_, ancestors, elements) = the_locale thy name;
|
12014
|
166 |
|
|
167 |
val prt_typ = Pretty.quote o Sign.pretty_typ sg;
|
|
168 |
val prt_term = Pretty.quote o Sign.pretty_term sg;
|
|
169 |
|
|
170 |
fun prt_syn syn =
|
|
171 |
let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
|
|
172 |
in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
|
|
173 |
fun prt_fix (x, T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
|
|
174 |
prt_typ T :: Pretty.brk 1 :: prt_syn syn);
|
|
175 |
|
|
176 |
fun prt_asm ((a, _), ts) = Pretty.block
|
|
177 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts));
|
|
178 |
fun prt_asms asms = Pretty.block
|
|
179 |
(flat (separate [Pretty.fbrk, Pretty.str "and"] (map (single o prt_asm) asms)));
|
|
180 |
|
|
181 |
fun prt_def ((a, _), (t, _)) = Pretty.block
|
|
182 |
[Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
|
|
183 |
|
|
184 |
fun prt_fact ((a, _), ths) = Pretty.block
|
|
185 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map Display.pretty_thm (flat (map fst ths))));
|
|
186 |
|
|
187 |
fun prt_elem (Fixes fixes) = Pretty.big_list "fixes" (map prt_fix fixes)
|
|
188 |
| prt_elem (Assumes asms) = Pretty.big_list "assumes" (map prt_asm asms)
|
|
189 |
| prt_elem (Defines defs) = Pretty.big_list "defines" (map prt_def defs)
|
|
190 |
| prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts)
|
|
191 |
| prt_elem (Uses _) = Pretty.str "FIXME";
|
|
192 |
|
|
193 |
val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
|
|
194 |
(if null ancestors then [] else
|
|
195 |
(flat (separate [Pretty.str "+", Pretty.brk 1] (map (single o Pretty.str) ancestors)) @
|
|
196 |
[Pretty.str "+"])));
|
|
197 |
in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elements)) end;
|
|
198 |
|
|
199 |
val print_locale = Pretty.writeln oo pretty_locale;
|
11896
|
200 |
|
|
201 |
|
12046
|
202 |
(** internalization of theorems and attributes **)
|
|
203 |
|
|
204 |
fun int_att attrib (x, srcs) = (x, map attrib srcs);
|
|
205 |
|
|
206 |
fun intern_att _ (Fixes fixes) = Fixes fixes
|
|
207 |
| intern_att attrib (Assumes asms) = Assumes (map (apfst (int_att attrib)) asms)
|
|
208 |
| intern_att attrib (Defines defs) = Defines (map (apfst (int_att attrib)) defs)
|
|
209 |
| intern_att attrib (Notes facts) =
|
|
210 |
Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts)
|
|
211 |
| intern_att _ (Uses FIXME) = Uses FIXME;
|
|
212 |
|
|
213 |
|
11896
|
214 |
|
12014
|
215 |
(** activate locales **)
|
11896
|
216 |
|
12014
|
217 |
(* FIXME old
|
|
218 |
fun pack_def eq =
|
|
219 |
let
|
|
220 |
val (lhs, rhs) = Logic.dest_equals eq;
|
|
221 |
val (f, xs) = Term.strip_comb lhs;
|
|
222 |
in (xs, Logic.mk_equals (f, foldr (uncurry lambda) (xs, rhs))) end;
|
11896
|
223 |
|
12014
|
224 |
fun unpack_def xs thm =
|
|
225 |
let
|
|
226 |
val cxs = map (Thm.cterm_of (Thm.sign_of_thm thm)) xs;
|
|
227 |
fun unpack (th, cx) =
|
|
228 |
Thm.combination th (Thm.reflexive cx)
|
|
229 |
|> MetaSimplifier.fconv_rule (Thm.beta_conversion true);
|
|
230 |
in foldl unpack (thm, cxs) end;
|
11896
|
231 |
|
12014
|
232 |
fun prep_def ((name, atts), eq) =
|
|
233 |
let val (xs, eq') = pack_def eq
|
|
234 |
in ((name, Drule.rule_attribute (K (unpack_def xs)) :: atts), [(eq', ([], []))]) end;
|
|
235 |
*)
|
11896
|
236 |
|
12046
|
237 |
fun read_elem closure ctxt =
|
|
238 |
fn (Fixes fixes) =>
|
|
239 |
let val vars =
|
|
240 |
#2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], Some T)) fixes))
|
|
241 |
in Fixes (map2 (fn (([x'], Some T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
|
|
242 |
| (Assumes asms) =>
|
|
243 |
Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
|
|
244 |
| (Defines defs) =>
|
|
245 |
let val propps =
|
|
246 |
#2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
|
|
247 |
in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
|
|
248 |
| (Notes facts) =>
|
|
249 |
Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts)
|
|
250 |
| (Uses FIXME) => Uses FIXME;
|
11896
|
251 |
|
12046
|
252 |
|
|
253 |
fun activate (ctxt, Fixes fixes) =
|
|
254 |
ProofContext.fix_direct (map (fn (x, T, FIXME) => ([x], Some T)) fixes) ctxt
|
|
255 |
| activate (ctxt, Assumes asms) = #1 (ProofContext.assume_i ProofContext.export_assume asms ctxt)
|
|
256 |
| activate (ctxt, Defines defs) = #1 (ProofContext.assume_i ProofContext.export_def
|
|
257 |
(map (fn (a, (t, ps)) => (a, [(t, (ps, []))])) defs) ctxt)
|
|
258 |
| activate (ctxt, Notes facts) = #1 (ProofContext.have_thmss facts ctxt)
|
|
259 |
| activate (ctxt, Uses FIXME) = ctxt;
|
11896
|
260 |
|
12046
|
261 |
(* FIXME closure? *)
|
|
262 |
fun read_activate (ctxt, elem) =
|
|
263 |
let val elem' = read_elem (PureThy.get_thms (ProofContext.theory_of ctxt)) ctxt elem
|
|
264 |
in (activate (ctxt, elem'), elem') end;
|
11896
|
265 |
|
12046
|
266 |
fun activate_elements_i elems ctxt = foldl activate (ctxt, elems);
|
|
267 |
fun activate_elements elems ctxt = foldl (#1 o read_activate) (ctxt, elems);
|
|
268 |
|
|
269 |
fun with_locale f name ctxt =
|
12014
|
270 |
let
|
|
271 |
val thy = ProofContext.theory_of ctxt;
|
12046
|
272 |
val locale = the_locale thy name;
|
12014
|
273 |
in
|
12046
|
274 |
f locale ctxt handle ProofContext.CONTEXT (msg, c) =>
|
12014
|
275 |
raise ProofContext.CONTEXT (msg ^ "\nThe error(s) above occurred in locale " ^
|
|
276 |
quote (cond_extern (Theory.sign_of thy) name), c)
|
|
277 |
end;
|
|
278 |
|
12046
|
279 |
val activate_locale_elements = with_locale (activate_elements_i o #3);
|
|
280 |
|
|
281 |
fun activate_locale_ancestors name ctxt =
|
|
282 |
foldl (fn (c, es) => activate_locale_elements es c)
|
|
283 |
(ctxt, #2 (the_locale (ProofContext.theory_of ctxt) name));
|
|
284 |
|
|
285 |
fun activate_locale_i name ctxt =
|
|
286 |
ctxt |> activate_locale_ancestors name |> activate_locale_elements name;
|
|
287 |
|
|
288 |
fun activate_locale xname ctxt =
|
|
289 |
activate_locale_i (intern (ProofContext.sign_of ctxt) xname) ctxt;
|
11896
|
290 |
|
|
291 |
|
|
292 |
|
12014
|
293 |
(* FIXME
|
11896
|
294 |
(** define locales **)
|
|
295 |
|
|
296 |
(* prepare types *)
|
|
297 |
|
|
298 |
fun read_typ sg (envT, s) =
|
|
299 |
let
|
|
300 |
fun def_sort (x, ~1) = assoc (envT, x)
|
|
301 |
| def_sort _ = None;
|
|
302 |
val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
|
|
303 |
in (Term.add_typ_tfrees (T, envT), T) end;
|
|
304 |
|
|
305 |
fun cert_typ sg (envT, raw_T) =
|
|
306 |
let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
|
|
307 |
in (Term.add_typ_tfrees (T, envT), T) end;
|
|
308 |
|
|
309 |
|
|
310 |
(* prepare props *)
|
|
311 |
|
|
312 |
(* Bind a term with !! over a list of "free" Free's.
|
|
313 |
To enable definitions like x + y == .... (without quantifier).
|
|
314 |
Complications, because x and y have to be removed from defaults *)
|
|
315 |
fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
|
|
316 |
let val diffl = rev(difflist term clist);
|
|
317 |
fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
|
|
318 |
| abs_o (_ , _) = error ("Can't be: abs_over_free");
|
|
319 |
val diffl' = map (fn (Free (s, T)) => s) diffl;
|
|
320 |
val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
|
|
321 |
in (defaults', (s, foldl abs_o (term, diffl))) end;
|
|
322 |
|
|
323 |
(* assume a definition, i.e assume the cterm of a definiton term and then eliminate
|
|
324 |
the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
|
|
325 |
fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
|
|
326 |
|
|
327 |
|
|
328 |
(* concrete syntax *)
|
|
329 |
|
|
330 |
fun mark_syn c = "\\<^locale>" ^ c;
|
|
331 |
|
|
332 |
fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
|
|
333 |
|
|
334 |
|
|
335 |
(* add_locale *)
|
|
336 |
|
12014
|
337 |
fun gen_add_locale prep_typ prep_term bname bpar raw_fixes raw_assumes raw_defs thy =
|
11896
|
338 |
let val sign = Theory.sign_of thy;
|
|
339 |
|
|
340 |
val name = Sign.full_name sign bname;
|
|
341 |
|
12014
|
342 |
val (envSb, old_loc_fixes, _) =
|
|
343 |
case bpar of
|
|
344 |
Some loc => (get_defaults thy loc)
|
11896
|
345 |
| None => ([],[],[]);
|
|
346 |
|
12014
|
347 |
val old_nosyn = case bpar of
|
|
348 |
Some loc => #nosyn(#2(the_locale thy loc))
|
11896
|
349 |
| None => [];
|
|
350 |
|
12014
|
351 |
(* Get the full name of the parent *)
|
|
352 |
val parent = case bparent of
|
|
353 |
Some loc => Some(#1(the_locale thy loc))
|
11896
|
354 |
| None => None;
|
|
355 |
|
12014
|
356 |
(* prepare locale fixes *)
|
11896
|
357 |
|
|
358 |
fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
|
|
359 |
let
|
|
360 |
val c = Syntax.const_name raw_c raw_mx;
|
|
361 |
val c_syn = mark_syn c;
|
|
362 |
val mx = Syntax.fix_mixfix raw_c raw_mx;
|
|
363 |
val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
|
|
364 |
error ("The error(s) above occured in locale constant " ^ quote c);
|
|
365 |
val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
|
|
366 |
in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
|
|
367 |
|
12014
|
368 |
val (envS0, loc_fixes_syn) = foldl_map prep_const (envSb, raw_fixes);
|
|
369 |
val loc_fixes = map #1 loc_fixes_syn;
|
|
370 |
val loc_fixes = old_loc_fixes @ loc_fixes;
|
|
371 |
val loc_syn = map #2 loc_fixes_syn;
|
|
372 |
val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_fixes_syn));
|
|
373 |
val loc_trfuns = mapfilter #3 loc_fixes_syn;
|
11896
|
374 |
|
|
375 |
|
|
376 |
(* 1st stage: syntax_thy *)
|
|
377 |
|
|
378 |
val syntax_thy =
|
|
379 |
thy
|
|
380 |
|> Theory.add_modesyntax_i ("", true) loc_syn
|
|
381 |
|> Theory.add_trfuns ([], loc_trfuns, [], []);
|
|
382 |
|
|
383 |
val syntax_sign = Theory.sign_of syntax_thy;
|
|
384 |
|
|
385 |
|
12014
|
386 |
(* prepare assumes and defs *)
|
11896
|
387 |
|
|
388 |
fun prep_axiom (env, (a, raw_t)) =
|
|
389 |
let
|
|
390 |
val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
|
|
391 |
error ("The error(s) above occured in locale rule / definition " ^ quote a);
|
|
392 |
in (env', (a, t)) end;
|
|
393 |
|
12014
|
394 |
val ((envS1, envT1, used1), loc_assumes) =
|
|
395 |
foldl_map prep_axiom ((envS0, loc_fixes, map fst envS0), raw_assumes);
|
|
396 |
val (defaults, loc_defs) =
|
|
397 |
foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
|
11896
|
398 |
|
12014
|
399 |
val old_loc_fixes = collect_fixes syntax_sign;
|
|
400 |
val new_loc_fixes = (map #1 loc_fixes);
|
|
401 |
val all_loc_fixes = old_loc_fixes @ new_loc_fixes;
|
11896
|
402 |
|
12014
|
403 |
val (defaults, loc_defs_terms) =
|
|
404 |
foldl_map (abs_over_free all_loc_fixes) (defaults, loc_defs);
|
|
405 |
val loc_defs_thms =
|
|
406 |
map (apsnd (prep_hyps (map #1 loc_fixes) syntax_sign)) loc_defs_terms;
|
|
407 |
val (defaults, loc_thms_terms) =
|
|
408 |
foldl_map (abs_over_free all_loc_fixes) (defaults, loc_assumes);
|
|
409 |
val loc_thms = map (apsnd (prep_hyps (map #1 loc_fixes) syntax_sign))
|
|
410 |
(loc_thms_terms)
|
11896
|
411 |
@ loc_defs_thms;
|
|
412 |
|
|
413 |
|
12014
|
414 |
(* error messages *)
|
11896
|
415 |
|
|
416 |
fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
|
|
417 |
|
|
418 |
val err_dup_locale =
|
|
419 |
if is_none (get_locale thy name) then []
|
|
420 |
else ["Duplicate definition of locale " ^ quote name];
|
|
421 |
|
12014
|
422 |
(* check if definientes are locale constants
|
11896
|
423 |
(in the same locale, so no redefining!) *)
|
|
424 |
val err_def_head =
|
12014
|
425 |
let fun peal_appl t =
|
|
426 |
case t of
|
11896
|
427 |
t1 $ t2 => peal_appl t1
|
|
428 |
| Free(t) => t
|
|
429 |
| _ => locale_error ("Bad form of LHS in locale definition");
|
12014
|
430 |
fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
|
|
431 |
| lhs _ = locale_error ("Definitions must use the == relation");
|
11896
|
432 |
val defs = map lhs loc_defs;
|
12014
|
433 |
val check = defs subset loc_fixes
|
|
434 |
in if check then []
|
11896
|
435 |
else ["defined item not declared fixed in locale " ^ quote name]
|
12014
|
436 |
end;
|
11896
|
437 |
|
|
438 |
(* check that variables on rhs of definitions are either fixed or on lhs *)
|
12014
|
439 |
val err_var_rhs =
|
|
440 |
let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
|
|
441 |
let val varl1 = difflist d1 all_loc_fixes;
|
|
442 |
val varl2 = difflist d2 all_loc_fixes
|
|
443 |
in t andalso (varl2 subset varl1)
|
|
444 |
end
|
|
445 |
| compare_var_sides (_,_) =
|
|
446 |
locale_error ("Definitions must use the == relation")
|
11896
|
447 |
val check = foldl compare_var_sides (true, loc_defs)
|
|
448 |
in if check then []
|
|
449 |
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
|
|
450 |
end;
|
|
451 |
|
|
452 |
val errs = err_dup_locale @ err_def_head @ err_var_rhs;
|
|
453 |
in
|
|
454 |
if null errs then ()
|
|
455 |
else error (cat_lines errs);
|
|
456 |
|
|
457 |
syntax_thy
|
12014
|
458 |
|> put_locale (name,
|
|
459 |
make_locale parent loc_fixes nosyn loc_thms_terms
|
11896
|
460 |
loc_defs_terms loc_thms defaults)
|
|
461 |
end;
|
|
462 |
|
|
463 |
|
|
464 |
val add_locale = gen_add_locale read_typ read_axm;
|
|
465 |
val add_locale_i = gen_add_locale cert_typ cert_axm;
|
|
466 |
|
12014
|
467 |
|
|
468 |
|
|
469 |
(*
|
|
470 |
(** support for legacy proof scripts (cf. goals.ML) **) (* FIXME move to goals.ML (!?) *)
|
|
471 |
|
|
472 |
(* hyps_in_scope *)
|
|
473 |
|
|
474 |
fun hyps_in_scope sg hyps =
|
|
475 |
let val locs = map #2 (#1 (get_scope_sg sg))
|
|
476 |
in gen_subset Term.aconv (hyps, map #2 (flat (map #assumes locs @ map #defines locs))) end;
|
|
477 |
|
11896
|
478 |
|
12014
|
479 |
(* get theorems *)
|
11896
|
480 |
|
12014
|
481 |
fun thmx get_local get_global name =
|
|
482 |
let val thy = Context.the_context () in
|
|
483 |
(case #2 (get_scope thy) of
|
|
484 |
None => get_global thy name
|
|
485 |
| Some ctxt => get_local ctxt name)
|
|
486 |
end;
|
|
487 |
|
|
488 |
val thm = thmx ProofContext.get_thm PureThy.get_thm;
|
|
489 |
val thms = thmx ProofContext.get_thms PureThy.get_thms;
|
11896
|
490 |
|
|
491 |
|
12014
|
492 |
(** scope operations -- for old-style goals **) (* FIXME move to goals.ML (!?) *)
|
|
493 |
|
|
494 |
(* open *)
|
|
495 |
|
|
496 |
local
|
|
497 |
|
|
498 |
fun is_open thy name = exists (equal name o #1) (#1 (get_scope thy));
|
|
499 |
|
|
500 |
fun open_loc thy name =
|
|
501 |
let
|
|
502 |
val (ancestors, elements) = the_locale thy name;
|
|
503 |
in
|
|
504 |
(case #parent locale of None => thy
|
|
505 |
| Some par =>
|
|
506 |
if is_open thy par then thy
|
|
507 |
else (writeln ("Opening locale " ^ quote par ^ "(required by " ^ quote name ^ ")");
|
|
508 |
open_loc name thy))
|
|
509 |
|> change_scope (fn (locs, _) => ((name, locale) :: locs, None))
|
|
510 |
end;
|
|
511 |
|
|
512 |
in
|
|
513 |
|
|
514 |
fun open_locale xname thy =
|
|
515 |
let val name = intern (Theory.sign_of thy) xname in
|
|
516 |
if is_open thy name then (warning ("Locale " ^ quote name ^ " already open"); thy)
|
|
517 |
else open_loc name thy
|
|
518 |
end;
|
|
519 |
|
|
520 |
end;
|
11896
|
521 |
|
|
522 |
|
12014
|
523 |
(* close *)
|
|
524 |
|
|
525 |
fun close_locale xname thy =
|
|
526 |
let val name = intern_locale (Theory.sign_of thy) xname in
|
|
527 |
thy |> change_scope (fn ([], _) => error "Currently no open locales"
|
|
528 |
| ((name', _) :: locs, _) =>
|
|
529 |
if name <> name' then error ("Locale " ^ quote name ^ " not at top of scope")
|
|
530 |
else (locs, None))
|
|
531 |
end;
|
|
532 |
|
|
533 |
|
|
534 |
(* implicit context versions *)
|
|
535 |
|
|
536 |
fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
|
|
537 |
fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
|
|
538 |
fun Print_scope () = (print_scope (Context.the_context ()); ());
|
|
539 |
*)
|
11896
|
540 |
|
|
541 |
|
|
542 |
(** locale theory setup **)
|
12014
|
543 |
*)
|
11896
|
544 |
val setup =
|
|
545 |
[LocalesData.init];
|
|
546 |
|
|
547 |
end;
|
|
548 |
|
|
549 |
structure BasicLocale: BASIC_LOCALE = Locale;
|
|
550 |
open BasicLocale;
|