src/Pure/context.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 51686 532e0ac5a66d
child 52682 77146b576ac7
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/context.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Generic theory contexts with unique identity, arbitrarily typed data,
     5 monotonic development graph and history support.  Generic proof
     6 contexts with arbitrarily typed data.
     7 
     8 Firm naming conventions:
     9    thy, thy', thy1, thy2: theory
    10    ctxt, ctxt', ctxt1, ctxt2: Proof.context
    11    context: Context.generic
    12 *)
    13 
    14 signature BASIC_CONTEXT =
    15 sig
    16   type theory
    17   type theory_ref
    18   exception THEORY of string * theory list
    19   structure Proof: sig type context end
    20   structure Proof_Context:
    21   sig
    22     val theory_of: Proof.context -> theory
    23     val init_global: theory -> Proof.context
    24     val get_global: theory -> string -> Proof.context
    25   end
    26 end;
    27 
    28 signature CONTEXT =
    29 sig
    30   include BASIC_CONTEXT
    31   (*theory context*)
    32   val timing: bool Unsynchronized.ref
    33   type pretty
    34   val parents_of: theory -> theory list
    35   val ancestors_of: theory -> theory list
    36   val theory_name: theory -> string
    37   val is_stale: theory -> bool
    38   val is_draft: theory -> bool
    39   val reject_draft: theory -> theory
    40   val PureN: string
    41   val display_names: theory -> string list
    42   val pretty_thy: theory -> Pretty.T
    43   val string_of_thy: theory -> string
    44   val pretty_abbrev_thy: theory -> Pretty.T
    45   val str_of_thy: theory -> string
    46   val get_theory: theory -> string -> theory
    47   val this_theory: theory -> string -> theory
    48   val deref: theory_ref -> theory
    49   val check_thy: theory -> theory_ref
    50   val eq_thy: theory * theory -> bool
    51   val subthy: theory * theory -> bool
    52   val joinable: theory * theory -> bool
    53   val merge: theory * theory -> theory
    54   val merge_refs: theory_ref * theory_ref -> theory_ref
    55   val copy_thy: theory -> theory
    56   val checkpoint_thy: theory -> theory
    57   val finish_thy: theory -> theory
    58   val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    59   (*proof context*)
    60   val raw_transfer: theory -> Proof.context -> Proof.context
    61   (*generic context*)
    62   datatype generic = Theory of theory | Proof of Proof.context
    63   val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a
    64   val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic
    65   val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) ->
    66     generic -> 'a * generic
    67   val the_theory: generic -> theory
    68   val the_proof: generic -> Proof.context
    69   val map_theory: (theory -> theory) -> generic -> generic
    70   val map_proof: (Proof.context -> Proof.context) -> generic -> generic
    71   val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
    72   val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic
    73   val theory_map: (generic -> generic) -> theory -> theory
    74   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    75   val theory_of: generic -> theory  (*total*)
    76   val proof_of: generic -> Proof.context  (*total*)
    77   (*pretty printing context*)
    78   val pretty: Proof.context -> pretty
    79   val pretty_global: theory -> pretty
    80   val pretty_generic: generic -> pretty
    81   val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    82   (*thread data*)
    83   val thread_data: unit -> generic option
    84   val the_thread_data: unit -> generic
    85   val set_thread_data: generic option -> unit
    86   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    87   val >> : (generic -> generic) -> unit
    88   val >>> : (generic -> 'a * generic) -> 'a
    89 end;
    90 
    91 signature PRIVATE_CONTEXT =
    92 sig
    93   include CONTEXT
    94   structure Theory_Data:
    95   sig
    96     val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
    97       (pretty -> Any.T * Any.T -> Any.T) -> serial
    98     val get: serial -> (Any.T -> 'a) -> theory -> 'a
    99     val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
   100   end
   101   structure Proof_Data:
   102   sig
   103     val declare: (theory -> Any.T) -> serial
   104     val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
   105     val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
   106   end
   107 end;
   108 
   109 structure Context: PRIVATE_CONTEXT =
   110 struct
   111 
   112 (*** theory context ***)
   113 
   114 (** theory data **)
   115 
   116 (* data kinds and access methods *)
   117 
   118 val timing = Unsynchronized.ref false;
   119 
   120 (*private copy avoids potential conflict of table exceptions*)
   121 structure Datatab = Table(type key = int val ord = int_ord);
   122 
   123 datatype pretty = Pretty of Any.T;
   124 
   125 local
   126 
   127 type kind =
   128  {pos: Position.T,
   129   empty: Any.T,
   130   extend: Any.T -> Any.T,
   131   merge: pretty -> Any.T * Any.T -> Any.T};
   132 
   133 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
   134 
   135 fun invoke name f k x =
   136   (case Datatab.lookup (Synchronized.value kinds) k of
   137     SOME kind =>
   138       if ! timing andalso name <> "" then
   139         Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
   140           (fn () => f kind x)
   141       else f kind x
   142   | NONE => raise Fail "Invalid theory data identifier");
   143 
   144 in
   145 
   146 fun invoke_empty k = invoke "" (K o #empty) k ();
   147 val invoke_extend = invoke "extend" #extend;
   148 fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
   149 
   150 fun declare_theory_data pos empty extend merge =
   151   let
   152     val k = serial ();
   153     val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
   154     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   155   in k end;
   156 
   157 val extend_data = Datatab.map invoke_extend;
   158 fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
   159 
   160 end;
   161 
   162 
   163 
   164 (** datatype theory **)
   165 
   166 datatype theory =
   167   Theory of
   168    (*identity*)
   169    {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
   170     draft: bool,                  (*draft mode -- linear destructive changes*)
   171     id: serial,                   (*identifier*)
   172     ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
   173    (*data*)
   174    Any.T Datatab.table *       (*body content*)
   175    (*ancestry*)
   176    {parents: theory list,         (*immediate predecessors*)
   177     ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
   178    (*history*)
   179    {name: string,                 (*official theory name*)
   180     stage: int};                  (*checkpoint counter*)
   181 
   182 exception THEORY of string * theory list;
   183 
   184 fun rep_theory (Theory args) = args;
   185 
   186 val identity_of = #1 o rep_theory;
   187 val data_of = #2 o rep_theory;
   188 val ancestry_of = #3 o rep_theory;
   189 val history_of = #4 o rep_theory;
   190 
   191 fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids};
   192 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   193 fun make_history name stage = {name = name, stage = stage};
   194 
   195 val the_self = the o #self o identity_of;
   196 val parents_of = #parents o ancestry_of;
   197 val ancestors_of = #ancestors o ancestry_of;
   198 val theory_name = #name o history_of;
   199 
   200 
   201 (* staleness *)
   202 
   203 fun eq_id (i: int, j) = i = j;
   204 
   205 fun is_stale
   206     (Theory ({self =
   207         SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   208       not (eq_id (id, id'))
   209   | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
   210 
   211 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   212   | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
   213       let
   214         val r = Unsynchronized.ref thy;
   215         val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
   216       in r := thy'; thy' end;
   217 
   218 
   219 (* draft mode *)
   220 
   221 val is_draft = #draft o identity_of;
   222 
   223 fun reject_draft thy =
   224   if is_draft thy then
   225     raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
   226   else thy;
   227 
   228 
   229 (* names *)
   230 
   231 val PureN = "Pure";
   232 val draftN = "#";
   233 val finished = ~1;
   234 
   235 fun display_names thy =
   236   let
   237     val draft = if is_draft thy then [draftN] else [];
   238     val {stage, ...} = history_of thy;
   239     val name =
   240       if stage = finished then theory_name thy
   241       else theory_name thy ^ ":" ^ string_of_int stage;
   242     val ancestor_names = map theory_name (ancestors_of thy);
   243     val stale = if is_stale thy then ["!"] else [];
   244   in rev (stale @ draft @ [name] @ ancestor_names) end;
   245 
   246 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   247 val string_of_thy = Pretty.string_of o pretty_thy;
   248 
   249 fun pretty_abbrev_thy thy =
   250   let
   251     val names = display_names thy;
   252     val n = length names;
   253     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   254   in Pretty.str_list "{" "}" abbrev end;
   255 
   256 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   257 
   258 fun get_theory thy name =
   259   if theory_name thy <> name then
   260     (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
   261       SOME thy' => thy'
   262     | NONE => error ("Unknown ancestor theory " ^ quote name))
   263   else if #stage (history_of thy) = finished then thy
   264   else error ("Unfinished theory " ^ quote name);
   265 
   266 fun this_theory thy name =
   267   if theory_name thy = name then thy
   268   else get_theory thy name;
   269 
   270 
   271 (* theory references *)
   272 
   273 (*theory_ref provides a safe way to store dynamic references to a
   274   theory in external data structures -- a plain theory value would
   275   become stale as the self reference moves on*)
   276 
   277 datatype theory_ref = Theory_Ref of theory Unsynchronized.ref;
   278 
   279 fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy;
   280 
   281 fun check_thy thy =  (*thread-safe version*)
   282   let val thy_ref = Theory_Ref (the_self thy) in
   283     if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
   284     else thy_ref
   285   end;
   286 
   287 
   288 (* build ids *)
   289 
   290 fun insert_id draft id ids =
   291   if draft then ids
   292   else Inttab.update (id, ()) ids;
   293 
   294 fun merge_ids
   295     (Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _))
   296     (Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) =
   297   Inttab.merge (K true) (ids1, ids2)
   298   |> insert_id draft1 id1
   299   |> insert_id draft2 id2;
   300 
   301 
   302 (* equality and inclusion *)
   303 
   304 val eq_thy = eq_id o pairself (#id o identity_of);
   305 
   306 fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
   307   Inttab.defined ids id;
   308 
   309 fun subthy thys = eq_thy thys orelse proper_subthy thys;
   310 
   311 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
   312 
   313 
   314 (* consistent ancestors *)
   315 
   316 fun eq_thy_consistent (thy1, thy2) =
   317   eq_thy (thy1, thy2) orelse
   318     (theory_name thy1 = theory_name thy2 andalso
   319       raise THEORY ("Duplicate theory name", [thy1, thy2]));
   320 
   321 fun extend_ancestors thy thys =
   322   if member eq_thy_consistent thys thy then
   323     raise THEORY ("Duplicate theory node", thy :: thys)
   324   else thy :: thys;
   325 
   326 val merge_ancestors = merge eq_thy_consistent;
   327 
   328 
   329 (* trivial merge *)
   330 
   331 fun merge (thy1, thy2) =
   332   if eq_thy (thy1, thy2) then thy1
   333   else if proper_subthy (thy2, thy1) then thy1
   334   else if proper_subthy (thy1, thy2) then thy2
   335   else error (cat_lines ["Attempt to perform non-trivial merge of theories:",
   336     str_of_thy thy1, str_of_thy thy2]);
   337 
   338 fun merge_refs (ref1, ref2) =
   339   if ref1 = ref2 then ref1
   340   else check_thy (merge (deref ref1, deref ref2));
   341 
   342 
   343 
   344 (** build theories **)
   345 
   346 (* primitives *)
   347 
   348 local
   349   val lock = Mutex.mutex ();
   350 in
   351   fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e;
   352 end;
   353 
   354 fun create_thy self draft ids data ancestry history =
   355   let val identity = make_identity self draft (serial ()) ids;
   356   in vitalize (Theory (identity, data, ancestry, history)) end;
   357 
   358 fun change_thy draft' f thy =
   359   let
   360     val Theory ({self, draft, id, ids}, data, ancestry, history) = thy;
   361     val (self', data', ancestry') =
   362       if draft then (self, data, ancestry)    (*destructive change!*)
   363       else if #stage history > 0
   364       then (NONE, data, ancestry)
   365       else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)));
   366     val ids' = insert_id draft id ids;
   367     val data'' = f data';
   368     val thy' = SYNCHRONIZED (fn () =>
   369       (check_thy thy; create_thy self' draft' ids' data'' ancestry' history));
   370   in thy' end;
   371 
   372 val name_thy = change_thy false I;
   373 val extend_thy = change_thy true I;
   374 val modify_thy = change_thy true;
   375 
   376 fun copy_thy thy =
   377   let
   378     val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
   379     val ids' = insert_id draft id ids;
   380     val thy' = SYNCHRONIZED (fn () =>
   381       (check_thy thy; create_thy NONE true ids' data ancestry history));
   382   in thy' end;
   383 
   384 val pre_pure_thy = create_thy NONE true Inttab.empty
   385   Datatab.empty (make_ancestry [] []) (make_history PureN 0);
   386 
   387 
   388 (* named theory nodes *)
   389 
   390 fun merge_thys pp (thy1, thy2) =
   391   let
   392     val ids = merge_ids thy1 thy2;
   393     val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   394     val ancestry = make_ancestry [] [];
   395     val history = make_history "" 0;
   396     val thy' = SYNCHRONIZED (fn () =>
   397      (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history));
   398   in thy' end;
   399 
   400 fun maximal_thys thys =
   401   thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
   402 
   403 fun begin_thy pp name imports =
   404   if name = "" orelse name = draftN then error ("Bad theory name: " ^ quote name)
   405   else
   406     let
   407       val parents = maximal_thys (distinct eq_thy imports);
   408       val ancestors =
   409         Library.foldl merge_ancestors ([], map ancestors_of parents)
   410         |> fold extend_ancestors parents;
   411 
   412       val Theory ({ids, ...}, data, _, _) =
   413         (case parents of
   414           [] => error "Missing theory imports"
   415         | [thy] => extend_thy thy
   416         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   417 
   418       val ancestry = make_ancestry parents ancestors;
   419       val history = make_history name 0;
   420       val thy' = SYNCHRONIZED (fn () =>
   421         (map check_thy imports; create_thy NONE true ids data ancestry history));
   422     in thy' end;
   423 
   424 
   425 (* history stages *)
   426 
   427 fun history_stage f thy =
   428   let
   429     val {name, stage} = history_of thy;
   430     val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]);
   431     val history' = make_history name (f stage);
   432     val thy' as Theory (identity', data', ancestry', _) = name_thy thy;
   433     val thy'' = SYNCHRONIZED (fn () =>
   434       (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
   435   in thy'' end;
   436 
   437 fun checkpoint_thy thy =
   438   if is_draft thy then history_stage (fn stage => stage + 1) thy
   439   else thy;
   440 
   441 val finish_thy = history_stage (fn _ => finished);
   442 
   443 
   444 (* theory data *)
   445 
   446 structure Theory_Data =
   447 struct
   448 
   449 val declare = declare_theory_data;
   450 
   451 fun get k dest thy =
   452   (case Datatab.lookup (data_of thy) k of
   453     SOME x => x
   454   | NONE => invoke_empty k) |> dest;
   455 
   456 fun put k mk x = modify_thy (Datatab.update (k, mk x));
   457 
   458 end;
   459 
   460 
   461 
   462 (*** proof context ***)
   463 
   464 (* datatype Proof.context *)
   465 
   466 structure Proof =
   467 struct
   468   datatype context = Context of Any.T Datatab.table * theory_ref;
   469 end;
   470 
   471 fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref;
   472 fun data_of_proof (Proof.Context (data, _)) = data;
   473 fun map_prf f (Proof.Context (data, thy_ref)) = Proof.Context (f data, thy_ref);
   474 
   475 
   476 (* proof data kinds *)
   477 
   478 local
   479 
   480 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
   481 
   482 fun invoke_init k =
   483   (case Datatab.lookup (Synchronized.value kinds) k of
   484     SOME init => init
   485   | NONE => raise Fail "Invalid proof data identifier");
   486 
   487 fun init_data thy =
   488   Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
   489 
   490 fun init_new_data data thy =
   491   Datatab.merge (K true) (data, init_data thy);
   492 
   493 in
   494 
   495 fun raw_transfer thy' (Proof.Context (data, thy_ref)) =
   496   let
   497     val thy = deref thy_ref;
   498     val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
   499     val _ = check_thy thy;
   500     val data' = init_new_data data thy';
   501     val thy_ref' = check_thy thy';
   502   in Proof.Context (data', thy_ref') end;
   503 
   504 structure Proof_Context =
   505 struct
   506   val theory_of = theory_of_proof;
   507   fun init_global thy = Proof.Context (init_data thy, check_thy thy);
   508   fun get_global thy name = init_global (get_theory thy name);
   509 end;
   510 
   511 structure Proof_Data =
   512 struct
   513 
   514 fun declare init =
   515   let
   516     val k = serial ();
   517     val _ = Synchronized.change kinds (Datatab.update (k, init));
   518   in k end;
   519 
   520 fun get k dest prf =
   521   dest (case Datatab.lookup (data_of_proof prf) k of
   522     SOME x => x
   523   | NONE => invoke_init k (Proof_Context.theory_of prf));   (*adhoc value*)
   524 
   525 fun put k mk x = map_prf (Datatab.update (k, mk x));
   526 
   527 end;
   528 
   529 end;
   530 
   531 
   532 
   533 (*** generic context ***)
   534 
   535 datatype generic = Theory of theory | Proof of Proof.context;
   536 
   537 fun cases f _ (Theory thy) = f thy
   538   | cases _ g (Proof prf) = g prf;
   539 
   540 fun mapping f g = cases (Theory o f) (Proof o g);
   541 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
   542 
   543 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
   544 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
   545 
   546 fun map_theory f = Theory o f o the_theory;
   547 fun map_proof f = Proof o f o the_proof;
   548 
   549 fun map_theory_result f = apsnd Theory o f o the_theory;
   550 fun map_proof_result f = apsnd Proof o f o the_proof;
   551 
   552 fun theory_map f = the_theory o f o Theory;
   553 fun proof_map f = the_proof o f o Proof;
   554 
   555 val theory_of = cases I Proof_Context.theory_of;
   556 val proof_of = cases Proof_Context.init_global I;
   557 
   558 
   559 (* pretty printing context *)
   560 
   561 exception PRETTY of generic;
   562 
   563 val pretty_generic = Pretty o PRETTY;
   564 val pretty = pretty_generic o Proof;
   565 val pretty_global = pretty_generic o Theory;
   566 
   567 fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   568 
   569 
   570 
   571 (** thread data **)
   572 
   573 local val tag = Universal.tag () : generic option Universal.tag in
   574 
   575 fun thread_data () =
   576   (case Thread.getLocal tag of
   577     SOME (SOME context) => SOME context
   578   | _ => NONE);
   579 
   580 fun the_thread_data () =
   581   (case thread_data () of
   582     SOME context => context
   583   | _ => error "Unknown context");
   584 
   585 fun set_thread_data context = Thread.setLocal (tag, context);
   586 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   587 
   588 end;
   589 
   590 fun >>> f =
   591   let
   592     val (res, context') = f (the_thread_data ());
   593     val _ = set_thread_data (SOME context');
   594   in res end;
   595 
   596 nonfix >>;
   597 fun >> f = >>> (fn context => ((), f context));
   598 
   599 val _ = set_thread_data (SOME (Theory pre_pure_thy));
   600 
   601 end;
   602 
   603 structure Basic_Context: BASIC_CONTEXT = Context;
   604 open Basic_Context;
   605 
   606 
   607 
   608 (*** type-safe interfaces for data declarations ***)
   609 
   610 (** theory data **)
   611 
   612 signature THEORY_DATA_PP_ARGS =
   613 sig
   614   type T
   615   val empty: T
   616   val extend: T -> T
   617   val merge: Context.pretty -> T * T -> T
   618 end;
   619 
   620 signature THEORY_DATA_ARGS =
   621 sig
   622   type T
   623   val empty: T
   624   val extend: T -> T
   625   val merge: T * T -> T
   626 end;
   627 
   628 signature THEORY_DATA =
   629 sig
   630   type T
   631   val get: theory -> T
   632   val put: T -> theory -> theory
   633   val map: (T -> T) -> theory -> theory
   634 end;
   635 
   636 functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
   637 struct
   638 
   639 type T = Data.T;
   640 exception Data of T;
   641 
   642 val kind =
   643   Context.Theory_Data.declare
   644     (Position.thread_data ())
   645     (Data Data.empty)
   646     (fn Data x => Data (Data.extend x))
   647     (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   648 
   649 val get = Context.Theory_Data.get kind (fn Data x => x);
   650 val put = Context.Theory_Data.put kind Data;
   651 fun map f thy = put (f (get thy)) thy;
   652 
   653 end;
   654 
   655 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   656   Theory_Data_PP
   657   (
   658     type T = Data.T;
   659     val empty = Data.empty;
   660     val extend = Data.extend;
   661     fun merge _ = Data.merge;
   662   );
   663 
   664 
   665 
   666 (** proof data **)
   667 
   668 signature PROOF_DATA_ARGS =
   669 sig
   670   type T
   671   val init: theory -> T
   672 end;
   673 
   674 signature PROOF_DATA =
   675 sig
   676   type T
   677   val get: Proof.context -> T
   678   val put: T -> Proof.context -> Proof.context
   679   val map: (T -> T) -> Proof.context -> Proof.context
   680 end;
   681 
   682 functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
   683 struct
   684 
   685 type T = Data.T;
   686 exception Data of T;
   687 
   688 val kind = Context.Proof_Data.declare (Data o Data.init);
   689 
   690 val get = Context.Proof_Data.get kind (fn Data x => x);
   691 val put = Context.Proof_Data.put kind Data;
   692 fun map f prf = put (f (get prf)) prf;
   693 
   694 end;
   695 
   696 
   697 
   698 (** generic data **)
   699 
   700 signature GENERIC_DATA_ARGS =
   701 sig
   702   type T
   703   val empty: T
   704   val extend: T -> T
   705   val merge: T * T -> T
   706 end;
   707 
   708 signature GENERIC_DATA =
   709 sig
   710   type T
   711   val get: Context.generic -> T
   712   val put: T -> Context.generic -> Context.generic
   713   val map: (T -> T) -> Context.generic -> Context.generic
   714 end;
   715 
   716 functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
   717 struct
   718 
   719 structure Thy_Data = Theory_Data(Data);
   720 structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
   721 
   722 type T = Data.T;
   723 
   724 fun get (Context.Theory thy) = Thy_Data.get thy
   725   | get (Context.Proof prf) = Prf_Data.get prf;
   726 
   727 fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
   728   | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
   729 
   730 fun map f ctxt = put (f (get ctxt)) ctxt;
   731 
   732 end;
   733 
   734 (*hide private interface*)
   735 structure Context: CONTEXT = Context;
   736