reduced code generator cache to the baremost minimum

--- a/src/Pure/Isar/code.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Pure/Isar/code.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -1,8 +1,9 @@
 (*  Title:      Pure/Isar/code.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Abstract executable code of theory.  Management of data dependent on
-executable code.  Cache assumes non-concurrent processing of a single theory.
+Abstract executable ingredients of theory.  Management of data
+dependent on executable ingredients as synchronized cache; purged
+on any change of underlying executable ingredients.
 *)
 
 signature CODE =
@@ -70,13 +71,11 @@
 sig
   type T
   val empty: T
-  val purge: theory -> string list -> 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;
@@ -84,10 +83,7 @@
 signature PRIVATE_CODE =
 sig
   include CODE
-  val declare_data: Object.T -> (theory -> string list -> Object.T -> Object.T)
-    -> serial
-  val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> 'a
+  val declare_data: Object.T -> serial
   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)
@@ -211,13 +207,9 @@
 
 local
 
-type kind = {
-  empty: Object.T,
-  purge: theory -> string list -> Object.T -> Object.T
-};
+type kind = { empty: Object.T };
 
 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
-val kind_keys = Unsynchronized.ref ([]: serial list);
 
 fun invoke f k = case Datatab.lookup (! kinds) k
  of SOME kind => f kind
@@ -225,20 +217,15 @@
 
 in
 
-fun declare_data empty purge =
+fun declare_data empty =
   let
     val k = serial ();
