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