# HG changeset patch # User wenzelm # Date 1333403725 -7200 # Node ID 57d486231c92b53cb60c104141e0318b591ac675 # Parent d6c76b1823fb2c02f0bfdbe6c354cde4d192dd32 more general standard_declaration; generic const declaration, which is applied to nested targets (named target only); diff -r d6c76b1823fb -r 57d486231c92 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Mon Apr 02 23:27:24 2012 +0200 +++ b/src/Pure/Isar/generic_target.ML Mon Apr 02 23:55:25 2012 +0200 @@ -25,7 +25,11 @@ string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val background_declaration: declaration -> local_theory -> local_theory val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory - val standard_declaration: declaration -> local_theory -> local_theory + val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory + val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> + Context.generic -> Context.generic + val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> + local_theory -> local_theory val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_notes: string -> @@ -215,9 +219,55 @@ Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); -fun standard_declaration decl lthy = - Local_Theory.map_contexts (fn _ => fn ctxt => - Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy; +fun standard_declaration pred decl lthy = + Local_Theory.map_contexts (fn level => fn ctxt => + if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt + else ctxt) lthy; + + +(* const declaration *) + +fun generic_const same_shape prmode ((b, mx), t) context = + let + val const_alias = + if same_shape then + (case t of + Const (c, T) => + let + val thy = Context.theory_of context; + val ctxt = Context.proof_of context; + val t' = Syntax.check_term ctxt (Const (c, dummyT)) + |> singleton (Variable.polymorphic ctxt); + in + (case t' of + Const (c', T') => + if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE + | _ => NONE) + end + | _ => NONE) + else NONE; + in + (case const_alias of + SOME c => + context + |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) + |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) + | NONE => + context + |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t) + |-> (fn (const as Const (c, _), _) => same_shape ? + (Proof_Context.generic_revert_abbrev (#1 prmode) c #> + Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) + end; + +fun const_declaration pred prmode ((b, mx), rhs) = + standard_declaration pred (fn phi => + let + val b' = Morphism.binding phi b; + val rhs' = Morphism.term phi rhs; + val rhs'' = Term.close_schematic_term rhs'; + val same_shape = Term.aconv_untyped (rhs, rhs'); + in generic_const same_shape prmode ((b', mx), rhs'') end); @@ -248,6 +298,6 @@ (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); fun theory_declaration decl = - background_declaration decl #> standard_declaration decl; + background_declaration decl #> standard_declaration (K true) decl; end; diff -r d6c76b1823fb -r 57d486231c92 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Mon Apr 02 23:27:24 2012 +0200 +++ b/src/Pure/Isar/named_target.ML Mon Apr 02 23:55:25 2012 +0200 @@ -46,40 +46,7 @@ (* consts in locale *) -fun generic_const same_shape prmode ((b, mx), t) context = - let - val const_alias = - if same_shape then - (case t of - Const (c, T) => - let - val thy = Context.theory_of context; - val ctxt = Context.proof_of context; - val t' = Syntax.check_term ctxt (Const (c, dummyT)) - |> singleton (Variable.polymorphic ctxt); - in - (case t' of - Const (c', T') => - if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE - | _ => NONE) - end - | _ => NONE) - else NONE; - in - (case const_alias of - SOME c => - context - |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) - |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) - | NONE => - context - |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t) - |-> (fn (const as Const (c, _), _) => same_shape ? - (Proof_Context.generic_revert_abbrev (#1 prmode) c #> - Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) - end; - -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = +fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = Generic_Target.locale_declaration target true (fn phi => let val b' = Morphism.binding phi b; @@ -94,27 +61,36 @@ andalso not (null prefix') andalso List.last prefix' = (Class.class_prefix target, false) orelse same_shape); - in not is_canonical_class ? generic_const same_shape prmode ((b', mx), rhs'') end); + in + not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs'') + end) #> + (fn lthy => lthy |> Generic_Target.const_declaration + (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); (* define *) +fun global_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) + #-> (fn (lhs, def) => Generic_Target.const_declaration (K true) Syntax.mode_default ((b, mx), lhs) + #> pair (lhs, def)); + fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) - #> pair (lhs, def)) + #> pair (lhs, def)); fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) (type_params, term_params) = Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) #> Class.const target ((b, mx), (type_params, lhs)) - #> pair (lhs, def)) + #> 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 - else Generic_Target.theory_foundation; + else global_foundation; (* notes *) @@ -151,9 +127,7 @@ lthy |> pervasive ? Generic_Target.background_declaration decl |> Generic_Target.locale_declaration target syntax decl - |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => - if level = 0 then ctxt - else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt)); + |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl); (* pretty *)