src/Pure/context.ML
author wenzelm
Mon Jun 20 22:14:03 2005 +0200 (2005-06-20)
changeset 16489 f66ab8a4e98f
parent 16436 7eb6b6cbd166
child 16533 f1152f75f6fc
permissions -rw-r--r--
improved treatment of intermediate checkpoints: actual copy
instead of extend, purge after end;
tuned;
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Generic theory contexts with unique identity, arbitrarily typed data,
     6 graph-based development.  Implicit theory context in ML.
     7 *)
     8 
     9 signature BASIC_CONTEXT =
    10 sig
    11   type theory
    12   type theory_ref
    13   exception THEORY of string * theory list
    14   val context: theory -> unit
    15   val the_context: unit -> theory
    16 end;
    17 
    18 signature CONTEXT =
    19 sig
    20   include BASIC_CONTEXT
    21   exception DATA_FAIL of exn * string
    22   (*theory context*)
    23   val theory_name: theory -> string
    24   val parents_of: theory -> theory list
    25   val ancestors_of: theory -> theory list
    26   val is_stale: theory -> bool
    27   val ProtoPureN: string
    28   val PureN: string
    29   val CPureN: string
    30   val draftN: string
    31   val exists_name: string -> theory -> bool
    32   val names_of: theory -> string list
    33   val pretty_thy: theory -> Pretty.T
    34   val string_of_thy: theory -> string
    35   val pprint_thy: theory -> pprint_args -> unit
    36   val pretty_abbrev_thy: theory -> Pretty.T
    37   val str_of_thy: theory -> string
    38   val check_thy: string -> theory -> theory
    39   val eq_thy: theory * theory -> bool
    40   val subthy: theory * theory -> bool
    41   val merge: theory * theory -> theory                     (*exception TERM*)
    42   val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    43   val self_ref: theory -> theory_ref
    44   val deref: theory_ref -> theory
    45   val copy_thy: theory -> theory
    46   val checkpoint_thy: theory -> theory
    47   val finish_thy: theory -> theory
    48   val theory_data: theory -> string list
    49   val pre_pure_thy: theory
    50   val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    51   (*ML theory context*)
    52   val get_context: unit -> theory option
    53   val set_context: theory option -> unit
    54   val reset_context: unit -> unit
    55   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
    56   val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    57   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    58   val save: ('a -> 'b) -> 'a -> 'b
    59   val >> : (theory -> theory) -> unit
    60   val ml_output: (string -> unit) * (string -> unit)
    61   val use_mltext: string -> bool -> theory option -> unit
    62   val use_mltext_theory: string -> bool -> theory -> theory
    63   val use_let: string -> string -> string -> theory -> theory
    64   val add_setup: (theory -> theory) list -> unit
    65   val setup: unit -> (theory -> theory) list
    66 end;
    67 
    68 signature PRIVATE_CONTEXT =
    69 sig
    70   include CONTEXT
    71   structure TheoryData:
    72   sig
    73     val declare: string -> Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
    74       (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    75     val init: serial -> theory -> theory
    76     val get: serial -> (Object.T -> 'a) -> theory -> 'a
    77     val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    78   end
    79 end;
    80 
    81 structure Context: PRIVATE_CONTEXT =
    82 struct
    83 
    84 (*** theory context ***)
    85 
    86 (** theory data **)
    87 
    88 (* data kinds and access methods *)
    89 
    90 exception DATA_FAIL of exn * string;
    91 
    92 local
    93 
    94 type kind =
    95  {name: string,
    96   empty: Object.T,
    97   copy: Object.T -> Object.T,
    98   extend: Object.T -> Object.T,
    99   merge: Pretty.pp -> Object.T * Object.T -> Object.T};
   100 
   101 val kinds = ref (Inttab.empty: kind Inttab.table);
   102 
   103 fun invoke meth_name meth_fn k =
   104   (case Inttab.lookup (! kinds, k) of
   105     SOME kind => meth_fn kind |> transform_failure (fn exn =>
   106       DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   107   | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   108 
   109 in
   110 
   111 fun invoke_name k    = invoke "name" (K o #name) k ();
   112 fun invoke_empty k   = invoke "empty" (K o #empty) k ();
   113 val invoke_copy      = invoke "copy" #copy;
   114 val invoke_extend    = invoke "extend" #extend;
   115 fun invoke_merge pp  = invoke "merge" (fn kind => #merge kind pp);
   116 
   117 fun declare_theory_data name e cp ext mrg =
   118   let
   119     val k = serial ();
   120     val kind = {name = name, empty = e, copy = cp, extend = ext, merge = mrg};
   121     val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   122       warning ("Duplicate declaration of theory data " ^ quote name));
   123     val _ = kinds := Inttab.update ((k, kind), ! kinds);
   124   in k end;
   125 
   126 val copy_data = Inttab.map' invoke_copy;
   127 val extend_data = Inttab.map' invoke_extend;
   128 fun merge_data pp = Inttab.join (SOME oo invoke_merge pp) o pairself extend_data;
   129 
   130 end;
   131 
   132 
   133 
   134 (** datatype theory **)
   135 
   136 datatype theory =
   137   Theory of
   138   (*identity*)
   139    {self: theory ref option,            (*dynamic self reference -- follows theory changes*)
   140     id: serial * string,                (*identifier of this theory*)
   141     ids: string Inttab.table,           (*identifiers of ancestors*)
   142     iids: string Inttab.table} *        (*identifiers of intermediate checkpoints*)
   143   (*data*)
   144   Object.T Inttab.table *               (*record of arbitrarily typed data*)
   145   (*ancestry of graph development*)
   146    {parents: theory list,               (*immediate predecessors*)
   147     ancestors: theory list} *           (*all predecessors*)
   148   (*history of linear development*)
   149    {name: string,                       (*prospective name of finished theory*)
   150     version: int,                       (*checkpoint counter*)
   151     intermediates: theory list};        (*intermediate checkpoints*)
   152 
   153 exception THEORY of string * theory list;
   154 
   155 fun rep_theory (Theory args) = args;
   156 
   157 val identity_of = #1 o rep_theory;
   158 val data_of     = #2 o rep_theory;
   159 val ancestry_of = #3 o rep_theory;
   160 val history_of  = #4 o rep_theory;
   161 
   162 fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
   163 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   164 fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
   165 
   166 val parents_of = #parents o ancestry_of;
   167 val ancestors_of = #ancestors o ancestry_of;
   168 val theory_name = #name o history_of;
   169 
   170 
   171 (* staleness *)
   172 
   173 fun eq_id ((i: int, _), (j, _)) = i = j;
   174 
   175 fun is_stale
   176     (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   177       not (eq_id (id, id'))
   178   | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
   179 
   180 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   181   | vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) =
   182       let
   183         val r = ref thy;
   184         val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history);
   185       in r := thy'; thy' end;
   186 
   187 
   188 (* names *)
   189 
   190 val ProtoPureN = "ProtoPure";
   191 val PureN = "Pure";
   192 val CPureN = "CPure";
   193 
   194 val draftN = "#";
   195 fun draft_id (_, name) = (name = draftN);
   196 val is_draft = draft_id o #id o identity_of;
   197 
   198 fun exists_name name (Theory ({id, ids, iids, ...}, _, _, _)) =
   199   name = #2 id orelse
   200   Inttab.exists (equal name o #2) ids orelse
   201   Inttab.exists (equal name o #2) iids;
   202 
   203 fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) =
   204   rev (#2 id :: Inttab.fold (cons o #2) iids (Inttab.fold (cons o #2) ids []));
   205 
   206 fun pretty_thy thy =
   207   Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
   208 
   209 val string_of_thy = Pretty.string_of o pretty_thy;
   210 val pprint_thy = Pretty.pprint o pretty_thy;
   211 
   212 fun pretty_abbrev_thy thy =
   213   let
   214     val names = names_of thy;
   215     val n = length names;
   216     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   217   in Pretty.str_list "{" "}" abbrev end;
   218 
   219 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   220 
   221 
   222 (* consistency *)
   223 
   224 fun check_thy pos thy =
   225   if is_stale thy then
   226     raise TERM ("Stale theory encountered (in " ^ pos ^ "):\n" ^ string_of_thy thy, [])
   227   else thy;
   228 
   229 fun check_ins id ids =
   230   if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids
   231   else if Inttab.exists (equal (#2 id) o #2) ids then
   232     raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
   233   else Inttab.update (id, ids);
   234 
   235 fun check_insert intermediate id (ids, iids) =
   236   let val ids' = check_ins id ids and iids' = check_ins id iids
   237   in if intermediate then (ids, iids') else (ids', iids) end;
   238 
   239 fun check_merge
   240     (Theory ({id = id1, ids = ids1, iids = iids1, ...}, _, _, history1))
   241     (Theory ({id = id2, ids = ids2, iids = iids2, ...}, _, _, history2)) =
   242   (Inttab.fold check_ins ids2 ids1, Inttab.fold check_ins iids2 iids1)
   243   |> check_insert (#version history1 > 0) id1
   244   |> check_insert (#version history2 > 0) id2;
   245 
   246 
   247 (* theory references *)
   248 
   249 (*theory_ref provides a safe way to store dynamic references to a
   250   theory -- a plain theory value would become stale as the self
   251   reference moves on*)
   252 
   253 datatype theory_ref = TheoryRef of theory ref;
   254 
   255 val self_ref = TheoryRef o the o #self o identity_of o check_thy "Context.self_ref";
   256 fun deref (TheoryRef (ref thy)) = thy;
   257 
   258 
   259 (* equality and inclusion *)  (* FIXME proper_subthy; no subthy_internal *)
   260 
   261 local
   262 
   263 fun exists_ids (Theory ({id, ids, iids, ...}, _, _, _)) (i, _) =
   264   i = #1 id orelse
   265   is_some (Inttab.lookup (ids, i)) orelse
   266   is_some (Inttab.lookup (iids, i));
   267 
   268 fun member_ids (Theory ({id, ...}, _, _, _), thy) = exists_ids thy id;
   269 
   270 fun subset_ids (Theory ({id, ids, iids, ...}, _, _, _), thy) =
   271   exists_ids thy id andalso
   272   Inttab.forall (exists_ids thy) ids andalso
   273   Inttab.forall (exists_ids thy) iids;
   274 
   275 in
   276 
   277 val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy");
   278 fun subthy thys = eq_thy thys orelse member_ids thys;
   279 fun subthy_internal thys = eq_thy thys orelse subset_ids thys;
   280 
   281 end;
   282 
   283 
   284 (* trivial merge *)
   285 
   286 fun merge (thy1, thy2) =
   287   if subthy (thy2, thy1) then thy1
   288   else if subthy (thy1, thy2) then thy2
   289   else (check_merge thy1 thy2;
   290     raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:",
   291       str_of_thy thy1, str_of_thy thy2], []));
   292 
   293 fun merge_refs (ref1, ref2) = self_ref (merge (deref ref1, deref ref2));
   294 
   295 
   296 
   297 (** build theories **)
   298 
   299 (* primitives *)
   300 
   301 fun create_thy name self id ids iids data ancestry history =
   302   let
   303     val intermediate = #version history > 0;
   304     val (ids', iids') = check_insert intermediate id (ids, iids);
   305     val id' = (serial (), name);
   306     val _ = check_insert intermediate id' (ids', iids');
   307     val identity' = make_identity self id' ids' iids';
   308   in vitalize (Theory (identity', data, ancestry, history)) end;
   309 
   310 fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) =
   311   let
   312     val _ = check_thy "Context.change_thy" thy;
   313     val (self', data', ancestry') =
   314       if is_draft thy then (self, data, ancestry)    (*destructive change!*)
   315       else if #version history > 0
   316       then (NONE, copy_data data, ancestry)
   317       else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
   318     val data'' = f data';
   319   in create_thy name self' id ids iids data'' ancestry' history end;
   320 
   321 fun name_thy name = change_thy name I;
   322 val modify_thy = change_thy draftN;
   323 val extend_thy = modify_thy I;
   324 
   325 fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
   326   (check_thy "Context.copy_thy" thy;
   327     create_thy draftN NONE id ids iids (copy_data data) ancestry history);
   328 
   329 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   330   Inttab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
   331 
   332 
   333 (* named theory nodes *)
   334 
   335 fun merge_thys pp (thy1, thy2) =
   336   if subthy_internal (thy2, thy1) then thy1
   337   else if subthy_internal (thy1, thy2) then thy2
   338   else if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   339     error "Cannot merge Pure and CPure developments"
   340   else
   341     let
   342       val (ids, iids) = check_merge thy1 thy2;
   343       val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   344       val ancestry = make_ancestry [] [];
   345       val history = make_history "" 0 [];
   346     in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   347 
   348 fun begin_thy pp name imports =
   349   if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   350   else
   351     let
   352       val parents = gen_distinct eq_thy imports;  (* FIXME maximals *)
   353       val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents));
   354       val Theory ({id, ids, iids, ...}, data, _, _) =
   355         (case parents of
   356           [] => error "No parent theories"
   357         | thy :: thys => extend_thy (Library.foldl (merge_thys pp) (thy, thys)));
   358       val ancestry = make_ancestry parents ancestors;
   359       val history = make_history name 0 [];
   360     in create_thy draftN NONE id ids iids data ancestry history end;
   361 
   362 
   363 (* undoable checkpoints *)
   364 
   365 fun checkpoint_thy thy =
   366   if not (is_draft thy) then thy
   367   else
   368     let
   369       val {name, version, intermediates} = history_of thy;
   370       val thy' as Theory (identity', data', ancestry', _) =
   371         name_thy (name ^ ":" ^ string_of_int version) thy;
   372       val history' = make_history name (version + 1) (thy' :: intermediates);
   373     in vitalize (Theory (identity', data', ancestry', history')) end;
   374 
   375 fun finish_thy thy =
   376   let
   377     val {name, version, intermediates} = history_of thy;
   378     val rs = map (the o #self o identity_of o check_thy "Context.finish_thy") intermediates;
   379     val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
   380     val identity' = make_identity self id ids Inttab.empty;
   381     val history' = make_history name 0 [];
   382     val thy'' = vitalize (Theory (identity', data', ancestry', history'));
   383   in List.app (fn r => r := thy'') rs; thy'' end;
   384 
   385 
   386 (* theory data *)
   387 
   388 fun theory_data thy =
   389   map invoke_name (Inttab.keys (data_of thy))
   390   |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest
   391   |> map (apsnd length)
   392   |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
   393 
   394 structure TheoryData =
   395 struct
   396 
   397 val declare = declare_theory_data;
   398 
   399 fun get k dest thy =
   400   (case Inttab.lookup (data_of thy, k) of
   401     SOME x => (dest x handle Match =>
   402       error ("Failed to access theory data " ^ quote (invoke_name k)))
   403   | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   404 
   405 fun put k mk x = modify_thy (curry Inttab.update (k, mk x));
   406 fun init k = put k I (invoke_empty k);
   407 
   408 end;
   409 
   410 
   411 
   412 (** ML theory context **)
   413 
   414 local
   415   val current_theory = ref (NONE: theory option);
   416 in
   417   fun get_context () = ! current_theory;
   418   fun set_context opt_thy = current_theory := opt_thy;
   419   fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
   420 end;
   421 
   422 fun the_context () =
   423   (case get_context () of
   424     SOME thy => thy
   425   | _ => error "Unknown theory context");
   426 
   427 fun context thy = set_context (SOME thy);
   428 fun reset_context () = set_context NONE;
   429 
   430 fun pass opt_thy f x =
   431   setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
   432 
   433 fun pass_theory thy f x =
   434   (case pass (SOME thy) f x of
   435     (y, SOME thy') => (y, thy')
   436   | (_, NONE) => error "Lost theory context in ML");
   437 
   438 fun save f x = setmp (get_context ()) f x;
   439 
   440 
   441 (* map context *)
   442 
   443 nonfix >>;
   444 fun >> f = set_context (SOME (f (the_context ())));
   445 
   446 
   447 (* use ML text *)
   448 
   449 val ml_output = (writeln, error_msg);
   450 
   451 fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
   452 
   453 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
   454 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
   455 
   456 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
   457 
   458 fun use_let bind body txt =
   459   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   460 
   461 
   462 (* delayed theory setup *)
   463 
   464 local
   465   val setup_fns = ref ([]: (theory -> theory) list);
   466 in
   467   fun add_setup fns = setup_fns := ! setup_fns @ fns;
   468   fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
   469 end;
   470 
   471 end;
   472 
   473 structure BasicContext: BASIC_CONTEXT = Context;
   474 open BasicContext;
   475 
   476 
   477 
   478 (*** type-safe interface for theory data ***)
   479 
   480 signature THEORY_DATA_ARGS =
   481 sig
   482   val name: string
   483   type T
   484   val empty: T
   485   val copy: T -> T
   486   val extend: T -> T
   487   val merge: Pretty.pp -> T * T -> T
   488   val print: theory -> T -> unit
   489 end;
   490 
   491 signature THEORY_DATA =
   492 sig
   493   type T
   494   val init: theory -> theory
   495   val print: theory -> unit
   496   val get: theory -> T
   497   val get_sg: theory -> T    (*obsolete*)
   498   val put: T -> theory -> theory
   499   val map: (T -> T) -> theory -> theory
   500 end;
   501 
   502 functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
   503 struct
   504 
   505 structure TheoryData = Context.TheoryData;
   506 
   507 type T = Data.T;
   508 exception Data of T;
   509 
   510 val kind = TheoryData.declare Data.name
   511   (Data Data.empty)
   512   (fn Data x => Data (Data.copy x))
   513   (fn Data x => Data (Data.extend x))
   514   (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   515 
   516 val init = TheoryData.init kind;
   517 val get = TheoryData.get kind (fn Data x => x);
   518 val get_sg = get;
   519 fun print thy = Data.print thy (get thy);
   520 val put = TheoryData.put kind Data;
   521 fun map f thy = put (f (get thy)) thy;
   522 
   523 end;
   524 
   525 (*hide private interface!*)
   526 structure Context: CONTEXT = Context;