Reapply mixin patch: base for performance improvements.
authorballarin
Mon May 24 10:48:32 2010 +0200 (2010-05-24)
changeset 371017099a9ed3be2
parent 37100 c11cdb5e7e97
child 37102 785348a83a2b
Reapply mixin patch: base for performance improvements.
src/FOL/ex/LocaleTest.thy
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Sun May 23 19:30:29 2010 -0700
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Mon May 24 10:48:32 2010 +0200
     1.3 @@ -533,7 +533,7 @@
     1.4    grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
     1.5    grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
     1.6  
     1.7 -text {* Mixin not applied to locales further up the hierachy. *}
     1.8 +text {* Setup *}
     1.9  
    1.10  locale mixin = reflexive
    1.11  begin
    1.12 @@ -548,16 +548,6 @@
    1.13      by (simp add: reflexive.less_def[OF reflexive] gless_def)
    1.14  qed
    1.15  
    1.16 -thm le.less_def  (* mixin not applied *)
    1.17 -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
    1.18 -thm le.less_thm  (* mixin applied *)
    1.19 -lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
    1.20 -
    1.21 -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
    1.22 -  by (rule le.less_def)
    1.23 -lemma "gless(x, y) <-> gle(x, y) & x ~= y"
    1.24 -  by (rule le.less_thm)
    1.25 -
    1.26  text {* Mixin propagated along the locale hierarchy *}
    1.27  
    1.28  locale mixin2 = mixin
     2.1 --- a/src/Pure/Isar/class.ML	Sun May 23 19:30:29 2010 -0700
     2.2 +++ b/src/Pure/Isar/class.ML	Mon May 24 10:48:32 2010 +0200
     2.3 @@ -293,8 +293,7 @@
     2.4      |-> (fn (param_map, params, assm_axiom) =>
     2.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     2.6      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
     2.7 -       Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
     2.8 -         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
     2.9 +       Locale.add_registration (class, base_morph)
    2.10           (Option.map (rpair true) eq_morph) export_morph
    2.11      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    2.12      |> Theory_Target.init (SOME class)
     3.1 --- a/src/Pure/Isar/locale.ML	Sun May 23 19:30:29 2010 -0700
     3.2 +++ b/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     3.3 @@ -384,9 +384,10 @@
     3.4    |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
     3.5      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
     3.6  
     3.7 -fun all_registrations thy = Registrations.get thy
     3.8 -  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
     3.9 -  (* without inherited mixins *)
    3.10 +fun all_registrations thy = Registrations.get thy (* FIXME clone *)
    3.11 +  (* with inherited mixins *)
    3.12 +  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
    3.13 +    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    3.14  
    3.15  fun activate_notes' activ_elem transfer thy export (name, morph) input =
    3.16    let
    3.17 @@ -462,19 +463,21 @@
    3.18  fun add_registration (name, base_morph) mixin export thy =
    3.19    let
    3.20      val base = instance_of thy name base_morph;
    3.21 +    val mix = case mixin of NONE => Morphism.identity
    3.22 +          | SOME (mix, _) => mix;
    3.23    in
    3.24      if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
    3.25      then thy
    3.26      else
    3.27        (get_idents (Context.Theory thy), thy)
    3.28        (* add new registrations with inherited mixins *)
    3.29 -      |> roundup thy (add_reg export) export (name, base_morph)
    3.30 +      |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
    3.31        |> snd
    3.32        (* add mixin *)
    3.33        |> (case mixin of NONE => I
    3.34 -           | SOME mixin => amend_registration (name, base_morph) mixin export)
    3.35 +           | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
    3.36        (* activate import hierarchy as far as not already active *)
    3.37 -      |> Context.theory_map (activate_facts' export (name, base_morph))
    3.38 +      |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
    3.39    end;
    3.40  
    3.41