src/Pure/Isar/local_theory.ML
author haftmann
Wed May 22 22:56:17 2013 +0200 (2013-05-22)
changeset 52119 90ba620333d0
parent 52118 2a976115c7c3
child 52140 88a69da5d3fa
permissions -rw-r--r--
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
wenzelm@18744
     1
(*  Title:      Pure/Isar/local_theory.ML
wenzelm@18744
     2
    Author:     Makarius
wenzelm@18744
     3
wenzelm@20888
     4
Local theory operations, with abstract target context.
wenzelm@18744
     5
*)
wenzelm@18744
     6
wenzelm@18951
     7
type local_theory = Proof.context;
wenzelm@37949
     8
type generic_theory = Context.generic;
wenzelm@18951
     9
wenzelm@18744
    10
signature LOCAL_THEORY =
wenzelm@18744
    11
sig
wenzelm@20888
    12
  type operations
wenzelm@47066
    13
  val assert: local_theory -> local_theory
wenzelm@47273
    14
  val restore: local_theory -> local_theory
wenzelm@47064
    15
  val level: Proof.context -> int
wenzelm@47066
    16
  val assert_bottom: bool -> local_theory -> local_theory
haftmann@51735
    17
  val mark_brittle: local_theory -> local_theory
haftmann@51735
    18
  val assert_nonbrittle: local_theory -> local_theory
wenzelm@50739
    19
  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
wenzelm@50739
    20
    local_theory -> local_theory
wenzelm@47064
    21
  val close_target: local_theory -> local_theory
wenzelm@47245
    22
  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
wenzelm@33166
    23
  val naming_of: local_theory -> Name_Space.naming
wenzelm@33166
    24
  val full_name: local_theory -> binding -> string
wenzelm@33166
    25
  val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
wenzelm@33166
    26
  val conceal: local_theory -> local_theory
wenzelm@33724
    27
  val new_group: local_theory -> local_theory
wenzelm@33724
    28
  val reset_group: local_theory -> local_theory
wenzelm@33276
    29
  val restore_naming: local_theory -> local_theory -> local_theory
wenzelm@47245
    30
  val standard_morphism: local_theory -> Proof.context -> morphism
wenzelm@47245
    31
  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
wenzelm@20960
    32
  val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
wenzelm@20960
    33
  val raw_theory: (theory -> theory) -> local_theory -> local_theory
wenzelm@38757
    34
  val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
wenzelm@38757
    35
  val background_theory: (theory -> theory) -> local_theory -> local_theory
wenzelm@47245
    36
  val target_of: local_theory -> Proof.context
wenzelm@20888
    37
  val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
wenzelm@47245
    38
  val target_morphism: local_theory -> morphism
haftmann@52119
    39
  val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory
wenzelm@37949
    40
  val propagate_ml_env: generic_theory -> generic_theory
wenzelm@47066
    41
  val operations_of: local_theory -> operations
wenzelm@33764
    42
  val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@28083
    43
    (term * (string * thm)) * local_theory
wenzelm@46992
    44
  val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@46992
    45
    (term * (string * thm)) * local_theory
wenzelm@33670
    46
  val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
wenzelm@33670
    47
  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
wenzelm@33670
    48
    local_theory -> (string * thm list) list * local_theory
wenzelm@33670
    49
  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
wenzelm@28083
    50
    local_theory -> (string * thm list) list * local_theory
haftmann@38308
    51
  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
haftmann@38308
    52
    (term * term) * local_theory
wenzelm@45291
    53
  val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
haftmann@38308
    54
  val pretty: local_theory -> Pretty.T list
wenzelm@36451
    55
  val set_defsort: sort -> local_theory -> local_theory
wenzelm@35412
    56
  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
wenzelm@24949
    57
  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
wenzelm@35738
    58
  val class_alias: binding -> class -> local_theory -> local_theory
wenzelm@35738
    59
  val type_alias: binding -> string -> local_theory -> local_theory
wenzelm@35738
    60
  val const_alias: binding -> string -> local_theory -> local_theory
wenzelm@47061
    61
  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
wenzelm@21292
    62
  val exit: local_theory -> Proof.context
wenzelm@28395
    63
  val exit_global: local_theory -> theory
wenzelm@28395
    64
  val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
wenzelm@28395
    65
  val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
wenzelm@18744
    66
end;
wenzelm@18744
    67
wenzelm@33671
    68
structure Local_Theory: LOCAL_THEORY =
wenzelm@18744
    69
struct
wenzelm@18744
    70
wenzelm@20888
    71
(** local theory data **)
wenzelm@19059
    72
wenzelm@20888
    73
(* type lthy *)
wenzelm@20888
    74
wenzelm@20888
    75
