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