139 |
139 |
140 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
140 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
141 |
141 |
142 |
142 |
143 |
143 |
144 (** theory data **) |
144 (** term and type instantiation, using symbol tables **) |
145 |
|
146 structure Termlisttab = TableFun(type key = term list |
|
147 val ord = Library.list_ord Term.term_ord); |
|
148 |
|
149 structure GlobalLocalesArgs = |
|
150 struct |
|
151 val name = "Isar/locales"; |
|
152 type T = NameSpace.T * locale Symtab.table * |
|
153 ((string * Attrib.src list) * thm list) Termlisttab.table |
|
154 Symtab.table; |
|
155 (* 1st entry: locale namespace, |
|
156 2nd entry: locales of the theory, |
|
157 3rd entry: registrations: theorems instantiating locale assumptions, |
|
158 with prefix and attributes, indexed by locale name and parameter |
|
159 instantiation *) |
|
160 |
|
161 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); |
|
162 val copy = I; |
|
163 val prep_ext = I; |
|
164 |
|
165 fun join_locs ({predicate, import, elems, params}: locale, |
|
166 {elems = elems', ...}: locale) = |
|
167 SOME {predicate = predicate, import = import, |
|
168 elems = gen_merge_lists eq_snd elems elems', |
|
169 params = params}; |
|
170 (* joining of registrations: prefix and attributes of left theory, |
|
171 thmsss are equal *) |
|
172 fun join_regs (reg, _) = SOME reg; |
|
173 fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = |
|
174 (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), |
|
175 Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2)); |
|
176 |
|
177 fun print _ (space, locs, _) = |
|
178 Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) |
|
179 |> Pretty.writeln; |
|
180 end; |
|
181 |
|
182 structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); |
|
183 val _ = Context.add_setup [GlobalLocalesData.init]; |
|
184 |
|
185 |
|
186 |
|
187 (** context data **) |
|
188 |
|
189 structure LocalLocalesArgs = |
|
190 struct |
|
191 val name = "Isar/locales"; |
|
192 type T = ((string * Args.src list) * thm list) Termlisttab.table |
|
193 Symtab.table; |
|
194 (* registrations: theorems instantiating locale assumptions, |
|
195 with prefix and attributes, indexed by locale name and parameter |
|
196 instantiation *) |
|
197 fun init _ = Symtab.empty; |
|
198 fun print _ _ = (); |
|
199 end; |
|
200 |
|
201 structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); |
|
202 val _ = Context.add_setup [LocalLocalesData.init]; |
|
203 |
|
204 |
|
205 (* access locales *) |
|
206 |
|
207 val print_locales = GlobalLocalesData.print; |
|
208 |
|
209 val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg; |
|
210 val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg; |
|
211 |
|
212 fun declare_locale name = |
|
213 GlobalLocalesData.map (fn (space, locs, regs) => |
|
214 (NameSpace.extend (space, [name]), locs, regs)); |
|
215 |
|
216 fun put_locale name loc = |
|
217 GlobalLocalesData.map (fn (space, locs, regs) => |
|
218 (space, Symtab.update ((name, loc), locs), regs)); |
|
219 |
|
220 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); |
|
221 |
|
222 fun the_locale thy name = |
|
223 (case get_locale thy name of |
|
224 SOME loc => loc |
|
225 | NONE => error ("Unknown locale " ^ quote name)); |
|
226 |
|
227 |
|
228 (* access registrations *) |
|
229 |
|
230 (* Ids of global registrations are varified, |
|
231 Ids of local registrations are not. |
|
232 Thms of registrations are never varified. *) |
|
233 |
|
234 (* retrieve registration from theory or context *) |
|
235 |
|
236 fun gen_get_registrations get thy_ctxt name = |
|
237 case Symtab.lookup (get thy_ctxt, name) of |
|
238 NONE => [] |
|
239 | SOME tab => Termlisttab.dest tab; |
|
240 |
|
241 val get_global_registrations = |
|
242 gen_get_registrations (#3 o GlobalLocalesData.get); |
|
243 val get_local_registrations = |
|
244 gen_get_registrations LocalLocalesData.get; |
|
245 |
|
246 fun gen_get_registration get thy_ctxt (name, ps) = |
|
247 case Symtab.lookup (get thy_ctxt, name) of |
|
248 NONE => NONE |
|
249 | SOME tab => Termlisttab.lookup (tab, ps); |
|
250 |
|
251 val get_global_registration = |
|
252 gen_get_registration (#3 o GlobalLocalesData.get); |
|
253 val get_local_registration = |
|
254 gen_get_registration LocalLocalesData.get; |
|
255 |
|
256 val test_global_registration = isSome oo get_global_registration; |
|
257 val test_local_registration = isSome oo get_local_registration; |
|
258 fun smart_test_registration ctxt id = |
|
259 let |
|
260 val thy = ProofContext.theory_of ctxt; |
|
261 in |
|
262 test_global_registration thy id orelse test_local_registration ctxt id |
|
263 end; |
|
264 |
|
265 |
|
266 (* add registration to theory or context, ignored if already present *) |
|
267 |
|
268 fun gen_put_registration map (name, ps) attn = |
|
269 map (fn regs => |
|
270 let |
|
271 val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty); |
|
272 in |
|
273 Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)), |
|
274 regs) |
|
275 end handle Termlisttab.DUP _ => regs); |
|
276 |
|
277 val put_global_registration = |
|
278 gen_put_registration (fn f => |
|
279 GlobalLocalesData.map (fn (space, locs, regs) => |
|
280 (space, locs, f regs))); |
|
281 val put_local_registration = gen_put_registration LocalLocalesData.map; |
|
282 |
|
283 (* TODO: needed? *) |
|
284 fun smart_put_registration id attn ctxt = |
|
285 (* ignore registration if already present in theory *) |
|
286 let |
|
287 val thy = ProofContext.theory_of ctxt; |
|
288 in case get_global_registration thy id of |
|
289 NONE => put_local_registration id attn ctxt |
|
290 | SOME _ => ctxt |
|
291 end; |
|
292 |
|
293 |
|
294 (* add witness theorem to registration in theory or context, |
|
295 ignored if registration not present *) |
|
296 |
|
297 fun gen_add_witness map (name, ps) thm = |
|
298 map (fn regs => |
|
299 let |
|
300 val tab = valOf (Symtab.lookup (regs, name)); |
|
301 val (x, thms) = valOf (Termlisttab.lookup (tab, ps)); |
|
302 in |
|
303 Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)), |
|
304 regs) |
|
305 end handle Option => regs); |
|
306 |
|
307 val add_global_witness = |
|
308 gen_add_witness (fn f => |
|
309 GlobalLocalesData.map (fn (space, locs, regs) => |
|
310 (space, locs, f regs))); |
|
311 val add_local_witness = gen_add_witness LocalLocalesData.map; |
|
312 |
|
313 |
|
314 (* import hierarchy |
|
315 implementation could be more efficient, eg. by maintaining a database |
|
316 of dependencies *) |
|
317 |
|
318 fun imports thy (upper, lower) = |
|
319 let |
|
320 val sign = sign_of thy; |
|
321 fun imps (Locale name) low = (name = low) orelse |
|
322 (case get_locale thy name of |
|
323 NONE => false |
|
324 | SOME {import, ...} => imps import low) |
|
325 | imps (Rename (expr, _)) low = imps expr low |
|
326 | imps (Merge es) low = exists (fn e => imps e low) es; |
|
327 in |
|
328 imps (Locale (intern sign upper)) (intern sign lower) |
|
329 end; |
|
330 |
|
331 |
|
332 (* printing of registrations *) |
|
333 |
|
334 fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt = |
|
335 let |
|
336 val ctxt = mk_ctxt thy_ctxt; |
|
337 val thy = ProofContext.theory_of ctxt; |
|
338 val sg = Theory.sign_of thy; |
|
339 |
|
340 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
|
341 val prt_atts = Args.pretty_attribs ctxt; |
|
342 fun prt_inst (ts, (("", []), thms)) = |
|
343 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)) |
|
344 | prt_inst (ts, ((prfx, atts), thms)) = |
|
345 Pretty.block (Pretty.breaks |
|
346 (Pretty.str prfx :: prt_atts atts @ [Pretty.str ":", Pretty.brk 1, |
|
347 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))])); |
|
348 |
|
349 val loc_int = intern sg loc; |
|
350 val regs = get_regs thy_ctxt; |
|
351 val loc_regs = Symtab.lookup (regs, loc_int); |
|
352 in |
|
353 (case loc_regs of |
|
354 NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") |
|
355 | SOME r => let |
|
356 val r' = Termlisttab.dest r; |
|
357 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; |
|
358 in Pretty.big_list ("Interpretations in " ^ msg ^ ":") |
|
359 (map prt_inst r'') |
|
360 end) |
|
361 |> Pretty.writeln |
|
362 end; |
|
363 |
|
364 val print_global_registrations = |
|
365 gen_print_registrations (#3 o GlobalLocalesData.get) |
|
366 ProofContext.init "theory"; |
|
367 val print_local_registrations' = |
|
368 gen_print_registrations LocalLocalesData.get |
|
369 I "context"; |
|
370 fun print_local_registrations loc ctxt = |
|
371 (print_global_registrations loc (ProofContext.theory_of ctxt); |
|
372 print_local_registrations' loc ctxt); |
|
373 |
|
374 |
|
375 (* diagnostics *) |
|
376 |
|
377 fun err_in_locale ctxt msg ids = |
|
378 let |
|
379 val sign = ProofContext.sign_of ctxt; |
|
380 fun prt_id (name, parms) = |
|
381 [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; |
|
382 val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
|
383 val err_msg = |
|
384 if forall (equal "" o #1) ids then msg |
|
385 else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
|
386 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
|
387 in raise ProofContext.CONTEXT (err_msg, ctxt) end; |
|
388 |
|
389 (* Version for identifiers with axioms *) |
|
390 |
|
391 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
|
392 |
|
393 |
|
394 (** primitives **) |
|
395 |
|
396 (* map elements *) |
|
397 |
|
398 fun map_elem {name, var, typ, term, fact, attrib} = |
|
399 fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => |
|
400 let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) |
|
401 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
|
402 ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) => |
|
403 (term t, (map term ps, map term qs)))))) |
|
404 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
|
405 ((name a, map attrib atts), (term t, map term ps)))) |
|
406 | Notes facts => Notes (facts |> map (fn ((a, atts), bs) => |
|
407 ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); |
|
408 |
|
409 fun map_values typ term thm = map_elem |
|
410 {name = I, var = I, typ = typ, term = term, fact = map thm, |
|
411 attrib = Args.map_values I typ term thm}; |
|
412 |
|
413 |
|
414 (* map attributes *) |
|
415 |
|
416 fun map_attrib_specs f = map (apfst (apsnd (map f))); |
|
417 fun map_attrib_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); |
|
418 |
|
419 fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f}; |
|
420 |
|
421 fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy)); |
|
422 |
|
423 fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem) |
|
424 | intern_attrib_elem_expr _ (Expr expr) = Expr expr; |
|
425 |
|
426 |
|
427 (* renaming *) |
|
428 |
|
429 fun rename ren x = getOpt (assoc_string (ren, x), x); |
|
430 |
|
431 fun rename_var ren (x, mx) = |
|
432 let val x' = rename ren x in |
|
433 if x = x' then (x, mx) |
|
434 else (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) |
|
435 end; |
|
436 |
|
437 fun rename_term ren (Free (x, T)) = Free (rename ren x, T) |
|
438 | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u |
|
439 | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) |
|
440 | rename_term _ a = a; |
|
441 |
|
442 fun rename_thm ren th = |
|
443 let |
|
444 val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; |
|
445 val cert = Thm.cterm_of sign; |
|
446 val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps)); |
|
447 val xs' = map (rename ren) xs; |
|
448 fun cert_frees names = map (cert o Free) (names ~~ Ts); |
|
449 fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); |
|
450 in |
|
451 if xs = xs' then th |
|
452 else |
|
453 th |
|
454 |> Drule.implies_intr_list (map cert hyps) |
|
455 |> Drule.forall_intr_list (cert_frees xs) |
|
456 |> Drule.forall_elim_list (cert_vars xs) |
|
457 |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') |
|
458 |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) |
|
459 end; |
|
460 |
|
461 fun rename_elem ren = |
|
462 map_values I (rename_term ren) (rename_thm ren) o |
|
463 map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren}; |
|
464 |
|
465 fun rename_facts prfx elem = |
|
466 let |
|
467 fun qualify (arg as ((name, atts), x)) = |
|
468 if prfx = "" orelse name = "" then arg |
|
469 else ((NameSpace.pack [prfx, name], atts), x); |
|
470 in |
|
471 (case elem of |
|
472 Fixes fixes => Fixes fixes |
|
473 | Assumes asms => Assumes (map qualify asms) |
|
474 | Defines defs => Defines (map qualify defs) |
|
475 | Notes facts => Notes (map qualify facts)) |
|
476 end; |
|
477 |
|
478 |
|
479 (* type instantiation *) |
|
480 |
|
481 fun inst_type [] T = T |
|
482 | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; |
|
483 |
|
484 fun inst_term [] t = t |
|
485 | inst_term env t = Term.map_term_types (inst_type env) t; |
|
486 |
|
487 fun inst_thm _ [] th = th |
|
488 | inst_thm ctxt env th = |
|
489 let |
|
490 val sign = ProofContext.sign_of ctxt; |
|
491 val cert = Thm.cterm_of sign; |
|
492 val certT = Thm.ctyp_of sign; |
|
493 val {hyps, prop, maxidx, ...} = Thm.rep_thm th; |
|
494 val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); |
|
495 val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; |
|
496 in |
|
497 if null env' then th |
|
498 else |
|
499 th |
|
500 |> Drule.implies_intr_list (map cert hyps) |
|
501 |> Drule.tvars_intr_list (map (#1 o #1) env') |
|
502 |> (fn (th', al) => th' |> |
|
503 Thm.instantiate ((map (fn ((a, _), T) => |
|
504 (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), [])) |
|
505 |> (fn th'' => Drule.implies_elim_list th'' |
|
506 (map (Thm.assume o cert o inst_term env') hyps)) |
|
507 end; |
|
508 |
|
509 fun inst_elem ctxt env = |
|
510 map_values (inst_type env) (inst_term env) (inst_thm ctxt env); |
|
511 |
|
512 |
|
513 (* term and type instantiation, variant using symbol tables *) |
|
514 |
145 |
515 (* instantiate TFrees *) |
146 (* instantiate TFrees *) |
516 |
147 |
517 fun tinst_tab_type tinst T = if Symtab.is_empty tinst |
148 fun tinst_tab_type tinst T = if Symtab.is_empty tinst |
518 then T |
149 then T |
591 |> Drule.forall_intr_list (map (cert o #1) inst') |
220 |> Drule.forall_intr_list (map (cert o #1) inst') |
592 |> Drule.forall_elim_list (map (cert o #2) inst') |
221 |> Drule.forall_elim_list (map (cert o #2) inst') |
593 |> (fn th => Drule.implies_elim_list th |
222 |> (fn th => Drule.implies_elim_list th |
594 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) |
223 (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) |
595 end; |
224 end; |
|
225 |
|
226 |
|
227 (** registration management **) |
|
228 |
|
229 structure Registrations : |
|
230 sig |
|
231 type T |
|
232 val empty: T |
|
233 val join: T * T -> T |
|
234 val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list |
|
235 val lookup: Sign.sg -> T * term list -> |
|
236 ((string * Attrib.src list) * thm list) option |
|
237 val insert: Sign.sg -> term list * (string * Attrib.src list) -> T -> |
|
238 T * (term list * ((string * Attrib.src list) * thm list)) list |
|
239 val add_witness: term list -> thm -> T -> T |
|
240 end = |
|
241 struct |
|
242 (* a registration consists of theorems instantiating locale assumptions |
|
243 and prefix and attributes, indexed by parameter instantiation *) |
|
244 type T = ((string * Attrib.src list) * thm list) Termtab.table; |
|
245 |
|
246 val empty = Termtab.empty; |
|
247 |
|
248 (* term list represented as single term, for simultaneous matching *) |
|
249 fun termify ts = |
|
250 Library.foldl (op $) (Const ("", map fastype_of ts ---> propT), ts); |
|
251 fun untermify t = |
|
252 let fun ut (Const _) ts = ts |
|
253 | ut (s $ t) ts = ut s (t::ts) |
|
254 in ut t [] end; |
|
255 |
|
256 (* joining of registrations: prefix and attributs of left theory, |
|
257 thms are equal, no attempt to subsumption testing *) |
|
258 val join = Termtab.join (fn (reg, _) => SOME reg); |
|
259 |
|
260 fun dest regs = map (apfst untermify) (Termtab.dest regs); |
|
261 |
|
262 (* registrations that subsume t *) |
|
263 fun subsumers tsig t regs = |
|
264 List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs); |
|
265 |
|
266 (* look up registration, pick one that subsumes the query *) |
|
267 fun lookup sign (regs, ts) = |
|
268 let |
|
269 val tsig = Sign.tsig_of sign; |
|
270 val t = termify ts; |
|
271 val subs = subsumers tsig t regs; |
|
272 in (case subs of |
|
273 [] => NONE |
|
274 | ((t', (attn, thms)) :: _) => let |
|
275 val (tinst, inst) = Pattern.match tsig (t', t); |
|
276 (* thms contain Frees, not Vars *) |
|
277 val tinst' = tinst |> Vartab.dest |
|
278 |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) |
|
279 |> Symtab.make; |
|
280 val inst' = inst |> Vartab.dest |
|
281 |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) |
|
282 |> Symtab.make; |
|
283 in |
|
284 SOME (attn, map (inst_tab_thm sign (inst', tinst')) thms) |
|
285 end) |
|
286 end; |
|
287 |
|
288 (* add registration if not subsumed by ones already present, |
|
289 additionally returns registrations that are strictly subsumed *) |
|
290 fun insert sign (ts, attn) regs = |
|
291 let |
|
292 val tsig = Sign.tsig_of sign; |
|
293 val t = termify ts; |
|
294 val subs = subsumers tsig t regs ; |
|
295 in (case subs of |
|
296 [] => let |
|
297 val sups = |
|
298 List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs); |
|
299 val sups' = map (apfst untermify) sups |
|
300 in (Termtab.update ((t, (attn, [])), regs), sups') end |
|
301 | _ => (regs, [])) |
|
302 end; |
|
303 |
|
304 (* add witness theorem to registration, |
|
305 only if instantiation is exact, otherwise excpetion Option raised *) |
|
306 fun add_witness ts thm regs = |
|
307 let |
|
308 val t = termify ts; |
|
309 val (x, thms) = valOf (Termtab.lookup (regs, t)); |
|
310 in |
|
311 Termtab.update ((t, (x, thm::thms)), regs) |
|
312 end; |
|
313 end; |
|
314 |
|
315 (** theory data **) |
|
316 |
|
317 structure GlobalLocalesArgs = |
|
318 struct |
|
319 val name = "Isar/locales"; |
|
320 type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table; |
|
321 (* 1st entry: locale namespace, |
|
322 2nd entry: locales of the theory, |
|
323 3rd entry: registrations, indexed by locale name *) |
|
324 |
|
325 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); |
|
326 val copy = I; |
|
327 val prep_ext = I; |
|
328 |
|
329 fun join_locs ({predicate, import, elems, params}: locale, |
|
330 {elems = elems', ...}: locale) = |
|
331 SOME {predicate = predicate, import = import, |
|
332 elems = gen_merge_lists eq_snd elems elems', |
|
333 params = params}; |
|
334 fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = |
|
335 (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), |
|
336 Symtab.join (SOME o Registrations.join) (regs1, regs2)); |
|
337 |
|
338 fun print _ (space, locs, _) = |
|
339 Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) |
|
340 |> Pretty.writeln; |
|
341 end; |
|
342 |
|
343 structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); |
|
344 val _ = Context.add_setup [GlobalLocalesData.init]; |
|
345 |
|
346 |
|
347 |
|
348 (** context data **) |
|
349 |
|
350 structure LocalLocalesArgs = |
|
351 struct |
|
352 val name = "Isar/locales"; |
|
353 type T = Registrations.T Symtab.table; |
|
354 (* registrations, indexed by locale name *) |
|
355 fun init _ = Symtab.empty; |
|
356 fun print _ _ = (); |
|
357 end; |
|
358 |
|
359 structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); |
|
360 val _ = Context.add_setup [LocalLocalesData.init]; |
|
361 |
|
362 |
|
363 (* access locales *) |
|
364 |
|
365 val print_locales = GlobalLocalesData.print; |
|
366 |
|
367 val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg; |
|
368 val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg; |
|
369 |
|
370 fun declare_locale name = |
|
371 GlobalLocalesData.map (fn (space, locs, regs) => |
|
372 (NameSpace.extend (space, [name]), locs, regs)); |
|
373 |
|
374 fun put_locale name loc = |
|
375 GlobalLocalesData.map (fn (space, locs, regs) => |
|
376 (space, Symtab.update ((name, loc), locs), regs)); |
|
377 |
|
378 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); |
|
379 |
|
380 fun the_locale thy name = |
|
381 (case get_locale thy name of |
|
382 SOME loc => loc |
|
383 | NONE => error ("Unknown locale " ^ quote name)); |
|
384 |
|
385 |
|
386 (* access registrations *) |
|
387 |
|
388 (* Ids of global registrations are varified, |
|
389 Ids of local registrations are not. |
|
390 Thms of registrations are never varified. *) |
|
391 |
|
392 (* retrieve registration from theory or context *) |
|
393 |
|
394 fun gen_get_registrations get thy_ctxt name = |
|
395 case Symtab.lookup (get thy_ctxt, name) of |
|
396 NONE => [] |
|
397 | SOME reg => Registrations.dest reg; |
|
398 |
|
399 val get_global_registrations = |
|
400 gen_get_registrations (#3 o GlobalLocalesData.get); |
|
401 val get_local_registrations = |
|
402 gen_get_registrations LocalLocalesData.get; |
|
403 |
|
404 fun gen_get_registration get get_sg thy_ctxt (name, ps) = |
|
405 case Symtab.lookup (get thy_ctxt, name) of |
|
406 NONE => NONE |
|
407 | SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps); |
|
408 |
|
409 val get_global_registration = |
|
410 gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of; |
|
411 val get_local_registration = |
|
412 gen_get_registration LocalLocalesData.get ProofContext.sign_of; |
|
413 |
|
414 val test_global_registration = isSome oo get_global_registration; |
|
415 val test_local_registration = isSome oo get_local_registration; |
|
416 fun smart_test_registration ctxt id = |
|
417 let |
|
418 val thy = ProofContext.theory_of ctxt; |
|
419 in |
|
420 test_global_registration thy id orelse test_local_registration ctxt id |
|
421 end; |
|
422 |
|
423 |
|
424 (* add registration to theory or context, ignored if subsumed *) |
|
425 |
|
426 fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt = |
|
427 map_data (fn regs => |
|
428 let |
|
429 val sg = get_sg thy_ctxt; |
|
430 val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty); |
|
431 val (reg', sups) = Registrations.insert sg (ps, attn) reg; |
|
432 val _ = if not (null sups) then warning |
|
433 ("Subsumed interpretation(s) of locale " ^ |
|
434 quote (cond_extern sg name) ^ |
|
435 "\nby interpretation(s) with the following prefix(es):\n" ^ |
|
436 commas_quote (map (fn (_, ((s, _), _)) => s) sups)) |
|
437 else (); |
|
438 in Symtab.update ((name, reg'), regs) end) thy_ctxt; |
|
439 |
|
440 val put_global_registration = |
|
441 gen_put_registration (fn f => |
|
442 GlobalLocalesData.map (fn (space, locs, regs) => |
|
443 (space, locs, f regs))) Theory.sign_of; |
|
444 val put_local_registration = |
|
445 gen_put_registration LocalLocalesData.map ProofContext.sign_of; |
|
446 |
|
447 (* TODO: needed? *) |
|
448 (* |
|
449 fun smart_put_registration id attn ctxt = |
|
450 (* ignore registration if already present in theory *) |
|
451 let |
|
452 val thy = ProofContext.theory_of ctxt; |
|
453 in case get_global_registration thy id of |
|
454 NONE => put_local_registration id attn ctxt |
|
455 | SOME _ => ctxt |
|
456 end; |
|
457 *) |
|
458 |
|
459 (* add witness theorem to registration in theory or context, |
|
460 ignored if registration not present *) |
|
461 |
|
462 fun gen_add_witness map (name, ps) thm = |
|
463 map (fn regs => |
|
464 let |
|
465 val reg = valOf (Symtab.lookup (regs, name)); |
|
466 in |
|
467 Symtab.update ((name, Registrations.add_witness ps thm reg), regs) |
|
468 end handle Option => regs); |
|
469 |
|
470 val add_global_witness = |
|
471 gen_add_witness (fn f => |
|
472 GlobalLocalesData.map (fn (space, locs, regs) => |
|
473 (space, locs, f regs))); |
|
474 val add_local_witness = gen_add_witness LocalLocalesData.map; |
|
475 |
|
476 |
|
477 (* import hierarchy |
|
478 implementation could be more efficient, eg. by maintaining a database |
|
479 of dependencies *) |
|
480 |
|
481 fun imports thy (upper, lower) = |
|
482 let |
|
483 val sign = sign_of thy; |
|
484 fun imps (Locale name) low = (name = low) orelse |
|
485 (case get_locale thy name of |
|
486 NONE => false |
|
487 | SOME {import, ...} => imps import low) |
|
488 | imps (Rename (expr, _)) low = imps expr low |
|
489 | imps (Merge es) low = exists (fn e => imps e low) es; |
|
490 in |
|
491 imps (Locale (intern sign upper)) (intern sign lower) |
|
492 end; |
|
493 |
|
494 |
|
495 (* printing of registrations *) |
|
496 |
|
497 fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt = |
|
498 let |
|
499 val ctxt = mk_ctxt thy_ctxt; |
|
500 val thy = ProofContext.theory_of ctxt; |
|
501 val sg = Theory.sign_of thy; |
|
502 |
|
503 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
|
504 val prt_atts = Args.pretty_attribs ctxt; |
|
505 fun prt_inst (ts, (("", []), thms)) = |
|
506 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)) |
|
507 | prt_inst (ts, ((prfx, atts), thms)) = |
|
508 Pretty.block ( |
|
509 (Pretty.breaks (Pretty.str prfx :: prt_atts atts) @ |
|
510 [Pretty.str ":", Pretty.brk 1, |
|
511 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))])); |
|
512 |
|
513 val loc_int = intern sg loc; |
|
514 val regs = get_regs thy_ctxt; |
|
515 val loc_regs = Symtab.lookup (regs, loc_int); |
|
516 in |
|
517 (case loc_regs of |
|
518 NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") |
|
519 | SOME r => let |
|
520 val r' = Registrations.dest r; |
|
521 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; |
|
522 in Pretty.big_list ("Interpretations in " ^ msg ^ ":") |
|
523 (map prt_inst r'') |
|
524 end) |
|
525 |> Pretty.writeln |
|
526 end; |
|
527 |
|
528 val print_global_registrations = |
|
529 gen_print_registrations (#3 o GlobalLocalesData.get) |
|
530 ProofContext.init "theory"; |
|
531 val print_local_registrations' = |
|
532 gen_print_registrations LocalLocalesData.get |
|
533 I "context"; |
|
534 fun print_local_registrations loc ctxt = |
|
535 (print_global_registrations loc (ProofContext.theory_of ctxt); |
|
536 print_local_registrations' loc ctxt); |
|
537 |
|
538 |
|
539 (* diagnostics *) |
|
540 |
|
541 fun err_in_locale ctxt msg ids = |
|
542 let |
|
543 val sign = ProofContext.sign_of ctxt; |
|
544 fun prt_id (name, parms) = |
|
545 [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; |
|
546 val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
|
547 val err_msg = |
|
548 if forall (equal "" o #1) ids then msg |
|
549 else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
|
550 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
|
551 in raise ProofContext.CONTEXT (err_msg, ctxt) end; |
|
552 |
|
553 (* Version for identifiers with axioms *) |
|
554 |
|
555 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
|
556 |
|
557 |
|
558 (** primitives **) |
|
559 |
|
560 (* map elements *) |
|
561 |
|
562 fun map_elem {name, var, typ, term, fact, attrib} = |
|
563 fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => |
|
564 let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) |
|
565 | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
|
566 ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) => |
|
567 (term t, (map term ps, map term qs)))))) |
|
568 | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
|
569 ((name a, map attrib atts), (term t, map term ps)))) |
|
570 | Notes facts => Notes (facts |> map (fn ((a, atts), bs) => |
|
571 ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); |
|
572 |
|
573 fun map_values typ term thm = map_elem |
|
574 {name = I, var = I, typ = typ, term = term, fact = map thm, |
|
575 attrib = Args.map_values I typ term thm}; |
|
576 |
|
577 |
|
578 (* map attributes *) |
|
579 |
|
580 fun map_attrib_specs f = map (apfst (apsnd (map f))); |
|
581 fun map_attrib_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); |
|
582 |
|
583 fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f}; |
|
584 |
|
585 fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy)); |
|
586 |
|
587 fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem) |
|
588 | intern_attrib_elem_expr _ (Expr expr) = Expr expr; |
|
589 |
|
590 |
|
591 (* renaming *) |
|
592 |
|
593 fun rename ren x = getOpt (assoc_string (ren, x), x); |
|
594 |
|
595 fun rename_var ren (x, mx) = |
|
596 let val x' = rename ren x in |
|
597 if x = x' then (x, mx) |
|
598 else (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) |
|
599 end; |
|
600 |
|
601 fun rename_term ren (Free (x, T)) = Free (rename ren x, T) |
|
602 | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u |
|
603 | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) |
|
604 | rename_term _ a = a; |
|
605 |
|
606 fun rename_thm ren th = |
|
607 let |
|
608 val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; |
|
609 val cert = Thm.cterm_of sign; |
|
610 val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps)); |
|
611 val xs' = map (rename ren) xs; |
|
612 fun cert_frees names = map (cert o Free) (names ~~ Ts); |
|
613 fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); |
|
614 in |
|
615 if xs = xs' then th |
|
616 else |
|
617 th |
|
618 |> Drule.implies_intr_list (map cert hyps) |
|
619 |> Drule.forall_intr_list (cert_frees xs) |
|
620 |> Drule.forall_elim_list (cert_vars xs) |
|
621 |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') |
|
622 |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) |
|
623 end; |
|
624 |
|
625 fun rename_elem ren = |
|
626 map_values I (rename_term ren) (rename_thm ren) o |
|
627 map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren}; |
|
628 |
|
629 fun rename_facts prfx elem = |
|
630 let |
|
631 fun qualify (arg as ((name, atts), x)) = |
|
632 if prfx = "" orelse name = "" then arg |
|
633 else ((NameSpace.pack [prfx, name], atts), x); |
|
634 in |
|
635 (case elem of |
|
636 Fixes fixes => Fixes fixes |
|
637 | Assumes asms => Assumes (map qualify asms) |
|
638 | Defines defs => Defines (map qualify defs) |
|
639 | Notes facts => Notes (map qualify facts)) |
|
640 end; |
|
641 |
|
642 |
|
643 (* type instantiation *) |
|
644 |
|
645 fun inst_type [] T = T |
|
646 | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T; |
|
647 |
|
648 fun inst_term [] t = t |
|
649 | inst_term env t = Term.map_term_types (inst_type env) t; |
|
650 |
|
651 fun inst_thm _ [] th = th |
|
652 | inst_thm ctxt env th = |
|
653 let |
|
654 val sign = ProofContext.sign_of ctxt; |
|
655 val cert = Thm.cterm_of sign; |
|
656 val certT = Thm.ctyp_of sign; |
|
657 val {hyps, prop, maxidx, ...} = Thm.rep_thm th; |
|
658 val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); |
|
659 val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; |
|
660 in |
|
661 if null env' then th |
|
662 else |
|
663 th |
|
664 |> Drule.implies_intr_list (map cert hyps) |
|
665 |> Drule.tvars_intr_list (map (#1 o #1) env') |
|
666 |> (fn (th', al) => th' |> |
|
667 Thm.instantiate ((map (fn ((a, _), T) => |
|
668 (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), [])) |
|
669 |> (fn th'' => Drule.implies_elim_list th'' |
|
670 (map (Thm.assume o cert o inst_term env') hyps)) |
|
671 end; |
|
672 |
|
673 fun inst_elem ctxt env = |
|
674 map_values (inst_type env) (inst_term env) (inst_thm ctxt env); |
|
675 |
|
676 |
|
677 (* term and type instantiation, variant using symbol tables *) |
|
678 |
|
679 (* instantiate TFrees *) |
|
680 |
|
681 fun tinst_tab_elem sg tinst = |
|
682 map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst); |
|
683 |
|
684 (* instantiate TFrees and Frees *) |
596 |
685 |
597 fun inst_tab_elem sg (inst as (_, tinst)) = |
686 fun inst_tab_elem sg (inst as (_, tinst)) = |
598 map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); |
687 map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); |
599 |
688 |
600 fun inst_tab_elems sign inst ((n, ps), elems) = |
689 fun inst_tab_elems sign inst ((n, ps), elems) = |