type operations =
wenzelm@46992
    76
 {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@28083
    77
    (term * (string * thm)) * local_theory,
wenzelm@26131
    78
  notes: string ->
wenzelm@28084
    79
    (Attrib.binding * (thm list * Attrib.src list) list) list ->
wenzelm@28083
    80
    local_theory -> (string * thm list) list * local_theory,
haftmann@38308
    81
  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
haftmann@38308
    82
    (term * term) * local_theory,
wenzelm@45291
    83
  declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
haftmann@38308
    84
  pretty: local_theory -> Pretty.T list,
wenzelm@21292
    85
  exit: local_theory -> Proof.context};
wenzelm@20888
    86
wenzelm@47064
    87
type lthy =
wenzelm@33166
    88
 {naming: Name_Space.naming,
wenzelm@20888
    89
  operations: operations,
wenzelm@50739
    90
  after_close: local_theory -> local_theory,
haftmann@52118
    91
  brittle: bool,
wenzelm@20888
    92
  target: Proof.context};
wenzelm@20888
    93
haftmann@52118
    94
fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
haftmann@52118
    95
  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
wenzelm@20888
    96
wenzelm@20888
    97
wenzelm@20888
    98
(* context data *)
wenzelm@18744
    99
wenzelm@33519
   100
structure Data = Proof_Data
wenzelm@18744
   101
(
haftmann@52118
   102
  type T = lthy list;
haftmann@52118
   103
  fun init _ = [];
wenzelm@18744
   104
);
wenzelm@18744
   105
wenzelm@47066
   106
fun assert lthy =
haftmann@52118
   107
  if null (Data.get lthy) then error "Missing local theory context" else lthy;
wenzelm@47066
   108
haftmann@52118
   109
val get_last_lthy = List.last o Data.get o assert;
haftmann@52118
   110
val get_first_lthy = hd o Data.get o assert;
wenzelm@47066
   111
wenzelm@50739
   112
fun map_first_lthy f =
wenzelm@50739
   113
  assert #>
haftmann@52118
   114
  Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
haftmann@52118
   115
    make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
wenzelm@47066
   116
haftmann@52118
   117
fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
wenzelm@47273
   118
wenzelm@47064
   119
wenzelm@47064
   120
(* nested structure *)
wenzelm@33166
   121
haftmann@52118
   122
val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
wenzelm@47066
   123
wenzelm@47066
   124
fun assert_bottom b lthy =
wenzelm@47066
   125
  let
wenzelm@47066
   126
    val _ = assert lthy;
wenzelm@47066
   127
    val b' = level lthy <= 1;
wenzelm@47066
   128
  in
wenzelm@47066
   129
    if b andalso not b' then error "Not at bottom of local theory nesting"
wenzelm@47066
   130
    else if not b andalso b' then error "Already at bottom of local theory nesting"
wenzelm@47066
   131
    else lthy
wenzelm@47066
   132
  end;
wenzelm@47066
   133
wenzelm@50739
   134
fun open_target naming operations after_close target =
wenzelm@50739
   135
  assert target
haftmann@52118
   136
  |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
wenzelm@47064
   137
wenzelm@47064
   138
fun close_target lthy =
wenzelm@50739
   139
  let
wenzelm@50739
   140
    val _ = assert_bottom false lthy;
haftmann@52118
   141
    val ({after_close, ...} :: rest) = Data.get lthy;
haftmann@52118
   142
  in lthy |> Data.put rest |> restore |> after_close end;
wenzelm@26131
   143
wenzelm@47245
   144
fun map_contexts f lthy =
wenzelm@47245
   145
  let val n = level lthy in
haftmann@52118
   146
    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
haftmann@52118
   147
      make_lthy (naming, operations, after_close, brittle,
wenzelm@47245
   148
        target
wenzelm@47245
   149
        |> Context_Position.set_visible false
wenzelm@47245
   150
        |> f (n - i - 1)
wenzelm@47245
   151
        |> Context_Position.restore_visible target))
wenzelm@47245
   152
    |> f n
wenzelm@47245
   153
  end;
wenzelm@47245
   154
wenzelm@26131
   155
haftmann@51735
   156
(* brittle context -- implicit for nested structures *)
haftmann@51735
   157
haftmann@52118
   158
fun mark_brittle lthy =
haftmann@52118
   159
  if level lthy = 1
haftmann@52118
   160
  then map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
haftmann@52118
   161
    (naming, operations, after_close, true, target)) lthy
haftmann@52118
   162
  else lthy;
haftmann@51735
   163
haftmann@51735
   164
fun assert_nonbrittle lthy =
haftmann@52118
   165
  if #brittle (get_first_lthy lthy)
haftmann@51735
   166
  then error "Brittle local theory context"
