src/Pure/Isar/local_theory.ML
author wenzelm
Wed Apr 01 13:32:32 2015 +0200 (2015-04-01)
changeset 59890 01aff5aa081d
parent 59887 43dc3c660f41
child 61111 2618e7e3b5ea
permissions -rw-r--r--
tuned signature;
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@57926
    10
structure Attrib =
wenzelm@57926
    11
struct
wenzelm@58011
    12
  type binding = binding * Token.src list;
wenzelm@57926
    13
end;
wenzelm@57926
    14
wenzelm@18744
    15
signature LOCAL_THEORY =
wenzelm@18744
    16
sig
wenzelm@20888
    17
  type operations
wenzelm@47066
    18
  val assert: local_theory -> local_theory
wenzelm@47273
    19
  val restore: local_theory -> local_theory
wenzelm@47064
    20
  val level: Proof.context -> int
wenzelm@47066
    21
  val assert_bottom: bool -> local_theory -> local_theory
wenzelm@57926
    22
  val mark_brittle: local_theory -> local_theory
haftmann@51735
    23
  val assert_nonbrittle: local_theory -> local_theory
wenzelm@47245
    24
  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
wenzelm@59880
    25
  val background_naming_of: local_theory -> Name_Space.naming
wenzelm@59880
    26
  val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
wenzelm@59880
    27
    local_theory -> local_theory
wenzelm@59880
    28
  val restore_background_naming: local_theory -> local_theory -> local_theory
wenzelm@33166
    29
  val full_name: local_theory -> binding -> string
wenzelm@33724
    30
  val new_group: local_theory -> local_theory
wenzelm@33724
    31
  val reset_group: local_theory -> local_theory
wenzelm@47245
    32
  val standard_morphism: local_theory -> Proof.context -> morphism
wenzelm@47245
    33
  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
wenzelm@20960
    34
  val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
wenzelm@20960
    35
  val raw_theory: (theory -> theory) -> local_theory -> local_theory
wenzelm@38757
    36
  val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
wenzelm@38757
    37
  val background_theory: (theory -> theory) -> local_theory -> local_theory
wenzelm@47245
    38
  val target_of: local_theory -> Proof.context
wenzelm@20888
    39
  val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
wenzelm@47245
    40
  val target_morphism: local_theory -> morphism
wenzelm@37949
    41
  val propagate_ml_env: generic_theory -> generic_theory
wenzelm@47066
    42
  val operations_of: local_theory -> operations
wenzelm@33764
    43
  val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@28083
    44
    (term * (string * thm)) * local_theory
wenzelm@46992
    45
  val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@46992
    46
    (term * (string * thm)) * local_theory
wenzelm@33670
    47
  val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
wenzelm@58011
    48
  val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@33670
    49
    local_theory -> (string * thm list) list * local_theory
wenzelm@58011
    50
  val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@28083
    51
    local_theory -> (string * thm list) list * local_theory
haftmann@38308
    52
  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
haftmann@38308
    53
    (term * term) * local_theory
wenzelm@45291
    54
  val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
haftmann@56723
    55
  val subscription: string * morphism -> (morphism * bool) option -> morphism ->
haftmann@56723
    56
    local_theory -> local_theory
haftmann@38308
    57
  val pretty: local_theory -> Pretty.T list
wenzelm@57929
    58
  val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
wenzelm@36451
    59
  val set_defsort: sort -> local_theory -> local_theory
wenzelm@35412
    60
  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
wenzelm@24949
    61
  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
wenzelm@57938
    62
  val generic_alias:
wenzelm@57938
    63
    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
wenzelm@57938
    64
    binding -> string -> local_theory -> local_theory
wenzelm@35738
    65
  val class_alias: binding -> class -> local_theory -> local_theory
wenzelm@35738
    66
  val type_alias: binding -> string -> local_theory -> local_theory
wenzelm@35738
    67
  val const_alias: binding -> string -> local_theory -> local_theory
wenzelm@47061
    68
  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
wenzelm@21292
    69
  val exit: local_theory -> Proof.context
wenzelm@28395
    70
  val exit_global: local_theory -> theory
wenzelm@28395
    71
  val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
wenzelm@28395
    72
  val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
