238 end; |
238 end; |
239 |
239 |
240 |
240 |
241 (*** Identifiers: activated locales in theory or proof context ***) |
241 (*** Identifiers: activated locales in theory or proof context ***) |
242 |
242 |
243 (* subsumption *) |
243 type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *) |
244 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts); |
244 |
245 (* smaller term is more general *) |
245 val empty_idents : idents = Symtab.empty; |
246 |
246 val insert_idents = Symtab.insert_list (eq_list (op aconv)); |
247 local |
247 val merge_idents = Symtab.merge_list (eq_list (op aconv)); |
248 |
248 |
249 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed; |
249 fun redundant_ident thy idents (name, instance) = |
250 |
250 exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name); |
251 structure Identifiers = Generic_Data |
251 |
|
252 structure Idents = Generic_Data |
252 ( |
253 ( |
253 type T = (string * term list) list delayed; |
254 type T = idents; |
254 val empty = Ready []; |
255 val empty = empty_idents; |
255 val extend = I; |
256 val extend = I; |
256 val merge = ToDo; |
257 val merge = merge_idents; |
257 ); |
258 ); |
258 |
|
259 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2) |
|
260 | finish _ (Ready ids) = ids; |
|
261 |
|
262 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy => |
|
263 (case Identifiers.get (Context.Theory thy) of |
|
264 Ready _ => NONE |
|
265 | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy))))); |
|
266 |
|
267 in |
|
268 |
|
269 val get_idents = (fn Ready ids => ids) o Identifiers.get; |
|
270 val put_idents = Identifiers.put o Ready; |
|
271 |
|
272 end; |
|
273 |
259 |
274 |
260 |
275 (** Resolve locale dependencies in a depth-first fashion **) |
261 (** Resolve locale dependencies in a depth-first fashion **) |
276 |
262 |
277 local |
263 local |
283 then error "Roundup bound exceeded (sublocale relation probably not terminating)." |
269 then error "Roundup bound exceeded (sublocale relation probably not terminating)." |
284 else |
270 else |
285 let |
271 let |
286 val instance = instance_of thy name (morph $> stem $> export); |
272 val instance = instance_of thy name (morph $> stem $> export); |
287 in |
273 in |
288 if member (ident_le thy) marked (name, instance) |
274 if redundant_ident thy marked (name, instance) then (deps, marked) |
289 then (deps, marked) |
|
290 else |
275 else |
291 let |
276 let |
292 val full_morph = morph $> compose_mixins mixins $> stem; |
277 val full_morph = morph $> compose_mixins mixins $> stem; |
293 (* no inheritance of mixins, regardless of requests by clients *) |
278 (* no inheritance of mixins, regardless of requests by clients *) |
294 val dependencies = dependencies_of thy name |> |
279 val dependencies = dependencies_of thy name |> |
295 map (fn ((name', (morph', export')), serial') => |
280 map (fn ((name', (morph', export')), serial') => |
296 (name', morph' $> export', mixins_of thy name serial')); |
281 (name', morph' $> export', mixins_of thy name serial')); |
297 val marked' = (name, instance) :: marked; |
282 val marked' = insert_idents (name, instance) marked; |
298 val (deps', marked'') = |
283 val (deps', marked'') = |
299 fold_rev (add thy (depth + 1) full_morph export) dependencies |
284 fold_rev (add thy (depth + 1) full_morph export) dependencies |
300 ([], marked'); |
285 ([], marked'); |
301 in |
286 in |
302 ((name, full_morph) :: deps' @ deps, marked'') |
287 ((name, full_morph) :: deps' @ deps, marked'') |
311 fun roundup thy activate_dep export (name, morph) (marked, input) = |
296 fun roundup thy activate_dep export (name, morph) (marked, input) = |
312 let |
297 let |
313 (* Find all dependencies including new ones (which are dependencies enriching |
298 (* Find all dependencies including new ones (which are dependencies enriching |
314 existing registrations). *) |
299 existing registrations). *) |
315 val (dependencies, marked') = |
300 val (dependencies, marked') = |
316 add thy 0 Morphism.identity export (name, morph, []) ([], []); |
301 add thy 0 Morphism.identity export (name, morph, []) ([], empty_idents); |
317 (* Filter out fragments from marked; these won't be activated. *) |
302 (* Filter out fragments from marked; these won't be activated. *) |
318 val dependencies' = filter_out (fn (name, morph) => |
303 val dependencies' = filter_out (fn (name, morph) => |
319 member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies; |
304 redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies; |
320 in |
305 in |
321 (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies') |
306 (merge_idents (marked, marked'), input |> fold_rev activate_dep dependencies') |
322 end; |
307 end; |
323 |
308 |
324 end; |
309 end; |
325 |
310 |
326 |
311 |
378 fun collect_mixins context (name, morph) = |
363 fun collect_mixins context (name, morph) = |
379 let |
364 let |
380 val thy = Context.theory_of context; |
365 val thy = Context.theory_of context; |
381 in |
366 in |
382 roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep)) |
367 roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep)) |
383 Morphism.identity (name, morph) ([(name, instance_of thy name morph)], []) |
368 Morphism.identity (name, morph) |
|
369 (insert_idents (name, instance_of thy name morph) empty_idents, []) |
384 |> snd |> filter (snd o fst) (* only inheritable mixins *) |
370 |> snd |> filter (snd o fst) (* only inheritable mixins *) |
385 |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph))) |
371 |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph))) |
386 |> compose_mixins |
372 |> compose_mixins |
387 end; |
373 end; |
388 |
374 |
448 |
434 |
449 fun activate_declarations dep = Context.proof_map (fn context => |
435 fun activate_declarations dep = Context.proof_map (fn context => |
450 let |
436 let |
451 val thy = Context.theory_of context; |
437 val thy = Context.theory_of context; |
452 in |
438 in |
453 roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context) |
439 roundup thy activate_syntax_decls Morphism.identity dep (Idents.get context, context) |
454 |-> put_idents |
440 |-> Idents.put |
455 end); |
441 end); |
456 |
442 |
457 fun activate_facts export dep context = |
443 fun activate_facts export dep context = |
458 let |
444 let |
459 val thy = Context.theory_of context; |
445 val thy = Context.theory_of context; |
460 val activate = |
446 val activate = |
461 activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export; |
447 activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export; |
462 in |
448 in |
463 roundup thy activate (the_default Morphism.identity export) dep (get_idents context, context) |
449 roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context) |
464 |-> put_idents |
450 |-> Idents.put |
465 end; |
451 end; |
466 |
452 |
467 fun init name thy = |
453 fun init name thy = |
468 activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) |
454 activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) |
469 ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of; |
455 (empty_idents, Context.Proof (Proof_Context.init_global thy)) |
|
456 |-> Idents.put |> Context.proof_of; |
470 |
457 |
471 |
458 |
472 (*** Add and extend registrations ***) |
459 (*** Add and extend registrations ***) |
473 |
460 |
474 fun amend_registration (name, morph) mixin export context = |
461 fun amend_registration (name, morph) mixin export context = |
494 val thy = Context.theory_of context; |
481 val thy = Context.theory_of context; |
495 val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); |
482 val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); |
496 val morph = base_morph $> mix; |
483 val morph = base_morph $> mix; |
497 val inst = instance_of thy name morph; |
484 val inst = instance_of thy name morph; |
498 in |
485 in |
499 if member (ident_le thy) (get_idents context) (name, inst) |
486 if redundant_ident thy (Idents.get context) (name, inst) |
500 then context (* FIXME amend mixins? *) |
487 then context (* FIXME amend mixins? *) |
501 else |
488 else |
502 (get_idents context, context) |
489 (Idents.get context, context) |
503 (* add new registrations with inherited mixins *) |
490 (* add new registrations with inherited mixins *) |
504 |> roundup thy (add_reg thy export) export (name, morph) |
491 |> roundup thy (add_reg thy export) export (name, morph) |
505 |> snd |
492 |> snd |
506 (* add mixin *) |
493 (* add mixin *) |
507 |> |
494 |> |
538 (apfst (cons ((name, (morph, export)), serial')) #> |
525 (apfst (cons ((name, (morph, export)), serial')) #> |
539 apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin)); |
526 apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin)); |
540 val context' = Context.Theory thy'; |
527 val context' = Context.Theory thy'; |
541 val (_, regs) = |
528 val (_, regs) = |
542 fold_rev (roundup thy' cons export) |
529 fold_rev (roundup thy' cons export) |
543 (registrations_of context' loc) (get_idents context', []); |
530 (registrations_of context' loc) (Idents.get context', []); |
544 in |
531 in |
545 thy' |
532 thy' |
546 |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs |
533 |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs |
547 end; |
534 end; |
548 |
535 |
638 val name = intern thy raw_name; |
625 val name = intern thy raw_name; |
639 val ctxt = init name thy; |
626 val ctxt = init name thy; |
640 fun cons_elem (elem as Notes _) = show_facts ? cons elem |
627 fun cons_elem (elem as Notes _) = show_facts ? cons elem |
641 | cons_elem elem = cons elem; |
628 | cons_elem elem = cons elem; |
642 val elems = |
629 val elems = |
643 activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], []) |
630 activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, []) |
644 |> snd |> rev; |
631 |> snd |> rev; |
645 in |
632 in |
646 Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems) |
633 Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems) |
647 |> Pretty.writeln |
634 |> Pretty.writeln |
648 end; |
635 end; |
659 end |> Pretty.writeln; |
646 end |> Pretty.writeln; |
660 |
647 |
661 fun print_dependencies ctxt clean export insts = |
648 fun print_dependencies ctxt clean export insts = |
662 let |
649 let |
663 val thy = Proof_Context.theory_of ctxt; |
650 val thy = Proof_Context.theory_of ctxt; |
664 val idents = if clean then [] else get_idents (Context.Proof ctxt); |
651 val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt); |
665 in |
652 in |
666 (case fold (roundup thy cons export) insts (idents, []) |> snd of |
653 (case fold (roundup thy cons export) insts (idents, []) |> snd of |
667 [] => Pretty.str "no dependencies" |
654 [] => Pretty.str "no dependencies" |
668 | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps))) |
655 | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps))) |
669 end |> Pretty.writeln; |
656 end |> Pretty.writeln; |