src/Pure/Isar/local_theory.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29581 b3b33e0298eb
child 30438 c2d49315b93b
permissions -rw-r--r--
use long names for old-style fold combinators;
     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   |> NameSpace.qualified_names;
   143 
   144 fun full_name naming = NameSpace.full_name (full_naming naming);
   145 
   146 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   147   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
   148   |> Sign.qualified_names
   149   |> f
   150   ||> Sign.restore_naming thy);
   151 
   152 fun theory f = #2 o theory_result (f #> pair ());
   153 
   154 fun target_result f lthy =
   155   let
   156     val (res, ctxt') = target_of lthy
   157       |> ContextPosition.set_visible false
   158       |> f
   159       ||> ContextPosition.restore_visible lthy;
   160     val thy' = ProofContext.theory_of ctxt';
   161     val lthy' = lthy
   162       |> map_target (K ctxt')
   163       |> ProofContext.transfer thy';
   164   in (res, lthy') end;
   165 
   166 fun target f = #2 o target_result (f #> pair ());
   167 
   168 
   169 (* basic operations *)
   170 
   171 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
   172 fun operation1 f x = operation (fn ops => f ops x);
   173 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
   174 
   175 val pretty = operation #pretty;
   176 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
   177 val define = apsnd checkpoint ooo operation2 #define;
   178 val notes = apsnd checkpoint ooo operation2 #notes;
   179 val type_syntax = checkpoint oo operation1 #type_syntax;
   180 val term_syntax = checkpoint oo operation1 #term_syntax;
   181 val declaration = checkpoint oo operation1 #declaration;
   182 
   183 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
   184 
   185 fun target_morphism lthy =
   186   ProofContext.norm_export_morphism lthy (target_of lthy);
   187 
   188 fun notation add mode raw_args lthy =
   189   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   190   in term_syntax (ProofContext.target_notation add mode args) lthy end;
   191 
   192 
   193 (* init *)
   194 
   195 fun init theory_prefix operations target = target |> Data.map
   196   (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
   197     | SOME _ => error "Local theory already initialized")
   198   |> checkpoint;
   199 
   200 fun restore lthy =
   201   let val {group = _, theory_prefix, operations, target} = get_lthy lthy
   202   in init theory_prefix operations target end;
   203 
   204 val reinit = checkpoint o operation #reinit;
   205 
   206 
   207 (* exit *)
   208 
   209 val exit = ProofContext.theory Theory.checkpoint o operation #exit;
   210 val exit_global = ProofContext.theory_of o exit;
   211 
   212 fun exit_result f (x, lthy) =
   213   let
   214     val ctxt = exit lthy;
   215     val phi = ProofContext.norm_export_morphism lthy ctxt;
   216   in (f phi x, ctxt) end;
   217 
   218 fun exit_result_global f (x, lthy) =
   219   let
   220     val thy = exit_global lthy;
   221     val thy_ctxt = ProofContext.init thy;
   222     val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
   223   in (f phi x, thy) end;
   224 
   225 end;