src/Pure/context.ML
author wenzelm
Fri Jul 17 21:40:47 2015 +0200 (2015-07-17)
changeset 60749 f727b99faaf7
parent 59163 857a600f0c94
child 60947 d5f7b424ba47
permissions -rw-r--r--
skeleton for interactive debugger;
     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 apply2 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 apply2 (#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 
   369 (* proof data kinds *)
   370 
   371 local
   372 
   373 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
   374 
   375 fun init_data thy =
   376   Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy);
   377 
   378 fun init_new_data thy =
   379   Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data =>
   380     if Datatab.defined data k then data
   381     else Datatab.update (k, init thy) data);
   382 
   383 fun init_fallback k thy =
   384   (case Datatab.lookup (Synchronized.value kinds) k of
   385     SOME init => init thy
   386   | NONE => raise Fail "Invalid proof data identifier");
   387 
   388 in
   389 
   390 fun raw_transfer thy' (Proof.Context (data, thy)) =
   391   let
   392     val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
   393     val data' = init_new_data thy' data;
   394   in Proof.Context (data', thy') end;
   395 
   396 structure Proof_Context =
   397 struct
   398   fun theory_of (Proof.Context (_, thy)) = thy;
   399   fun init_global thy = Proof.Context (init_data thy, thy);
   400   fun get_global thy name = init_global (get_theory thy name);
   401 end;
   402 
   403 structure Proof_Data =
   404 struct
   405 
   406 fun declare init =
   407   let
   408     val k = serial ();
   409     val _ = Synchronized.change kinds (Datatab.update (k, init));
   410   in k end;
   411 
   412 fun get k dest (Proof.Context (data, thy)) =
   413   (case Datatab.lookup data k of
   414     SOME x => x
   415   | NONE => init_fallback k thy) |> dest;
   416 
   417 fun put k mk x (Proof.Context (data, thy)) =
   418   Proof.Context (Datatab.update (k, mk x) data, thy);
   419 
   420 end;
   421 
   422 end;
   423 
   424 
   425 
   426 (*** generic context ***)
   427 
   428 datatype generic = Theory of theory | Proof of Proof.context;
   429 
   430 fun cases f _ (Theory thy) = f thy
   431   | cases _ g (Proof prf) = g prf;
   432 
   433 fun mapping f g = cases (Theory o f) (Proof o g);
   434 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
   435 
   436 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
   437 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
   438 
   439 fun map_theory f = Theory o f o the_theory;
   440 fun map_proof f = Proof o f o the_proof;
   441 
   442 fun map_theory_result f = apsnd Theory o f o the_theory;
   443 fun map_proof_result f = apsnd Proof o f o the_proof;
   444 
   445 fun theory_map f = the_theory o f o Theory;
   446 fun proof_map f = the_proof o f o Proof;
   447 
   448 val theory_of = cases I Proof_Context.theory_of;
   449 val proof_of = cases Proof_Context.init_global I;
   450 
   451 
   452 (* pretty printing context *)
   453 
   454 exception PRETTY of generic;
   455 
   456 val pretty_generic = Pretty o PRETTY;
   457 val pretty = pretty_generic o Proof;
   458 val pretty_global = pretty_generic o Theory;
   459 
   460 fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   461 
   462 
   463 
   464 (** thread data **)
   465 
   466 local val tag = Universal.tag () : generic option Universal.tag in
   467 
   468 fun thread_data () =
   469   (case Thread.getLocal tag of
   470     SOME (SOME context) => SOME context
   471   | _ => NONE);
   472 
   473 fun the_thread_data () =
   474   (case thread_data () of
   475     SOME context => context
   476   | _ => error "Unknown context");
   477 
   478 fun set_thread_data context = Thread.setLocal (tag, context);
   479 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   480 
   481 end;
   482 
   483 fun >>> f =
   484   let
   485     val (res, context') = f (the_thread_data ());
   486     val _ = set_thread_data (SOME context');
   487   in res end;
   488 
   489 nonfix >>;
   490 fun >> f = >>> (fn context => ((), f context));
   491 
   492 val _ = set_thread_data (SOME (Theory pre_pure_thy));
   493 
   494 end;
   495 
   496 structure Basic_Context: BASIC_CONTEXT = Context;
   497 open Basic_Context;
   498 
   499 
   500 
   501 (*** type-safe interfaces for data declarations ***)
   502 
   503 (** theory data **)
   504 
   505 signature THEORY_DATA_PP_ARGS =
   506 sig
   507   type T
   508   val empty: T
   509   val extend: T -> T
   510   val merge: Context.pretty -> T * T -> T
   511 end;
   512 
   513 signature THEORY_DATA_ARGS =
   514 sig
   515   type T
   516   val empty: T
   517   val extend: T -> T
   518   val merge: T * T -> T
   519 end;
   520 
   521 signature THEORY_DATA =
   522 sig
   523   type T
   524   val get: theory -> T
   525   val put: T -> theory -> theory
   526   val map: (T -> T) -> theory -> theory
   527 end;
   528 
   529 functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
   530 struct
   531 
   532 type T = Data.T;
   533 exception Data of T;
   534 
   535 val kind =
   536   Context.Theory_Data.declare
   537     (Position.thread_data ())
   538     (Data Data.empty)
   539     (fn Data x => Data (Data.extend x))
   540     (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   541 
   542 val get = Context.Theory_Data.get kind (fn Data x => x);
   543 val put = Context.Theory_Data.put kind Data;
   544 fun map f thy = put (f (get thy)) thy;
   545 
   546 end;
   547 
   548 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   549   Theory_Data_PP
   550   (
   551     type T = Data.T;
   552     val empty = Data.empty;
   553     val extend = Data.extend;
   554     fun merge _ = Data.merge;
   555   );
   556 
   557 
   558 
   559 (** proof data **)
   560 
   561 signature PROOF_DATA_ARGS =
   562 sig
   563   type T
   564   val init: theory -> T
   565 end;
   566 
   567 signature PROOF_DATA =
   568 sig
   569   type T
   570   val get: Proof.context -> T
   571   val put: T -> Proof.context -> Proof.context
   572   val map: (T -> T) -> Proof.context -> Proof.context
   573 end;
   574 
   575 functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
   576 struct
   577 
   578 type T = Data.T;
   579 exception Data of T;
   580 
   581 val kind = Context.Proof_Data.declare (Data o Data.init);
   582 
   583 val get = Context.Proof_Data.get kind (fn Data x => x);
   584 val put = Context.Proof_Data.put kind Data;
   585 fun map f prf = put (f (get prf)) prf;
   586 
   587 end;
   588 
   589 
   590 
   591 (** generic data **)
   592 
   593 signature GENERIC_DATA_ARGS =
   594 sig
   595   type T
   596   val empty: T
   597   val extend: T -> T
   598   val merge: T * T -> T
   599 end;
   600 
   601 signature GENERIC_DATA =
   602 sig
   603   type T
   604   val get: Context.generic -> T
   605   val put: T -> Context.generic -> Context.generic
   606   val map: (T -> T) -> Context.generic -> Context.generic
   607 end;
   608 
   609 functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
   610 struct
   611 
   612 structure Thy_Data = Theory_Data(Data);
   613 structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
   614 
   615 type T = Data.T;
   616 
   617 fun get (Context.Theory thy) = Thy_Data.get thy
   618   | get (Context.Proof prf) = Prf_Data.get prf;
   619 
   620 fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
   621   | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
   622 
   623 fun map f ctxt = put (f (get ctxt)) ctxt;
   624 
   625 end;
   626 
   627 (*hide private interface*)
   628 structure Context: CONTEXT = Context;
   629