12014
|
1 |
(* Title: Pure/Isar/locale.ML
|
11896
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
|
12058
|
6 |
Locales -- Isar proof contexts as meta-level predicates, with local
|
12063
|
7 |
syntax and implicit structures. Draws basic ideas from Florian
|
12263
|
8 |
Kammüller's original version of locales, but uses the rich
|
12063
|
9 |
infrastructure of Isar instead of the raw meta-logic.
|
11896
|
10 |
*)
|
|
11 |
|
|
12 |
signature BASIC_LOCALE =
|
|
13 |
sig
|
|
14 |
val print_locales: theory -> unit
|
12063
|
15 |
val print_locale: theory -> xstring -> unit
|
11896
|
16 |
end;
|
|
17 |
|
|
18 |
signature LOCALE =
|
|
19 |
sig
|
|
20 |
include BASIC_LOCALE
|
12046
|
21 |
type context
|
|
22 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
23 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
24 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
25 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
12273
|
26 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list
|
|
27 |
datatype expr =
|
|
28 |
Locale of string |
|
|
29 |
Rename of expr * string option list |
|
|
30 |
Merge of expr list
|
|
31 |
val empty: expr
|
|
32 |
datatype ('typ, 'term, 'fact, 'att) elem_expr =
|
|
33 |
Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr
|
12046
|
34 |
type 'att element
|
|
35 |
type 'att element_i
|
|
36 |
type locale
|
12273
|
37 |
val the_locale: theory -> string -> locale (* FIXME *)
|
12046
|
38 |
val intern: Sign.sg -> xstring -> string
|
12014
|
39 |
val cond_extern: Sign.sg -> string -> xstring
|
12273
|
40 |
val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
|
|
41 |
-> ('typ, 'term, 'thm, context attribute) elem_expr
|
12046
|
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
|
12273
|
46 |
val add_locale: bstring -> expr -> context attribute element list -> theory -> theory
|
|
47 |
val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory
|
|
48 |
val add_thmss: string -> ((string * thm list) * context attribute list) list -> theory -> theory
|
11896
|
49 |
val setup: (theory -> theory) list
|
|
50 |
end;
|
|
51 |
|
|
52 |
structure Locale: LOCALE =
|
|
53 |
struct
|
|
54 |
|
|
55 |
|
12273
|
56 |
(** locale elements and expressions **)
|
11896
|
57 |
|
12014
|
58 |
type context = ProofContext.context;
|
11896
|
59 |
|
12046
|
60 |
datatype ('typ, 'term, 'fact, 'att) elem =
|
12058
|
61 |
Fixes of (string * 'typ option * mixfix option) list |
|
12046
|
62 |
Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
|
|
63 |
Defines of ((string * 'att list) * ('term * 'term list)) list |
|
12273
|
64 |
Notes of ((string * 'att list) * ('fact * 'att list) list) list;
|
|
65 |
|
|
66 |
datatype expr =
|
|
67 |
Locale of string |
|
|
68 |
Rename of expr * string option list |
|
|
69 |
Merge of expr list;
|
11896
|
70 |
|
12273
|
71 |
val empty = Merge [];
|
|
72 |
|
|
73 |
datatype ('typ, 'term, 'fact, 'att) elem_expr =
|
|
74 |
Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr;
|
|
75 |
|
|
76 |
type 'att element = (string, string, string, 'att) elem_expr;
|
|
77 |
type 'att element_i = (typ, term, thm list, 'att) elem_expr;
|
12070
|
78 |
|
|
79 |
type locale =
|
12273
|
80 |
{import: expr, (*dynamic import*)
|
|
81 |
elems: (typ, term, thm list, context attribute) elem list, (*static content*)
|
|
82 |
params: (string * typ option) list * (string * typ option) list, (*all vs. local params*)
|
|
83 |
text: (string * typ) list * term list, (*logical representation*)
|
|
84 |
closed: bool}; (*disallow further notes*)
|
12063
|
85 |
|
12273
|
86 |
fun make_locale import elems params text closed =
|
|
87 |
{import = import, elems = elems, params = params, text = text, closed = closed}: locale;
|
12063
|
88 |
|
11896
|
89 |
|
|
90 |
|
|
91 |
(** theory data **)
|
|
92 |
|
|
93 |
structure LocalesArgs =
|
|
94 |
struct
|
12014
|
95 |
val name = "Isar/locales";
|
12063
|
96 |
type T = NameSpace.T * locale Symtab.table;
|
11896
|
97 |
|
12063
|
98 |
val empty = (NameSpace.empty, Symtab.empty);
|
|
99 |
val copy = I;
|
12118
|
100 |
val prep_ext = I;
|
12273
|
101 |
fun merge ((space1, locs1), (space2, locs2)) =
|
|
102 |
(NameSpace.merge (space1, space2), Symtab.merge (K true) (locs1, locs2));
|
|
103 |
fun finish (space, locs) = (space, Symtab.map (fn {import, elems, params, text, closed = _} =>
|
|
104 |
make_locale import elems params text true) locs);
|
|
105 |
fun print _ (space, locs) =
|
|
106 |
Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs))
|
12014
|
107 |
|> Pretty.writeln;
|
11896
|
108 |
end;
|
|
109 |
|
|
110 |
structure LocalesData = TheoryDataFun(LocalesArgs);
|
|
111 |
val print_locales = LocalesData.print;
|
|
112 |
|
12063
|
113 |
fun declare_locale name =
|
|
114 |
LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name]))));
|
11896
|
115 |
|
12273
|
116 |
fun put_locale name loc = LocalesData.map (apsnd (fn locs => Symtab.update ((name, loc), locs)));
|
12063
|
117 |
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
|
11896
|
118 |
|
12014
|
119 |
fun the_locale thy name =
|
|
120 |
(case get_locale thy name of
|
|
121 |
Some loc => loc
|
|
122 |
| None => error ("Unknown locale " ^ quote name));
|
11896
|
123 |
|
|
124 |
|
12046
|
125 |
|
12273
|
126 |
(** internalization **)
|
|
127 |
|
|
128 |
(* names *)
|
|
129 |
|
|
130 |
val intern = NameSpace.intern o #1 o LocalesData.get_sg;
|
|
131 |
val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg;
|
|
132 |
|
12063
|
133 |
|
12263
|
134 |
(* read *)
|
|
135 |
|
12063
|
136 |
fun read_elem ctxt =
|
|
137 |
fn Fixes fixes =>
|
|
138 |
let val vars =
|
|
139 |
#2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
|
|
140 |
in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end
|
|
141 |
| Assumes asms =>
|
|
142 |
Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms)))
|
|
143 |
| Defines defs =>
|
|
144 |
let val propps =
|
|
145 |
#2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs))
|
|
146 |
in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end
|
|
147 |
| Notes facts =>
|
12273
|
148 |
Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts);
|
|
149 |
|
|
150 |
fun read_expr ctxt (Locale xname) = Locale (intern (ProofContext.sign_of ctxt) xname)
|
|
151 |
| read_expr ctxt (Merge exprs) = Merge (map (read_expr ctxt) exprs)
|
|
152 |
| read_expr ctxt (Rename (expr, xs)) =
|
|
153 |
(case duplicates (mapfilter I xs) of [] => Rename (read_expr ctxt expr, xs)
|
|
154 |
| ds => raise ProofContext.CONTEXT ("Duplicates in renaming: " ^ commas_quote ds, ctxt));;
|
|
155 |
|
|
156 |
fun read_element ctxt (Elem e) = Elem (read_elem ctxt e)
|
|
157 |
| read_element ctxt (Expr e) = Expr (read_expr ctxt e);
|
12063
|
158 |
|
|
159 |
|
12273
|
160 |
(* attribute *)
|
12063
|
161 |
|
|
162 |
local fun int_att attrib (x, srcs) = (x, map attrib srcs) in
|
|
163 |
|
12273
|
164 |
fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
|
|
165 |
| attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (int_att attrib)) asms))
|
|
166 |
| attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (int_att attrib)) defs))
|
|
167 |
| attribute attrib (Elem (Notes facts)) =
|
|
168 |
Elem (Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts))
|
|
169 |
| attribute _ (Expr expr) = Expr expr;
|
12063
|
170 |
|
|
171 |
end;
|
12046
|
172 |
|
|
173 |
|
12273
|
174 |
|
12263
|
175 |
(** renaming **)
|
|
176 |
|
|
177 |
fun rename ren x = if_none (assoc_string (ren, x)) x;
|
|
178 |
|
|
179 |
fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
|
|
180 |
| rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
|
|
181 |
| rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
|
|
182 |
| rename_term _ a = a;
|
|
183 |
|
|
184 |
fun rename_thm ren th =
|
|
185 |
let
|
|
186 |
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
|
|
187 |
val cert = Thm.cterm_of sign;
|
|
188 |
val (xs, Ts) = Library.split_list (foldl Drule.add_frees ([], prop :: hyps));
|
|
189 |
val xs' = map (rename ren) xs;
|
|
190 |
fun cert_frees names = map (cert o Free) (names ~~ Ts);
|
|
191 |
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
|
|
192 |
in
|
|
193 |
if xs = xs' then th
|
|
194 |
else
|
|
195 |
th
|
|
196 |
|> Drule.implies_intr_list (map cert hyps)
|
|
197 |
|> Drule.forall_intr_list (cert_frees xs)
|
|
198 |
|> Drule.forall_elim_list (cert_vars xs)
|
|
199 |
|> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs')
|
|
200 |
|> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))
|
|
201 |
end;
|
|
202 |
|
|
203 |
fun rename_elem ren (Fixes fixes) = Fixes (map (fn (x, T, mx) =>
|
12273
|
204 |
(rename ren x, T, if mx = None then mx else Some Syntax.NoSyn)) fixes) (*drops syntax!*)
|
12263
|
205 |
| rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
|
|
206 |
(rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms)
|
|
207 |
| rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
|
|
208 |
(rename_term ren t, map (rename_term ren) ps))) defs)
|
12273
|
209 |
| rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);
|
12263
|
210 |
|
|
211 |
|
11896
|
212 |
|
12273
|
213 |
(** evaluation **)
|
11896
|
214 |
|
12273
|
215 |
fun eval_expr ctxt expr =
|
12014
|
216 |
let
|
|
217 |
val thy = ProofContext.theory_of ctxt;
|
12263
|
218 |
|
12273
|
219 |
fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys
|
|
220 |
| renaming (None :: xs) (y :: ys) = renaming xs ys
|
|
221 |
| renaming [] _ = []
|
|
222 |
| renaming xs [] = raise ProofContext.CONTEXT ("Extraneous arguments in renaming: " ^
|
|
223 |
commas (map (fn None => "_" | Some x => quote x) xs), ctxt);
|
12263
|
224 |
|
12273
|
225 |
fun identify ((ids, parms), Locale name) =
|
|
226 |
let
|
|
227 |
val {import, params, ...} = the_locale thy name;
|
|
228 |
val ps = map #1 (#1 params);
|
|
229 |
in
|
|
230 |
if (name, ps) mem ids then (ids, parms)
|
|
231 |
else identify (((name, ps) :: ids, merge_lists parms ps), import)
|
|
232 |
end
|
|
233 |
| identify ((ids, parms), Rename (e, xs)) =
|
|
234 |
let
|
|
235 |
val (ids', parms') = identify (([], []), e);
|
|
236 |
val ren = renaming xs parms';
|
|
237 |
val ids'' = map (apsnd (map (rename ren))) ids' \\ ids;
|
|
238 |
in (ids'' @ ids, merge_lists parms (map (rename ren) parms')) end
|
|
239 |
| identify (arg, Merge es) = foldl identify (arg, es);
|
12014
|
240 |
|
12273
|
241 |
val idents = rev (#1 (identify (([], []), expr)));
|
|
242 |
val FIXME = PolyML.print idents;
|
|
243 |
|
|
244 |
fun eval (name, ps') =
|
|
245 |
let
|
|
246 |
val {params = (ps, _), elems, ...} = the_locale thy name;
|
|
247 |
val ren = filter_out (op =) (map #1 ps ~~ ps');
|
|
248 |
in
|
|
249 |
if null ren then ((name, ps), elems)
|
|
250 |
else ((name, map (apfst (rename ren)) ps), map (rename_elem ren) elems)
|
|
251 |
end;
|
|
252 |
(* FIXME unify types; specific errors (name) *)
|
|
253 |
|
|
254 |
in map eval idents end;
|
|
255 |
|
|
256 |
fun eval_elements ctxt =
|
|
257 |
flat o map (fn Elem e => [e] | Expr e => flat (map #2 (eval_expr ctxt e)));
|
12046
|
258 |
|
12070
|
259 |
|
12273
|
260 |
|
|
261 |
(** activation **)
|
12070
|
262 |
|
12273
|
263 |
fun activate_elem (Fixes fixes) = ProofContext.add_syntax fixes o
|
|
264 |
ProofContext.fix_direct (map (fn (x, T, mx) => ([x], T)) fixes)
|
|
265 |
| activate_elem (Assumes asms) =
|
|
266 |
#1 o ProofContext.assume_i ProofContext.export_assume asms o
|
|
267 |
ProofContext.fix_frees (flat (map (map #1 o #2) asms))
|
|
268 |
| activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def
|
|
269 |
(map (fn ((name, atts), (t, ps)) =>
|
|
270 |
let val (c, t') = ProofContext.cert_def ctxt t
|
|
271 |
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt))
|
|
272 |
| activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts;
|
12263
|
273 |
|
12273
|
274 |
fun activate_elems es ctxt = foldl (fn (c, e) => activate_elem e c) (ctxt, es);
|
|
275 |
|
|
276 |
fun activate_elements_i elements ctxt = activate_elems (eval_elements ctxt elements) ctxt;
|
|
277 |
fun activate_elements elements ctxt = activate_elements_i (map (read_element ctxt) elements) ctxt;
|
|
278 |
|
|
279 |
fun activate_locale_i name = activate_elements_i [Expr (Locale name)];
|
|
280 |
fun activate_locale xname = activate_elements [Expr (Locale xname)];
|
11896
|
281 |
|
|
282 |
|
|
283 |
|
12070
|
284 |
(** print locale **)
|
|
285 |
|
|
286 |
fun pretty_locale thy xname =
|
|
287 |
let
|
|
288 |
val sg = Theory.sign_of thy;
|
|
289 |
val name = intern sg xname;
|
12273
|
290 |
val {import, elems, params = _, text = _, closed = _} = the_locale thy name;
|
12070
|
291 |
val locale_ctxt = ProofContext.init thy |> activate_locale_i name;
|
|
292 |
|
|
293 |
val prt_typ = Pretty.quote o ProofContext.pretty_typ locale_ctxt;
|
|
294 |
val prt_term = Pretty.quote o ProofContext.pretty_term locale_ctxt;
|
|
295 |
val prt_thm = Pretty.quote o ProofContext.pretty_thm locale_ctxt;
|
|
296 |
|
|
297 |
fun prt_syn syn =
|
|
298 |
let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
|
|
299 |
in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
|
|
300 |
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
|
|
301 |
prt_typ T :: Pretty.brk 1 :: prt_syn syn)
|
|
302 |
| prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
|
|
303 |
|
|
304 |
fun prt_asm (("", _), ts) = Pretty.block (Pretty.breaks (map (prt_term o fst) ts))
|
|
305 |
| prt_asm ((a, _), ts) = Pretty.block
|
|
306 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts));
|
|
307 |
fun prt_asms asms = Pretty.block
|
|
308 |
(flat (separate [Pretty.fbrk, Pretty.str "and"] (map (single o prt_asm) asms)));
|
|
309 |
|
|
310 |
fun prt_def (("", _), (t, _)) = Pretty.block [Pretty.brk 1, prt_term t]
|
|
311 |
| prt_def ((a, _), (t, _)) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
|
|
312 |
|
|
313 |
fun prt_fact (("", _), ths) = Pretty.block (Pretty.breaks (map prt_thm (flat (map fst ths))))
|
|
314 |
| prt_fact ((a, _), ths) = Pretty.block
|
|
315 |
(Pretty.breaks (Pretty.str (a ^ ":") :: map prt_thm (flat (map fst ths))));
|
|
316 |
|
12263
|
317 |
fun prt_expr (Locale name) = Pretty.str (cond_extern sg name)
|
|
318 |
| prt_expr (Merge exprs) = Pretty.enclose "(" ")"
|
|
319 |
(flat (separate [Pretty.str " +", Pretty.brk 1]
|
|
320 |
(map (single o prt_expr) exprs)))
|
|
321 |
| prt_expr (Rename (expr, xs)) = Pretty.enclose "(" ")"
|
|
322 |
(Pretty.breaks (prt_expr expr :: map (fn x => Pretty.str (if_none x "_")) xs));
|
|
323 |
|
12070
|
324 |
fun prt_elem (Fixes fixes) = Pretty.big_list "fixes" (map prt_fix fixes)
|
|
325 |
| prt_elem (Assumes asms) = Pretty.big_list "assumes" (map prt_asm asms)
|
|
326 |
| prt_elem (Defines defs) = Pretty.big_list "defines" (map prt_def defs)
|
12273
|
327 |
| prt_elem (Notes facts) = Pretty.big_list "notes" (map prt_fact facts);
|
12070
|
328 |
|
|
329 |
val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") ::
|
12273
|
330 |
(if import = empty then [] else [Pretty.str " ", prt_expr import] @
|
|
331 |
(if null elems then [] else [Pretty.str " +"]) @ [Pretty.brk 1]));
|
|
332 |
in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elems)) end;
|
12070
|
333 |
|
|
334 |
val print_locale = Pretty.writeln oo pretty_locale;
|
|
335 |
|
|
336 |
|
|
337 |
|
11896
|
338 |
(** define locales **)
|
|
339 |
|
12063
|
340 |
(* closeup dangling frees *)
|
|
341 |
|
|
342 |
fun close_frees_wrt ctxt t =
|
|
343 |
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t)))
|
|
344 |
in curry Term.list_all_free frees end;
|
11896
|
345 |
|
12063
|
346 |
fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
|
|
347 |
(a, propps |> map (fn (t, (ps1, ps2)) =>
|
|
348 |
let val close = close_frees_wrt ctxt t in (close t, (map close ps1, map close ps2)) end))))
|
|
349 |
| closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
|
|
350 |
let
|
12084
|
351 |
val (_, t') = ProofContext.cert_def ctxt t;
|
12063
|
352 |
val close = close_frees_wrt ctxt t';
|
|
353 |
in (a, (close t', map close ps)) end))
|
|
354 |
| closeup ctxt elem = elem;
|
11896
|
355 |
|
|
356 |
|
12063
|
357 |
(* add_locale(_i) *)
|
11896
|
358 |
|
12273
|
359 |
fun gen_add_locale prep_expr prep_element bname raw_import raw_elements thy =
|
12063
|
360 |
let
|
|
361 |
val sign = Theory.sign_of thy;
|
11896
|
362 |
val name = Sign.full_name sign bname;
|
12063
|
363 |
val _ =
|
|
364 |
if is_none (get_locale thy name) then () else
|
|
365 |
error ("Duplicate definition of locale " ^ quote name);
|
11896
|
366 |
|
12273
|
367 |
val thy_ctxt = ProofContext.init thy;
|
|
368 |
|
|
369 |
val import = prep_expr thy_ctxt raw_import;
|
|
370 |
val (import_ids, import_elemss) = split_list (eval_expr thy_ctxt import);
|
|
371 |
val import_ctxt = activate_elems (flat import_elemss) thy_ctxt;
|
|
372 |
|
|
373 |
fun prep (ctxt, raw_element) =
|
|
374 |
let val elems = map (closeup ctxt) (eval_elements ctxt [prep_element ctxt raw_element]);
|
|
375 |
in (activate_elems elems ctxt, elems) end;
|
|
376 |
val (locale_ctxt, elemss) = foldl_map prep (import_ctxt, raw_elements);
|
|
377 |
|
|
378 |
val elems = flat elemss;
|
|
379 |
val local_ps = (* FIXME proper types *)
|
|
380 |
flat (map (fn Fixes fixes => map (fn (x, T, _) => (x, T)) fixes | _ => []) elems);
|
|
381 |
val all_ps = distinct (flat (map #2 import_ids)) @ local_ps;
|
|
382 |
val text = ([], []); (* FIXME *)
|
12063
|
383 |
in
|
|
384 |
thy
|
|
385 |
|> declare_locale name
|
12273
|
386 |
|> put_locale name (make_locale import elems (all_ps, local_ps) text false)
|
12063
|
387 |
end;
|
|
388 |
|
12273
|
389 |
val add_locale = gen_add_locale read_expr read_element;
|
12063
|
390 |
val add_locale_i = gen_add_locale (K I) (K I);
|
|
391 |
|
11896
|
392 |
|
12063
|
393 |
|
12070
|
394 |
(** store results **)
|
11896
|
395 |
|
12143
|
396 |
fun add_thmss name args thy =
|
12063
|
397 |
let
|
12273
|
398 |
val {import, params, elems, text, closed} = the_locale thy name;
|
12143
|
399 |
val _ = conditional closed (fn () =>
|
|
400 |
error ("Cannot store results in closed locale: " ^ quote name));
|
|
401 |
val note = Notes (map (fn ((a, ths), atts) =>
|
|
402 |
((a, atts), [(map (curry Thm.name_thm a) ths, [])])) args);
|
12063
|
403 |
in
|
12273
|
404 |
thy |> ProofContext.init |> activate_locale_i name |> activate_elem note; (*test attributes!*)
|
|
405 |
thy |> put_locale name (make_locale import (elems @ [note]) params text closed)
|
12063
|
406 |
end;
|
11896
|
407 |
|
12063
|
408 |
|
11896
|
409 |
|
|
410 |
(** locale theory setup **)
|
12063
|
411 |
|
11896
|
412 |
val setup =
|
|
413 |
[LocalesData.init];
|
|
414 |
|
|
415 |
end;
|
|
416 |
|
|
417 |
structure BasicLocale: BASIC_LOCALE = Locale;
|
|
418 |
open BasicLocale;
|