simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
authorwenzelm
Mon May 07 00:50:09 2007 +0200 (2007-05-07)
changeset 2284722da6c4bc422
parent 22846 fb79144af9a3
child 22848 f65a76867179
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Mon May 07 00:49:59 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Mon May 07 00:50:09 2007 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Generic theory contexts with unique identity, arbitrarily typed data,
     1.7 -development graph and history support. Generic proof contexts with
     1.8 +development graph and history support.  Generic proof contexts with
     1.9  arbitrarily typed data.
    1.10  *)
    1.11  
    1.12 @@ -45,7 +45,6 @@
    1.13    val copy_thy: theory -> theory
    1.14    val checkpoint_thy: theory -> theory
    1.15    val finish_thy: theory -> theory
    1.16 -  val theory_data_of: theory -> string list
    1.17    val pre_pure_thy: theory
    1.18    val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.19    (*proof context*)
    1.20 @@ -53,7 +52,6 @@
    1.21    val theory_of_proof: proof -> theory
    1.22    val transfer_proof: theory -> proof -> proof
    1.23    val init_proof: theory -> proof
    1.24 -  val proof_data_of: theory -> string list
    1.25    (*generic context*)
    1.26    datatype generic = Theory of theory | Proof of proof
    1.27    val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
    1.28 @@ -77,16 +75,14 @@
    1.29    include CONTEXT
    1.30    structure TheoryData:
    1.31    sig
    1.32 -    val declare: string -> Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
    1.33 +    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
    1.34        (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    1.35 -    val init: serial -> theory -> theory
    1.36      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.37      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.38    end
    1.39    structure ProofData:
    1.40    sig
    1.41 -    val declare: string -> (theory -> Object.T) -> serial
    1.42 -    val init: serial -> theory -> theory
    1.43 +    val declare: (theory -> Object.T) -> serial
    1.44      val get: serial -> (Object.T -> 'a) -> proof -> 'a
    1.45      val put: serial -> ('a -> Object.T) -> 'a -> proof -> proof
    1.46    end
    1.47 @@ -107,36 +103,29 @@
    1.48  local
    1.49  
    1.50  type kind =
    1.51 - {name: string,
    1.52 -  empty: Object.T,
    1.53 + {empty: Object.T,
    1.54    copy: Object.T -> Object.T,
    1.55    extend: Object.T -> Object.T,
    1.56    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    1.57  
    1.58  val kinds = ref (Datatab.empty: kind Datatab.table);
    1.59  
    1.60 -fun invoke meth_name meth_fn k =
    1.61 +fun invoke f k =
    1.62    (case Datatab.lookup (! kinds) k of
    1.63 -    SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.64 -      EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.65 -  | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
    1.66 +    SOME kind => f kind
    1.67 +  | NONE => sys_error "Invalid theory data identifier");
    1.68  
    1.69  in
    1.70  
    1.71 -fun invoke_name k    = invoke "name" (K o #name) k ();
    1.72 -fun invoke_empty k   = invoke "empty" (K o #empty) k ();
    1.73 -val invoke_copy      = invoke "copy" #copy;
    1.74 -val invoke_extend    = invoke "extend" #extend;
    1.75 -fun invoke_merge pp  = invoke "merge" (fn kind => #merge kind pp);
    1.76 +fun invoke_empty k   = invoke (K o #empty) k ();
    1.77 +val invoke_copy      = invoke #copy;
    1.78 +val invoke_extend    = invoke #extend;
    1.79 +fun invoke_merge pp  = invoke (fn kind => #merge kind pp);
    1.80  
    1.81 -fun declare_theory_data name empty copy extend merge =
    1.82 +fun declare_theory_data empty copy extend merge =
    1.83    let
    1.84      val k = serial ();
    1.85 -    val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
    1.86 -    val _ =
    1.87 -      if Datatab.exists (equal name o #name o #2) (! kinds) then
    1.88 -        warning ("Duplicate declaration of theory data " ^ quote name)
    1.89 -      else ();
    1.90 +    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
    1.91      val _ = change kinds (Datatab.update (k, kind));
    1.92    in k end;
    1.93  
    1.94 @@ -158,8 +147,7 @@
    1.95      ids: string Inttab.table,           (*identifiers of ancestors*)
    1.96      iids: string Inttab.table} *        (*identifiers of intermediate checkpoints*)
    1.97     (*data*)
    1.98 -   {theory: Object.T Datatab.table,     (*theory data record*)
    1.99 -    proof: unit Datatab.table} *        (*proof data kinds*)
   1.100 +   Object.T Datatab.table *
   1.101     (*ancestry*)
   1.102     {parents: theory list,               (*immediate predecessors*)
   1.103      ancestors: theory list} *           (*all predecessors*)
   1.104 @@ -178,13 +166,9 @@
   1.105  val history_of  = #4 o rep_theory;
   1.106  
   1.107  fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
   1.108 -fun make_data theory proof = {theory = theory, proof = proof};
   1.109  fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
   1.110  fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
   1.111  
   1.112 -fun map_theory_data f {theory, proof} = make_data (f theory) proof;
   1.113 -fun map_proof_data f {theory, proof} = make_data theory (f proof);
   1.114 -
   1.115  val the_self = the o #self o identity_of;
   1.116  val parents_of = #parents o ancestry_of;
   1.117  val ancestors_of = #ancestors o ancestry_of;
   1.118 @@ -330,8 +314,8 @@
   1.119      val (self', data', ancestry') =
   1.120        if is_draft thy then (self, data, ancestry)    (*destructive change!*)
   1.121        else if #version history > 0
   1.122 -      then (NONE, map_theory_data copy_data data, ancestry)
   1.123 -      else (NONE, map_theory_data extend_data data,
   1.124 +      then (NONE, copy_data data, ancestry)
   1.125 +      else (NONE, extend_data data,
   1.126          make_ancestry [thy] (thy :: #ancestors ancestry));
   1.127      val data'' = f data';
   1.128    in create_thy name self' id ids iids data'' ancestry' history end;
   1.129 @@ -341,11 +325,10 @@
   1.130  val extend_thy = modify_thy I;
   1.131  
   1.132  fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
   1.133 -  (check_thy thy;
   1.134 -    create_thy draftN NONE id ids iids (map_theory_data copy_data data) ancestry history);
   1.135 +  (check_thy thy; create_thy draftN NONE id ids iids (copy_data data) ancestry history);
   1.136  
   1.137  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   1.138 -  (make_data Datatab.empty Datatab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []);
   1.139 +  Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
   1.140  
   1.141  
   1.142  (* named theory nodes *)
   1.143 @@ -356,10 +339,7 @@
   1.144    else
   1.145      let
   1.146        val (ids, iids) = check_merge thy1 thy2;
   1.147 -      val data1 = data_of thy1 and data2 = data_of thy2;
   1.148 -      val data = make_data
   1.149 -        (merge_data (pp thy1) (#theory data1, #theory data2))
   1.150 -        (Datatab.merge (K true) (#proof data1, #proof data2));
   1.151 +      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   1.152        val ancestry = make_ancestry [] [];
   1.153        val history = make_history "" 0 [];
   1.154      in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   1.155 @@ -410,27 +390,17 @@
   1.156  
   1.157  (* theory data *)
   1.158  
   1.159 -fun dest_data name_of tab =
   1.160 -  map name_of (Datatab.keys tab)
   1.161 -  |> map (rpair ()) |> Symtab.make_list |> Symtab.dest
   1.162 -  |> map (apsnd length)
   1.163 -  |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
   1.164 -
   1.165 -val theory_data_of = dest_data invoke_name o #theory o data_of;
   1.166 -
   1.167  structure TheoryData =
   1.168  struct
   1.169  
   1.170  val declare = declare_theory_data;
   1.171  
   1.172  fun get k dest thy =
   1.173 -  (case Datatab.lookup (#theory (data_of thy)) k of
   1.174 -    SOME x => (dest x handle Match =>
   1.175 -      error ("Failed to access theory data " ^ quote (invoke_name k)))
   1.176 -  | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   1.177 +  dest ((case Datatab.lookup (data_of thy) k of
   1.178 +    SOME x => x
   1.179 +  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
   1.180  
   1.181 -fun put k mk x = modify_thy (map_theory_data (Datatab.update (k, mk x)));
   1.182 -fun init k = put k I (invoke_empty k);
   1.183 +fun put k mk x = modify_thy (Datatab.update (k, mk x));
   1.184  
   1.185  end;
   1.186  
   1.187 @@ -446,59 +416,47 @@
   1.188  fun data_of_proof (Proof (_, data)) = data;
   1.189  fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
   1.190  
   1.191 -fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
   1.192 -  if not (subthy (deref thy_ref, thy')) then
   1.193 -    error "transfer proof context: not a super theory"
   1.194 -  else Proof (self_ref thy', data);
   1.195 -
   1.196  
   1.197  (* proof data kinds *)
   1.198  
   1.199  local
   1.200  
   1.201 -type kind =
   1.202 - {name: string,
   1.203 -  init: theory -> Object.T};
   1.204 -
   1.205 -val kinds = ref (Datatab.empty: kind Datatab.table);
   1.206 +val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
   1.207  
   1.208 -fun invoke meth_name meth_fn k =
   1.209 +fun invoke_init k =
   1.210    (case Datatab.lookup (! kinds) k of
   1.211 -    SOME kind => meth_fn kind |> transform_failure (fn exn =>
   1.212 -      EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   1.213 -  | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   1.214 +    SOME init => init
   1.215 +  | NONE => sys_error "Invalid proof data identifier");
   1.216  
   1.217 -fun invoke_name k = invoke "name" (K o #name) k ();
   1.218 -val invoke_init   = invoke "init" #init;
   1.219 +fun init_data thy =
   1.220 +  Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
   1.221 +
   1.222 +fun init_new_data data thy =
   1.223 +  Datatab.merge (K true) (data, init_data thy);
   1.224  
   1.225  in
   1.226  
   1.227 -val proof_data_of = dest_data invoke_name o #proof o data_of;
   1.228 +fun init_proof thy = Proof (self_ref thy, init_data thy);
   1.229  
   1.230 -fun init_proof thy =
   1.231 -  Proof (self_ref thy, Datatab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
   1.232 +fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
   1.233 +  if not (subthy (deref thy_ref, thy')) then
   1.234 +    error "transfer proof context: not a super theory"
   1.235 +  else Proof (self_ref thy', init_new_data data thy');
   1.236 +
   1.237  
   1.238  structure ProofData =
   1.239  struct
   1.240  
   1.241 -fun declare name init =
   1.242 +fun declare init =
   1.243    let
   1.244      val k = serial ();
   1.245 -    val kind = {name = name, init = init};
   1.246 -    val _ =
   1.247 -      if Datatab.exists (equal name o #name o #2) (! kinds) then
   1.248 -        warning ("Duplicate declaration of proof data " ^ quote name)
   1.249 -      else ();
   1.250 -    val _ = change kinds (Datatab.update (k, kind));
   1.251 +    val _ = change kinds (Datatab.update (k, init));
   1.252    in k end;
   1.253  
   1.254 -fun init k = modify_thy (map_proof_data (Datatab.update (k, ())));
   1.255 -
   1.256  fun get k dest prf =
   1.257 -  (case Datatab.lookup (data_of_proof prf) k of
   1.258 -    SOME x => (dest x handle Match =>
   1.259 -      error ("Failed to access proof data " ^ quote (invoke_name k)))
   1.260 -  | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
   1.261 +  dest (case Datatab.lookup (data_of_proof prf) k of
   1.262 +    SOME x => x
   1.263 +  | NONE => invoke_init k (theory_of_proof prf));   (*adhoc value*)
   1.264  
   1.265  fun put k mk x = map_prf (Datatab.update (k, mk x));
   1.266  
   1.267 @@ -554,23 +512,20 @@
   1.268  
   1.269  signature THEORY_DATA_ARGS =
   1.270  sig
   1.271 -  val name: string
   1.272    type T
   1.273    val empty: T
   1.274    val copy: T -> T
   1.275    val extend: T -> T
   1.276    val merge: Pretty.pp -> T * T -> T
   1.277 -  val print: theory -> T -> unit
   1.278  end;
   1.279  
   1.280  signature THEORY_DATA =
   1.281  sig
   1.282    type T
   1.283 -  val init: theory -> theory
   1.284 -  val print: theory -> unit
   1.285    val get: theory -> T
   1.286    val put: T -> theory -> theory
   1.287    val map: (T -> T) -> theory -> theory
   1.288 +  val init: theory -> theory
   1.289  end;
   1.290  
   1.291  functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
   1.292 @@ -581,19 +536,18 @@
   1.293  type T = Data.T;
   1.294  exception Data of T;
   1.295  
   1.296 -val kind = TheoryData.declare Data.name
   1.297 +val kind = TheoryData.declare
   1.298    (Data Data.empty)
   1.299    (fn Data x => Data (Data.copy x))
   1.300    (fn Data x => Data (Data.extend x))
   1.301    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   1.302  
   1.303 -val init = TheoryData.init kind;
   1.304  val get = TheoryData.get kind (fn Data x => x);
   1.305 -val get_sg = get;
   1.306 -fun print thy = Data.print thy (get thy);
   1.307  val put = TheoryData.put kind Data;
   1.308  fun map f thy = put (f (get thy)) thy;
   1.309  
   1.310 +fun init thy = map I thy;
   1.311 +
   1.312  end;
   1.313  
   1.314  
   1.315 @@ -602,17 +556,13 @@
   1.316  
   1.317  signature PROOF_DATA_ARGS =
   1.318  sig
   1.319 -  val name: string
   1.320    type T
   1.321    val init: theory -> T
   1.322 -  val print: Context.proof -> T -> unit
   1.323  end;
   1.324  
   1.325  signature PROOF_DATA =
   1.326  sig
   1.327    type T
   1.328 -  val init: theory -> theory
   1.329 -  val print: Context.proof -> unit
   1.330    val get: Context.proof -> T
   1.331    val put: T -> Context.proof -> Context.proof
   1.332    val map: (T -> T) -> Context.proof -> Context.proof
   1.333 @@ -626,11 +576,9 @@
   1.334  type T = Data.T;
   1.335  exception Data of T;
   1.336  
   1.337 -val kind = ProofData.declare Data.name (Data o Data.init);
   1.338 +val kind = ProofData.declare (Data o Data.init);
   1.339  
   1.340 -val init = ProofData.init kind;
   1.341  val get = ProofData.get kind (fn Data x => x);
   1.342 -fun print prf = Data.print prf (get prf);
   1.343  val put = ProofData.put kind Data;
   1.344  fun map f prf = put (f (get prf)) prf;
   1.345  
   1.346 @@ -642,33 +590,27 @@
   1.347  
   1.348  signature GENERIC_DATA_ARGS =
   1.349  sig
   1.350 -  val name: string
   1.351    type T
   1.352    val empty: T
   1.353    val extend: T -> T
   1.354    val merge: Pretty.pp -> T * T -> T
   1.355 -  val print: Context.generic -> T -> unit
   1.356  end;
   1.357  
   1.358  signature GENERIC_DATA =
   1.359  sig
   1.360    type T
   1.361 -  val init: theory -> theory
   1.362    val get: Context.generic -> T
   1.363    val put: T -> Context.generic -> Context.generic
   1.364    val map: (T -> T) -> Context.generic -> Context.generic
   1.365 -  val print: Context.generic -> unit
   1.366  end;
   1.367  
   1.368  functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
   1.369  struct
   1.370  
   1.371 -structure ThyData = TheoryDataFun(open Data val copy = I fun print _ _ = ());
   1.372 -structure PrfData =
   1.373 -  ProofDataFun(val name = Data.name type T = Data.T val init = ThyData.get fun print _ _ = ());
   1.374 +structure ThyData = TheoryDataFun(open Data val copy = I);
   1.375 +structure PrfData = ProofDataFun(type T = Data.T val init = ThyData.get);
   1.376  
   1.377  type T = Data.T;
   1.378 -val init = ThyData.init #> PrfData.init;
   1.379  
   1.380  fun get (Context.Theory thy) = ThyData.get thy
   1.381    | get (Context.Proof prf) = PrfData.get prf;
   1.382 @@ -678,8 +620,6 @@
   1.383  
   1.384  fun map f ctxt = put (f (get ctxt)) ctxt;
   1.385  
   1.386 -fun print ctxt = Data.print ctxt (get ctxt);
   1.387 -
   1.388  end;
   1.389  
   1.390  (*hide private interface*)