src/Pure/Isar/local_theory.ML
author wenzelm
Wed Mar 11 16:36:27 2009 +0100 (2009-03-11 ago)
changeset 30438 c2d49315b93b
parent 29581 b3b33e0298eb
child 30469 de9e8f1d927c
permissions -rw-r--r--
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
     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 
     9 signature LOCAL_THEORY =
    10 sig
    11   type operations
    12   val group_of: local_theory -> string
    13   val group_properties_of: local_theory -> Properties.T
    14   val group_position_of: local_theory -> Properties.T
    15   val set_group: string -> local_theory -> local_theory
    16   val target_of: local_theory -> Proof.context
    17   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    18   val raw_theory: (theory -> theory) -> local_theory -> local_theory
    19   val checkpoint: local_theory -> local_theory
    20   val full_naming: local_theory -> NameSpace.naming
    21   val full_name: local_theory -> binding -> string
    22   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    23   val theory: (theory -> theory) -> local_theory -> local_theory
    24   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    25   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    26   val affirm: local_theory -> local_theory
    27   val pretty: local_theory -> Pretty.T list
    28   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    29     (term * term) * local_theory
    30   val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    31     (term * (string * thm)) * local_theory
    32   val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
    33   val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    34     local_theory -> (string * thm list) list * local_theory
    35   val type_syntax: declaration -> local_theory -> local_theory
    36   val term_syntax: declaration -> local_theory -> local_theory
    37   val declaration: declaration -> local_theory -> local_theory
    38   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    39   val target_morphism: local_theory -> morphism
    40   val init: string -> operations -> Proof.context -> local_theory
    41   val restore: local_theory -> local_theory
    42   val reinit: local_theory -> local_theory
    43   val exit: local_theory -> Proof.context
    44   val exit_global: local_theory -> theory
    45   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
    46   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
    47 end;
    48 
    49 structure LocalTheory: LOCAL_THEORY =
    50 struct
    51 
    52 (** local theory data **)
    53 
    54 (* type lthy *)
    55 
    56 type operations =
    57  {pretty: local_theory -> Pretty.T list,
    58   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    59     (term * term) * local_theory,
    60   define: string ->
    61     (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    62     (term * (string * thm)) * local_theory,
    63   notes: string ->
    64     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    65     local_theory -> (string * thm list) list * local_theory,
    66   type_syntax: declaration -> local_theory -> local_theory,
    67   term_syntax: declaration -> local_theory -> local_theory,
    68   declaration: declaration -> local_theory -> local_theory,
    69   reinit: local_theory -> local_theory,
    70   exit: local_theory -> Proof.context};
    71 
    72 datatype lthy = LThy of
    73  {group: string,
    74   theory_prefix: string,
    75   operations: operations,
    76   target: Proof.context};
    77 
    78 fun make_lthy (group, theory_prefix, operations, target) =
    79   LThy {group = group, theory_prefix = theory_prefix, operations = operations, target = target};
    80 
    81 
    82 (* context data *)
    83 
    84 structure Data = ProofDataFun
    85 (
    86   type T = lthy option;
    87   fun init _ = NONE;
    88 );
    89 
    90 fun get_lthy lthy =
    91   (case Data.get lthy of
    92     NONE => error "No local theory context"
    93   | SOME (LThy data) => data);
    94 
    95 fun map_lthy f lthy =
    96   let val {group, theory_prefix, operations, target} = get_lthy lthy
    97   in Data.put (SOME (make_lthy (f (group, theory_prefix, operations, target)))) lthy end;
    98 
    99 
   100 (* group *)
   101 
   102 val group_of = #group o get_lthy;
   103 
   104 fun group_properties_of lthy =
   105   (case group_of lthy of
   106     "" => []
   107   | group => [(Markup.groupN, group)]);
   108 
   109 fun group_position_of lthy =
   110   group_properties_of lthy @ Position.properties_of (Position.thread_data ());
   111 
   112 fun set_group group = map_lthy (fn (_, theory_prefix, operations, target) =>
   113   (group, theory_prefix, operations, target));
   114 
   115 
   116 (* target *)
   117 
   118 val target_of = #target o get_lthy;
   119 val affirm = tap target_of;
   120 
   121 fun map_target f = map_lthy (fn (group, theory_prefix, operations, target) =>
   122   (group, theory_prefix, operations, f target));
   123 
   124 
   125 (* substructure mappings *)
   126 
   127 fun raw_theory_result f lthy =
   128   let
   129     val (res, thy') = f (ProofContext.theory_of lthy);
   130     val lthy' = lthy
   131       |> map_target (ProofContext.transfer thy')
   132       |> ProofContext.transfer thy';
   133   in (res, lthy') end;
   134 
   135 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
   136 
   137 val checkpoint = raw_theory Theory.checkpoint;
   138 
   139 fun full_naming lthy =
   140   Sign.naming_of (ProofContext.theory_of lthy)
   141   |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
   142 
   143 fun full_name naming = NameSpace.full_name (full_naming naming);
   144 
   145 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   146   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
   147   |> f
   148   ||> Sign.restore_naming thy);
   149 
   150 fun theory f = #2 o theory_result (f #> pair ());
   151 
   152 fun target_result f lthy =
   153   let
   154     val (res, ctxt') = target_of lthy
   155       |> ContextPosition.set_visible false
   156       |> f
   157       ||> ContextPosition.restore_visible lthy;
   158     val thy' = ProofContext.theory_of ctxt';
   159     val lthy' = lthy
   160       |> map_target (K ctxt')
   161       |> ProofContext.transfer thy';
   162   in (res, lthy') end;
   163 
   164 fun target f = #2 o target_result (f #> pair ());
   165 
   166 
   167 (* basic operations *)
   168 
   169 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
   170 fun operation1 f x = operation (fn ops => f ops x);
   171 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
   172 
   173 val pretty = operation #pretty;
   174 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
   175 val define = apsnd checkpoint ooo operation2 #define;
   176 val notes = apsnd checkpoint ooo operation2 #notes;
   177 val type_syntax = checkpoint oo operation1 #type_syntax;
   178 val term_syntax = checkpoint oo operation1 #term_syntax;
   179 val declaration = checkpoint oo operation1 #declaration;
   180 
   181 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
   182 
   183 fun target_morphism lthy =
   184   ProofContext.norm_export_morphism lthy (target_of lthy);
   185 
   186 fun notation add mode raw_args lthy =
   187   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   188   in term_syntax (ProofContext.target_notation add mode args) lthy end;
   189 
   190 
   191 (* init *)
   192 
   193 fun init theory_prefix operations target = target |> Data.map
   194   (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
   195     | SOME _ => error "Local theory already initialized")
   196   |> checkpoint;
   197 
   198 fun restore lthy =
   199   let val {group = _, theory_prefix, operations, target} = get_lthy lthy
   200   in init theory_prefix operations target end;
   201 
   202 val reinit = checkpoint o operation #reinit;
   203 
   204 
   205 (* exit *)
   206 
   207 val exit = ProofContext.theory Theory.checkpoint o operation #exit;
   208 val exit_global = ProofContext.theory_of o exit;
   209 
   210 fun exit_result f (x, lthy) =
   211   let
   212     val ctxt = exit lthy;
   213     val phi = ProofContext.norm_export_morphism lthy ctxt;
   214   in (f phi x, ctxt) end;
   215 
   216 fun exit_result_global f (x, lthy) =
   217   let
   218     val thy = exit_global lthy;
   219     val thy_ctxt = ProofContext.init thy;
   220     val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
   221   in (f phi x, thy) end;
   222 
   223 end;