wenzelm@59890
    73
  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
wenzelm@59890
    74
    local_theory -> Binding.scope * local_theory
wenzelm@59890
    75
  val open_target: local_theory -> Binding.scope * local_theory
wenzelm@59890
    76
  val close_target: local_theory -> local_theory
wenzelm@18744
    77
end;
wenzelm@18744
    78
wenzelm@33671
    79
structure Local_Theory: LOCAL_THEORY =
wenzelm@18744
    80
struct
wenzelm@18744
    81
wenzelm@20888
    82
(** local theory data **)
wenzelm@19059
    83
wenzelm@20888
    84
(* type lthy *)
wenzelm@20888
    85
wenzelm@20888
    86
type operations =
wenzelm@46992
    87
 {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@28083
    88
    (term * (string * thm)) * local_theory,
wenzelm@26131
    89
  notes: string ->
wenzelm@58011
    90
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@28083
    91
    local_theory -> (string * thm list) list * local_theory,
haftmann@38308
    92
  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
haftmann@38308
    93
    (term * term) * local_theory,
wenzelm@45291
    94
  declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
haftmann@56723
    95
  subscription: string * morphism -> (morphism * bool) option -> morphism ->
haftmann@56723
    96
     local_theory -> local_theory,
haftmann@38308
    97
  pretty: local_theory -> Pretty.T list,
wenzelm@21292
    98
  exit: local_theory -> Proof.context};
wenzelm@20888
    99
wenzelm@47064
   100
type lthy =
wenzelm@59880
   101
 {background_naming: Name_Space.naming,
wenzelm@20888
   102
  operations: operations,
wenzelm@50739
   103
  after_close: local_theory -> local_theory,
haftmann@52118
   104
  brittle: bool,
wenzelm@20888
   105
  target: Proof.context};
wenzelm@20888
   106
wenzelm@59880
   107
fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
wenzelm@59880
   108
  {background_naming = background_naming, operations = operations,
wenzelm@59880
   109
    after_close = after_close, brittle = brittle, target = target};
wenzelm@20888
   110
wenzelm@20888
   111
wenzelm@20888
   112
(* context data *)
wenzelm@18744
   113
wenzelm@33519
   114
structure Data = Proof_Data
wenzelm@18744
   115
(
haftmann@52118
   116
  type T = lthy list;
haftmann@52118
   117
  fun init _ = [];
wenzelm@18744
   118
);
wenzelm@18744
   119
wenzelm@47066
   120
fun assert lthy =
haftmann@52118
   121
  if null (Data.get lthy) then error "Missing local theory context" else lthy;
wenzelm@47066
   122
haftmann@57194
   123
val bottom_of = List.last o Data.get o assert;
haftmann@57194
   124
val top_of = hd o Data.get o assert;
wenzelm@47066
   125
wenzelm@57925
   126
fun map_top f =
wenzelm@50739
   127
  assert #>
wenzelm@59880
   128
  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
wenzelm@59880
   129
    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
wenzelm@47066
   130
haftmann@57194
   131
fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
wenzelm@47273
   132
wenzelm@47064
   133
wenzelm@47064
   134
(* nested structure *)
wenzelm@33166
   135
haftmann@52118
   136
val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
wenzelm@47066
   137
wenzelm@47066
   138
fun assert_bottom b lthy =
wenzelm@47066
   139
  let
wenzelm@47066
   140
    val _ = assert lthy;
wenzelm@47066
   141
    val b' = level lthy <= 1;
wenzelm@47066
   142
  in
wenzelm@47066
   143
    if b andalso not b' then error "Not at bottom of local theory nesting"
wenzelm@47066
   144
    else if not b andalso b' then error "Already at bottom of local theory nesting"
wenzelm@47066
   145
    else lthy
wenzelm@47066
   146
  end;
wenzelm@47066
   147
wenzelm@47245
   148
fun map_contexts f lthy =
wenzelm@47245
   149
  let val n = level lthy in
wenzelm@59880
   150
    lthy |> (Data.map o map_index)
wenzelm@59880
   151
      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