haftmann@51735
   167
  else lthy;
haftmann@51735
   168
haftmann@51735
   169
wenzelm@33166
   170
(* naming *)
wenzelm@26131
   171
wenzelm@47245
   172
val naming_of = #naming o get_first_lthy;
wenzelm@33166
   173
val full_name = Name_Space.full_name o naming_of;
wenzelm@26131
   174
wenzelm@47245
   175
fun map_naming f =
haftmann@52118
   176
  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
haftmann@52118
   177
    (f naming, operations, after_close, brittle, target));
wenzelm@26131
   178
wenzelm@33166
   179
val conceal = map_naming Name_Space.conceal;
wenzelm@33724
   180
val new_group = map_naming Name_Space.new_group;
wenzelm@33724
   181
val reset_group = map_naming Name_Space.reset_group;
wenzelm@26131
   182
wenzelm@33276
   183
val restore_naming = map_naming o K o naming_of;
wenzelm@33276
   184
wenzelm@26131
   185
wenzelm@47245
   186
(* standard morphisms *)
wenzelm@18767
   187
wenzelm@47245
   188
fun standard_morphism lthy ctxt =
wenzelm@47245
   189
  Proof_Context.norm_export_morphism lthy ctxt $>
wenzelm@47245
   190
  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
wenzelm@18767
   191
wenzelm@47245
   192
fun standard_form lthy ctxt x =
wenzelm@47245
   193
  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
wenzelm@18767
   194
wenzelm@18767
   195
wenzelm@47245
   196
(* background theory *)
wenzelm@19661
   197
wenzelm@20960
   198
fun raw_theory_result f lthy =
wenzelm@20960
   199
  let