-    val kind = {empty = empty, purge = purge};
-    val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
-    val _ = Unsynchronized.change kind_keys (cons k);
+    val kind = { empty = empty };
+    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
 fun invoke_init k = invoke (fn kind => #empty kind) k;
 
-fun invoke_purge_all thy cs =
-  fold (fn k => Datatab.map_entry k
-    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
-
 end; (*local*)
 
 
@@ -247,26 +234,27 @@
 local
 
 type data = Object.T Datatab.table;
-val empty_data = Datatab.empty : data;
+fun create_data data = Synchronized.var "code data" data;
+fun empty_data () = create_data Datatab.empty;
 
 structure Code_Data = TheoryDataFun
 (
-  type T = spec * data Unsynchronized.ref;
+  type T = spec * data Synchronized.var;
   val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
-    (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
-  fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
+    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
+  fun copy (spec, data) = (spec, create_data (Synchronized.value data));
   val extend = copy;
   fun merge _ ((spec1, _), (spec2, _)) =
-    (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
+    (merge_spec (spec1, spec2), empty_data ());
 );
 
 fun thy_data f thy = f ((snd o Code_Data.get) thy);
 
-fun get_ensure_init kind data_ref =
-  case Datatab.lookup (! data_ref) kind
+fun get_ensure_init kind data =
+  case Datatab.lookup (Synchronized.value data) kind
    of SOME x => x
     | NONE => let val y = invoke_init kind
-        in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
+        in (Synchronized.change data (Datatab.update (kind, y)); y) end;
 
 in
 
@@ -274,19 +262,12 @@
 
 val the_exec = fst o Code_Data.get;
 
-fun complete_class_params thy cs =
-  fold (fn c => case AxClass.inst_of_param thy c
-   of NONE => insert (op =) c
-    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
+fun map_exec_purge f =
+  Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
 
-fun map_exec_purge touched f thy =
-  Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
-   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
-    | NONE => empty_data))) thy;
+val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
 
-val purge_data = (Code_Data.map o apsnd) (fn _ => Unsynchronized.ref empty_data);
-
-fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
+fun change_eqns delete c f = (map_exec_purge o map_eqns
   o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
     o apfst) (fn (_, eqns) => (true, f eqns));
 
@@ -323,15 +304,13 @@
 
 (* access to data dependent on abstract executable code *)
 
-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 (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
+      in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   in thy_data chnge end;
 
 fun change_yield_data (kind, mk, dest) =
@@ -340,7 +319,7 @@
       let
         val data = get_ensure_init kind data_ref;
         val (x, data') = f (dest data);
-      in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
+      in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   in thy_data chnge end;
 
 end; (*local*)
@@ -707,7 +686,7 @@
 fun add_type tyco thy =
   case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco
    of SOME (Type.Abbreviation (vs, _, _)) =>
-          (map_exec_purge NONE o map_signatures o apfst)
+          (map_exec_purge o map_signatures o apfst)
             (Symtab.update (tyco, length vs)) thy
     | _ => error ("No such type abbreviation: " ^ quote tyco);
 
@@ -723,7 +702,7 @@
       error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty);
   in
     thy
-    |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty))
+    |> (map_exec_purge o map_signatures o apsnd) (Symtab.update (c, ty))
   end;
 
 val add_signature = gen_add_signature (K I) cert_signature;
@@ -747,7 +726,7 @@
   in
     thy
     |> fold (del_eqns o fst) cs
-    |> map_exec_purge NONE
+    |> map_exec_purge
         ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
         #> (map_cases o apfst) drop_outdated_cases)
     |> Type_Interpretation.data (tyco, serial ())
@@ -838,29 +817,27 @@
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
     val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
-  in (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
 
 fun add_undefined c thy =
-  (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
+  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
 
 end; (*struct*)
 
 
 (** type-safe interfaces for data dependent on executable code **)
 
-functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
+functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA =
 struct
 
 type T = Data.T;
 exception Data of T;
 fun dest (Data x) = x
 
-val kind = Code.declare_data (Data Data.empty)
-  (fn thy => fn cs => fn Data x => Data (Data.purge thy cs x));
+val kind = Code.declare_data (Data Data.empty);
 
 val data_op = (kind, Data, dest);
 
-val get = Code.get_data data_op;
 val change = Code.change_data data_op;
 fun change_yield thy = Code.change_yield_data data_op thy;
 

--- a/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -445,22 +445,10 @@
 
 (** store for preprocessed arities and code equations **)
 
-structure Wellsorted = Code_Data_Fun
+structure Wellsorted = Code_Data
 (
   type T = ((string * class) * sort list) list * code_graph;
   val empty = ([], Graph.empty);
-  fun purge thy cs (arities, eqngr) =
-    let
-      val del_cs = ((Graph.all_preds eqngr
-        o filter (can (Graph.get_node eqngr))) cs);
-      val del_arities = del_cs
-        |> map_filter (AxClass.inst_of_param thy)
-        |> maps (fn (c, tyco) =>
-             (map (rpair tyco) o Sign.complete_sort thy o the_list
-               o AxClass.class_of_param thy) c);
-      val arities' = fold (AList.delete (op =)) del_arities arities;
-      val eqngr' = Graph.del_nodes del_cs eqngr;
-    in (arities', eqngr') end;
 );
 
 

--- a/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -356,15 +356,9 @@
       (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   in fold (insert (op =)) cs5 cs1 end;
 
-fun cached_program thy = 
-  let
-    val (naming, program) = Code_Thingol.cached_program thy;
-  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
-
 fun export_code thy cs seris =
   let
-    val (cs', (naming, program)) = if null cs then cached_program thy
-      else Code_Thingol.consts_program thy cs;
+    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
     fun mk_seri_dest dest = case dest
      of NONE => compile
       | SOME "-" => export
@@ -514,7 +508,7 @@
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 
 val code_exprP =
-  (Scan.repeat P.term_group
+  (Scan.repeat1 P.term_group
   -- Scan.repeat (P.$$$ inK |-- P.name
      -- Scan.option (P.$$$ module_nameK |-- P.name)
      -- Scan.option (P.$$$ fileK |-- P.name)

--- a/src/Tools/Code/code_thingol.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -90,7 +90,6 @@
   val canonize_thms: theory -> thm list -> thm list
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
-  val cached_program: theory -> naming * program
   val eval_conv: theory
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
@@ -843,22 +842,12 @@
 
 (* store *)
 
-structure Program = Code_Data_Fun
+structure Program = Code_Data
 (
   type T = naming * program;
   val empty = (empty_naming, Graph.empty);
-  fun purge thy cs (naming, program) =
-    let
-      val names_delete = cs
-        |> map_filter (lookup_const naming)
-        |> filter (can (Graph.get_node program))
-        |> Graph.all_preds program;
-      val program' = Graph.del_nodes names_delete program;
-    in (naming, program') end;
 );
 
-val cached_program = Program.get;
-
 fun invoke_generation thy (algebra, eqngr) f name =
   Program.change_yield thy (fn naming_program => (NONE, naming_program)
     |> f thy algebra eqngr name
@@ -943,10 +932,10 @@
 fun code_depgr thy consts =
   let
     val (_, eqngr) = Code_Preproc.obtain thy consts [];
-    val select = Graph.all_succs eqngr consts;
+    val all_consts = Graph.all_succs eqngr consts;
   in
     eqngr
-    |> not (null consts) ? Graph.subgraph (member (op =) select) 
+    |> Graph.subgraph (member (op =) all_consts) 
     |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
   end;
 
@@ -983,13 +972,13 @@
 
 val _ =
   OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
-    (Scan.repeat P.term_group
+    (Scan.repeat1 P.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
 
 val _ =
   OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
-    (Scan.repeat P.term_group
+    (Scan.repeat1 P.term_group
       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
 

--- a/src/Tools/nbe.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Tools/nbe.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -505,18 +505,10 @@
 
 (* function store *)
 
-structure Nbe_Functions = Code_Data_Fun
+structure Nbe_Functions = Code_Data
 (
   type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
   val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
-  fun purge thy cs (naming, (gr, (maxidx, idx_tab))) =
-    let
-      val names_delete = cs
-        |> map_filter (Code_Thingol.lookup_const naming)
-        |> filter (can (Graph.get_node gr))
-        |> Graph.all_preds gr;
-      val gr' = Graph.del_nodes names_delete gr;
-    in (naming, (gr', (maxidx, idx_tab))) end;
 );
 
 (* compilation, evaluation and reification *)