wenzelm@59880
   152
        make_lthy (background_naming, operations, after_close, brittle,
wenzelm@59880
   153
          target
wenzelm@59880
   154
          |> Context_Position.set_visible false
wenzelm@59880
   155
          |> f (n - i - 1)
wenzelm@59880
   156
          |> Context_Position.restore_visible target))
wenzelm@59880
   157
      |> f n
wenzelm@47245
   158
  end;
wenzelm@47245
   159
wenzelm@26131
   160
haftmann@51735
   161
(* brittle context -- implicit for nested structures *)
haftmann@51735
   162
haftmann@52118
   163
fun mark_brittle lthy =
wenzelm@57924
   164
  if level lthy = 1 then
wenzelm@59880
   165
    map_top (fn (background_naming, operations, after_close, _, target) =>
wenzelm@59880
   166
      (background_naming, operations, after_close, true, target)) lthy
haftmann@52118
   167
  else lthy;
haftmann@51735
   168
haftmann@51735
   169
fun assert_nonbrittle lthy =
wenzelm@57924
   170
  if #brittle (top_of lthy) then error "Brittle local theory context"
haftmann@51735
   171
  else lthy;
haftmann@51735
   172
haftmann@51735
   173
wenzelm@59880
   174
(* naming for background theory *)
wenzelm@26131
   175
wenzelm@59880
   176
val background_naming_of = #background_naming o top_of;
wenzelm@26131
   177
wenzelm@59880
   178
fun map_background_naming f =
wenzelm@59880
   179
  map_top (fn (background_naming, operations, after_close, brittle, target) =>
wenzelm@59880
   180
    (f background_naming, operations, after_close, brittle, target));
wenzelm@26131
   181
wenzelm@59880
   182
val restore_background_naming = map_background_naming o K o background_naming_of;
wenzelm@26131
   183
wenzelm@59880
   184
val full_name = Name_Space.full_name o background_naming_of;
wenzelm@59880
   185
wenzelm@59880
   186
val new_group = map_background_naming Name_Space.new_group;
wenzelm@59880
   187
val reset_group = map_background_naming Name_Space.reset_group;
wenzelm@33276
   188
wenzelm@26131
   189
wenzelm@47245
   190
(* standard morphisms *)
wenzelm@18767
   191
wenzelm@47245
   192
fun standard_morphism lthy ctxt =
wenzelm@47245
   193
  Proof_Context.norm_export_morphism lthy ctxt $>
wenzelm@54740
   194
  Morphism.binding_morphism "Local_Theory.standard_binding"
wenzelm@59880
   195
    (Name_Space.transform_binding (Proof_Context.naming_of lthy));
wenzelm@18767
   196
wenzelm@47245
   197
fun standard_form lthy ctxt x =
wenzelm@47245
   198
  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
wenzelm@18767
   199
wenzelm@18767
   200
wenzelm@47245
   201
(* background theory *)
wenzelm@19661
   202
wenzelm@20960
   203
fun raw_theory_result f lthy =
wenzelm@20960
   204
  let