wenzelm@42360
   200
    val (res, thy') = f (Proof_Context.theory_of lthy);
wenzelm@47245
   201
    val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
wenzelm@20960
   202
  in (res, lthy') end;
wenzelm@20960
   203
wenzelm@20960
   204
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
wenzelm@20960
   205
wenzelm@28379
   206
val checkpoint = raw_theory Theory.checkpoint;
wenzelm@28379
   207
wenzelm@38757
   208
fun background_theory_result f lthy =
wenzelm@33166
   209
  lthy |> raw_theory_result (fn thy =>
wenzelm@33157
   210
    thy
wenzelm@33166
   211
    |> Sign.map_naming (K (naming_of lthy))
wenzelm@33157
   212
    |> f
wenzelm@36004
   213
    ||> Sign.restore_naming thy
wenzelm@36004
   214
    ||> Theory.checkpoint);
wenzelm@19661
   215
wenzelm@38757
   216
fun background_theory f = #2 o background_theory_result (f #> pair ());
wenzelm@19661
   217
wenzelm@47245
   218
wenzelm@47245
   219
(* target contexts *)
wenzelm@47245
   220
wenzelm@47245
   221
val target_of = #target o get_last_lthy;
wenzelm@47245
   222
wenzelm@47245
   223
fun target f lthy =
wenzelm@18744
   224
  let
wenzelm@47245
   225
    val ctxt = target_of lthy;
wenzelm@47245
   226
    val ctxt' = ctxt
wenzelm@33383
   227
      |> Context_Position.set_visible false
wenzelm@28406
   228
      |> f
wenzelm@47245
   229
      |> Context_Position.restore_visible ctxt;
wenzelm@42360
   230
    val thy' = Proof_Context.theory_of ctxt';
wenzelm@47245
   231
  in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
wenzelm@18876
   232
wenzelm@47245
   233
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
wenzelm@18767
   234
haftmann@52119
   235
fun surface_target f =
haftmann@52119
   236
  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
haftmann@52119
   237
    (naming, operations, after_close, brittle, f target));
haftmann@52119
   238
wenzelm@37949
   239
fun propagate_ml_env (context as Context.Proof lthy) =
wenzelm@47064
   240
      let val inherit = ML_Env.inherit context in
wenzelm@47064
   241
        lthy
wenzelm@47064
   242
        |> background_theory (Context.theory_map inherit)
wenzelm@47245
   243
        |> map_contexts (K (Context.proof_map inherit))
wenzelm@47064
   244
        |> Context.Proof
wenzelm@47064
   245
      end
wenzelm@37949
   246
  | propagate_ml_env context = context;
wenzelm@37949
   247
wenzelm@18767
   248
wenzelm@47064
   249
wenzelm@47064
   250
(** operations **)
wenzelm@47064
   251
wenzelm@47245
   252
val operations_of = #operations o get_first_lthy;
wenzelm@47066
   253
wenzelm@47066
   254
wenzelm@47064
   255
(* primitives *)
wenzelm@18781
   256
wenzelm@47066
   257
fun operation f lthy = f (operations_of lthy) lthy;
wenzelm@47061
   258
fun operation2 f x y = operation (fn ops => f ops x y);
wenzelm@18781
   259
wenzelm@20888
   260
val pretty = operation #pretty;
wenzelm@28379
   261
val abbrev = apsnd checkpoint ooo operation2 #abbrev;
wenzelm@46992
   262
val define = apsnd checkpoint oo operation2 #define false;
wenzelm@46992
   263
val define_internal = apsnd checkpoint oo operation2 #define true;
wenzelm@33670
   264
val notes_kind = apsnd checkpoint ooo operation2 #notes;
wenzelm@33456
   265
val declaration = checkpoint ooo operation2 #declaration;
wenzelm@18781
   266
wenzelm@36451
   267
wenzelm@47064
   268
(* basic derived operations *)
wenzelm@36451
   269
wenzelm@33670
   270
val notes = notes_kind "";
wenzelm@33670
   271
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
wenzelm@18781
   272
wenzelm@36451
   273
fun set_defsort S =
wenzelm@45291
   274
  declaration {syntax = true, pervasive = false}
wenzelm@45291
   275
    (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
wenzelm@36451
   276
wenzelm@35738
   277
wenzelm@35738
   278
(* notation *)
wenzelm@35738
   279
wenzelm@35412
   280
fun type_notation add mode raw_args lthy =
wenzelm@50741
   281
  let
wenzelm@50741
   282
    val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
wenzelm@50741
   283
  in
wenzelm@45291
   284
    declaration {syntax = true, pervasive = false}
wenzelm@47247
   285
      (Proof_Context.generic_type_notation add mode args) lthy
wenzelm@45291
   286
  end;
wenzelm@35412
   287
wenzelm@24949
   288
fun notation add mode raw_args lthy =
wenzelm@50741
   289
  let
wenzelm@50741
   290
    val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
wenzelm@50741
   291
  in
wenzelm@45291
   292
    declaration {syntax = true, pervasive = false}
wenzelm@47247
   293
      (Proof_Context.generic_notation add mode args) lthy
wenzelm@45291
   294
  end;
wenzelm@21743
   295
wenzelm@21664
   296
wenzelm@35738
   297
(* name space aliases *)
wenzelm@35738
   298
wenzelm@35798
   299
fun alias global_alias local_alias b name =
wenzelm@45291
   300
  declaration {syntax = true, pervasive = false} (fn phi =>
wenzelm@35738
   301
    let val b' = Morphism.binding phi b
wenzelm@45298
   302
    in Context.mapping (global_alias b' name) (local_alias b' name) end);
wenzelm@35738
   303
wenzelm@42360
   304
val class_alias = alias Sign.class_alias Proof_Context.class_alias;
wenzelm@42360
   305
val type_alias = alias Sign.type_alias Proof_Context.type_alias;
wenzelm@42360
   306
val const_alias = alias Sign.const_alias Proof_Context.const_alias;
wenzelm@35738
   307
wenzelm@35738
   308
wenzelm@36451
   309
wenzelm@36451
   310
(** init and exit **)
wenzelm@36451
   311
wenzelm@28395
   312
(* init *)
wenzelm@20910
   313
wenzelm@47061
   314
fun init naming operations target =
haftmann@52118
   315
  target |> Data.map
haftmann@52118
   316
    (fn [] => [make_lthy (naming, operations, I, false, target)]
wenzelm@47064
   317
      | _ => error "Local theory already initialized")
wenzelm@47061
   318
  |> checkpoint;
wenzelm@20910
   319
wenzelm@28395
   320
wenzelm@28395
   321
(* exit *)
wenzelm@28395
   322
wenzelm@42360
   323
val exit = Proof_Context.background_theory Theory.checkpoint o operation #exit;
wenzelm@42360
   324
val exit_global = Proof_Context.theory_of o exit;
wenzelm@28395
   325
wenzelm@28395
   326
fun exit_result f (x, lthy) =
wenzelm@28395
   327
  let
wenzelm@28395
   328
    val ctxt = exit lthy;
wenzelm@33281
   329
    val phi = standard_morphism lthy ctxt;
wenzelm@28395
   330
  in (f phi x, ctxt) end;
wenzelm@28395
   331
wenzelm@28395
   332
fun exit_result_global f (x, lthy) =
wenzelm@28395
   333
  let
wenzelm@28395
   334
    val thy = exit_global lthy;
wenzelm@42360
   335
    val thy_ctxt = Proof_Context.init_global thy;
wenzelm@33281
   336
    val phi = standard_morphism lthy thy_ctxt;
wenzelm@28395
   337
  in (f phi x, thy) end;
wenzelm@20910
   338
wenzelm@18781
   339
end;