src/Pure/context.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70459 f0a445c5a82c
child 70586 57df8a85317a
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     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   exception THEORY of string * theory list
    18   structure Proof: sig type context end
    19   structure Proof_Context:
    20   sig
    21     val theory_of: Proof.context -> theory
    22     val init_global: theory -> Proof.context
    23     val get_global: theory -> string -> Proof.context
    24   end
    25 end;
    26 
    27 signature CONTEXT =
    28 sig
    29   include BASIC_CONTEXT
    30   (*theory context*)
    31   type theory_id
    32   val theory_id: theory -> theory_id
    33   val timing: bool Unsynchronized.ref
    34   val parents_of: theory -> theory list
    35   val ancestors_of: theory -> theory list
    36   val theory_id_ord: theory_id * theory_id -> order
    37   val theory_id_long_name: theory_id -> string
    38   val theory_id_name: theory_id -> string
    39   val theory_long_name: theory -> string
    40   val theory_name: theory -> string
    41   val theory_name': {long: bool} -> theory -> string
    42   val PureN: string
    43   val pretty_thy: theory -> Pretty.T
    44   val pretty_abbrev_thy: theory -> Pretty.T
    45   val get_theory: {long: bool} -> theory -> string -> theory
    46   val eq_thy_id: theory_id * theory_id -> bool
    47   val eq_thy: theory * theory -> bool
    48   val proper_subthy_id: theory_id * theory_id -> bool
    49   val proper_subthy: theory * theory -> bool
    50   val subthy_id: theory_id * theory_id -> bool
    51   val subthy: theory * theory -> bool
    52   val trace_theories: bool Unsynchronized.ref
    53   val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int}
    54   val join_thys: theory * theory -> theory
    55   val begin_thy: string -> theory list -> theory
    56   val finish_thy: theory -> theory
    57   val theory_data_size: theory -> (Position.T * int) list
    58   (*proof context*)
    59   val raw_transfer: theory -> Proof.context -> Proof.context
    60   (*certificate*)
    61   datatype certificate = Certificate of theory | Certificate_Id of theory_id
    62   val certificate_theory: certificate -> theory
    63   val certificate_theory_id: certificate -> theory_id
    64   val eq_certificate: certificate * certificate -> bool
    65   val join_certificate: certificate * certificate -> certificate
    66   (*generic context*)
    67   datatype generic = Theory of theory | Proof of Proof.context
    68   val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a
    69   val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic
    70   val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) ->
    71     generic -> 'a * generic
    72   val the_theory: generic -> theory
    73   val the_proof: generic -> Proof.context
    74   val map_theory: (theory -> theory) -> generic -> generic
    75   val map_proof: (Proof.context -> Proof.context) -> generic -> generic
    76   val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
    77   val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic
    78   val theory_map: (generic -> generic) -> theory -> theory
    79   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    80   val theory_of: generic -> theory  (*total*)
    81   val proof_of: generic -> Proof.context  (*total*)
    82   (*thread data*)
    83   val get_generic_context: unit -> generic option
    84   val put_generic_context: generic option -> unit
    85   val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b
    86   val the_generic_context: unit -> generic
    87   val the_global_context: unit -> theory
    88   val the_local_context: unit -> Proof.context
    89   val >> : (generic -> generic) -> unit
    90   val >>> : (generic -> 'a * generic) -> 'a
    91 end;
    92 
    93 signature PRIVATE_CONTEXT =
    94 sig
    95   include CONTEXT
    96   structure Theory_Data:
    97   sig
    98     val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
    99       (theory * theory -> Any.T * Any.T -> Any.T) -> serial
   100     val get: serial -> (Any.T -> 'a) -> theory -> 'a
   101     val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
   102   end
   103   structure Proof_Data:
   104   sig
   105     val declare: (theory -> Any.T) -> serial
   106     val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
   107     val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
   108   end
   109 end;
   110 
   111 structure Context: PRIVATE_CONTEXT =
   112 struct
   113 
   114 (*** theory context ***)
   115 
   116 (*private copy avoids potential conflict of table exceptions*)
   117 structure Datatab = Table(type key = int val ord = int_ord);
   118 
   119 
   120 (** datatype theory **)
   121 
   122 type stage = int * int Synchronized.var;
   123 fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1);
   124 fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state);
   125 
   126 abstype theory_id =
   127   Theory_Id of
   128    (*identity*)
   129    {id: serial,                   (*identifier*)
   130     ids: Inttab.set} *            (*cumulative identifiers -- symbolic body content*)
   131    (*history*)
   132    {name: string,                 (*official theory name*)
   133     stage: stage option}          (*index and counter for anonymous updates*)
   134 with
   135 
   136 fun rep_theory_id (Theory_Id args) = args;
   137 val make_theory_id = Theory_Id;
   138 
   139 end;
   140 
   141 datatype theory =
   142   Theory of
   143    (*identity*)
   144    {theory_id: theory_id,
   145     token: Position.T Unsynchronized.ref} *
   146    (*ancestry*)
   147    {parents: theory list,         (*immediate predecessors*)
   148     ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
   149    (*data*)
   150    Any.T Datatab.table;           (*body content*)
   151 
   152 exception THEORY of string * theory list;
   153 
   154 fun rep_theory (Theory args) = args;
   155 
   156 val theory_identity = #1 o rep_theory;
   157 val theory_id = #theory_id o theory_identity;
   158 
   159 val identity_of_id = #1 o rep_theory_id;
   160 val identity_of = identity_of_id o theory_id;
   161 val history_of_id = #2 o rep_theory_id;
   162 val history_of = history_of_id o theory_id;
   163 val ancestry_of = #2 o rep_theory;
   164 val data_of = #3 o rep_theory;
   165 
   166 fun make_identity id ids = {id = id, ids = ids};
   167 fun make_history name = {name = name, stage = SOME (init_stage ())};
   168 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   169 
   170 val theory_id_ord = int_ord o apply2 (#id o identity_of_id);
   171 val theory_id_long_name = #name o history_of_id;
   172 val theory_id_name = Long_Name.base_name o theory_id_long_name;
   173 val theory_long_name = #name o history_of;
   174 val theory_name = Long_Name.base_name o theory_long_name;
   175 fun theory_name' {long} = if long then theory_long_name else theory_name;
   176 
   177 val parents_of = #parents o ancestry_of;
   178 val ancestors_of = #ancestors o ancestry_of;
   179 
   180 
   181 (* names *)
   182 
   183 val PureN = "Pure";
   184 
   185 fun display_name thy_id =
   186   (case history_of_id thy_id of
   187     {name, stage = NONE} => name
   188   | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i);
   189 
   190 fun display_names thy =
   191   let
   192     val name = display_name (theory_id thy);
   193     val ancestor_names = map theory_long_name (ancestors_of thy);
   194   in rev (name :: ancestor_names) end;
   195 
   196 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   197 
   198 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
   199 
   200 fun pretty_abbrev_thy thy =
   201   let
   202     val names = display_names thy;
   203     val n = length names;
   204     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   205   in Pretty.str_list "{" "}" abbrev end;
   206 
   207 fun get_theory long thy name =
   208   if theory_name' long thy <> name then
   209     (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
   210       SOME thy' => thy'
   211     | NONE => error ("Unknown ancestor theory " ^ quote name))
   212   else if is_none (#stage (history_of thy)) then thy
   213   else error ("Unfinished theory " ^ quote name);
   214 
   215 
   216 (* build ids *)
   217 
   218 fun insert_id id ids = Inttab.update (id, ()) ids;
   219 
   220 val merge_ids =
   221   apply2 (theory_id #> rep_theory_id #> #1) #>
   222   (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) =>
   223     Inttab.merge (K true) (ids1, ids2)
   224     |> insert_id id1
   225     |> insert_id id2);
   226 
   227 
   228 (* equality and inclusion *)
   229 
   230 val eq_thy_id = op = o apply2 (#id o identity_of_id);
   231 val eq_thy = op = o apply2 (#id o identity_of);
   232 
   233 val proper_subthy_id =
   234   apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Inttab.defined ids id);
   235 val proper_subthy = proper_subthy_id o apply2 theory_id;
   236 
   237 fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
   238 val subthy = subthy_id o apply2 theory_id;
   239 
   240 
   241 (* consistent ancestors *)
   242 
   243 fun eq_thy_consistent (thy1, thy2) =
   244   eq_thy (thy1, thy2) orelse
   245     (theory_name thy1 = theory_name thy2 andalso
   246       raise THEORY ("Duplicate theory name", [thy1, thy2]));
   247 
   248 fun extend_ancestors thy thys =
   249   if member eq_thy_consistent thys thy then
   250     raise THEORY ("Duplicate theory node", thy :: thys)
   251   else thy :: thys;
   252 
   253 val merge_ancestors = merge eq_thy_consistent;
   254 
   255 
   256 
   257 (** theory data **)
   258 
   259 (* data kinds and access methods *)
   260 
   261 val timing = Unsynchronized.ref false;
   262 
   263 local
   264 
   265 type kind =
   266  {pos: Position.T,
   267   empty: Any.T,
   268   extend: Any.T -> Any.T,
   269   merge: theory * theory -> Any.T * Any.T -> Any.T};
   270 
   271 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
   272 
   273 fun invoke name f k x =
   274   (case Datatab.lookup (Synchronized.value kinds) k of
   275     SOME kind =>
   276       if ! timing andalso name <> "" then
   277         Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
   278           (fn () => f kind x)
   279       else f kind x
   280   | NONE => raise Fail "Invalid theory data identifier");
   281 
   282 in
   283 
   284 fun invoke_pos k = invoke "" (K o #pos) k ();
   285 fun invoke_empty k = invoke "" (K o #empty) k ();
   286 val invoke_extend = invoke "extend" #extend;
   287 fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
   288 
   289 fun declare_theory_data pos empty extend merge =
   290   let
   291     val k = serial ();
   292     val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
   293     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   294   in k end;
   295 
   296 val extend_data = Datatab.map invoke_extend;
   297 fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
   298 
   299 end;
   300 
   301 
   302 
   303 (** build theories **)
   304 
   305 (* create theory *)
   306 
   307 val trace_theories = Unsynchronized.ref false;
   308 
   309 local
   310 
   311 val theories =
   312   Synchronized.var "theory_tokens"
   313     ([]: Position.T Unsynchronized.ref option Unsynchronized.ref list);
   314 
   315 val dummy_token = Unsynchronized.ref Position.none;
   316 
   317 fun make_token () =
   318   if ! trace_theories then
   319     let
   320       val token = Unsynchronized.ref (Position.thread_data ());
   321       val _ = Synchronized.change theories (cons (Weak.weak (SOME token)));
   322     in token end
   323   else dummy_token;
   324 
   325 in
   326 
   327 fun theories_trace () =
   328   let
   329     val trace = Synchronized.value theories;
   330     val _ = ML_Heap.full_gc ();
   331     val active_positions =
   332       fold (fn Unsynchronized.ref (SOME pos) => cons (! pos) | _ => I) trace [];
   333   in
   334     {active_positions = active_positions,
   335      active = length active_positions,
   336      total = length trace}
   337   end;
   338 
   339 fun create_thy ids history ancestry data =
   340   let
   341     val theory_id = make_theory_id (make_identity (serial ()) ids, history);
   342     val token = make_token ();
   343   in Theory ({theory_id = theory_id, token = token}, ancestry, data) end;
   344 
   345 end;
   346 
   347 
   348 (* primitives *)
   349 
   350 val pre_pure_thy =
   351   create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
   352 
   353 local
   354 
   355 fun change_thy finish f thy =
   356   let
   357     val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy);
   358     val Theory (_, ancestry, data) = thy;
   359     val (ancestry', data') =
   360       if is_none stage then
   361         (make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data)
   362       else (ancestry, data);
   363     val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
   364     val ids' = insert_id id ids;
   365     val data'' = f data';
   366   in create_thy ids' history' ancestry' data'' end;
   367 
   368 in
   369 
   370 val update_thy = change_thy false;
   371 val extend_thy = update_thy I;
   372 val finish_thy = change_thy true I #> tap extend_thy;
   373 
   374 end;
   375 
   376 
   377 (* join: anonymous theory nodes *)
   378 
   379 local
   380 
   381 fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]);
   382 
   383 fun join_history thys =
   384   apply2 history_of thys |>
   385   (fn ({name, stage}, {name = name', stage = stage'}) =>
   386     if name = name' andalso is_some stage andalso is_some stage' then
   387       {name = name, stage = Option.map next_stage stage}
   388     else bad_join thys);
   389 
   390 fun join_ancestry thys =
   391   apply2 ancestry_of thys |>
   392   (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
   393     if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')
   394     then ancestry else bad_join thys);
   395 
   396 in
   397 
   398 fun join_thys thys =
   399   let
   400     val ids = merge_ids thys;
   401     val history = join_history thys;
   402     val ancestry = join_ancestry thys;
   403     val data = merge_data thys (apply2 data_of thys);
   404   in create_thy ids history ancestry data end;
   405 
   406 end;
   407 
   408 
   409 (* merge: named theory nodes *)
   410 
   411 local
   412 
   413 fun merge_thys thys =
   414   let
   415     val ids = merge_ids thys;
   416     val history = make_history "";
   417     val ancestry = make_ancestry [] [];
   418     val data = merge_data thys (apply2 data_of thys);
   419   in create_thy ids history ancestry data end;
   420 
   421 fun maximal_thys thys =
   422   thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
   423 
   424 in
   425 
   426 fun begin_thy name imports =
   427   if name = "" then error ("Bad theory name: " ^ quote name)
   428   else
   429     let
   430       val parents = maximal_thys (distinct eq_thy imports);
   431       val ancestors =
   432         Library.foldl merge_ancestors ([], map ancestors_of parents)
   433         |> fold extend_ancestors parents;
   434 
   435       val thy0 =
   436         (case parents of
   437           [] => error "Missing theory imports"
   438         | [thy] => extend_thy thy
   439         | thy :: thys => Library.foldl merge_thys (thy, thys));
   440       val ({ids, ...}, _) = rep_theory_id (theory_id thy0);
   441 
   442       val history = make_history name;
   443       val ancestry = make_ancestry parents ancestors;
   444     in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
   445 
   446 end;
   447 
   448 
   449 (* theory data *)
   450 
   451 structure Theory_Data =
   452 struct
   453 
   454 val declare = declare_theory_data;
   455 
   456 fun get k dest thy =
   457   (case Datatab.lookup (data_of thy) k of
   458     SOME x => x
   459   | NONE => invoke_empty k) |> dest;
   460 
   461 fun put k mk x = update_thy (Datatab.update (k, mk x));
   462 
   463 fun obj_size k thy =
   464   Datatab.lookup (data_of thy) k |> Option.map ML_Heap.obj_size;
   465 
   466 end;
   467 
   468 fun theory_data_size thy =
   469   (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
   470     (case Theory_Data.obj_size k thy of
   471       NONE => I
   472     | SOME n => (cons (invoke_pos k, n))));
   473 
   474 
   475 
   476 (*** proof context ***)
   477 
   478 (* datatype Proof.context *)
   479 
   480 structure Proof =
   481 struct
   482   datatype context = Context of Any.T Datatab.table * theory;
   483 end;
   484 
   485 
   486 (* proof data kinds *)
   487 
   488 local
   489 
   490 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
   491 
   492 fun init_data thy =
   493   Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy);
   494 
   495 fun init_new_data thy =
   496   Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data =>
   497     if Datatab.defined data k then data
   498     else Datatab.update (k, init thy) data);
   499 
   500 fun init_fallback k thy =
   501   (case Datatab.lookup (Synchronized.value kinds) k of
   502     SOME init => init thy
   503   | NONE => raise Fail "Invalid proof data identifier");
   504 
   505 in
   506 
   507 fun raw_transfer thy' (Proof.Context (data, thy)) =
   508   let
   509     val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
   510     val data' = init_new_data thy' data;
   511   in Proof.Context (data', thy') end;
   512 
   513 structure Proof_Context =
   514 struct
   515   fun theory_of (Proof.Context (_, thy)) = thy;
   516   fun init_global thy = Proof.Context (init_data thy, thy);
   517   fun get_global thy name = init_global (get_theory {long = false} thy name);
   518 end;
   519 
   520 structure Proof_Data =
   521 struct
   522 
   523 fun declare init =
   524   let
   525     val k = serial ();
   526     val _ = Synchronized.change kinds (Datatab.update (k, init));
   527   in k end;
   528 
   529 fun get k dest (Proof.Context (data, thy)) =
   530   (case Datatab.lookup data k of
   531     SOME x => x
   532   | NONE => init_fallback k thy) |> dest;
   533 
   534 fun put k mk x (Proof.Context (data, thy)) =
   535   Proof.Context (Datatab.update (k, mk x) data, thy);
   536 
   537 end;
   538 
   539 end;
   540 
   541 
   542 
   543 (*** theory certificate ***)
   544 
   545 datatype certificate = Certificate of theory | Certificate_Id of theory_id;
   546 
   547 fun certificate_theory (Certificate thy) = thy
   548   | certificate_theory (Certificate_Id thy_id) =
   549       error ("No content for theory certificate " ^ display_name thy_id);
   550 
   551 fun certificate_theory_id (Certificate thy) = theory_id thy
   552   | certificate_theory_id (Certificate_Id thy_id) = thy_id;
   553 
   554 fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2)
   555   | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2)
   556   | eq_certificate _ = false;
   557 
   558 fun join_certificate (cert1, cert2) =
   559   let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in
   560     if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2)
   561     else if proper_subthy_id (thy_id2, thy_id1) then cert1
   562     else if proper_subthy_id (thy_id1, thy_id2) then cert2
   563     else
   564       error ("Cannot join unrelated theory certificates " ^
   565         display_name thy_id1 ^ " and " ^ display_name thy_id2)
   566   end;
   567 
   568 
   569 
   570 (*** generic context ***)
   571 
   572 datatype generic = Theory of theory | Proof of Proof.context;
   573 
   574 fun cases f _ (Theory thy) = f thy
   575   | cases _ g (Proof prf) = g prf;
   576 
   577 fun mapping f g = cases (Theory o f) (Proof o g);
   578 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
   579 
   580 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
   581 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
   582 
   583 fun map_theory f = Theory o f o the_theory;
   584 fun map_proof f = Proof o f o the_proof;
   585 
   586 fun map_theory_result f = apsnd Theory o f o the_theory;
   587 fun map_proof_result f = apsnd Proof o f o the_proof;
   588 
   589 fun theory_map f = the_theory o f o Theory;
   590 fun proof_map f = the_proof o f o Proof;
   591 
   592 val theory_of = cases I Proof_Context.theory_of;
   593 val proof_of = cases Proof_Context.init_global I;
   594 
   595 
   596 
   597 (** thread data **)
   598 
   599 local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in
   600 
   601 fun get_generic_context () = Thread_Data.get generic_context_var;
   602 val put_generic_context = Thread_Data.put generic_context_var;
   603 fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context;
   604 
   605 fun the_generic_context () =
   606   (case get_generic_context () of
   607     SOME context => context
   608   | _ => error "Unknown context");
   609 
   610 val the_global_context = theory_of o the_generic_context;
   611 val the_local_context = proof_of o the_generic_context;
   612 
   613 end;
   614 
   615 fun >>> f =
   616   let
   617     val (res, context') = f (the_generic_context ());
   618     val _ = put_generic_context (SOME context');
   619   in res end;
   620 
   621 nonfix >>;
   622 fun >> f = >>> (fn context => ((), f context));
   623 
   624 val _ = put_generic_context (SOME (Theory pre_pure_thy));
   625 
   626 end;
   627 
   628 structure Basic_Context: BASIC_CONTEXT = Context;
   629 open Basic_Context;
   630 
   631 
   632 
   633 (*** type-safe interfaces for data declarations ***)
   634 
   635 (** theory data **)
   636 
   637 signature THEORY_DATA'_ARGS =
   638 sig
   639   type T
   640   val empty: T
   641   val extend: T -> T
   642   val merge: theory * theory -> T * T -> T
   643 end;
   644 
   645 signature THEORY_DATA_ARGS =
   646 sig
   647   type T
   648   val empty: T
   649   val extend: T -> T
   650   val merge: T * T -> T
   651 end;
   652 
   653 signature THEORY_DATA =
   654 sig
   655   type T
   656   val get: theory -> T
   657   val put: T -> theory -> theory
   658   val map: (T -> T) -> theory -> theory
   659 end;
   660 
   661 functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
   662 struct
   663 
   664 type T = Data.T;
   665 exception Data of T;
   666 
   667 val kind =
   668   Context.Theory_Data.declare
   669     (Position.thread_data ())
   670     (Data Data.empty)
   671     (fn Data x => Data (Data.extend x))
   672     (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
   673 
   674 val get = Context.Theory_Data.get kind (fn Data x => x);
   675 val put = Context.Theory_Data.put kind Data;
   676 fun map f thy = put (f (get thy)) thy;
   677 
   678 end;
   679 
   680 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   681   Theory_Data'
   682   (
   683     type T = Data.T;
   684     val empty = Data.empty;
   685     val extend = Data.extend;
   686     fun merge _ = Data.merge;
   687   );
   688 
   689 
   690 
   691 (** proof data **)
   692 
   693 signature PROOF_DATA_ARGS =
   694 sig
   695   type T
   696   val init: theory -> T
   697 end;
   698 
   699 signature PROOF_DATA =
   700 sig
   701   type T
   702   val get: Proof.context -> T
   703   val put: T -> Proof.context -> Proof.context
   704   val map: (T -> T) -> Proof.context -> Proof.context
   705 end;
   706 
   707 functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
   708 struct
   709 
   710 type T = Data.T;
   711 exception Data of T;
   712 
   713 val kind = Context.Proof_Data.declare (Data o Data.init);
   714 
   715 val get = Context.Proof_Data.get kind (fn Data x => x);
   716 val put = Context.Proof_Data.put kind Data;
   717 fun map f prf = put (f (get prf)) prf;
   718 
   719 end;
   720 
   721 
   722 
   723 (** generic data **)
   724 
   725 signature GENERIC_DATA_ARGS =
   726 sig
   727   type T
   728   val empty: T
   729   val extend: T -> T
   730   val merge: T * T -> T
   731 end;
   732 
   733 signature GENERIC_DATA =
   734 sig
   735   type T
   736   val get: Context.generic -> T
   737   val put: T -> Context.generic -> Context.generic
   738   val map: (T -> T) -> Context.generic -> Context.generic
   739 end;
   740 
   741 functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
   742 struct
   743 
   744 structure Thy_Data = Theory_Data(Data);
   745 structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
   746 
   747 type T = Data.T;
   748 
   749 fun get (Context.Theory thy) = Thy_Data.get thy
   750   | get (Context.Proof prf) = Prf_Data.get prf;
   751 
   752 fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
   753   | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
   754 
   755 fun map f ctxt = put (f (get ctxt)) ctxt;
   756 
   757 end;
   758 
   759 (*hide private interface*)
   760 structure Context: CONTEXT = Context;