1.1 --- a/src/Pure/Isar/generic_target.ML Mon Apr 02 23:27:24 2012 +0200
1.2 +++ b/src/Pure/Isar/generic_target.ML Mon Apr 02 23:55:25 2012 +0200
1.3 @@ -25,7 +25,11 @@
1.4 string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
1.5 val background_declaration: declaration -> local_theory -> local_theory
1.6 val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
1.7 - val standard_declaration: declaration -> local_theory -> local_theory
1.8 + val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory
1.9 + val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term ->
1.10 + Context.generic -> Context.generic
1.11 + val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
1.12 + local_theory -> local_theory
1.13 val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
1.14 term list * term list -> local_theory -> (term * thm) * local_theory
1.15 val theory_notes: string ->
1.16 @@ -215,9 +219,55 @@
1.17 Locale.add_declaration locale syntax
1.18 (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
1.19
1.20 -fun standard_declaration decl lthy =
1.21 - Local_Theory.map_contexts (fn _ => fn ctxt =>
1.22 - Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy;
1.23 +fun standard_declaration pred decl lthy =
1.24 + Local_Theory.map_contexts (fn level => fn ctxt =>
1.25 + if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
1.26 + else ctxt) lthy;
1.27 +
1.28 +
1.29 +(* const declaration *)
1.30 +
1.31 +fun generic_const same_shape prmode ((b, mx), t) context =
1.32 + let
1.33 + val const_alias =
1.34 + if same_shape then
1.35 + (case t of
1.36 + Const (c, T) =>
1.37 + let
1.38 + val thy = Context.theory_of context;
1.39 + val ctxt = Context.proof_of context;
1.40 + val t' = Syntax.check_term ctxt (Const (c, dummyT))
1.41 + |> singleton (Variable.polymorphic ctxt);
1.42 + in
1.43 + (case t' of
1.44 + Const (c', T') =>
1.45 + if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
1.46 + | _ => NONE)
1.47 + end
1.48 + | _ => NONE)
1.49 + else NONE;
1.50 + in
1.51 + (case const_alias of
1.52 + SOME c =>
1.53 + context
1.54 + |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
1.55 + |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
1.56 + | NONE =>
1.57 + context
1.58 + |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
1.59 + |-> (fn (const as Const (c, _), _) => same_shape ?
1.60 + (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
1.61 + Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
1.62 + end;
1.63 +
1.64 +fun const_declaration pred prmode ((b, mx), rhs) =
1.65 + standard_declaration pred (fn phi =>
1.66 + let
1.67 + val b' = Morphism.binding phi b;
1.68 + val rhs' = Morphism.term phi rhs;
1.69 + val rhs'' = Term.close_schematic_term rhs';
1.70 + val same_shape = Term.aconv_untyped (rhs, rhs');
1.71 + in generic_const same_shape prmode ((b', mx), rhs'') end);
1.72
1.73
1.74
1.75 @@ -248,6 +298,6 @@
1.76 (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
1.77
1.78 fun theory_declaration decl =
1.79 - background_declaration decl #> standard_declaration decl;
1.80 + background_declaration decl #> standard_declaration (K true) decl;
1.81
1.82 end;
2.1 --- a/src/Pure/Isar/named_target.ML Mon Apr 02 23:27:24 2012 +0200
2.2 +++ b/src/Pure/Isar/named_target.ML Mon Apr 02 23:55:25 2012 +0200
2.3 @@ -46,40 +46,7 @@
2.4
2.5 (* consts in locale *)
2.6
2.7 -fun generic_const same_shape prmode ((b, mx), t) context =
2.8 - let
2.9 - val const_alias =
2.10 - if same_shape then
2.11 - (case t of
2.12 - Const (c, T) =>
2.13 - let
2.14 - val thy = Context.theory_of context;
2.15 - val ctxt = Context.proof_of context;
2.16 - val t' = Syntax.check_term ctxt (Const (c, dummyT))
2.17 - |> singleton (Variable.polymorphic ctxt);
2.18 - in
2.19 - (case t' of
2.20 - Const (c', T') =>
2.21 - if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
2.22 - | _ => NONE)
2.23 - end
2.24 - | _ => NONE)
2.25 - else NONE;
2.26 - in
2.27 - (case const_alias of
2.28 - SOME c =>
2.29 - context
2.30 - |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
2.31 - |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
2.32 - | NONE =>
2.33 - context
2.34 - |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
2.35 - |-> (fn (const as Const (c, _), _) => same_shape ?
2.36 - (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
2.37 - Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
2.38 - end;
2.39 -
2.40 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
2.41 +fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) =
2.42 Generic_Target.locale_declaration target true (fn phi =>
2.43 let
2.44 val b' = Morphism.binding phi b;
2.45 @@ -94,27 +61,36 @@
2.46 andalso not (null prefix')
2.47 andalso List.last prefix' = (Class.class_prefix target, false)
2.48 orelse same_shape);
2.49 - in not is_canonical_class ? generic_const same_shape prmode ((b', mx), rhs'') end);
2.50 + in
2.51 + not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs'')
2.52 + end) #>
2.53 + (fn lthy => lthy |> Generic_Target.const_declaration
2.54 + (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));
2.55
2.56
2.57 (* define *)
2.58
2.59 +fun global_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
2.60 + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
2.61 + #-> (fn (lhs, def) => Generic_Target.const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
2.62 + #> pair (lhs, def));
2.63 +
2.64 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
2.65 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
2.66 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
2.67 - #> pair (lhs, def))
2.68 + #> pair (lhs, def));
2.69
2.70 fun class_foundation (ta as Target {target, ...})
2.71 (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
2.72 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
2.73 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
2.74 #> Class.const target ((b, mx), (type_params, lhs))
2.75 - #> pair (lhs, def))
2.76 + #> pair (lhs, def));
2.77
2.78 fun target_foundation (ta as Target {is_locale, is_class, ...}) =
2.79 if is_class then class_foundation ta
2.80 else if is_locale then locale_foundation ta
2.81 - else Generic_Target.theory_foundation;
2.82 + else global_foundation;
2.83
2.84
2.85 (* notes *)
2.86 @@ -151,9 +127,7 @@
2.87 lthy
2.88 |> pervasive ? Generic_Target.background_declaration decl
2.89 |> Generic_Target.locale_declaration target syntax decl
2.90 - |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
2.91 - if level = 0 then ctxt
2.92 - else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
2.93 + |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
2.94
2.95
2.96 (* pretty *)