added type theory: generic theory contexts with unique identity,
authorwenzelm
Fri Jun 17 18:33:21 2005 +0200 (2005-06-17)
changeset 164367eb6b6cbd166
parent 16435 3b17850023f1
child 16437 aa87badf7a3c
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;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Fri Jun 17 18:33:20 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Fri Jun 17 18:33:21 2005 +0200
     1.3 @@ -2,11 +2,15 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Theory contexts.
     1.8 +Generic theory contexts with unique identity, arbitrarily typed data,
     1.9 +linear and graph development.  Implicit ML theory context.
    1.10  *)
    1.11  
    1.12  signature BASIC_CONTEXT =
    1.13  sig
    1.14 +  type theory
    1.15 +  type theory_ref
    1.16 +  exception THEORY of string * theory list
    1.17    val context: theory -> unit
    1.18    val the_context: unit -> theory
    1.19  end;
    1.20 @@ -14,6 +18,40 @@
    1.21  signature CONTEXT =
    1.22  sig
    1.23    include BASIC_CONTEXT
    1.24 +  (*theory context*)
    1.25 +  val parents_of: theory -> theory list
    1.26 +  val ancestors_of: theory -> theory list
    1.27 +  val is_stale: theory -> bool
    1.28 +  val ProtoPureN: string
    1.29 +  val PureN: string
    1.30 +  val CPureN: string
    1.31 +  val draftN: string
    1.32 +  val is_draft: theory -> bool
    1.33 +  val exists_name: string -> theory -> bool
    1.34 +  val names_of: theory -> string list
    1.35 +  val pretty_thy: theory -> Pretty.T
    1.36 +  val string_of_thy: theory -> string
    1.37 +  val pprint_thy: theory -> pprint_args -> unit
    1.38 +  val pretty_abbrev_thy: theory -> Pretty.T
    1.39 +  val str_of_thy: theory -> string
    1.40 +  val check_thy: string -> theory -> theory
    1.41 +  val eq_thy: theory * theory -> bool
    1.42 +  val subthy: theory * theory -> bool
    1.43 +  val self_ref: theory -> theory_ref
    1.44 +  val deref: theory_ref -> theory
    1.45 +  exception DATA_FAIL of exn * string
    1.46 +  val theory_data: theory -> string list
    1.47 +  val print_all_data: theory -> unit
    1.48 +  val copy_thy: theory -> theory
    1.49 +  val checkpoint_thy: theory -> theory
    1.50 +  val pre_pure: theory
    1.51 +  val merge: theory * theory -> theory                     (*exception TERM*)
    1.52 +  val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    1.53 +  val theory_name: theory -> string
    1.54 +  val begin_theory: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.55 +  val end_theory: theory -> theory
    1.56 +
    1.57 +  (*ML context*)
    1.58    val get_context: unit -> theory option
    1.59    val set_context: theory option -> unit
    1.60    val reset_context: unit -> unit
    1.61 @@ -30,11 +68,343 @@
    1.62    val setup: unit -> (theory -> theory) list
    1.63  end;
    1.64  
    1.65 -structure Context: CONTEXT =
    1.66 +signature PRIVATE_CONTEXT =
    1.67 +sig
    1.68 +  include CONTEXT
    1.69 +  structure TheoryData:
    1.70 +  sig
    1.71 +    val declare: string -> Object.T -> (Object.T -> Object.T) ->
    1.72 +      (Object.T -> Object.T) -> (Pretty.pp -> Object.T * Object.T -> Object.T) ->
    1.73 +      (theory -> Object.T -> unit) -> serial
    1.74 +    val init: serial -> theory -> theory
    1.75 +    val print: serial -> theory -> unit
    1.76 +    val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.77 +    val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.78 +  end;
    1.79 +end;
    1.80 +
    1.81 +structure Context: PRIVATE_CONTEXT =
    1.82  struct
    1.83  
    1.84 +(*** theory context ***)
    1.85  
    1.86 -(** implicit theory context in ML **)
    1.87 +datatype theory =
    1.88 +  Theory of
    1.89 +  (*identity*)
    1.90 +   {self: theory ref option,
    1.91 +    id: serial * string,
    1.92 +    ids: string Inttab.table} *
    1.93 +  (*data*)
    1.94 +  Object.T Inttab.table *
    1.95 +  (*history of linear development*)
    1.96 +   {name: string,
    1.97 +    version: int,
    1.98 +    intermediates: theory list} *
    1.99 +  (*ancestry of graph development*)
   1.100 +   {parents: theory list,
   1.101 +    ancestors: theory list};
   1.102 +
   1.103 +exception THEORY of string * theory list;
   1.104 +
   1.105 +fun rep_theory (Theory args) = args;
   1.106 +
   1.107 +val identity_of = #1 o rep_theory;
   1.108 +val data_of     = #2 o rep_theory;
   1.109 +val history_of  = #3 o rep_theory;
   1.110 +val ancestry_of = #4 o rep_theory;
   1.111 +
   1.112 +fun make_identity self id ids = {self = self, id = id, ids = ids};
   1.113 +fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
   1.114 +fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   1.115 +
   1.116 +val parents_of = #parents o ancestry_of;
   1.117 +val ancestors_of = #ancestors o ancestry_of;
   1.118 +
   1.119 +
   1.120 +
   1.121 +(** theory identity **)
   1.122 +
   1.123 +(* staleness *)
   1.124 +
   1.125 +fun eq_id ((i: int, _), (j, _)) = i = j;
   1.126 +
   1.127 +fun is_stale
   1.128 +    (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   1.129 +      not (eq_id (id, id'))
   1.130 +  | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
   1.131 +
   1.132 +fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   1.133 +  | vitalize (thy as Theory ({self = NONE, id, ids}, data, history, ancestry)) =
   1.134 +      let
   1.135 +        val r = ref thy;
   1.136 +        val thy' = Theory (make_identity (SOME r) id ids, data, history, ancestry);
   1.137 +      in r := thy'; thy' end;
   1.138 +
   1.139 +
   1.140 +(* names *)
   1.141 +
   1.142 +val ProtoPureN = "ProtoPure";
   1.143 +val PureN = "Pure";
   1.144 +val CPureN = "CPure";
   1.145 +
   1.146 +val draftN = "#";
   1.147 +fun draft_id (_, name) = (name = draftN);
   1.148 +val is_draft = draft_id o #id o identity_of;
   1.149 +
   1.150 +fun exists_name name (Theory ({id, ids, ...}, _, _, _)) =
   1.151 +  name = #2 id orelse Inttab.exists (equal name o #2) ids;
   1.152 +
   1.153 +fun names_of (Theory ({id, ids, ...}, _, _, _)) =
   1.154 +  map #2 (Inttab.dest ids @ [id]);
   1.155 +
   1.156 +fun pretty_thy thy =
   1.157 +  Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
   1.158 +
   1.159 +val string_of_thy = Pretty.string_of o pretty_thy;
   1.160 +val pprint_thy = Pretty.pprint o pretty_thy;
   1.161 +
   1.162 +fun pretty_abbrev_thy thy =
   1.163 +  let
   1.164 +    val names = names_of thy;
   1.165 +    val n = length names;
   1.166 +    val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   1.167 +  in Pretty.str_list "{" "}" abbrev end;
   1.168 +
   1.169 +val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   1.170 +
   1.171 +
   1.172 +(* consistency *)
   1.173 +
   1.174 +fun check_thy pos thy =
   1.175 +  if is_stale thy then
   1.176 +    raise TERM ("Stale theory encountered (see " ^ pos ^ "):\n" ^ string_of_thy thy, [])
   1.177 +  else thy;
   1.178 +
   1.179 +fun check_insert id ids =
   1.180 +  if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids
   1.181 +  else if Inttab.exists (equal (#2 id) o #2) ids then
   1.182 +    raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
   1.183 +  else Inttab.update (id, ids);
   1.184 +
   1.185 +fun check_merge thy1 thy2 =
   1.186 +  let
   1.187 +    val {id = id1, ids = ids1, ...} = identity_of thy1;
   1.188 +    val {id = id2, ids = ids2, ...} = identity_of thy2;
   1.189 +  in check_insert id2 (Inttab.fold check_insert ids2 (check_insert id1 ids1)) end;
   1.190 +
   1.191 +
   1.192 +(* equality and inclusion *)
   1.193 +
   1.194 +local
   1.195 +
   1.196 +fun exists_ids (Theory ({id, ids, ...}, _, _, _)) (i, _) =
   1.197 +  i = #1 id orelse is_some (Inttab.lookup (ids, i));
   1.198 +
   1.199 +fun member_ids (Theory ({id, ...}, _, _, _), thy) = exists_ids thy id;
   1.200 +
   1.201 +fun subset_ids (Theory ({id, ids, ...}, _, _, _), thy) =
   1.202 +  exists_ids thy id andalso Inttab.forall (exists_ids thy) ids;
   1.203 +
   1.204 +in
   1.205 +
   1.206 +val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy");
   1.207 +fun subthy thys = eq_thy thys orelse member_ids thys;
   1.208 +fun subthy_internal thys = eq_thy thys orelse subset_ids thys;
   1.209 +
   1.210 +end;
   1.211 +
   1.212 +
   1.213 +(* external references *)
   1.214 +
   1.215 +datatype theory_ref = TheoryRef of theory ref;
   1.216 +
   1.217 +val self_ref = TheoryRef o the o #self o identity_of o check_thy "Context.self_ref";
   1.218 +fun deref (TheoryRef (ref thy)) = thy;
   1.219 +
   1.220 +
   1.221 +
   1.222 +(** theory data **)
   1.223 +
   1.224 +(* data kinds and access methods *)
   1.225 +
   1.226 +exception DATA_FAIL of exn * string;
   1.227 +
   1.228 +local
   1.229 +
   1.230 +type kind =
   1.231 + {name: string,
   1.232 +  empty: Object.T,
   1.233 +  copy: Object.T -> Object.T,
   1.234 +  extend: Object.T -> Object.T,
   1.235 +  merge: Pretty.pp -> Object.T * Object.T -> Object.T,
   1.236 +  print: theory -> Object.T -> unit};
   1.237 +
   1.238 +val kinds = ref (Inttab.empty: kind Inttab.table);
   1.239 +
   1.240 +fun invoke meth_name meth_fn k =
   1.241 +  (case Inttab.lookup (! kinds, k) of
   1.242 +    SOME kind => meth_fn kind |> transform_failure (fn exn =>
   1.243 +      DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   1.244 +  | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   1.245 +
   1.246 +in
   1.247 +
   1.248 +fun invoke_name k    = invoke "name" (K o #name) k ();
   1.249 +fun invoke_empty k   = invoke "empty" (K o #empty) k ();
   1.250 +val invoke_copy      = invoke "copy" #copy;
   1.251 +val invoke_extend    = invoke "extend" #extend;
   1.252 +fun invoke_merge pp  = invoke "merge" (fn kind => #merge kind pp);
   1.253 +fun invoke_print thy = invoke "print" (fn kind => #print kind thy);
   1.254 +
   1.255 +fun declare name e cp ext mrg prt =
   1.256 +  let
   1.257 +    val k = serial ();
   1.258 +    val kind = {name = name, empty = e, copy = cp, extend = ext, merge = mrg, print = prt};
   1.259 +    val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   1.260 +      warning ("Duplicate declaration of theory data " ^ quote name));
   1.261 +    val _ = kinds := Inttab.update ((k, kind), ! kinds);
   1.262 +  in k end;
   1.263 +
   1.264 +val copy_data = Inttab.map' invoke_copy;
   1.265 +val extend_data = Inttab.map' invoke_extend;
   1.266 +fun merge_data pp = Inttab.join (SOME oo invoke_merge pp) o pairself extend_data;
   1.267 +
   1.268 +fun theory_data thy =
   1.269 +  map invoke_name (Inttab.keys (data_of thy))
   1.270 +  |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest
   1.271 +  |> map (apsnd length)
   1.272 +  |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
   1.273 +
   1.274 +fun print_all_data thy =
   1.275 +  List.app (uncurry (invoke_print thy)) (Inttab.dest (data_of thy));
   1.276 +
   1.277 +end;
   1.278 +
   1.279 +
   1.280 +
   1.281 +(** build theories **)
   1.282 +
   1.283 +(* primitives *)
   1.284 +
   1.285 +fun create_thy name self id ids data history ancestry =
   1.286 +  let
   1.287 +    val ids' = check_insert id ids;
   1.288 +    val id' = (serial (), name);
   1.289 +    val _ = check_insert id' ids';
   1.290 +    val identity' = make_identity self id' ids';
   1.291 +  in vitalize (Theory (identity', data, history, ancestry)) end;
   1.292 +
   1.293 +fun copy_thy (thy as Theory ({id, ids, ...}, data, history, ancestry)) =
   1.294 +  let val _ = check_thy "Context.copy_thy" thy;
   1.295 +  in create_thy draftN NONE id ids (copy_data data) history ancestry end;
   1.296 +
   1.297 +fun change_thy name f (thy as Theory ({self, id, ids}, data, history, ancestry)) =
   1.298 +  let
   1.299 +    val _ = check_thy "Context.change_thy" thy;
   1.300 +    val (self', data', ancestry') =
   1.301 +      if is_draft thy then (self, data, ancestry)
   1.302 +      else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
   1.303 +  in create_thy name self' id ids (f data') history ancestry' end;
   1.304 +
   1.305 +fun name_thy name = change_thy name I;
   1.306 +val map_thy = change_thy draftN;
   1.307 +val extend_thy = map_thy I;
   1.308 +
   1.309 +fun checkpoint_thy thy =
   1.310 +  if not (is_draft thy) then thy
   1.311 +  else
   1.312 +    let
   1.313 +      val {name, version, intermediates} = history_of thy;
   1.314 +      val thy' as Theory (identity', data', _, ancestry') =
   1.315 +        name_thy (name ^ ":" ^ string_of_int version) thy;
   1.316 +      val history' = make_history name (version + 1) (thy' :: intermediates);
   1.317 +    in vitalize (Theory (identity', data', history', ancestry')) end;
   1.318 +
   1.319 +
   1.320 +(* theory data *)
   1.321 +
   1.322 +structure TheoryData =
   1.323 +struct
   1.324 +
   1.325 +val declare = declare;
   1.326 +
   1.327 +fun get k dest thy =
   1.328 +  (case Inttab.lookup (data_of thy, k) of
   1.329 +    SOME x => (dest x handle Match =>
   1.330 +      error ("Failed to access theory data " ^ quote (invoke_name k)))
   1.331 +  | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   1.332 +
   1.333 +fun print k thy = invoke_print thy k (get k I thy);
   1.334 +fun put k mk x = map_thy (curry Inttab.update (k, mk x));
   1.335 +fun init k = put k I (invoke_empty k);
   1.336 +
   1.337 +end;
   1.338 +
   1.339 +
   1.340 +(* pre_pure *)
   1.341 +
   1.342 +val pre_pure = create_thy draftN NONE (serial (), draftN) Inttab.empty
   1.343 +  Inttab.empty (make_history ProtoPureN 0 []) (make_ancestry [] []);
   1.344 +
   1.345 +
   1.346 +(* trivial merge *)
   1.347 +
   1.348 +fun merge (thy1, thy2) =
   1.349 +  if subthy (thy2, thy1) then thy1
   1.350 +  else if subthy (thy1, thy2) then thy2
   1.351 +  else (check_merge thy1 thy2;
   1.352 +    raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:",
   1.353 +      str_of_thy thy1, str_of_thy thy2], []));
   1.354 +
   1.355 +fun merge_refs (ref1, ref2) = self_ref (merge (deref ref1, deref ref2));
   1.356 +
   1.357 +
   1.358 +(* non-trivial merge *)
   1.359 +
   1.360 +fun merge_internal pp (thy1, thy2) =
   1.361 +  if subthy_internal (thy2, thy1) then thy1
   1.362 +  else if subthy_internal (thy1, thy2) then thy2
   1.363 +  else if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   1.364 +    error "Cannot merge Pure and CPure developments"
   1.365 +  else
   1.366 +    let
   1.367 +      val ids = check_merge thy1 thy2;
   1.368 +      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   1.369 +      val history = make_history "" 0 [];
   1.370 +      val ancestry = make_ancestry [] [];
   1.371 +    in create_thy draftN NONE (serial (), draftN) ids data history ancestry end;
   1.372 +
   1.373 +
   1.374 +(* named theory nodes *)
   1.375 +
   1.376 +val theory_name = #name o history_of;
   1.377 +
   1.378 +fun begin_theory pp name imports =
   1.379 +  if name = draftN then
   1.380 +    error ("Illegal theory name: " ^ quote draftN)
   1.381 +  else if exists is_draft imports then
   1.382 +    error "Attempt to import draft theories"
   1.383 +  else
   1.384 +    let
   1.385 +      val parents = gen_distinct eq_thy imports;
   1.386 +      val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents));
   1.387 +      val Theory ({id, ids, ...}, data, _, _) =
   1.388 +        (case parents of
   1.389 +          [] => error "No parent theories"
   1.390 +        | thy :: thys => extend_thy (Library.foldl (merge_internal pp) (thy, thys)));
   1.391 +      val history = make_history name 0 [];
   1.392 +      val ancestry = make_ancestry parents ancestors;
   1.393 +    in create_thy draftN NONE id ids data history ancestry end;
   1.394 +
   1.395 +fun end_theory thy =
   1.396 +  thy
   1.397 +(*|> purge_thy  FIXME *)
   1.398 +  |> name_thy (theory_name thy);
   1.399 +
   1.400 +
   1.401 +
   1.402 +
   1.403 +(*** ML theory context ***)
   1.404  
   1.405  local
   1.406    val current_theory = ref (NONE: theory option);
   1.407 @@ -71,7 +441,7 @@
   1.408  
   1.409  (* use ML text *)
   1.410  
   1.411 -val ml_output = (writeln, error_msg: string -> unit);
   1.412 +val ml_output = (writeln, error_msg);
   1.413  
   1.414  fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
   1.415  
   1.416 @@ -84,8 +454,7 @@
   1.417    use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   1.418  
   1.419  
   1.420 -
   1.421 -(** delayed theory setup **)
   1.422 +(* delayed theory setup *)
   1.423  
   1.424  local
   1.425    val setup_fns = ref ([]: (theory -> theory) list);
   1.426 @@ -94,8 +463,59 @@
   1.427    fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
   1.428  end;
   1.429  
   1.430 -
   1.431  end;
   1.432  
   1.433  structure BasicContext: BASIC_CONTEXT = Context;
   1.434  open BasicContext;
   1.435 +
   1.436 +
   1.437 +
   1.438 +(*** type-safe interface for theory data ***)
   1.439 +
   1.440 +signature THEORY_DATA_ARGS =
   1.441 +sig
   1.442 +  val name: string
   1.443 +  type T
   1.444 +  val empty: T
   1.445 +  val copy: T -> T
   1.446 +  val extend: T -> T
   1.447 +  val merge: Pretty.pp -> T * T -> T
   1.448 +  val print: theory -> T -> unit
   1.449 +end;
   1.450 +
   1.451 +signature THEORY_DATA =
   1.452 +sig
   1.453 +  type T
   1.454 +  val init: theory -> theory
   1.455 +  val print: theory -> unit
   1.456 +  val get: theory -> T
   1.457 +  val put: T -> theory -> theory
   1.458 +  val map: (T -> T) -> theory -> theory
   1.459 +end;
   1.460 +
   1.461 +functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
   1.462 +struct
   1.463 +
   1.464 +structure TheoryData = Context.TheoryData;
   1.465 +
   1.466 +type T = Data.T;
   1.467 +exception Data of T;
   1.468 +
   1.469 +val kind = TheoryData.declare Data.name
   1.470 +  (Data Data.empty)
   1.471 +  (fn Data x => Data (Data.copy x))
   1.472 +  (fn Data x => Data (Data.extend x))
   1.473 +  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
   1.474 +  (fn thy => fn Data x => Data.print thy x);
   1.475 +
   1.476 +val init = TheoryData.init kind;
   1.477 +val print = TheoryData.print kind;
   1.478 +val get = TheoryData.get kind (fn Data x => x);
   1.479 +val get_sg = get;    (*obsolete*)
   1.480 +val put = TheoryData.put kind Data;
   1.481 +fun map f thy = put (f (get thy)) thy;
   1.482 +
   1.483 +end;
   1.484 +
   1.485 +(*hide private interface!*)
   1.486 +structure Context: CONTEXT = Context;