src/Pure/context.ML
author wenzelm
Mon Mar 10 15:04:01 2014 +0100 (2014-03-10)
changeset 56026 893fe12639bc
parent 55547 384bfd19ee61
child 59058 a78612c67ec0
permissions -rw-r--r--
tuned signature -- prefer Name_Space.get with its builtin error;
     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   val timing: bool Unsynchronized.ref
    32   type pretty
    33   val parents_of: theory -> theory list
    34   val ancestors_of: theory -> theory list
    35   val theory_name: theory -> string
    36   val PureN: string
    37   val display_names: theory -> string list
    38   val pretty_thy: theory -> Pretty.T
    39   val string_of_thy: theory -> string
    40   val pretty_abbrev_thy: theory -> Pretty.T
    41   val str_of_thy: theory -> string
    42   val get_theory: theory -> string -> theory
    43   val this_theory: theory -> string -> theory
    44   val eq_thy: theory * theory -> bool
    45   val subthy: theory * theory -> bool
    46   val merge: theory * theory -> theory
    47   val finish_thy: theory -> theory
    48   val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    49   (*proof context*)
    50   val raw_transfer: theory -> Proof.context -> Proof.context
    51   (*generic context*)
    52   datatype generic = Theory of theory | Proof of Proof.context
    53   val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a
    54   val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic
    55   val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) ->
    56     generic -> 'a * generic
    57   val the_theory: generic -> theory
    58   val the_proof: generic -> Proof.context
    59   val map_theory: (theory -> theory) -> generic -> generic
    60   val map_proof: (Proof.context -> Proof.context) -> generic -> generic
    61   val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
    62   val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic
    63   val theory_map: (generic -> generic) -> theory -> theory
    64   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    65   val theory_of: generic -> theory  (*total*)
    66   val proof_of: generic -> Proof.context  (*total*)
    67   (*pretty printing context*)
    68   val pretty: Proof.context -> pretty
    69   val pretty_global: theory -> pretty
    70   val pretty_generic: generic -> pretty
    71   val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    72   (*thread data*)
    73   val thread_data: unit -> generic option
    74   val the_thread_data: unit -> generic
    75   val set_thread_data: generic option -> unit
    76   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    77   val >> : (generic -> generic) -> unit
    78   val >>> : (generic -> 'a * generic) -> 'a
    79 end;
    80 
    81 signature PRIVATE_CONTEXT =
    82 sig
    83   include CONTEXT
    84   structure Theory_Data:
    85   sig
    86     val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
    87       (pretty -> Any.T * Any.T -> Any.T) -> serial
    88     val get: serial -> (Any.T -> 'a) -> theory -> 'a
    89     val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
    90   end
    91   structure Proof_Data:
    92   sig
    93     val declare: (theory -> Any.T) -> serial
    94     val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
    95     val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
    96   end
    97 end;
    98 
    99 structure Context: PRIVATE_CONTEXT =
   100 struct
   101 
   102 (*** theory context ***)
   103 
   104 (** theory data **)
   105 
   106 (* data kinds and access methods *)
   107 
   108 val timing = Unsynchronized.ref false;
   109 
   110 (*private copy avoids potential conflict of table exceptions*)
   111 structure Datatab = Table(type key = int val ord = int_ord);
   112 
   113 datatype pretty = Pretty of Any.T;
   114 
   115 local
   116 
   117 type kind =
   118  {pos: Position.T,
   119   empty: Any.T,
   120   extend: Any.T -> Any.T,
   121   merge: pretty -> Any.T * Any.T -> Any.T};
   122 
   123 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
   124 
   125 fun invoke name f k x =
   126   (case Datatab.lookup (Synchronized.value kinds) k of
   127     SOME kind =>
   128       if ! timing andalso name <> "" then
   129         Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
   130           (fn () => f kind x)
   131       else f kind x
   132   | NONE => raise Fail "Invalid theory data identifier");
   133 
   134 in
   135 
   136 fun invoke_empty k = invoke "" (K o #empty) k ();
   137 val invoke_extend = invoke "extend" #extend;
   138 fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
   139 
   140 fun declare_theory_data pos empty extend merge =
   141   let
   142     val k = serial ();
   143     val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
   144     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   145   in k end;
   146 
   147 val extend_data = Datatab.map invoke_extend;
   148 fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
   149 
   150 end;
   151 
   152 
   153 
   154 (** datatype theory **)
   155 
   156 datatype theory =
   157   Theory of
   158    (*identity*)
   159    {id: serial,                   (*identifier*)
   160     ids: Inttab.set} *            (*cumulative identifiers -- symbolic body content*)
   161    (*data*)
   162    Any.T Datatab.table *          (*body content*)
   163    (*ancestry*)
   164    {parents: theory list,         (*immediate predecessors*)
   165     ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
   166    (*history*)
   167    {name: string,                 (*official theory name*)
   168     stage: int};                  (*counter for anonymous updates*)
   169 
   170 exception THEORY of string * theory list;
   171 
   172 fun rep_theory (Theory args) = args;
   173 
   174 val identity_of = #1 o rep_theory;
   175 val data_of = #2 o rep_theory;
   176 val ancestry_of = #3 o rep_theory;
   177 val history_of = #4 o rep_theory;
   178 
   179 fun make_identity id ids = {id = id, ids = ids};
   180 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   181 fun make_history name stage = {name = name, stage = stage};
   182 
   183 val parents_of = #parents o ancestry_of;
   184 val ancestors_of = #ancestors o ancestry_of;
   185 val theory_name = #name o history_of;
   186 
   187 
   188 (* names *)
   189 
   190 val PureN = "Pure";
   191 val finished = ~1;
   192 
   193 fun display_names thy =
   194   let
   195     val {name, stage} = history_of thy;
   196     val name' =
   197       if stage = finished then name
   198       else name ^ ":" ^ string_of_int stage;
   199     val ancestor_names = map theory_name (ancestors_of thy);
   200   in rev (name' :: ancestor_names) end;
   201 
   202 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   203 val string_of_thy = Pretty.string_of o pretty_thy;
   204 
   205 fun pretty_abbrev_thy thy =
   206   let
   207     val names = display_names thy;
   208     val n = length names;
   209     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   210   in Pretty.str_list "{" "}" abbrev end;
   211 
   212 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   213 
   214 fun get_theory thy name =
   215   if theory_name thy <> name then
   216     (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
   217       SOME thy' => thy'
   218     | NONE => error ("Unknown ancestor theory " ^ quote name))
   219   else if #stage (history_of thy) = finished then thy
   220   else error ("Unfinished theory " ^ quote name);
   221 
   222 fun this_theory thy name =
   223   if theory_name thy = name then thy
   224   else get_theory thy name;
   225 
   226 
   227 (* build ids *)
   228 
   229 fun insert_id id ids = Inttab.update (id, ()) ids;
   230 
   231 fun merge_ids
   232     (Theory ({id = id1, ids = ids1, ...}, _, _, _))
   233     (Theory ({id = id2, ids = ids2, ...}, _, _, _)) =
   234   Inttab.merge (K true) (ids1, ids2)
   235   |> insert_id id1
   236   |> insert_id id2;
   237 
   238 
   239 (* equality and inclusion *)
   240 
   241 val eq_thy = op = o pairself (#id o identity_of);
   242 
   243 fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
   244   Inttab.defined ids id;
   245 
   246 fun subthy thys = eq_thy thys orelse proper_subthy thys;
   247 
   248 
   249 (* consistent ancestors *)
   250 
   251 fun eq_thy_consistent (thy1, thy2) =
   252   eq_thy (thy1, thy2) orelse
   253     (theory_name thy1 = theory_name thy2 andalso
   254       raise THEORY ("Duplicate theory name", [thy1, thy2]));
   255 
   256 fun extend_ancestors thy thys =
   257   if member eq_thy_consistent thys thy then
   258     raise THEORY ("Duplicate theory node", thy :: thys)
   259   else thy :: thys;
   260 
   261 val merge_ancestors = merge eq_thy_consistent;
   262 
   263 
   264 (* trivial merge *)
   265 
   266 fun merge (thy1, thy2) =
   267   if eq_thy (thy1, thy2) then thy1
   268   else if proper_subthy (thy2, thy1) then thy1
   269   else if proper_subthy (thy1, thy2) then thy2
   270   else error (cat_lines ["Attempt to perform non-trivial merge of theories:",
   271     str_of_thy thy1, str_of_thy thy2]);
   272 
   273 
   274 
   275 (** build theories **)
   276 
   277 (* primitives *)
   278 
   279 fun create_thy ids data ancestry history =
   280   Theory (make_identity (serial ()) ids, data, ancestry, history);
   281 
   282 val pre_pure_thy =
   283   create_thy Inttab.empty Datatab.empty (make_ancestry [] []) (make_history PureN 0);
   284 
   285 local
   286 
   287 fun change_thy finish f thy =
   288   let
   289     val Theory ({id, ids}, data, ancestry, {name, stage}) = thy;
   290     val (data', ancestry') =
   291       if stage = finished then
   292         (extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)))
   293       else (data, ancestry);
   294     val history' = {name = name, stage = if finish then finished else stage + 1};
   295     val ids' = insert_id id ids;
   296     val data'' = f data';
   297   in create_thy ids' data'' ancestry' history' end;
   298 
   299 in
   300 
   301 val update_thy = change_thy false;
   302 val extend_thy = update_thy I;
   303 val finish_thy = change_thy true I;
   304 
   305 end;
   306 
   307 
   308 (* named theory nodes *)
   309 
   310 fun merge_thys pp (thy1, thy2) =
   311   let
   312     val ids = merge_ids thy1 thy2;
   313     val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   314     val ancestry = make_ancestry [] [];
   315     val history = make_history "" 0;
   316   in create_thy ids data ancestry history end;
   317 
   318 fun maximal_thys thys =
   319   thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
   320 
   321 fun begin_thy pp name imports =
   322   if name = "" then error ("Bad theory name: " ^ quote name)
   323   else
   324     let
   325       val parents = maximal_thys (distinct eq_thy imports);
   326       val ancestors =
   327         Library.foldl merge_ancestors ([], map ancestors_of parents)
   328         |> fold extend_ancestors parents;
   329 
   330       val Theory ({ids, ...}, data, _, _) =
   331         (case parents of
   332           [] => error "Missing theory imports"
   333         | [thy] => extend_thy thy
   334         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   335 
   336       val ancestry = make_ancestry parents ancestors;
   337       val history = make_history name 0;
   338     in create_thy ids data ancestry history end;
   339 
   340 
   341 (* theory data *)
   342 
   343 structure Theory_Data =
   344 struct
   345 
   346 val declare = declare_theory_data;
   347 
   348 fun get k dest thy =
   349   (case Datatab.lookup (data_of thy) k of
   350     SOME x => x
   351   | NONE => invoke_empty k) |> dest;
   352 
   353 fun put k mk x = update_thy (Datatab.update (k, mk x));
   354 
   355 end;
   356 
   357 
   358 
   359 (*** proof context ***)
   360 
   361 (* datatype Proof.context *)
   362 
   363 structure Proof =
   364 struct
   365   datatype context = Context of Any.T Datatab.table * theory;
   366 end;
   367 
   368 fun theory_of_proof (Proof.Context (_, thy)) = thy;
   369 fun data_of_proof (Proof.Context (data, _)) = data;
   370 fun map_prf f (Proof.Context (data, thy)) = Proof.Context (f data, thy);
   371 
   372 
   373 (* proof data kinds *)
   374 
   375 local
   376 
   377 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
   378 
   379 fun invoke_init k =
   380   (case Datatab.lookup (Synchronized.value kinds) k of
   381     SOME init => init
   382   | NONE => raise Fail "Invalid proof data identifier");
   383 
   384 fun init_data thy =
   385   Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
   386 
   387 fun init_new_data data thy =
   388   Datatab.merge (K true) (data, init_data thy);
   389 
   390 in
   391 
   392 fun raw_transfer thy' (Proof.Context (data, thy)) =
   393   let
   394     val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
   395     val data' = init_new_data data thy';
   396   in Proof.Context (data', thy') end;
   397 
   398 structure Proof_Context =
   399 struct
   400   val theory_of = theory_of_proof;
   401   fun init_global thy = Proof.Context (init_data thy, thy);
   402   fun get_global thy name = init_global (get_theory thy name);
   403 end;
   404 
   405 structure Proof_Data =
   406 struct
   407 
   408 fun declare init =
   409   let
   410     val k = serial ();
   411     val _ = Synchronized.change kinds (Datatab.update (k, init));
   412   in k end;
   413 
   414 fun get k dest prf =
   415   (case Datatab.lookup (data_of_proof prf) k of
   416     SOME x => x
   417   | NONE => invoke_init k (Proof_Context.theory_of prf)) |> dest;  (*adhoc value for old theories*)
   418 
   419 fun put k mk x = map_prf (Datatab.update (k, mk x));
   420 
   421 end;
   422 
   423 end;
   424 
   425 
   426 
   427 (*** generic context ***)
   428 
   429 datatype generic = Theory of theory | Proof of Proof.context;
   430 
   431 fun cases f _ (Theory thy) = f thy
   432   | cases _ g (Proof prf) = g prf;
   433 
   434 fun mapping f g = cases (Theory o f) (Proof o g);
   435 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
   436 
   437 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
   438 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
   439 
   440 fun map_theory f = Theory o f o the_theory;
   441 fun map_proof f = Proof o f o the_proof;
   442 
   443 fun map_theory_result f = apsnd Theory o f o the_theory;
   444 fun map_proof_result f = apsnd Proof o f o the_proof;
   445 
   446 fun theory_map f = the_theory o f o Theory;
   447 fun proof_map f = the_proof o f o Proof;
   448 
   449 val theory_of = cases I Proof_Context.theory_of;
   450 val proof_of = cases Proof_Context.init_global I;
   451 
   452 
   453 (* pretty printing context *)
   454 
   455 exception PRETTY of generic;
   456 
   457 val pretty_generic = Pretty o PRETTY;
   458 val pretty = pretty_generic o Proof;
   459 val pretty_global = pretty_generic o Theory;
   460 
   461 fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   462 
   463 
   464 
   465 (** thread data **)
   466 
   467 local val tag = Universal.tag () : generic option Universal.tag in
   468 
   469 fun thread_data () =
   470   (case Thread.getLocal tag of
   471     SOME (SOME context) => SOME context
   472   | _ => NONE);
   473 
   474 fun the_thread_data () =
   475   (case thread_data () of
   476     SOME context => context
   477   | _ => error "Unknown context");
   478 
   479 fun set_thread_data context = Thread.setLocal (tag, context);
   480 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   481 
   482 end;
   483 
   484 fun >>> f =
   485   let
   486     val (res, context') = f (the_thread_data ());
   487     val _ = set_thread_data (SOME context');
   488   in res end;
   489 
   490 nonfix >>;
   491 fun >> f = >>> (fn context => ((), f context));
   492 
   493 val _ = set_thread_data (SOME (Theory pre_pure_thy));
   494 
   495 end;
   496 
   497 structure Basic_Context: BASIC_CONTEXT = Context;
   498 open Basic_Context;
   499 
   500 
   501 
   502 (*** type-safe interfaces for data declarations ***)
   503 
   504 (** theory data **)
   505 
   506 signature THEORY_DATA_PP_ARGS =
   507 sig
   508   type T
   509   val empty: T
   510   val extend: T -> T
   511   val merge: Context.pretty -> T * T -> T
   512 end;
   513 
   514 signature THEORY_DATA_ARGS =
   515 sig
   516   type T
   517   val empty: T
   518   val extend: T -> T
   519   val merge: T * T -> T
   520 end;
   521 
   522 signature THEORY_DATA =
   523 sig
   524   type T
   525   val get: theory -> T
   526   val put: T -> theory -> theory
   527   val map: (T -> T) -> theory -> theory
   528 end;
   529 
   530 functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
   531 struct
   532 
   533 type T = Data.T;
   534 exception Data of T;
   535 
   536 val kind =
   537   Context.Theory_Data.declare
   538     (Position.thread_data ())
   539     (Data Data.empty)
   540     (fn Data x => Data (Data.extend x))
   541     (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   542 
   543 val get = Context.Theory_Data.get kind (fn Data x => x);
   544 val put = Context.Theory_Data.put kind Data;
   545 fun map f thy = put (f (get thy)) thy;
   546 
   547 end;
   548 
   549 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   550   Theory_Data_PP
   551   (
   552     type T = Data.T;
   553     val empty = Data.empty;
   554     val extend = Data.extend;
   555     fun merge _ = Data.merge;
   556   );
   557 
   558 
   559 
   560 (** proof data **)
   561 
   562 signature PROOF_DATA_ARGS =
   563 sig
   564   type T
   565   val init: theory -> T
   566 end;
   567 
   568 signature PROOF_DATA =
   569 sig
   570   type T
   571   val get: Proof.context -> T
   572   val put: T -> Proof.context -> Proof.context
   573   val map: (T -> T) -> Proof.context -> Proof.context
   574 end;
   575 
   576 functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
   577 struct
   578 
   579 type T = Data.T;
   580 exception Data of T;
   581 
   582 val kind = Context.Proof_Data.declare (Data o Data.init);
   583 
   584 val get = Context.Proof_Data.get kind (fn Data x => x);
   585 val put = Context.Proof_Data.put kind Data;
   586 fun map f prf = put (f (get prf)) prf;
   587 
   588 end;
   589 
   590 
   591 
   592 (** generic data **)
   593 
   594 signature GENERIC_DATA_ARGS =
   595 sig
   596   type T
   597   val empty: T
   598   val extend: T -> T
   599   val merge: T * T -> T
   600 end;
   601 
   602 signature GENERIC_DATA =
   603 sig
   604   type T
   605   val get: Context.generic -> T
   606   val put: T -> Context.generic -> Context.generic
   607   val map: (T -> T) -> Context.generic -> Context.generic
   608 end;
   609 
   610 functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
   611 struct
   612 
   613 structure Thy_Data = Theory_Data(Data);
   614 structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
   615 
   616 type T = Data.T;
   617 
   618 fun get (Context.Theory thy) = Thy_Data.get thy
   619   | get (Context.Proof prf) = Prf_Data.get prf;
   620 
   621 fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
   622   | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
   623 
   624 fun map f ctxt = put (f (get ctxt)) ctxt;
   625 
   626 end;
   627 
   628 (*hide private interface*)
   629 structure Context: CONTEXT = Context;
   630