src/Pure/Isar/named_target.ML
author wenzelm
Sat Nov 05 22:01:19 2011 +0100 (2011-11-05 ago)
changeset 45352 0b4038361a3a
parent 45311 ca9e66c523a2
child 45353 68f3e073ee21
permissions -rw-r--r--
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
haftmann@38308
   120
    val global_facts' = Attrib.map_facts (K 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)];
haftmann@38310
   161
    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
wenzelm@42360
   162
      (#1 (Proof_Context.inferred_fixes ctxt));
haftmann@38310
   163
    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
haftmann@38310
   164
      (Assumption.all_assms_of ctxt);
haftmann@38308
   165
    val elems =
haftmann@38308
   166
      (if null fixes then [] else [Element.Fixes fixes]) @
haftmann@38308
   167
      (if null assumes then [] else [Element.Assumes assumes]);
wenzelm@40782
   168
    val body_elems =
wenzelm@40782
   169
      if not is_locale then []
haftmann@39639
   170
      else if null elems then [Pretty.block target_name]
haftmann@39639
   171
      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
wenzelm@40782
   172
        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
haftmann@38308
   173
  in
haftmann@39639
   174
    Pretty.block [Pretty.command "theory", Pretty.brk 1,
wenzelm@42360
   175
      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
haftmann@38308
   176
  end;
haftmann@38308
   177
haftmann@38308
   178
haftmann@38378
   179
(* init *)
wenzelm@25291
   180
wenzelm@41585
   181
fun init_context (Target {target, is_locale, is_class, ...}) =
wenzelm@42360
   182
  if not is_locale then Proof_Context.init_global
haftmann@29576
   183
  else if not is_class then Locale.init target
haftmann@38379
   184
  else Class.init target;
haftmann@25269
   185
wenzelm@41585
   186
fun init before_exit target thy =
haftmann@39639
   187
  let
wenzelm@41585
   188
    val ta = named_target thy target before_exit;
haftmann@39639
   189
  in
haftmann@39639
   190
    thy
haftmann@39639
   191
    |> init_context ta
haftmann@39639
   192
    |> Data.put (SOME ta)
haftmann@39639
   193
    |> Local_Theory.init NONE (Long_Name.base_name target)
haftmann@39639
   194
       {define = Generic_Target.define (target_foundation ta),
haftmann@39639
   195
        notes = Generic_Target.notes (target_notes ta),
haftmann@39639
   196
        abbrev = Generic_Target.abbrev (target_abbrev ta),
wenzelm@45291
   197
        declaration = target_declaration ta,
haftmann@39639
   198
        pretty = pretty ta,
wenzelm@41585
   199
        exit = Local_Theory.target_of o before_exit}
haftmann@39639
   200
  end;
haftmann@38247
   201
wenzelm@41585
   202
val theory_init = init I "";
haftmann@25269
   203
wenzelm@38757
   204
fun reinit lthy =
wenzelm@41585
   205
  (case Data.get lthy of
wenzelm@45352
   206
    SOME (Target {target, before_exit, ...}) =>
wenzelm@45352
   207
      init before_exit target o Local_Theory.exit_global
wenzelm@38757
   208
  | NONE => error "Not in a named target");
haftmann@38391
   209
wenzelm@41585
   210
fun context_cmd "-" thy = init I "" thy
wenzelm@41585
   211
  | context_cmd target thy = init I (Locale.intern thy target) thy;
wenzelm@33282
   212
wenzelm@20894
   213
end;