src/Pure/Isar/generic_target.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 60924 610794dff23c
child 61701 e89cfc004f18
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm@41959
     1
(*  Title:      Pure/Isar/generic_target.ML
haftmann@38309
     2
    Author:     Makarius
haftmann@38309
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@38309
     4
haftmann@38309
     5
Common target infrastructure.
haftmann@38309
     6
*)
haftmann@38309
     7
haftmann@38309
     8
signature GENERIC_TARGET =
haftmann@38309
     9
sig
haftmann@60345
    10
  (*auxiliary*)
haftmann@60345
    11
  val export_abbrev: Proof.context ->
haftmann@60345
    12
      (term -> term) -> term -> term * ((string * sort) list * (term list * term list))
haftmann@60345
    13
  val check_mixfix_global: binding * bool -> mixfix -> mixfix
haftmann@60345
    14
haftmann@60340
    15
  (*background primitives*)
haftmann@57190
    16
  val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
haftmann@57190
    17
    term list * term list -> local_theory -> (term * thm) * local_theory
haftmann@57190
    18
  val background_declaration: declaration -> local_theory -> local_theory
haftmann@57190
    19
  val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
haftmann@57190
    20
haftmann@60340
    21
  (*nested local theories primitives*)
haftmann@60340
    22
  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
haftmann@60340
    23
    local_theory -> local_theory
haftmann@60340
    24
haftmann@60340
    25
  (*lifting target primitives to local theory operations*)
wenzelm@40782
    26
  val define: (((binding * typ) * mixfix) * (binding * term) ->
wenzelm@40782
    27
      term list * term list -> local_theory -> (term * thm) * local_theory) ->
wenzelm@46992
    28
    bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@40782
    29
    (term * (string * thm)) * local_theory
wenzelm@47250
    30
  val notes:
wenzelm@58011
    31
    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    32
      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
wenzelm@58011
    33
    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
wenzelm@40782
    34
    (string * thm list) list * local_theory
haftmann@60337
    35
  val abbrev: (Syntax.mode -> binding * mixfix -> term ->
haftmann@57160
    36
      term list * term list -> local_theory -> local_theory) ->
haftmann@60337
    37
    Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
haftmann@57190
    38
haftmann@60341
    39
  (*theory target primitives*)
haftmann@60341
    40
  val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
haftmann@60341
    41
     term list * term list -> local_theory -> (term * thm) * local_theory
haftmann@60341
    42
  val theory_target_notes: string ->
wenzelm@58011
    43
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    44
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@40782
    45
    local_theory -> local_theory
haftmann@60341
    46
  val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
haftmann@60341
    47
    local_theory -> local_theory
haftmann@60341
    48
haftmann@60341
    49
  (*theory target operations*)
haftmann@60344
    50
  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
haftmann@60344
    51
    local_theory -> (term * term) * local_theory
haftmann@57190
    52
  val theory_declaration: declaration -> local_theory -> local_theory
haftmann@52153
    53
  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
haftmann@52153
    54
    local_theory -> local_theory
haftmann@57190
    55
haftmann@60341
    56
  (*locale target primitives*)
haftmann@60341
    57
  val locale_target_notes: string -> string ->
wenzelm@58011
    58
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    59
    (Attrib.binding * (thm list * Token.src list) list) list ->
haftmann@57190
    60
    local_theory -> local_theory
haftmann@60344
    61
  val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
haftmann@60344
    62
    local_theory -> local_theory
haftmann@57192
    63
  val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
haftmann@60341
    64
  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
haftmann@60341
    65
    (binding * mixfix) * term -> local_theory -> local_theory
haftmann@60341
    66
haftmann@60341
    67
  (*locale operations*)
haftmann@60344
    68
  val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
haftmann@60344
    69
    local_theory -> (term * term) * local_theory
haftmann@57193
    70
  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
haftmann@57193
    71
    local_theory -> local_theory
haftmann@57190
    72
  val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
haftmann@57190
    73
    local_theory -> local_theory
haftmann@52153
    74
  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
