simplified data setup

--- a/src/Pure/Tools/codegen_data.ML	Wed May 30 21:09:17 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Wed May 30 21:09:18 2007 +0200
@@ -40,29 +40,47 @@
   val trace: bool ref
 end;
 
+signature CODE_DATA_ARGS =
+sig
+  type T
+  val empty: T
+  val merge: Pretty.pp -> T * T -> T
+  val purge: theory option -> CodegenConsts.const list option -> T -> T
+end;
+
+signature CODE_DATA =
+sig
+  type T
+  val get: theory -> T
+  val change: theory -> (T -> T) -> T
+  val change_yield: theory -> (T -> 'a * T) -> 'a * T
+end;
+
 signature PRIVATE_CODEGEN_DATA =
 sig
   include CODEGEN_DATA
-  type data
-  structure CodeData: THEORY_DATA
-  val declare: string -> Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
+  val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
     -> (theory option -> CodegenConsts.const list option -> Object.T -> Object.T) -> serial
-  val init: serial -> theory -> theory
-  val get: serial -> (Object.T -> 'a) -> data -> 'a
-  val put: serial -> ('a -> Object.T) -> 'a -> data -> data
+  val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
+    -> theory -> 'a
+  val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
+    -> theory -> ('a -> 'a) -> 'a
+  val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
+    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
 end;
 
 structure CodegenData : PRIVATE_CODEGEN_DATA =
 struct
 
-(** diagnostics **)
+(* auxiliary, diagnostics *)
+
+structure Consttab = CodegenConsts.Consttab;
 
 val trace = ref false;
 fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
 
 
-
-(** lazy theorems, certificate theorems **)
+(* lazy theorems, certificate theorems *)
 
 val eval_always = ref false;
 
@@ -107,9 +125,6 @@
         | _ => (apsnd (lazy_thms o K)) (merge_thms (Susp.force r1, Susp.force r2));
 
 
-
-(** code theorems **)
-
 (* pairs of (selected, deleted) defining equations *)
 
 type sdthms = thm list Susp.T * thm list;
@@ -159,9 +174,7 @@
   end;
 
 
-(** data structures **)
-
-structure Consttab = CodegenConsts.Consttab;
+(** exeuctable content **)
 
 datatype preproc = Preproc of {
   inlines: thm list,
@@ -260,55 +273,52 @@
 val map_dtyps = map_exec o apsnd o map_spec o apsnd;
 
 
-(** code data structures **)
+(* data slots dependent on executable content *)
 
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = TableFun(type key = int val ord = int_ord);
 
-
-(* data slots *)
-
 local
 
 type kind = {
-  name: string,
   empty: Object.T,
   merge: Pretty.pp -> Object.T * Object.T -> Object.T,
   purge: theory option -> CodegenConsts.const list option -> Object.T -> Object.T
 };
 
 val kinds = ref (Datatab.empty: kind Datatab.table);
+val kind_keys = ref ([]: serial list);
 
-fun invoke meth_name meth_fn k =
-  (case Datatab.lookup (! kinds) k of
-    SOME kind => meth_fn kind |> transform_failure (fn exn =>
-      EXCEPTION (exn, "Code data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
-  | NONE => sys_error ("Invalid code data identifier " ^ string_of_int k));
-
+fun invoke f k = case Datatab.lookup (! kinds) k
+ of SOME kind => f kind
+  | NONE => sys_error "Invalid code data identifier";
 
 in
 
-fun invoke_name k   = invoke "name" (K o #name) k ();
-fun invoke_empty k  = invoke "empty" (K o #empty) k ();
-fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
-fun invoke_purge thy_opt cs = invoke "purge" (fn kind => #purge kind thy_opt cs);
-
-fun declare name empty merge purge =
+fun declare_data empty merge purge =
   let
     val k = serial ();
-    val kind = {name = name, empty = empty, merge = merge, purge = purge};
-    val _ =
-      if Datatab.exists (equal name o #name o #2) (! kinds) then
-        warning ("Duplicate declaration of code data " ^ quote name)
-      else ();
+    val kind = {empty = empty, merge = merge, purge = purge};
     val _ = change kinds (Datatab.update (k, kind));
+    val _ = change kind_keys (cons k);
   in k end;
 
+fun invoke_empty k = invoke (fn kind => #empty kind) k;
+
+fun invoke_merge_all pp = Datatab.join
+  (invoke (fn kind => #merge kind pp));
+
+fun invoke_purge_all thy_opt cs =
+  fold (fn k => Datatab.map_entry k
+    (invoke (fn kind => #purge kind thy_opt cs) k)) (! kind_keys);
+
 end; (*local*)
 
 
 (* theory store *)
 
+local
+
 type data = Object.T Datatab.table;
 
 structure CodeData = TheoryDataFun
@@ -320,16 +330,65 @@
   fun merge pp ((exec1, data1), (exec2, data2)) =
     let
       val (touched, exec) = merge_exec (exec1, exec2);
-      val data1' = Datatab.map' (invoke_purge NONE touched) (! data1);
-      val data2' = Datatab.map' (invoke_purge NONE touched) (! data2);
-      val data = Datatab.join (invoke_merge pp) (data1', data2');
+      val data1' = invoke_purge_all NONE touched (! data1);
+      val data2' = invoke_purge_all NONE touched (! data2);
+      val data = invoke_merge_all pp (data1', data2');
     in (exec, ref data) end;
 );
 
+val _ = Context.add_setup CodeData.init;
+
+fun ch r f = let val x = f (! r) in (r := x; x) end;
+fun thy_data f thy = f ((snd o CodeData.get) thy);
+
+fun get_ensure_init kind data_ref =
+  case Datatab.lookup (! data_ref) kind
+   of SOME x => x
+    | NONE => let val y = invoke_empty kind
+        in (change data_ref (Datatab.update (kind, y)); y) end;
+
+in
+
+(* access to executable content *)
+
+val get_exec = fst o CodeData.get;
+
+fun map_exec_purge touched f thy =
+  CodeData.map (fn (exec, data) => 
+    (f exec, ref (invoke_purge_all (SOME thy) touched (! data)))) thy;
+
+
+(* access to data dependent on abstract executable content *)
+
+fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest);
+
+fun change_data (kind, mk, dest) =
+  let
+    fun chnge data_ref f =
+      let
+        val data = get_ensure_init kind data_ref;
+        val data' = f (dest data);
+      in (change data_ref (Datatab.update (kind, mk data')); data') end;
+  in thy_data chnge end;
+
+fun change_yield_data (kind, mk, dest) =
+  let
+    fun chnge data_ref f =
+      let
+        val data = get_ensure_init kind data_ref;
+        val (x, data') = f (dest data);
+      in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
+  in thy_data chnge end;
+
+end; (*local*)
+
+
+(* print executable content *)
+
 fun print_codesetup thy =
   let
     val ctxt = ProofContext.init thy;
-    val (exec, _) = CodeData.get thy;
+    val exec = get_exec thy;
     fun pretty_func (s, lthms) =
       (Pretty.block o Pretty.fbreaks) (
         Pretty.str s :: pretty_sdthms ctxt lthms
@@ -386,25 +445,6 @@
     ]
   end;
 
-fun init k = CodeData.map
-  (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
-
-fun get k dest data =
-  (case Datatab.lookup data k of
-    SOME x => (dest x handle Match =>
-      error ("Failed to access code data " ^ quote (invoke_name k)))
-  | NONE => error ("Uninitialized code data " ^ quote (invoke_name k)));
-
-fun put k mk x = Datatab.update (k, mk x);
-
-fun map_exec_purge touched f thy =
-  CodeData.map (fn (exec, data) => 
-    (f exec, ref (Datatab.map' (invoke_purge (SOME thy) touched) (! data)))) thy;
-
-val get_exec = fst o CodeData.get;
-
-val _ = Context.add_setup CodeData.init;
-
 
 
 (** theorem transformation and certification **)
@@ -582,6 +622,8 @@
 
 end;
 
+
+
 (** interfaces **)
 
 fun add_func true thm thy =
@@ -799,24 +841,6 @@
 
 (** type-safe interfaces for data depedent on executable content **)
 
-signature CODE_DATA_ARGS =
-sig
-  val name: string
-  type T
-  val empty: T
-  val merge: Pretty.pp -> T * T -> T
-  val purge: theory option -> CodegenConsts.const list option -> T -> T
-end;
-
-signature CODE_DATA =
-sig
-  type T
-  val init: theory -> theory
-  val get: theory -> T
-  val change: theory -> (T -> T) -> T
-  val change_yield: theory -> (T -> 'a * T) -> 'a * T
-end;
-
 functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA =
 struct
 
@@ -824,27 +848,15 @@
 exception Data of T;
 fun dest (Data x) = x
 
-val kind = CodegenData.declare Data.name (Data Data.empty)
+val kind = CodegenData.declare_data (Data Data.empty)
   (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
   (fn thy_opt => fn cs => fn Data x => Data (Data.purge thy_opt cs x));
 
-val init = CodegenData.init kind;
-
-fun get thy = CodegenData.get kind dest ((! o snd o CodegenData.CodeData.get) thy);
+val data_op = (kind, Data, dest);
 
-fun change thy f =
-  let
-    val data_ref = (snd o CodegenData.CodeData.get) thy;
-    val x = (f o CodegenData.get kind dest o !) data_ref;
-    val data = CodegenData.put kind Data x (! data_ref);
-  in (data_ref := data; x) end;
-
-fun change_yield thy f =
-  let
-    val data_ref = (snd o CodegenData.CodeData.get) thy;
-    val (y, x) = (f o CodegenData.get kind dest o !) data_ref;
-    val data = CodegenData.put kind Data x (! data_ref);
-  in (data_ref := data; (y, x)) end;
+val get = CodegenData.get_data data_op;
+val change = CodegenData.change_data data_op;
+fun change_yield thy = CodegenData.change_yield_data data_op thy;
 
 end;
 

--- a/src/Pure/Tools/codegen_funcgr.ML	Wed May 30 21:09:17 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Wed May 30 21:09:18 2007 +0200
@@ -24,7 +24,6 @@
   val make: theory -> CodegenConsts.const list -> T
   val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T
   val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
-  val init: theory -> theory
 end;
 
 structure CodegenFuncgr = (*signature is added later*)
@@ -348,7 +347,7 @@
 
 end; (*struct*)
 
-functor CodegenFuncgrRetrieval (val name: string; val rewrites: theory -> thm list) : CODEGEN_FUNCGR_RETRIEVAL =
+functor CodegenFuncgrRetrieval (val rewrites: theory -> thm list) : CODEGEN_FUNCGR_RETRIEVAL =
 struct
 
 (** code data **)
@@ -357,7 +356,6 @@
 
 structure Funcgr = CodeDataFun
 (struct
-  val name = name;
   type T = T;
   val empty = CodegenFuncgr.Constgraph.empty;
   fun merge _ _ = CodegenFuncgr.Constgraph.empty;
@@ -376,8 +374,6 @@
 fun make_term thy f =
   Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f;
 
-val init = Funcgr.init;
-
 end; (*functor*)
 
 structure CodegenFuncgr : CODEGEN_FUNCGR =

--- a/src/Pure/Tools/codegen_names.ML	Wed May 30 21:09:17 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Wed May 30 21:09:18 2007 +0200
@@ -295,7 +295,6 @@
 
 structure ConstName = CodeDataFun
 (
-  val name = "Pure/codegen_names";
   type T = const Consttab.table * (string * string option) Symtab.table;
   val empty = (Consttab.empty, Symtab.empty);
   fun merge _ ((const1, constrev1), (const2, constrev2)) =
@@ -306,7 +305,7 @@
         fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
 );
 
-val _ = Context.add_setup (CodeName.init #> ConstName.init);
+val _ = Context.add_setup (CodeName.init);
 
 
 (* forward lookup with cache update *)

--- a/src/Pure/Tools/codegen_package.ML	Wed May 30 21:09:17 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed May 30 21:09:18 2007 +0200
@@ -60,11 +60,7 @@
     (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
 );
 
-structure Funcgr = CodegenFuncgrRetrieval
-(
-  val name = "Pure/codegen_package_thms";
-  fun rewrites thy = [];
-);
+structure Funcgr = CodegenFuncgrRetrieval (fun rewrites thy = []);
 
 fun code_depgr thy [] = Funcgr.make thy []
   | code_depgr thy consts =
@@ -94,7 +90,6 @@
 
 structure Code = CodeDataFun
 (
-  val name = "Pure/codegen_package_code";
   type T = CodegenThingol.code;
   val empty = CodegenThingol.empty_code;
   fun merge _ = CodegenThingol.merge_code;
@@ -111,7 +106,6 @@
         in Graph.del_nodes dels code end;
 );
 
-val _ = Context.add_setup (Funcgr.init #> Code.init);
 
 
 (* preparing defining equations *)

--- a/src/Pure/Tools/nbe.ML	Wed May 30 21:09:17 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Wed May 30 21:09:18 2007 +0200
@@ -65,24 +65,18 @@
 
 (* theorem store *)
 
-structure Funcgr = CodegenFuncgrRetrieval (
-  val name = "Pure/nbe_thms";
-  val rewrites = the_pres;
-);
+structure Funcgr = CodegenFuncgrRetrieval (val rewrites = the_pres);
 
 (* code store *)
 
 structure NBE_Data = CodeDataFun
 (struct
-  val name = "Pure/mbe";
   type T = NBE_Eval.Univ Symtab.table;
   val empty = Symtab.empty;
   fun merge _ = Symtab.merge (K true);
   fun purge _ _ _ = Symtab.empty;
 end);
 
-val _ = Context.add_setup (Funcgr.init #> NBE_Data.init);
-
 
 (** norm by eval **)