begin_thy: merge maximal imports;
authorwenzelm
Wed Jun 22 19:41:18 2005 +0200 (2005-06-22)
changeset 16533f1152f75f6fc
parent 16532 e248ffc956c7
child 16534 95460b6eb712
begin_thy: merge maximal imports;
incorporate proof data;
added generic context;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Jun 22 19:41:17 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jun 22 19:41:18 2005 +0200
     1.3 @@ -3,7 +3,8 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Generic theory contexts with unique identity, arbitrarily typed data,
     1.7 -graph-based development.  Implicit theory context in ML.
     1.8 +development graph and history support.  Implicit theory contexts in ML.
     1.9 +Generic proof contexts with arbitrarily typed data.
    1.10  *)
    1.11  
    1.12  signature BASIC_CONTEXT =
    1.13 @@ -45,7 +46,7 @@
    1.14    val copy_thy: theory -> theory
    1.15    val checkpoint_thy: theory -> theory
    1.16    val finish_thy: theory -> theory
    1.17 -  val theory_data: theory -> string list
    1.18 +  val theory_data_of: theory -> string list
    1.19    val pre_pure_thy: theory
    1.20    val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.21    (*ML theory context*)
    1.22 @@ -63,6 +64,15 @@
    1.23    val use_let: string -> string -> string -> theory -> theory
    1.24    val add_setup: (theory -> theory) list -> unit
    1.25    val setup: unit -> (theory -> theory) list
    1.26 +  (*proof context*)
    1.27 +  type proof
    1.28 +  val theory_of_proof: proof -> theory
    1.29 +  val init_proof: theory -> proof
    1.30 +  val proof_data_of: theory -> string list
    1.31 +  (*generic context*)
    1.32 +  datatype context = Theory of theory | Proof of proof
    1.33 +  val theory_of: context -> theory
    1.34 +  val proof_of: context -> proof
    1.35  end;
    1.36  
    1.37  signature PRIVATE_CONTEXT =
    1.38 @@ -76,6 +86,13 @@
    1.39      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.40      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.41    end
    1.42 +  structure ProofData:
    1.43 +  sig
    1.44 +    val declare: string -> (theory -> Object.T) -> serial
    1.45 +    val init: serial -> theory -> theory
    1.46 +    val get: serial -> (Object.T -> 'a) -> proof -> 'a
    1.47 +    val put: serial -> ('a -> Object.T) -> 'a -> proof -> proof
    1.48 +  end
    1.49  end;
    1.50  
    1.51  structure Context: PRIVATE_CONTEXT =
    1.52 @@ -114,10 +131,10 @@
    1.53  val invoke_extend    = invoke "extend" #extend;
    1.54  fun invoke_merge pp  = invoke "merge" (fn kind => #merge kind pp);
    1.55  
    1.56 -fun declare_theory_data name e cp ext mrg =
    1.57 +fun declare_theory_data name empty copy extend merge =
    1.58    let
    1.59      val k = serial ();
    1.60 -    val kind = {name = name, empty = e, copy = cp, extend = ext, merge = mrg};
    1.61 +    val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
    1.62      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    1.63        warning ("Duplicate declaration of theory data " ^ quote name));
    1.64      val _ = kinds := Inttab.update ((k, kind), ! kinds);
    1.65 @@ -135,17 +152,18 @@
    1.66  
    1.67  datatype theory =
    1.68    Theory of
    1.69 -  (*identity*)
    1.70 +   (*identity*)
    1.71     {self: theory ref option,            (*dynamic self reference -- follows theory changes*)
    1.72      id: serial * string,                (*identifier of this theory*)
    1.73      ids: string Inttab.table,           (*identifiers of ancestors*)
    1.74      iids: string Inttab.table} *        (*identifiers of intermediate checkpoints*)
    1.75 -  (*data*)
    1.76 -  Object.T Inttab.table *               (*record of arbitrarily typed data*)
    1.77 -  (*ancestry of graph development*)
    1.78 +   (*data*)
    1.79 +   {theory: Object.T Inttab.table,      (*theory data record*)
    1.80 +    proof: unit Inttab.table} *         (*proof data kinds*)
    1.81 +   (*ancestry*)
    1.82     {parents: theory list,               (*immediate predecessors*)
    1.83      ancestors: theory list} *           (*all predecessors*)
    1.84 -  (*history of linear development*)
    1.85 +   (*history*)
    1.86     {name: string,                       (*prospective name of finished theory*)
    1.87      version: int,                       (*checkpoint counter*)
    1.88      intermediates: theory list};        (*intermediate checkpoints*)
    1.89 @@ -160,9 +178,14 @@
    1.90  val history_of  = #4 o rep_theory;
    1.91  
    1.92  fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
    1.93 +fun make_data theory proof = {theory = theory, proof = proof};
    1.94  fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
    1.95  fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
    1.96  
    1.97 +fun map_theory f {theory, proof} = make_data (f theory) proof;
    1.98 +fun map_proof f {theory, proof} = make_data theory (f proof);
    1.99 +
   1.100 +val the_self = the o #self o identity_of;
   1.101  val parents_of = #parents o ancestry_of;
   1.102  val ancestors_of = #ancestors o ancestry_of;
   1.103  val theory_name = #name o history_of;
   1.104 @@ -170,7 +193,7 @@
   1.105  
   1.106  (* staleness *)
   1.107  
   1.108 -fun eq_id ((i: int, _), (j, _)) = i = j;
   1.109 +fun eq_id ((i: int, _), (j, _)) = (i = j);
   1.110  
   1.111  fun is_stale
   1.112      (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
   1.113 @@ -219,7 +242,7 @@
   1.114  val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   1.115  
   1.116  
   1.117 -(* consistency *)
   1.118 +(* consistency *)    (*exception TERM*)
   1.119  
   1.120  fun check_thy pos thy =
   1.121    if is_stale thy then
   1.122 @@ -244,44 +267,32 @@
   1.123    |> check_insert (#version history2 > 0) id2;
   1.124  
   1.125  
   1.126 +(* equality and inclusion *)
   1.127 +
   1.128 +val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy");
   1.129 +
   1.130 +fun proper_subthy
   1.131 +  (thy1 as Theory ({id = (i, _), ...}, _, _, _),
   1.132 +    thy2 as Theory ({ids, iids, ...}, _, _, _)) =
   1.133 +  (pairself (check_thy "Context.proper_subthy") (thy1, thy2);
   1.134 +    is_some (Inttab.lookup (ids, i)) orelse is_some (Inttab.lookup (iids, i)));
   1.135 +
   1.136 +fun subthy thys = eq_thy thys orelse proper_subthy thys;
   1.137 +
   1.138 +
   1.139  (* theory references *)
   1.140  
   1.141  (*theory_ref provides a safe way to store dynamic references to a
   1.142 -  theory -- a plain theory value would become stale as the self
   1.143 -  reference moves on*)
   1.144 +  theory in external data structures -- a plain theory value would
   1.145 +  become stale as the self reference moves on*)
   1.146  
   1.147  datatype theory_ref = TheoryRef of theory ref;
   1.148  
   1.149 -val self_ref = TheoryRef o the o #self o identity_of o check_thy "Context.self_ref";
   1.150 +val self_ref = TheoryRef o the_self o check_thy "Context.self_ref";
   1.151  fun deref (TheoryRef (ref thy)) = thy;
   1.152  
   1.153  
   1.154 -(* equality and inclusion *)  (* FIXME proper_subthy; no subthy_internal *)
   1.155 -
   1.156 -local
   1.157 -
   1.158 -fun exists_ids (Theory ({id, ids, iids, ...}, _, _, _)) (i, _) =
   1.159 -  i = #1 id orelse
   1.160 -  is_some (Inttab.lookup (ids, i)) orelse
   1.161 -  is_some (Inttab.lookup (iids, i));
   1.162 -
   1.163 -fun member_ids (Theory ({id, ...}, _, _, _), thy) = exists_ids thy id;
   1.164 -
   1.165 -fun subset_ids (Theory ({id, ids, iids, ...}, _, _, _), thy) =
   1.166 -  exists_ids thy id andalso
   1.167 -  Inttab.forall (exists_ids thy) ids andalso
   1.168 -  Inttab.forall (exists_ids thy) iids;
   1.169 -
   1.170 -in
   1.171 -
   1.172 -val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy");
   1.173 -fun subthy thys = eq_thy thys orelse member_ids thys;
   1.174 -fun subthy_internal thys = eq_thy thys orelse subset_ids thys;
   1.175 -
   1.176 -end;
   1.177 -
   1.178 -
   1.179 -(* trivial merge *)
   1.180 +(* trivial merge *)    (*exception TERM*)
   1.181  
   1.182  fun merge (thy1, thy2) =
   1.183    if subthy (thy2, thy1) then thy1
   1.184 @@ -313,8 +324,8 @@
   1.185      val (self', data', ancestry') =
   1.186        if is_draft thy then (self, data, ancestry)    (*destructive change!*)
   1.187        else if #version history > 0
   1.188 -      then (NONE, copy_data data, ancestry)
   1.189 -      else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
   1.190 +      then (NONE, map_theory copy_data data, ancestry)
   1.191 +      else (NONE, map_theory extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
   1.192      val data'' = f data';
   1.193    in create_thy name self' id ids iids data'' ancestry' history end;
   1.194  
   1.195 @@ -324,37 +335,43 @@
   1.196  
   1.197  fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
   1.198    (check_thy "Context.copy_thy" thy;
   1.199 -    create_thy draftN NONE id ids iids (copy_data data) ancestry history);
   1.200 +    create_thy draftN NONE id ids iids (map_theory copy_data data) ancestry history);
   1.201  
   1.202  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   1.203 -  Inttab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
   1.204 +  (make_data Inttab.empty Inttab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []);
   1.205  
   1.206  
   1.207  (* named theory nodes *)
   1.208  
   1.209  fun merge_thys pp (thy1, thy2) =
   1.210 -  if subthy_internal (thy2, thy1) then thy1
   1.211 -  else if subthy_internal (thy1, thy2) then thy2
   1.212 -  else if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   1.213 +  if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   1.214      error "Cannot merge Pure and CPure developments"
   1.215    else
   1.216      let
   1.217        val (ids, iids) = check_merge thy1 thy2;
   1.218 -      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   1.219 +      val data1 = data_of thy1 and data2 = data_of thy2;
   1.220 +      val data = make_data
   1.221 +        (merge_data (pp thy1) (#theory data1, #theory data2))
   1.222 +        (Inttab.merge (K true) (#proof data1, #proof data2));
   1.223        val ancestry = make_ancestry [] [];
   1.224        val history = make_history "" 0 [];
   1.225      in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   1.226  
   1.227 +fun maximal_thys thys =
   1.228 +  thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
   1.229 +
   1.230  fun begin_thy pp name imports =
   1.231    if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   1.232    else
   1.233      let
   1.234 -      val parents = gen_distinct eq_thy imports;  (* FIXME maximals *)
   1.235 +      val parents =
   1.236 +        maximal_thys (gen_distinct eq_thy (map (check_thy "Context.begin_thy") imports));
   1.237        val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents));
   1.238        val Theory ({id, ids, iids, ...}, data, _, _) =
   1.239          (case parents of
   1.240            [] => error "No parent theories"
   1.241 -        | thy :: thys => extend_thy (Library.foldl (merge_thys pp) (thy, thys)));
   1.242 +        | [thy] => extend_thy thy
   1.243 +        | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   1.244        val ancestry = make_ancestry parents ancestors;
   1.245        val history = make_history name 0 [];
   1.246      in create_thy draftN NONE id ids iids data ancestry history end;
   1.247 @@ -375,41 +392,44 @@
   1.248  fun finish_thy thy =
   1.249    let
   1.250      val {name, version, intermediates} = history_of thy;
   1.251 -    val rs = map (the o #self o identity_of o check_thy "Context.finish_thy") intermediates;
   1.252 +    val rs = map (the_self o check_thy "Context.finish_thy") intermediates;
   1.253      val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
   1.254      val identity' = make_identity self id ids Inttab.empty;
   1.255      val history' = make_history name 0 [];
   1.256      val thy'' = vitalize (Theory (identity', data', ancestry', history'));
   1.257 -  in List.app (fn r => r := thy'') rs; thy'' end;
   1.258 +    val _ = List.app (fn r => r := thy'') rs;
   1.259 +  in thy'' end;
   1.260  
   1.261  
   1.262  (* theory data *)
   1.263  
   1.264 -fun theory_data thy =
   1.265 -  map invoke_name (Inttab.keys (data_of thy))
   1.266 +fun dest_data name_of tab =
   1.267 +  map name_of (Inttab.keys tab)
   1.268    |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest
   1.269    |> map (apsnd length)
   1.270    |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
   1.271  
   1.272 +val theory_data_of = dest_data invoke_name o #theory o data_of;
   1.273 +
   1.274  structure TheoryData =
   1.275  struct
   1.276  
   1.277  val declare = declare_theory_data;
   1.278  
   1.279  fun get k dest thy =
   1.280 -  (case Inttab.lookup (data_of thy, k) of
   1.281 +  (case Inttab.lookup (#theory (data_of thy), k) of
   1.282      SOME x => (dest x handle Match =>
   1.283        error ("Failed to access theory data " ^ quote (invoke_name k)))
   1.284    | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   1.285  
   1.286 -fun put k mk x = modify_thy (curry Inttab.update (k, mk x));
   1.287 +fun put k mk x = modify_thy (map_theory (curry Inttab.update (k, mk x)));
   1.288  fun init k = put k I (invoke_empty k);
   1.289  
   1.290  end;
   1.291  
   1.292  
   1.293  
   1.294 -(** ML theory context **)
   1.295 +(*** ML theory context ***)
   1.296  
   1.297  local
   1.298    val current_theory = ref (NONE: theory option);
   1.299 @@ -468,6 +488,82 @@
   1.300    fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
   1.301  end;
   1.302  
   1.303 +
   1.304 +
   1.305 +(*** proof context ***)
   1.306 +
   1.307 +(* datatype proof *)
   1.308 +
   1.309 +datatype proof = Proof of theory * Object.T Inttab.table;
   1.310 +
   1.311 +fun theory_of_proof (Proof (thy, _)) = thy;
   1.312 +fun data_of_proof (Proof (_, data)) = data;
   1.313 +fun map_prf f (Proof (thy, data)) = Proof (thy, f data);
   1.314 +
   1.315 +
   1.316 +(* proof data kinds *)
   1.317 +
   1.318 +local
   1.319 +
   1.320 +type kind =
   1.321 + {name: string,
   1.322 +  init: theory -> Object.T};
   1.323 +
   1.324 +val kinds = ref (Inttab.empty: kind Inttab.table);
   1.325 +
   1.326 +fun invoke meth_name meth_fn k =
   1.327 +  (case Inttab.lookup (! kinds, k) of
   1.328 +    SOME kind => meth_fn kind |> transform_failure (fn exn =>
   1.329 +      DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   1.330 +  | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   1.331 +
   1.332 +fun invoke_name k = invoke "name" (K o #name) k ();
   1.333 +val invoke_init   = invoke "init" #init;
   1.334 +
   1.335 +in
   1.336 +
   1.337 +val proof_data_of = dest_data invoke_name o #proof o data_of;
   1.338 +
   1.339 +fun init_proof thy =
   1.340 +  Proof (thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
   1.341 +
   1.342 +structure ProofData =
   1.343 +struct
   1.344 +
   1.345 +fun declare name init =
   1.346 +  let
   1.347 +    val k = serial ();
   1.348 +    val kind = {name = name, init = init};
   1.349 +    val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   1.350 +      warning ("Duplicate declaration of proof data " ^ quote name));
   1.351 +    val _ = kinds := Inttab.update ((k, kind), ! kinds);
   1.352 +  in k end;
   1.353 +
   1.354 +fun init k = modify_thy (map_proof (curry Inttab.update (k, ())));
   1.355 +
   1.356 +fun get k dest prf =
   1.357 +  (case Inttab.lookup (data_of_proof prf, k) of
   1.358 +    SOME x => (dest x handle Match =>
   1.359 +      error ("Failed to access proof data " ^ quote (invoke_name k)))
   1.360 +  | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
   1.361 +
   1.362 +fun put k mk x = map_prf (curry Inttab.update (k, mk x));
   1.363 +
   1.364 +end;
   1.365 +
   1.366 +end;
   1.367 +
   1.368 +
   1.369 +(*** generic context ***)
   1.370 +
   1.371 +datatype context = Theory of theory | Proof of proof;
   1.372 +
   1.373 +fun theory_of (Theory thy) = thy
   1.374 +  | theory_of (Proof prf) = theory_of_proof prf;
   1.375 +
   1.376 +fun proof_of (Theory thy) = init_proof thy
   1.377 +  | proof_of (Proof prf) = prf;
   1.378 +
   1.379  end;
   1.380  
   1.381  structure BasicContext: BASIC_CONTEXT = Context;
   1.382 @@ -475,7 +571,9 @@
   1.383  
   1.384  
   1.385  
   1.386 -(*** type-safe interface for theory data ***)
   1.387 +(*** type-safe interfaces for data declarations ***)
   1.388 +
   1.389 +(** theory data **)
   1.390  
   1.391  signature THEORY_DATA_ARGS =
   1.392  sig
   1.393 @@ -522,5 +620,45 @@
   1.394  
   1.395  end;
   1.396  
   1.397 -(*hide private interface!*)
   1.398 +
   1.399 +
   1.400 +(** proof data **)
   1.401 +
   1.402 +signature PROOF_DATA_ARGS =
   1.403 +sig
   1.404 +  val name: string
   1.405 +  type T
   1.406 +  val init: theory -> T
   1.407 +  val print: Context.proof -> T -> unit
   1.408 +end;
   1.409 +
   1.410 +signature PROOF_DATA =
   1.411 +sig
   1.412 +  type T
   1.413 +  val init: theory -> theory
   1.414 +  val print: Context.proof -> unit
   1.415 +  val get: Context.proof -> T
   1.416 +  val put: T -> Context.proof -> Context.proof
   1.417 +  val map: (T -> T) -> Context.proof -> Context.proof
   1.418 +end;
   1.419 +
   1.420 +functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
   1.421 +struct
   1.422 +
   1.423 +structure ProofData = Context.ProofData;
   1.424 +
   1.425 +type T = Data.T;
   1.426 +exception Data of T;
   1.427 +
   1.428 +val kind = ProofData.declare Data.name (Data o Data.init);
   1.429 +
   1.430 +val init = ProofData.init kind;
   1.431 +val get = ProofData.get kind (fn Data x => x);
   1.432 +fun print prf = Data.print prf (get prf);
   1.433 +val put = ProofData.put kind Data;
   1.434 +fun map f prf = put (f (get prf)) prf;
   1.435 +
   1.436 +end;
   1.437 +
   1.438 +(*hide private interface*)
   1.439  structure Context: CONTEXT = Context;