366 end; |
366 end; |
367 |
367 |
368 fun collect_mixins thy (name, morph) = |
368 fun collect_mixins thy (name, morph) = |
369 roundup thy (fn dep => fn mixins => |
369 roundup thy (fn dep => fn mixins => |
370 merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], []) |
370 merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], []) |
371 |> snd |> filter (snd o fst); (* only inheritable mixins *) |
371 |> snd |> filter (snd o fst); (* only inheritable mixins *) (* FIXME *) |
372 (* FIXME refactor usage *) |
372 (* FIXME refactor usage *) |
373 |
373 |
374 fun compose_mixins mixins = |
374 fun compose_mixins mixins = |
375 fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; |
375 fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; |
376 |
376 |
460 (* Note that a registration that would be subsumed by an existing one will not be |
460 (* Note that a registration that would be subsumed by an existing one will not be |
461 generated, and it will not be possible to amend it. *) |
461 generated, and it will not be possible to amend it. *) |
462 |
462 |
463 fun add_registration (name, base_morph) mixin export thy = |
463 fun add_registration (name, base_morph) mixin export thy = |
464 let |
464 let |
465 val base = instance_of thy name base_morph; |
|
466 val mix = case mixin of NONE => Morphism.identity |
465 val mix = case mixin of NONE => Morphism.identity |
467 | SOME (mix, _) => mix; |
466 | SOME (mix, _) => mix; |
468 in |
467 val morph = base_morph $> mix; |
469 if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base) |
468 val inst = instance_of thy name morph; |
|
469 in |
|
470 if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, inst) |
470 then thy |
471 then thy |
471 else |
472 else |
472 (get_idents (Context.Theory thy), thy) |
473 (get_idents (Context.Theory thy), thy) |
473 (* add new registrations with inherited mixins *) |
474 (* add new registrations with inherited mixins *) |
474 |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *) |
475 |> roundup thy (add_reg export) export (name, morph) |
475 |> snd |
476 |> snd |
476 (* add mixin *) |
477 (* add mixin *) |
477 |> (case mixin of NONE => I |
478 |> (case mixin of NONE => I |
478 | SOME mixin => amend_registration (name, base_morph $> mix) mixin export) |
479 | SOME mixin => amend_registration (name, morph) mixin export) |
479 (* activate import hierarchy as far as not already active *) |
480 (* activate import hierarchy as far as not already active *) |
480 |> Context.theory_map (activate_facts' export (name, base_morph $> mix)) |
481 |> Context.theory_map (activate_facts' export (name, morph)) |
481 end; |
482 end; |
482 |
483 |
483 |
484 |
484 (*** Dependencies ***) |
485 (*** Dependencies ***) |
485 |
486 |
486 fun add_reg_activate_facts export (dep, morph) thy = |
487 fun add_dependency loc (name, morph) export thy = |
487 (get_idents (Context.Theory thy), thy) |
488 let |
488 |> roundup thy (add_reg export) export (dep, morph) |
489 val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy; |
489 |> snd |
490 val (_, regs) = fold_rev (roundup thy' cons export) |
490 |> Context.theory_map (activate_facts' export (dep, morph)); |
491 (all_registrations thy') (get_idents (Context.Theory thy'), []); |
491 |
492 in |
492 fun add_dependency loc (dep, morph) export thy = |
493 thy' |
493 thy |
494 |> fold_rev (fn dep => add_registration dep NONE export) regs |
494 |> (change_locale loc o apsnd) (cons ((dep, (morph, export)), serial ())) |
495 end; |
495 |> (fn thy => fold_rev (add_reg_activate_facts export) |
|
496 (all_registrations thy) thy); |
|
497 |
496 |
498 |
497 |
499 (*** Storing results ***) |
498 (*** Storing results ***) |
500 |
499 |
501 (* Theorems *) |
500 (* Theorems *) |