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