haftmann@52153
    75
    local_theory -> local_theory
wenzelm@45353
    76
end
haftmann@38309
    77
haftmann@38309
    78
structure Generic_Target: GENERIC_TARGET =
haftmann@38309
    79
struct
haftmann@38309
    80
haftmann@57190
    81
(** consts **)
haftmann@38312
    82
haftmann@60345
    83
fun export_abbrev lthy preprocess rhs =
haftmann@60342
    84
  let
haftmann@60342
    85
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
haftmann@60342
    86
haftmann@60342
    87
    val rhs' = rhs
haftmann@60342
    88
      |> Assumption.export_term lthy (Local_Theory.target_of lthy)
haftmann@60342
    89
      |> preprocess;
haftmann@60342
    90
    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
haftmann@60342
    91
    val u = fold_rev lambda term_params rhs';
haftmann@60342
    92
    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
haftmann@60342
    93
haftmann@60342
    94
    val extra_tfrees =
haftmann@60342
    95
      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
haftmann@60342
    96
    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
haftmann@60345
    97
  in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
haftmann@60342
    98
haftmann@38312
    99
fun check_mixfix ctxt (b, extra_tfrees) mx =
haftmann@38312
   100
  if null extra_tfrees then mx
haftmann@38312
   101
  else
wenzelm@56294
   102
   (if Context_Position.is_visible ctxt then
wenzelm@56294
   103
      warning
wenzelm@56294
   104
        ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
wenzelm@60924
   105
          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
wenzelm@56294
   106
          (if mx = NoSyn then ""
wenzelm@56294
   107
           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
wenzelm@56294
   108
    else (); NoSyn);
haftmann@38312
   109
wenzelm@47291
   110
fun check_mixfix_global (b, no_params) mx =
wenzelm@47291
   111
  if no_params orelse mx = NoSyn then mx
wenzelm@47291
   112
  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
wenzelm@47291
   113
    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
wenzelm@47291
   114
haftmann@57190
   115
fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
haftmann@57190
   116
  if phi_pred phi then
haftmann@57190
   117
    let
haftmann@57190
   118
      val b' = Morphism.binding phi b;
haftmann@57190
   119
      val rhs' = Morphism.term phi rhs;
haftmann@57190
   120
      val same_shape = Term.aconv_untyped (rhs, rhs');
haftmann@57190
   121
      val const_alias =
haftmann@57190
   122
        if same_shape then
haftmann@57190
   123
          (case rhs' of
haftmann@57190
   124
            Const (c, T) =>
haftmann@57190
   125
              let
haftmann@57190
   126
                val thy = Context.theory_of context;
haftmann@57190
   127
                val ctxt = Context.proof_of context;
haftmann@57190
   128
              in
haftmann@57190
   129
                (case Type_Infer_Context.const_type ctxt c of
haftmann@57190
   130
                  SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
haftmann@57190
   131
                | NONE => NONE)
haftmann@57190
   132
              end
haftmann@57190
   133
          | _ => NONE)
haftmann@57190
   134
        else NONE;
haftmann@57190
   135
    in
wenzelm@60283
   136
      (case const_alias of
haftmann@57190
   137
        SOME c =>
haftmann@57190
   138
          context
haftmann@57190
   139
          |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
haftmann@57190
   140
          |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
haftmann@57190
   141
      | NONE =>
haftmann@57190
   142
          context
haftmann@57190
   143
          |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
haftmann@57190
   144
          |-> (fn (const as Const (c, _), _) => same_shape ?
haftmann@57190
   145
                (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
wenzelm@60283
   146
                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
haftmann@57190
   147
    end
haftmann@57190
   148
  else context;
haftmann@57190
   149
haftmann@57190
   150
wenzelm@60283
   151
haftmann@57190
   152
(** background primitives **)
haftmann@57190
   153
haftmann@57190
   154
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
haftmann@57190
   155
  let
haftmann@57190
   156
    val params = type_params @ term_params;
haftmann@57190
   157
    val mx' = check_mixfix_global (b, null params) mx;
haftmann@57190
   158
haftmann@57190
   159
    val (const, lthy2) = lthy
haftmann@57190
   160
      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
haftmann@57190
   161
    val lhs = Term.list_comb (const, params);
haftmann@57190
   162
haftmann@57190
   163
    val ((_, def), lthy3) = lthy2
haftmann@57190
   164
      |> Local_Theory.background_theory_result
wenzelm@61261
   165
        (Thm.add_def (Proof_Context.defs_context lthy2) false false
haftmann@57190
   166
          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
haftmann@57190
   167
  in ((lhs, def), lthy3) end;
haftmann@57190
   168
haftmann@57190
   169
fun background_declaration decl lthy =
haftmann@57190
   170
  let
haftmann@57190
   171
    val theory_decl =
haftmann@57190
   172
      Local_Theory.standard_form lthy
haftmann@57190
   173
        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
haftmann@57190
   174
  in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
haftmann@57190
   175
haftmann@57190
   176
fun background_abbrev (b, global_rhs) params =
haftmann@57190
   177
  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
wenzelm@59058
   178
  #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
haftmann@57190
   179
haftmann@57190
   180
wenzelm@60283
   181
haftmann@60340
   182
(** nested local theories primitives **)
haftmann@60340
   183
haftmann@60340
   184
fun standard_facts lthy ctxt =
haftmann@60340
   185
  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
haftmann@60340
   186
haftmann@60340
   187
fun standard_notes pred kind facts lthy =
haftmann@60340
   188
  Local_Theory.map_contexts (fn level => fn ctxt =>
haftmann@60340
   189
    if pred (Local_Theory.level lthy, level)
haftmann@60340
   190
    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
haftmann@60340
   191
    else ctxt) lthy;
haftmann@60340
   192
haftmann@60340
   193
fun standard_declaration pred decl lthy =
haftmann@60340
   194
  Local_Theory.map_contexts (fn level => fn ctxt =>
haftmann@60340
   195
    if pred (Local_Theory.level lthy, level)
haftmann@60340
   196
    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
haftmann@60340
   197
    else ctxt) lthy;
haftmann@60340
   198
haftmann@60340
   199
fun standard_const pred prmode ((b, mx), rhs) =
haftmann@60340
   200
  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
haftmann@60340
   201
haftmann@60340
   202
haftmann@60340
   203
(** lifting target primitives to local theory operations **)
haftmann@38312
   204
haftmann@38309
   205
(* define *)
haftmann@38309
   206
wenzelm@46992
   207
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
haftmann@38309
   208
  let
wenzelm@59616
   209
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
haftmann@38309
   210
haftmann@38309
   211
    (*term and type parameters*)
wenzelm@59621
   212
    val ((defs, _), rhs') = Thm.cterm_of lthy rhs
wenzelm@47276
   213
      |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
haftmann@38309
   214
wenzelm@47272
   215
    val xs = Variable.add_fixed lthy rhs' [];
haftmann@38309
   216
    val T = Term.fastype_of rhs;
haftmann@38309
   217
    val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
haftmann@38309
   218
    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
haftmann@38312
   219
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
haftmann@38309
   220
haftmann@38309
   221
    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
wenzelm@59058
   222
    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs);
haftmann@38309
   223
    val params = type_params @ term_params;
haftmann@38309
   224
haftmann@38309
   225
    val U = map Term.fastype_of params ---> T;
haftmann@38309
   226
haftmann@38309
   227
    (*foundation*)
wenzelm@45353
   228
    val ((lhs', global_def), lthy2) = lthy
wenzelm@45353
   229
      |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
haftmann@38309
   230
haftmann@38309
   231
    (*local definition*)
haftmann@38315
   232
    val ((lhs, local_def), lthy3) = lthy2
haftmann@38309
   233
      |> Local_Defs.add_def ((b, NoSyn), lhs');
wenzelm@47240
   234
wenzelm@47240
   235
    (*result*)
wenzelm@47238
   236
    val def =
wenzelm@47240
   237
      Thm.transitive local_def global_def
wenzelm@59621
   238
      |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
haftmann@38315
   239
    val ([(res_name, [res])], lthy4) = lthy3
wenzelm@47080
   240
      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
haftmann@38315
   241
  in ((lhs, (res_name, res)), lthy4) end;
haftmann@38309
   242
haftmann@38309
   243
haftmann@38309
   244
(* notes *)
haftmann@38309
   245
wenzelm@47250
   246
local
wenzelm@47250
   247
haftmann@38309
   248
fun import_export_proof ctxt (name, raw_th) =
haftmann@38309
   249
  let
wenzelm@59616
   250
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
haftmann@38309
   251
haftmann@38309
   252
    (*export assumes/defines*)
wenzelm@54883
   253
    val th = Goal.norm_result ctxt raw_th;
wenzelm@45407
   254
    val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
wenzelm@54742
   255
    val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
haftmann@38309
   256
haftmann@38309
   257
    (*export fixes*)
haftmann@38309
   258
    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
haftmann@38309
   259
    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
wenzelm@45352
   260
    val (th'' :: vs) =
wenzelm@59621
   261
      (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
haftmann@38309
   262
      |> Variable.export ctxt thy_ctxt
haftmann@38309
   263
      |> Drule.zero_var_indexes_list;
haftmann@38309
   264
haftmann@38309
   265
    (*thm definition*)
wenzelm@45413
   266
    val result = Global_Theory.name_thm true true name th'';
haftmann@38309
   267
haftmann@38309
   268
    (*import fixes*)
haftmann@38309
   269
    val (tvars, vars) =
haftmann@38309
   270
      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
haftmann@38309
   271
      |>> map Logic.dest_type;
haftmann@38309
   272
haftmann@38309
   273
    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
wenzelm@60642
   274
    val inst =
wenzelm@60642
   275
      map_filter
wenzelm@60642
   276
        (fn (Var (xi, T), t) =>
wenzelm@60642
   277
          SOME ((xi, Term_Subst.instantiateT instT T),
wenzelm@60642
   278
            Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
wenzelm@60642
   279
        | _ => NONE) (vars ~~ frees);
wenzelm@60642
   280
    val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
haftmann@38309
   281
haftmann@38309
   282
    (*import assumes/defines*)
haftmann@38309
   283
    val result'' =
wenzelm@45407
   284
      (fold (curry op COMP) asms' result'
wenzelm@45407
   285
        handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
wenzelm@54742
   286
      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
wenzelm@54883
   287
      |> Goal.norm_result ctxt
wenzelm@39557
   288
      |> Global_Theory.name_thm false false name;
haftmann@38309
   289
haftmann@38309
   290
  in (result'', result) end;
haftmann@38309
   291
wenzelm@47250
   292
in
wenzelm@47250
   293
haftmann@60341
   294
fun notes target_notes kind facts lthy =
haftmann@38309
   295
  let
haftmann@38309
   296
    val facts' = facts
wenzelm@39557
   297
      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
haftmann@38309
   298
          (Local_Theory.full_name lthy (fst a))) bs))
wenzelm@39557
   299
      |> Global_Theory.map_facts (import_export_proof lthy);
wenzelm@39557
   300
    val local_facts = Global_Theory.map_facts #1 facts';
wenzelm@39557
   301
    val global_facts = Global_Theory.map_facts #2 facts';
haftmann@38309
   302
  in
haftmann@38309
   303
    lthy
haftmann@60341
   304
    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
wenzelm@47249
   305
    |> Attrib.local_notes kind local_facts
haftmann@38309
   306
  end;
haftmann@38309
   307
wenzelm@47250
   308
end;
wenzelm@47250
   309
haftmann@38309
   310
haftmann@38309
   311
(* abbrev *)
haftmann@38309
   312
haftmann@60341
   313
fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
haftmann@38309
   314
  let
haftmann@60345
   315
    val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs;
haftmann@38312
   316
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
haftmann@38309
   317
  in
haftmann@38309
   318
    lthy
haftmann@60341
   319
    |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
haftmann@57109
   320
    |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
haftmann@57109
   321
    |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
haftmann@38309
   322
  end;
haftmann@38309
   323
haftmann@38341
   324
wenzelm@60283
   325
haftmann@60341
   326
(** theory target primitives **)
haftmann@38341
   327
haftmann@60341
   328
fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
wenzelm@47284
   329
  background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
haftmann@57192
   330
  #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
haftmann@57057
   331
    #> pair (lhs, def));
wenzelm@47284
   332
haftmann@60341
   333
fun theory_target_notes kind global_facts local_facts =
haftmann@57191
   334
  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
haftmann@57191
   335
  #> standard_notes (op <>) kind local_facts;
haftmann@38341
   336
haftmann@60341
   337
fun theory_target_abbrev prmode (b, mx) global_rhs params =
wenzelm@47286
   338
  Local_Theory.background_theory_result
haftmann@57109
   339
    (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
wenzelm@47291
   340
      (fn (lhs, _) =>  (* FIXME type_params!? *)
haftmann@57160
   341
        Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
haftmann@57192
   342
  #-> (fn lhs => standard_const (op <>) prmode
haftmann@57160
   343
          ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
haftmann@38341
   344
haftmann@60341
   345
haftmann@60341
   346
(** theory operations **)
haftmann@60341
   347
haftmann@60344
   348
val theory_abbrev = abbrev theory_target_abbrev;
haftmann@60344
   349
haftmann@60341
   350
fun theory_declaration decl =
haftmann@60341
   351
  background_declaration decl #> standard_declaration (K true) decl;
haftmann@60341
   352
haftmann@57190
   353
val theory_registration =
haftmann@57190
   354
  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
haftmann@57190
   355
haftmann@57190
   356
wenzelm@60283
   357
haftmann@60341
   358
(** locale target primitives **)
haftmann@57190
   359
haftmann@60341
   360
fun locale_target_notes locale kind global_facts local_facts =
haftmann@57190
   361
  Local_Theory.background_theory
haftmann@57190
   362
    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
haftmann@57190
   363
  (fn lthy => lthy |>
haftmann@57190
   364
    Local_Theory.target (fn ctxt => ctxt |>
haftmann@57190
   365
      Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
haftmann@57191
   366
  standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
haftmann@57190
   367
haftmann@57192
   368
fun locale_target_declaration locale syntax decl lthy = lthy
haftmann@57190
   369
  |> Local_Theory.target (fn ctxt => ctxt |>
haftmann@57190
   370
    Locale.add_declaration locale syntax
haftmann@57190
   371
      (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
haftmann@57190
   372
haftmann@60341
   373
fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
haftmann@60341
   374
  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
haftmann@60341
   375
haftmann@60341
   376
haftmann@60341
   377
(** locale operations **)
haftmann@60341
   378
haftmann@57193
   379
fun locale_declaration locale {syntax, pervasive} decl =
haftmann@57193
   380
  pervasive ? background_declaration decl
haftmann@57193
   381
  #> locale_target_declaration locale syntax decl
haftmann@57193
   382
  #> standard_declaration (fn (_, other) => other <> 0) decl;
haftmann@57193
   383
haftmann@57190
   384
fun locale_const locale prmode ((b, mx), rhs) =
haftmann@57192
   385
  locale_target_const locale (K true) prmode ((b, mx), rhs)
haftmann@57192
   386
  #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
haftmann@57190
   387
haftmann@57190
   388
fun locale_dependency locale dep_morph mixin export =
haftmann@57190
   389
  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
wenzelm@57926
   390
  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
wenzelm@47279
   391
haftmann@60344
   392
haftmann@60344
   393
(** locale abbreviations **)
haftmann@60344
   394
haftmann@60344
   395
fun locale_target_abbrev locale prmode (b, mx) global_rhs params =
haftmann@60344
   396
  background_abbrev (b, global_rhs) (snd params)
haftmann@60344
   397
  #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs));
haftmann@60344
   398
haftmann@60344
   399
fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
haftmann@60344
   400
haftmann@38309
   401
end;