# HG changeset patch # User haftmann # Date 1400770789 -7200 # Node ID 78651e94746f851c714f6ad79e142d2c93ae3c86 # Parent 2869310dae2a9bcc44a12d7dec2f464ad17109fb tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction diff -r 2869310dae2a -r 78651e94746f src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Thu May 22 16:59:49 2014 +0200 +++ b/src/Pure/Isar/named_target.ML Thu May 22 16:59:49 2014 +0200 @@ -58,10 +58,22 @@ end; -(* consts in locale *) +(* consts *) -fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = - Generic_Target.locale_declaration target true (fn phi => +fun locale_const locale prmode ((b, mx), rhs) = + Generic_Target.locale_declaration locale true (fn phi => + let + val b' = Morphism.binding phi b; + val rhs' = Morphism.term phi rhs; + val same_shape = Term.aconv_untyped (rhs, rhs'); + in + Generic_Target.generic_const same_shape prmode ((b', mx), rhs') + end) #> + Generic_Target.const_declaration + (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); + +fun class_const class prmode (b, rhs) = + Generic_Target.locale_declaration class true (fn phi => let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; @@ -69,34 +81,34 @@ (* FIXME workaround based on educated guess *) val prefix' = Binding.prefix_of b'; - val is_canonical_class = is_class andalso - (Binding.eq_name (b, b') + val is_canonical_class = + Binding.eq_name (b, b') andalso not (null prefix') - andalso List.last prefix' = (Class.class_prefix target, false) - orelse same_shape); + andalso List.last prefix' = (Class.class_prefix class, false) + orelse same_shape; in - not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs') + not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs') end) #> Generic_Target.const_declaration - (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); + (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs); (* define *) -fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = +fun locale_foundation target (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params - #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) + #-> (fn (lhs, def) => locale_const target Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); -fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = +fun class_foundation target (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params - #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) + #-> (fn (lhs, def) => class_const target Syntax.mode_default (b, lhs) #> Class.const target ((b, mx), (#1 params, #2 params, lhs)) #> pair (lhs, def)); -fun target_foundation (ta as Target {is_locale, is_class, ...}) = - if is_class then class_foundation ta - else if is_locale then locale_foundation ta +fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = + if is_class then class_foundation target + else if is_locale then locale_foundation target else Generic_Target.theory_foundation; @@ -109,18 +121,21 @@ (* abbrev *) -fun locale_abbrev ta prmode ((b, mx), t) xs = - Local_Theory.background_theory_result - (Sign.add_abbrev Print_Mode.internal (b, t)) #-> - (fn (lhs, _) => - locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); +fun locale_abbrev target prmode (b, mx) (t, _) xs = + Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) + #-> (fn (lhs, _) => + locale_const target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); -fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = - if is_locale then - lthy - |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs - |> is_class ? Class.abbrev target prmode ((b, mx), t') - else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; +fun class_abbrev target prmode (b, mx) (t, t') xs = + Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) + #-> (fn (lhs, _) => + class_const target prmode (b, Term.list_comb (Logic.unvarify_global lhs, xs))) + #> Class.abbrev target prmode ((b, mx), t'); + +fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = + if is_class then class_abbrev target + else if is_locale then locale_abbrev target + else Generic_Target.theory_abbrev; (* declaration *)