wenzelm@42360
   205
    val (res, thy') = f (Proof_Context.theory_of lthy);
wenzelm@47245
   206
    val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
wenzelm@20960
   207
  in (res, lthy') end;
wenzelm@20960
   208
wenzelm@20960
   209
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
wenzelm@20960
   210
wenzelm@38757
   211
fun background_theory_result f lthy =
wenzelm@59887
   212
  let
wenzelm@59887
   213
    val naming =
wenzelm@59887
   214
      background_naming_of lthy
wenzelm@59887
   215
      |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
wenzelm@59887
   216
  in
wenzelm@59887
   217
    lthy |> raw_theory_result (fn thy =>
wenzelm@59887
   218
      thy
wenzelm@59887
   219
      |> Sign.map_naming (K naming)
wenzelm@59887
   220
      |> f
wenzelm@59887
   221
      ||> Sign.restore_naming thy)
wenzelm@59887
   222
  end;
wenzelm@19661
   223
wenzelm@38757
   224
fun background_theory f = #2 o background_theory_result (f #> pair ());
wenzelm@19661
   225
wenzelm@47245
   226
wenzelm@47245
   227
(* target contexts *)
wenzelm@47245
   228
haftmann@57194
   229
val target_of = #target o bottom_of;
wenzelm@47245
   230
wenzelm@47245
   231
fun target f lthy =
wenzelm@18744
   232
  let
wenzelm@47245
   233
    val ctxt = target_of lthy;
wenzelm@47245
   234
    val ctxt' = ctxt
wenzelm@33383
   235
      |> Context_Position.set_visible false
wenzelm@28406
   236
      |> f
wenzelm@47245
   237
      |> Context_Position.restore_visible ctxt;
wenzelm@42360
   238
    val thy' = Proof_Context.theory_of ctxt';
wenzelm@47245
   239
  in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
wenzelm@18876
   240
wenzelm@47245
   241
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
wenzelm@18767
   242
wenzelm@37949
   243
fun propagate_ml_env (context as Context.Proof lthy) =
wenzelm@47064
   244
      let val inherit = ML_Env.inherit context in
wenzelm@47064
   245
        lthy
wenzelm@47064
   246
        |> background_theory (Context.theory_map inherit)
wenzelm@47245
   247
        |> map_contexts (K (Context.proof_map inherit))
wenzelm@47064
   248
        |> Context.Proof
wenzelm@47064
   249
      end
wenzelm@37949
   250
  | propagate_ml_env context = context;
wenzelm@37949
   251
wenzelm@18767
   252
wenzelm@47064
   253
wenzelm@47064
   254
(** operations **)
wenzelm@47064
   255
haftmann@57194
   256
val operations_of = #operations o top_of;
wenzelm@47066
   257
wenzelm@57938
   258
fun operation f lthy = f (operations_of lthy) lthy;
wenzelm@57938
   259
fun operation2 f x y = operation (fn ops => f ops x y);
wenzelm@57938
   260
wenzelm@47066
   261
wenzelm@47064
   262
(* primitives *)
wenzelm@18781
   263
wenzelm@20888
   264
val pretty = operation #pretty;
wenzelm@52788
   265
val abbrev = operation2 #abbrev;
wenzelm@52788
   266
val define = operation2 #define false;
wenzelm@52788
   267
val define_internal = operation2 #define true;
wenzelm@52788
   268
val notes_kind = operation2 #notes;
wenzelm@52788
   269
val declaration = operation2 #declaration;
haftmann@56809
   270
fun subscription dep_morph mixin export =
haftmann@56809
   271
  assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
wenzelm@18781
   272
wenzelm@36451
   273
wenzelm@57938
   274
(* theorems *)
wenzelm@36451
   275
wenzelm@33670
   276
val notes = notes_kind "";
wenzelm@33670
   277
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
wenzelm@18781
   278
wenzelm@57929
   279
fun add_thms_dynamic (binding, f) lthy =
wenzelm@57929
   280
  lthy
wenzelm@57929
   281
  |> background_theory_result (fn thy => thy
wenzelm@57929
   282
      |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
wenzelm@57929
   283
  |-> (fn name =>
wenzelm@57929
   284
    map_contexts (fn _ => fn ctxt =>
wenzelm@57929
   285
      Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
wenzelm@57929
   286
    declaration {syntax = false, pervasive = false} (fn phi =>
wenzelm@57929
   287
      let val binding' = Morphism.binding phi binding in
wenzelm@57929
   288
        Context.mapping
wenzelm@57929
   289
          (Global_Theory.alias_fact binding' name)
wenzelm@57929
   290
          (Proof_Context.fact_alias binding' name)
wenzelm@57929
   291
      end));
wenzelm@57929
   292
wenzelm@57938
   293
wenzelm@57938
   294
(* default sort *)
wenzelm@57938
   295
wenzelm@36451
   296
fun set_defsort S =
wenzelm@45291
   297
  declaration {syntax = true, pervasive = false}
wenzelm@45291
   298
    (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
wenzelm@36451
   299
wenzelm@35738
   300
wenzelm@35738
   301
(* notation *)
wenzelm@35738
   302
wenzelm@35412
   303
fun type_notation add mode raw_args lthy =
wenzelm@50741
   304
  let
wenzelm@50741
   305
    val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
wenzelm@50741
   306
  in
wenzelm@45291
   307
    declaration {syntax = true, pervasive = false}
wenzelm@47247
   308
      (Proof_Context.generic_type_notation add mode args) lthy
wenzelm@45291
   309
  end;
wenzelm@35412
   310
wenzelm@24949
   311
fun notation add mode raw_args lthy =
wenzelm@50741
   312
  let
wenzelm@50741
   313
    val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
wenzelm@50741
   314
  in
wenzelm@45291
   315
    declaration {syntax = true, pervasive = false}
wenzelm@47247
   316
      (Proof_Context.generic_notation add mode args) lthy
wenzelm@45291
   317
  end;
wenzelm@21743
   318
wenzelm@21664
   319
wenzelm@35738
   320
(* name space aliases *)
wenzelm@35738
   321
wenzelm@57938
   322
fun generic_alias app b name =
wenzelm@57938
   323
  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
wenzelm@57938
   324
    let
wenzelm@57938
   325
      val naming = Name_Space.naming_of context;
wenzelm@57938
   326
      val b' = Morphism.binding phi b;
wenzelm@57938
   327
    in app (Name_Space.alias_table naming b' name) context end);
wenzelm@57938
   328
wenzelm@57938
   329
fun syntax_alias global_alias local_alias b name =
wenzelm@45291
   330
  declaration {syntax = true, pervasive = false} (fn phi =>
wenzelm@35738
   331
    let val b' = Morphism.binding phi b
wenzelm@45298
   332
    in Context.mapping (global_alias b' name) (local_alias b' name) end);
wenzelm@35738
   333
wenzelm@57938
   334
val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
wenzelm@57938
   335
val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
wenzelm@57938
   336
val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
wenzelm@35738
   337
wenzelm@35738
   338
wenzelm@56055
   339
wenzelm@59890
   340
(** manage targets **)
wenzelm@36451
   341
wenzelm@59890
   342
(* outermost target *)
wenzelm@20910
   343
wenzelm@59880
   344
fun init background_naming operations target =
haftmann@52118
   345
  target |> Data.map
wenzelm@59880
   346
    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
wenzelm@52788
   347
      | _ => error "Local theory already initialized");
wenzelm@20910
   348
wenzelm@52788
   349
val exit = operation #exit;
wenzelm@42360
   350
val exit_global = Proof_Context.theory_of o exit;
wenzelm@28395
   351
wenzelm@28395
   352
fun exit_result f (x, lthy) =
wenzelm@28395
   353
  let
wenzelm@28395
   354
    val ctxt = exit lthy;
wenzelm@33281
   355
    val phi = standard_morphism lthy ctxt;
wenzelm@28395
   356
  in (f phi x, ctxt) end;
wenzelm@28395
   357
wenzelm@28395
   358
fun exit_result_global f (x, lthy) =
wenzelm@28395
   359
  let
wenzelm@28395
   360
    val thy = exit_global lthy;
wenzelm@42360
   361
    val thy_ctxt = Proof_Context.init_global thy;
wenzelm@33281
   362
    val phi = standard_morphism lthy thy_ctxt;
wenzelm@28395
   363
  in (f phi x, thy) end;
wenzelm@20910
   364
wenzelm@59890
   365
wenzelm@59890
   366
(* nested targets *)
wenzelm@59890
   367
wenzelm@59890
   368
fun init_target background_naming operations after_close lthy =
wenzelm@59890
   369
  let
wenzelm@59890
   370
    val _ = assert lthy;
wenzelm@59890
   371
    val (scope, target) = Proof_Context.new_scope lthy;
wenzelm@59890
   372
    val lthy' =
wenzelm@59890
   373
      target
wenzelm@59890
   374
      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
wenzelm@59890
   375
  in (scope, lthy') end;
wenzelm@59890
   376
wenzelm@59890
   377
fun open_target lthy =
wenzelm@59890
   378
  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
wenzelm@59890
   379
wenzelm@59890
   380
fun close_target lthy =
wenzelm@59890
   381
  let
wenzelm@59890
   382
    val _ = assert_bottom false lthy;
wenzelm@59890
   383
    val ({after_close, ...} :: rest) = Data.get lthy;
wenzelm@59890
   384
  in lthy |> Data.put rest |> restore |> after_close end;
wenzelm@59890
   385
wenzelm@18781
   386
end;