src/Pure/Isar/named_target.ML
author wenzelm
Sun Nov 06 21:51:46 2011 +0100 (2011-11-06 ago)
changeset 45375 7fe19930dfc9
parent 45353 68f3e073ee21
child 45390 e29521ef9059
permissions -rw-r--r--
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
misc tuning;
wenzelm@41959
     1
(*  Title:      Pure/Isar/named_target.ML
wenzelm@20894
     2
    Author:     Makarius
wenzelm@30437
     3
    Author:     Florian Haftmann, TU Muenchen
wenzelm@20894
     4
haftmann@38350
     5
Targets for theory, locale and class.
wenzelm@20894
     6
*)
wenzelm@20894
     7
haftmann@38350
     8
signature NAMED_TARGET =
wenzelm@20894
     9
sig
wenzelm@41585
    10
  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
haftmann@38388
    11
  val theory_init: theory -> local_theory
haftmann@38391
    12
  val reinit: local_theory -> local_theory -> local_theory
wenzelm@35205
    13
  val context_cmd: xstring -> theory -> local_theory
haftmann@38391
    14
  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
wenzelm@20894
    15
end;
wenzelm@20894
    16
haftmann@38350
    17
structure Named_Target: NAMED_TARGET =
wenzelm@20894
    18
struct
wenzelm@20894
    19
wenzelm@21006
    20
(* context data *)
wenzelm@21006
    21
wenzelm@41585
    22
datatype target =
wenzelm@41585
    23
  Target of {target: string, is_locale: bool, is_class: bool,
wenzelm@41585
    24
    before_exit: local_theory -> local_theory};
wenzelm@25012
    25
wenzelm@41585
    26
fun make_target target is_locale is_class before_exit =
wenzelm@41585
    27
  Target {target = target, is_locale = is_locale, is_class = is_class,
wenzelm@41585
    28
    before_exit = before_exit};
wenzelm@41585
    29
wenzelm@41585
    30
fun named_target _ "" before_exit = make_target "" false false before_exit
wenzelm@41585
    31
  | named_target thy locale before_exit =
haftmann@38378
    32
      if Locale.defined thy locale
wenzelm@41585
    33
      then make_target locale true (Class.is_class thy locale) before_exit
haftmann@38378
    34
      else error ("No such locale: " ^ quote locale);
wenzelm@25012
    35
wenzelm@33519
    36
structure Data = Proof_Data
wenzelm@21006
    37
(
haftmann@38391
    38
  type T = target option;
haftmann@38391
    39
  fun init _ = NONE;
wenzelm@21006
    40
);
wenzelm@21006
    41
wenzelm@41585
    42
val peek =
wenzelm@41585
    43
  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
wenzelm@41585
    44
    {target = target, is_locale = is_locale, is_class = is_class});
wenzelm@21006
    45
wenzelm@21006
    46
wenzelm@33456
    47
(* generic declarations *)
wenzelm@33456
    48
wenzelm@45311
    49
fun locale_declaration locale syntax decl lthy =
haftmann@24838
    50
  let
haftmann@38305
    51
    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
haftmann@38305
    52
    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
haftmann@24838
    53
  in
haftmann@38305
    54
    lthy
haftmann@38305
    55
    |> Local_Theory.target (add locale locale_decl)
haftmann@24838
    56
  end;
haftmann@24838
    57
wenzelm@45311
    58
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl =
wenzelm@45311
    59
  if target = "" then Generic_Target.theory_declaration decl
wenzelm@45311
    60
  else
wenzelm@45311
    61
    locale_declaration target syntax decl
wenzelm@45311
    62
    #> pervasive ? Generic_Target.theory_declaration decl
wenzelm@45311
    63
    #> not pervasive ? Context.proof_map (Morphism.form decl);
haftmann@24838
    64
wenzelm@21611
    65
haftmann@38297
    66
(* consts in locales *)
haftmann@38297
    67
wenzelm@45352
    68
fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
wenzelm@45352
    69
  locale_declaration target true (fn phi =>
wenzelm@45352
    70
    let
wenzelm@45352
    71
      val b' = Morphism.binding phi b;
wenzelm@45352
    72
      val rhs' = Morphism.term phi rhs;
wenzelm@45352
    73
      val arg = (b', Term.close_schematic_term rhs');
wenzelm@45352
    74
      val same_shape = Term.aconv_untyped (rhs, rhs');
haftmann@38297
    75
wenzelm@45352
    76
      (* FIXME workaround based on educated guess *)
wenzelm@45352
    77
      val prefix' = Binding.prefix_of b';
wenzelm@45352
    78
      val is_canonical_class = is_class andalso
wenzelm@45352
    79
        (Binding.eq_name (b, b')
wenzelm@45352
    80
          andalso not (null prefix')
wenzelm@45352
    81
          andalso List.last prefix' = (Class.class_prefix target, false)
wenzelm@45352
    82
        orelse same_shape);
wenzelm@45352
    83
    in
wenzelm@45352
    84
      not is_canonical_class ?
wenzelm@45352
    85
        (Context.mapping_result
wenzelm@45352
    86
          (Sign.add_abbrev Print_Mode.internal arg)
wenzelm@45352
    87
          (Proof_Context.add_abbrev Print_Mode.internal arg)
wenzelm@45352
    88
        #-> (fn (lhs' as Const (d, _), _) =>
wenzelm@45352
    89
            same_shape ?
wenzelm@45352
    90
              (Context.mapping
wenzelm@45352
    91
                (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
wenzelm@45352
    92
               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
wenzelm@45352
    93
    end);
haftmann@38305
    94
haftmann@38297
    95
haftmann@38318
    96
(* define *)
haftmann@38318
    97
haftmann@38318
    98
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
haftmann@38341
    99
  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
wenzelm@45352
   100
  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
haftmann@38318
   101
    #> pair (lhs, def))
haftmann@38318
   102
haftmann@38318
   103
fun class_foundation (ta as Target {target, ...})
haftmann@38318
   104
    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
haftmann@38341
   105
  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
wenzelm@45352
   106
  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
haftmann@38619
   107
    #> Class.const target ((b, mx), (type_params, lhs))
haftmann@38318
   108
    #> pair (lhs, def))
haftmann@38318
   109
haftmann@39639
   110
fun target_foundation (ta as Target {is_locale, is_class, ...}) =
haftmann@38349
   111
  if is_class then class_foundation ta
haftmann@38349
   112
  else if is_locale then locale_foundation ta
haftmann@38349
   113
  else Generic_Target.theory_foundation;
haftmann@38303
   114
wenzelm@24939
   115
haftmann@38308
   116
(* notes *)
haftmann@38308
   117
wenzelm@40782
   118
fun locale_notes locale kind global_facts local_facts lthy =
haftmann@38308
   119
  let
wenzelm@45375
   120
    val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
haftmann@38310
   121
    val local_facts' = Element.facts_map
wenzelm@45290
   122
      (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
haftmann@38308
   123
  in
haftmann@38308
   124
    lthy
wenzelm@39557
   125
    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
haftmann@38308
   126
    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
haftmann@38308
   127
  end
haftmann@38308
   128
haftmann@39639
   129
fun target_notes (Target {target, is_locale, ...}) =
haftmann@38319
   130
  if is_locale then locale_notes target
wenzelm@40782
   131
  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
haftmann@38308
   132
haftmann@38308
   133
haftmann@38308
   134
(* abbrev *)
haftmann@38308
   135
wenzelm@38757
   136
fun locale_abbrev ta prmode ((b, mx), t) xs =
wenzelm@38757
   137
  Local_Theory.background_theory_result
wenzelm@38757
   138
    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
wenzelm@45352
   139
      (fn (lhs, _) => locale_const ta prmode
wenzelm@38757
   140
        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
haftmann@38308
   141
haftmann@38308
   142
fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
haftmann@38312
   143
    prmode (b, mx) (global_rhs, t') xs lthy =
wenzelm@38757
   144
  if is_locale then
wenzelm@38757
   145
    lthy
wenzelm@38757
   146
    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
wenzelm@38757
   147
    |> is_class ? Class.abbrev target prmode ((b, mx), t')
wenzelm@38757
   148
  else
wenzelm@38757
   149
    lthy
wenzelm@38757
   150
    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
haftmann@38308
   151
haftmann@38308
   152
haftmann@38308
   153
(* pretty *)
haftmann@38308
   154
haftmann@39639
   155
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
haftmann@38308
   156
  let
wenzelm@42360
   157
    val thy = Proof_Context.theory_of ctxt;
haftmann@38308
   158
    val target_name =
haftmann@38308
   159
      [Pretty.command (if is_class then "class" else "locale"),
haftmann@38308
   160
        Pretty.str (" " ^ Locale.extern thy target)];
wenzelm@45353
   161
    val fixes =
wenzelm@45353
   162
      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
wenzelm@45353
   163
        (#1 (Proof_Context.inferred_fixes ctxt));
wenzelm@45353
   164
    val assumes =
wenzelm@45353
   165
      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
wenzelm@45353
   166
        (Assumption.all_assms_of ctxt);
haftmann@38308
   167
    val elems =
haftmann@38308
   168
      (if null fixes then [] else [Element.Fixes fixes]) @
haftmann@38308
   169
      (if null assumes then [] else [Element.Assumes assumes]);
wenzelm@40782
   170
    val body_elems =
wenzelm@40782
   171
      if not is_locale then []
haftmann@39639
   172
      else if null elems then [Pretty.block target_name]
haftmann@39639
   173
      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
wenzelm@40782
   174
        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
haftmann@38308
   175
  in
haftmann@39639
   176
    Pretty.block [Pretty.command "theory", Pretty.brk 1,
wenzelm@42360
   177
      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
haftmann@38308
   178
  end;
haftmann@38308
   179
haftmann@38308
   180
haftmann@38378
   181
(* init *)
wenzelm@25291
   182
wenzelm@41585
   183
fun init_context (Target {target, is_locale, is_class, ...}) =
wenzelm@42360
   184
  if not is_locale then Proof_Context.init_global
haftmann@29576
   185
  else if not is_class then Locale.init target
haftmann@38379
   186
  else Class.init target;
haftmann@25269
   187
wenzelm@41585
   188
fun init before_exit target thy =
haftmann@39639
   189
  let
wenzelm@41585
   190
    val ta = named_target thy target before_exit;
haftmann@39639
   191
  in
haftmann@39639
   192
    thy
haftmann@39639
   193
    |> init_context ta
haftmann@39639
   194
    |> Data.put (SOME ta)
haftmann@39639
   195
    |> Local_Theory.init NONE (Long_Name.base_name target)
haftmann@39639
   196
       {define = Generic_Target.define (target_foundation ta),
haftmann@39639
   197
        notes = Generic_Target.notes (target_notes ta),
haftmann@39639
   198
        abbrev = Generic_Target.abbrev (target_abbrev ta),
wenzelm@45291
   199
        declaration = target_declaration ta,
haftmann@39639
   200
        pretty = pretty ta,
wenzelm@41585
   201
        exit = Local_Theory.target_of o before_exit}
haftmann@39639
   202
  end;
haftmann@38247
   203
wenzelm@41585
   204
val theory_init = init I "";
haftmann@25269
   205
wenzelm@38757
   206
fun reinit lthy =
wenzelm@41585
   207
  (case Data.get lthy of
wenzelm@45352
   208
    SOME (Target {target, before_exit, ...}) =>
wenzelm@45352
   209
      init before_exit target o Local_Theory.exit_global
wenzelm@38757
   210
  | NONE => error "Not in a named target");
haftmann@38391
   211
wenzelm@41585
   212
fun context_cmd "-" thy = init I "" thy
wenzelm@41585
   213
  | context_cmd target thy = init I (Locale.intern thy target) thy;
wenzelm@33282
   214
wenzelm@20894
   215
end;