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