11896
|
1 |
(* Title: Pure/locale.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
4 |
Author: Markus Wenzel, TU Muenchen
|
|
5 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
6 |
|
|
7 |
Locales. The theory section 'locale' declarings constants, assumptions and
|
|
8 |
definitions that have local scope. Typical form is
|
|
9 |
|
|
10 |
locale Locale_name =
|
|
11 |
fixes (*variables that are fixed in the locale's scope*)
|
|
12 |
v :: T
|
|
13 |
assumes (*meta-hypothesis that hold in the locale*)
|
|
14 |
Asm_name "meta-formula"
|
|
15 |
defines (*local definitions of fixed variables in terms of others*)
|
|
16 |
v_def "v x == ...x..."
|
|
17 |
|
|
18 |
TODO:
|
|
19 |
- operations on locales: renaming.
|
|
20 |
*)
|
|
21 |
|
|
22 |
signature BASIC_LOCALE =
|
|
23 |
sig
|
|
24 |
val print_locales: theory -> unit
|
|
25 |
val thm: xstring -> thm
|
|
26 |
val thms: xstring -> thm list
|
|
27 |
val Open_locale: xstring -> unit
|
|
28 |
val Close_locale: xstring -> unit
|
|
29 |
val Print_scope: unit -> unit
|
|
30 |
end;
|
|
31 |
|
|
32 |
signature LOCALE =
|
|
33 |
sig
|
|
34 |
include BASIC_LOCALE
|
|
35 |
val get_thm: theory -> xstring -> thm
|
|
36 |
val get_thms: theory -> xstring -> thm list
|
|
37 |
type locale
|
|
38 |
val add_locale: bstring -> (bstring option) -> (string * string * mixfix) list ->
|
|
39 |
(string * string) list -> (string * string) list -> theory -> theory
|
|
40 |
val add_locale_i: bstring -> (bstring option) -> (string * typ * mixfix) list ->
|
|
41 |
(string * term) list -> (string * term) list -> theory -> theory
|
|
42 |
val open_locale: xstring -> theory -> theory
|
|
43 |
val close_locale: xstring -> theory -> theory
|
|
44 |
val print_scope: theory -> unit
|
|
45 |
val in_locale: term list -> Sign.sg -> bool
|
|
46 |
val is_open_loc_sg: Sign.sg -> bool
|
|
47 |
val is_open_loc: theory -> bool
|
|
48 |
val read_cterm: Sign.sg -> string * typ -> cterm
|
|
49 |
val get_scope: theory -> (string * locale) list
|
|
50 |
val get_scope_sg: Sign.sg -> (string * locale) list
|
|
51 |
val collect_consts: Sign.sg -> string list
|
|
52 |
val setup: (theory -> theory) list
|
|
53 |
end;
|
|
54 |
|
|
55 |
structure Locale: LOCALE =
|
|
56 |
struct
|
|
57 |
|
|
58 |
|
|
59 |
(** type locale **)
|
|
60 |
|
|
61 |
type locale =
|
|
62 |
{ancestor: string option,
|
|
63 |
consts: (string * typ) list,
|
|
64 |
nosyn: string list,
|
|
65 |
rules: (string * term) list,
|
|
66 |
defs: (string * term) list,
|
|
67 |
thms: (string * thm) list,
|
|
68 |
defaults: (string * sort) list * (string * typ) list * string list};
|
|
69 |
|
|
70 |
fun make_locale ancestor consts nosyn rules defs thms defaults =
|
|
71 |
{ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
|
|
72 |
defs = defs, thms = thms, defaults = defaults}: locale;
|
|
73 |
|
|
74 |
fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
|
|
75 |
let
|
|
76 |
val prt_typ = Pretty.quote o Sign.pretty_typ sg;
|
|
77 |
val prt_term = Pretty.quote o Sign.pretty_term sg;
|
|
78 |
|
|
79 |
fun pretty_const (c, T) = Pretty.block
|
|
80 |
[Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
|
|
81 |
|
|
82 |
fun pretty_axiom (a, t) = Pretty.block
|
|
83 |
[Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
|
|
84 |
|
|
85 |
val anc = case ancestor of
|
|
86 |
None => ""
|
|
87 |
| Some(loc) => ((Sign.base_name loc) ^ " +")
|
|
88 |
in
|
|
89 |
Pretty.big_list (name ^ " = " ^ anc)
|
|
90 |
[Pretty.big_list "consts:" (map pretty_const consts),
|
|
91 |
Pretty.big_list "rules:" (map pretty_axiom rules),
|
|
92 |
Pretty.big_list "defs:" (map pretty_axiom defs)]
|
|
93 |
end;
|
|
94 |
|
|
95 |
|
|
96 |
|
|
97 |
(** theory data **)
|
|
98 |
|
|
99 |
(* data kind 'Pure/locales' *)
|
|
100 |
|
|
101 |
type locale_data =
|
|
102 |
{space: NameSpace.T,
|
|
103 |
locales: locale Symtab.table,
|
|
104 |
scope: (string * locale) list ref};
|
|
105 |
|
|
106 |
fun make_locale_data space locales scope =
|
|
107 |
{space = space, locales = locales, scope = scope}: locale_data;
|
|
108 |
|
|
109 |
structure LocalesArgs =
|
|
110 |
struct
|
|
111 |
val name = "Pure/locales";
|
|
112 |
type T = locale_data;
|
|
113 |
|
|
114 |
val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
|
|
115 |
fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
|
|
116 |
fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
|
|
117 |
fun merge ({space = space1, locales = locales1, scope = _},
|
|
118 |
{space = space2, locales = locales2, scope = _}) =
|
|
119 |
make_locale_data (NameSpace.merge (space1, space2))
|
|
120 |
(Symtab.merge (K true) (locales1, locales2))
|
|
121 |
(ref []);
|
|
122 |
|
|
123 |
fun print sg {space, locales, scope} =
|
|
124 |
let
|
|
125 |
fun extrn name =
|
|
126 |
if ! long_names then name else NameSpace.extern space name;
|
|
127 |
val locs = map (apfst extrn) (Symtab.dest locales);
|
|
128 |
val scope_names = rev (map (extrn o fst) (! scope));
|
|
129 |
in
|
|
130 |
[Display.pretty_name_space ("locale name space", space),
|
|
131 |
Pretty.big_list "locales:" (map (pretty_locale sg) locs),
|
|
132 |
Pretty.strs ("current scope:" :: scope_names)]
|
|
133 |
|> Pretty.chunks |> Pretty.writeln
|
|
134 |
end;
|
|
135 |
end;
|
|
136 |
|
|
137 |
|
|
138 |
structure LocalesData = TheoryDataFun(LocalesArgs);
|
|
139 |
val print_locales = LocalesData.print;
|
|
140 |
|
|
141 |
|
|
142 |
(* access locales *)
|
|
143 |
|
|
144 |
fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
|
|
145 |
|
|
146 |
val get_locale = get_locale_sg o Theory.sign_of;
|
|
147 |
|
|
148 |
fun put_locale (name, locale) thy =
|
|
149 |
let
|
|
150 |
val {space, locales, scope} = LocalesData.get thy;
|
|
151 |
val space' = NameSpace.extend (space, [name]);
|
|
152 |
val locales' = Symtab.update ((name, locale), locales);
|
|
153 |
in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
|
|
154 |
|
|
155 |
fun lookup_locale thy xname =
|
|
156 |
let
|
|
157 |
val {space, locales, ...} = LocalesData.get thy;
|
|
158 |
val name = NameSpace.intern space xname;
|
|
159 |
in apsome (pair name) (get_locale thy name) end;
|
|
160 |
|
|
161 |
|
|
162 |
(* access scope *)
|
|
163 |
|
|
164 |
fun get_scope_sg sg =
|
|
165 |
if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
|
|
166 |
else ! (#scope (LocalesData.get_sg sg));
|
|
167 |
|
|
168 |
val get_scope = get_scope_sg o Theory.sign_of;
|
|
169 |
|
|
170 |
fun change_scope f thy =
|
|
171 |
let val {scope, ...} = LocalesData.get thy
|
|
172 |
in scope := f (! scope) end;
|
|
173 |
|
|
174 |
|
|
175 |
|
|
176 |
(** scope operations **)
|
|
177 |
|
|
178 |
(* change scope *)
|
|
179 |
|
|
180 |
fun the_locale thy xname =
|
|
181 |
(case lookup_locale thy xname of
|
|
182 |
Some loc => loc
|
|
183 |
| None => error ("Unknown locale " ^ quote xname));
|
|
184 |
|
|
185 |
fun open_locale xname thy =
|
|
186 |
let val loc = the_locale thy xname;
|
|
187 |
val anc = #ancestor(#2(loc));
|
|
188 |
val cur_sc = get_scope thy;
|
|
189 |
fun opn lc th = (change_scope (cons lc) th; th)
|
|
190 |
in case anc of
|
|
191 |
None => opn loc thy
|
|
192 |
| Some(loc') =>
|
|
193 |
if loc' mem (map fst cur_sc)
|
|
194 |
then opn loc thy
|
|
195 |
else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
|
|
196 |
quote xname);
|
|
197 |
opn loc (open_locale (Sign.base_name loc') thy))
|
|
198 |
end;
|
|
199 |
|
|
200 |
fun pop_locale [] = error "Currently no open locales"
|
|
201 |
| pop_locale (_ :: locs) = locs;
|
|
202 |
|
|
203 |
fun close_locale name thy =
|
|
204 |
let val lname = (case get_scope thy of (ln,_)::_ => ln
|
|
205 |
| _ => error "No locales are open!")
|
|
206 |
val ok = (name = Sign.base_name lname) handle _ => false
|
|
207 |
in if ok then (change_scope pop_locale thy; thy)
|
|
208 |
else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
|
|
209 |
end;
|
|
210 |
|
|
211 |
fun print_scope thy =
|
|
212 |
Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
|
|
213 |
|
|
214 |
(*implicit context versions*)
|
|
215 |
fun Open_locale xname = (open_locale xname (Context.the_context ()); ());
|
|
216 |
fun Close_locale xname = (close_locale xname (Context.the_context ()); ());
|
|
217 |
fun Print_scope () = (print_scope (Context.the_context ()); ());
|
|
218 |
|
|
219 |
|
|
220 |
(** functions for goals.ML **)
|
|
221 |
|
|
222 |
(* in_locale: check if hyps (: term list) of a proof are contained in the
|
|
223 |
(current) scope. This function is needed in prepare_proof. It needs to
|
|
224 |
refer to the signature, because theory is not available in prepare_proof. *)
|
|
225 |
|
|
226 |
fun in_locale hyps sg =
|
|
227 |
let val cur_sc = get_scope_sg sg;
|
|
228 |
val rule_lists = map (#rules o snd) cur_sc;
|
|
229 |
val def_lists = map (#defs o snd) cur_sc;
|
|
230 |
val rules = map snd (foldr (op union) (rule_lists, []));
|
|
231 |
val defs = map snd (foldr (op union) (def_lists, []));
|
|
232 |
val defnrules = rules @ defs;
|
|
233 |
in
|
|
234 |
hyps subset defnrules
|
|
235 |
end;
|
|
236 |
|
|
237 |
|
|
238 |
(* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
|
|
239 |
fun is_open_loc_sg sign =
|
|
240 |
let val cur_sc = get_scope_sg sign
|
|
241 |
in not(null(cur_sc)) end;
|
|
242 |
|
|
243 |
val is_open_loc = is_open_loc_sg o Theory.sign_of;
|
|
244 |
|
|
245 |
|
|
246 |
(* get theorems *)
|
|
247 |
|
|
248 |
fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
|
|
249 |
|
|
250 |
fun get_thmx f get thy name =
|
|
251 |
(case get_first (get_thm_locale name) (get_scope thy) of
|
|
252 |
Some thm => f thm
|
|
253 |
| None => get thy name);
|
|
254 |
|
|
255 |
val get_thm = get_thmx I PureThy.get_thm;
|
|
256 |
val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
|
|
257 |
|
|
258 |
fun thm name = get_thm (Context.the_context ()) name;
|
|
259 |
fun thms name = get_thms (Context.the_context ()) name;
|
|
260 |
|
|
261 |
|
|
262 |
(* get the defaults of a locale, for extension *)
|
|
263 |
|
|
264 |
fun get_defaults thy name =
|
|
265 |
let val (lname, loc) = the_locale thy name;
|
|
266 |
in #defaults(loc)
|
|
267 |
end;
|
|
268 |
|
|
269 |
|
|
270 |
(** define locales **)
|
|
271 |
|
|
272 |
(* prepare types *)
|
|
273 |
|
|
274 |
fun read_typ sg (envT, s) =
|
|
275 |
let
|
|
276 |
fun def_sort (x, ~1) = assoc (envT, x)
|
|
277 |
| def_sort _ = None;
|
|
278 |
val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
|
|
279 |
in (Term.add_typ_tfrees (T, envT), T) end;
|
|
280 |
|
|
281 |
fun cert_typ sg (envT, raw_T) =
|
|
282 |
let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
|
|
283 |
in (Term.add_typ_tfrees (T, envT), T) end;
|
|
284 |
|
|
285 |
|
|
286 |
(* prepare props *)
|
|
287 |
|
|
288 |
val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
|
|
289 |
|
|
290 |
fun enter_term t (envS, envT, used) =
|
|
291 |
(Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
|
|
292 |
|
|
293 |
fun read_axm sg ((envS, envT, used), (name, s)) =
|
|
294 |
let
|
|
295 |
fun def_sort (x, ~1) = assoc (envS, x)
|
|
296 |
| def_sort _ = None;
|
|
297 |
fun def_type (x, ~1) = assoc (envT, x)
|
|
298 |
| def_type _ = None;
|
|
299 |
val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
|
|
300 |
in
|
|
301 |
(enter_term t (envS, envT, used), t)
|
|
302 |
end;
|
|
303 |
|
|
304 |
|
|
305 |
fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
|
|
306 |
let val (_, t) = Theory.cert_axm sg (name, raw_t)
|
|
307 |
in (enter_term t (envS, envT, used), t) end;
|
|
308 |
|
|
309 |
|
|
310 |
(* Locale.read_cterm: read in a string as a certified term, and respect the bindings
|
|
311 |
that already exist for subterms. If no locale is open, this function is equal to
|
|
312 |
Thm.read_cterm *)
|
|
313 |
|
|
314 |
fun read_cterm sign =
|
|
315 |
let val cur_sc = get_scope_sg sign;
|
|
316 |
val defaults = map (#defaults o snd) cur_sc;
|
|
317 |
val envS = flat (map #1 defaults);
|
|
318 |
val envT = flat (map #2 defaults);
|
|
319 |
val used = flat (map #3 defaults);
|
|
320 |
fun def_sort (x, ~1) = assoc (envS, x)
|
|
321 |
| def_sort _ = None;
|
|
322 |
fun def_type (x, ~1) = assoc (envT, x)
|
|
323 |
| def_type _ = None;
|
|
324 |
in (if (is_open_loc_sg sign)
|
|
325 |
then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
|
|
326 |
else Thm.read_cterm sign)
|
|
327 |
end;
|
|
328 |
|
|
329 |
(* basic functions needed for definitions and display *)
|
|
330 |
(* collect all locale constants of a scope, i.e. a list of locales *)
|
|
331 |
fun collect_consts sg =
|
|
332 |
let val cur_sc = get_scope_sg sg;
|
|
333 |
val locale_list = map snd cur_sc;
|
|
334 |
val const_list = flat (map #consts locale_list)
|
|
335 |
in map fst const_list end;
|
|
336 |
|
|
337 |
(* filter out the Free's in a term *)
|
|
338 |
fun list_frees t =
|
|
339 |
case t of Const(c,T) => []
|
|
340 |
| Var(v,T) => []
|
|
341 |
| Free(v,T)=> [Free(v,T)]
|
|
342 |
| Bound x => []
|
|
343 |
| Abs(a,T,u) => list_frees u
|
|
344 |
| t1 $ t2 => (list_frees t1) @ (list_frees t2);
|
|
345 |
|
|
346 |
(* filter out all Free's in a term that are not contained
|
|
347 |
in a list of strings. Used to prepare definitions. The list of strings
|
|
348 |
will be the consts of the scope. We filter out the "free" Free's to be
|
|
349 |
able to bind them *)
|
|
350 |
fun difflist term clist =
|
|
351 |
let val flist = list_frees term;
|
|
352 |
fun builddiff [] sl = []
|
|
353 |
| builddiff (t :: tl) sl =
|
|
354 |
let val Free(v,T) = t
|
|
355 |
in
|
|
356 |
if (v mem sl)
|
|
357 |
then builddiff tl sl
|
|
358 |
else t :: (builddiff tl sl)
|
|
359 |
end;
|
|
360 |
in distinct(builddiff flist clist) end;
|
|
361 |
|
|
362 |
(* Bind a term with !! over a list of "free" Free's.
|
|
363 |
To enable definitions like x + y == .... (without quantifier).
|
|
364 |
Complications, because x and y have to be removed from defaults *)
|
|
365 |
fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
|
|
366 |
let val diffl = rev(difflist term clist);
|
|
367 |
fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
|
|
368 |
| abs_o (_ , _) = error ("Can't be: abs_over_free");
|
|
369 |
val diffl' = map (fn (Free (s, T)) => s) diffl;
|
|
370 |
val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
|
|
371 |
in (defaults', (s, foldl abs_o (term, diffl))) end;
|
|
372 |
|
|
373 |
(* assume a definition, i.e assume the cterm of a definiton term and then eliminate
|
|
374 |
the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
|
|
375 |
fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
|
|
376 |
|
|
377 |
|
|
378 |
(* concrete syntax *)
|
|
379 |
|
|
380 |
fun mark_syn c = "\\<^locale>" ^ c;
|
|
381 |
|
|
382 |
fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
|
|
383 |
|
|
384 |
|
|
385 |
(* add_locale *)
|
|
386 |
|
|
387 |
fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
|
|
388 |
let val sign = Theory.sign_of thy;
|
|
389 |
|
|
390 |
val name = Sign.full_name sign bname;
|
|
391 |
|
|
392 |
val (envSb, old_loc_consts, _) =
|
|
393 |
case bancestor of
|
|
394 |
Some(loc) => (get_defaults thy loc)
|
|
395 |
| None => ([],[],[]);
|
|
396 |
|
|
397 |
val old_nosyn = case bancestor of
|
|
398 |
Some(loc) => #nosyn(#2(the_locale thy loc))
|
|
399 |
| None => [];
|
|
400 |
|
|
401 |
(* Get the full name of the ancestor *)
|
|
402 |
val ancestor = case bancestor of
|
|
403 |
Some(loc) => Some(#1(the_locale thy loc))
|
|
404 |
| None => None;
|
|
405 |
|
|
406 |
(* prepare locale consts *)
|
|
407 |
|
|
408 |
fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
|
|
409 |
let
|
|
410 |
val c = Syntax.const_name raw_c raw_mx;
|
|
411 |
val c_syn = mark_syn c;
|
|
412 |
val mx = Syntax.fix_mixfix raw_c raw_mx;
|
|
413 |
val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
|
|
414 |
error ("The error(s) above occured in locale constant " ^ quote c);
|
|
415 |
val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
|
|
416 |
in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
|
|
417 |
|
|
418 |
val (envS0, loc_consts_syn) = foldl_map prep_const (envSb, raw_consts);
|
|
419 |
val loc_consts = map #1 loc_consts_syn;
|
|
420 |
val loc_consts = old_loc_consts @ loc_consts;
|
|
421 |
val loc_syn = map #2 loc_consts_syn;
|
|
422 |
val nosyn = old_nosyn @ (map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn));
|
|
423 |
val loc_trfuns = mapfilter #3 loc_consts_syn;
|
|
424 |
|
|
425 |
|
|
426 |
(* 1st stage: syntax_thy *)
|
|
427 |
|
|
428 |
val syntax_thy =
|
|
429 |
thy
|
|
430 |
|> Theory.add_modesyntax_i ("", true) loc_syn
|
|
431 |
|> Theory.add_trfuns ([], loc_trfuns, [], []);
|
|
432 |
|
|
433 |
val syntax_sign = Theory.sign_of syntax_thy;
|
|
434 |
|
|
435 |
|
|
436 |
(* prepare rules and defs *)
|
|
437 |
|
|
438 |
fun prep_axiom (env, (a, raw_t)) =
|
|
439 |
let
|
|
440 |
val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
|
|
441 |
error ("The error(s) above occured in locale rule / definition " ^ quote a);
|
|
442 |
in (env', (a, t)) end;
|
|
443 |
|
|
444 |
val ((envS1, envT1, used1), loc_rules) =
|
|
445 |
foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
|
|
446 |
val (defaults, loc_defs) =
|
|
447 |
foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
|
|
448 |
|
|
449 |
val old_loc_consts = collect_consts syntax_sign;
|
|
450 |
val new_loc_consts = (map #1 loc_consts);
|
|
451 |
val all_loc_consts = old_loc_consts @ new_loc_consts;
|
|
452 |
|
|
453 |
val (defaults, loc_defs_terms) =
|
|
454 |
foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
|
|
455 |
val loc_defs_thms =
|
|
456 |
map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
|
|
457 |
val (defaults, loc_thms_terms) =
|
|
458 |
foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
|
|
459 |
val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
|
|
460 |
(loc_thms_terms)
|
|
461 |
@ loc_defs_thms;
|
|
462 |
|
|
463 |
|
|
464 |
(* error messages *)
|
|
465 |
|
|
466 |
fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
|
|
467 |
|
|
468 |
val err_dup_locale =
|
|
469 |
if is_none (get_locale thy name) then []
|
|
470 |
else ["Duplicate definition of locale " ^ quote name];
|
|
471 |
|
|
472 |
(* check if definientes are locale constants
|
|
473 |
(in the same locale, so no redefining!) *)
|
|
474 |
val err_def_head =
|
|
475 |
let fun peal_appl t =
|
|
476 |
case t of
|
|
477 |
t1 $ t2 => peal_appl t1
|
|
478 |
| Free(t) => t
|
|
479 |
| _ => locale_error ("Bad form of LHS in locale definition");
|
|
480 |
fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
|
|
481 |
| lhs _ = locale_error ("Definitions must use the == relation");
|
|
482 |
val defs = map lhs loc_defs;
|
|
483 |
val check = defs subset loc_consts
|
|
484 |
in if check then []
|
|
485 |
else ["defined item not declared fixed in locale " ^ quote name]
|
|
486 |
end;
|
|
487 |
|
|
488 |
(* check that variables on rhs of definitions are either fixed or on lhs *)
|
|
489 |
val err_var_rhs =
|
|
490 |
let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
|
|
491 |
let val varl1 = difflist d1 all_loc_consts;
|
|
492 |
val varl2 = difflist d2 all_loc_consts
|
|
493 |
in t andalso (varl2 subset varl1)
|
|
494 |
end
|
|
495 |
| compare_var_sides (_,_) =
|
|
496 |
locale_error ("Definitions must use the == relation")
|
|
497 |
val check = foldl compare_var_sides (true, loc_defs)
|
|
498 |
in if check then []
|
|
499 |
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
|
|
500 |
end;
|
|
501 |
|
|
502 |
val errs = err_dup_locale @ err_def_head @ err_var_rhs;
|
|
503 |
in
|
|
504 |
if null errs then ()
|
|
505 |
else error (cat_lines errs);
|
|
506 |
|
|
507 |
syntax_thy
|
|
508 |
|> put_locale (name,
|
|
509 |
make_locale ancestor loc_consts nosyn loc_thms_terms
|
|
510 |
loc_defs_terms loc_thms defaults)
|
|
511 |
end;
|
|
512 |
|
|
513 |
|
|
514 |
val add_locale = gen_add_locale read_typ read_axm;
|
|
515 |
val add_locale_i = gen_add_locale cert_typ cert_axm;
|
|
516 |
|
|
517 |
(** print functions **)
|
|
518 |
(* idea: substitute all locale contants (Free's) that are syntactical by their
|
|
519 |
"real" constant representation (i.e. \\<^locale>constname).
|
|
520 |
- function const_ssubst does this substitution
|
|
521 |
- function Locale.pretty_term:
|
|
522 |
if locale is open then do this substitution & then call Sign.pretty_term
|
|
523 |
else call Sign.pretty_term
|
|
524 |
*)
|
|
525 |
(* substitutes all Free variables s in t by Const's s *)
|
|
526 |
fun const_ssubst t s =
|
|
527 |
case t of
|
|
528 |
Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
|
|
529 |
| Const(c,T) => Const(c,T)
|
|
530 |
| Var(v,T) => Var(v,T)
|
|
531 |
| Bound x => Bound x
|
|
532 |
| Abs(a,T,u) => Abs(a,T, const_ssubst u s)
|
|
533 |
| t1 $ t2 => const_ssubst t1 s $ const_ssubst t2 s;
|
|
534 |
|
|
535 |
(* FIXME: improve: can be expressed with foldl *)
|
|
536 |
fun const_ssubst_list [] t = t
|
|
537 |
| const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
|
|
538 |
|
|
539 |
(* Locale.pretty_term *)
|
|
540 |
fun pretty_term sign =
|
|
541 |
if (is_open_loc_sg sign) then
|
|
542 |
let val locale_list = map snd(get_scope_sg sign);
|
|
543 |
val nosyn = flat (map #nosyn locale_list);
|
|
544 |
val str_list = (collect_consts sign) \\ nosyn
|
|
545 |
in Sign.pretty_term sign o (const_ssubst_list str_list)
|
|
546 |
end
|
|
547 |
else Sign.pretty_term sign;
|
|
548 |
|
|
549 |
|
|
550 |
|
|
551 |
|
|
552 |
|
|
553 |
|
|
554 |
(** locale theory setup **)
|
|
555 |
|
|
556 |
val setup =
|
|
557 |
[LocalesData.init];
|
|
558 |
|
|
559 |
end;
|
|
560 |
|
|
561 |
structure BasicLocale: BASIC_LOCALE = Locale;
|
|
562 |
open BasicLocale;
|