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