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