reduced code generator cache to the baremost minimum
authorhaftmann
Wed Dec 23 08:31:15 2009 +0100 (2009-12-23)
changeset 34173458ced35abb8
parent 34172 4301e9ea1c54
child 34174 70210e9a8b4a
reduced code generator cache to the baremost minimum
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/code.ML	Wed Dec 23 08:31:14 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Dec 23 08:31:15 2009 +0100
     1.3 @@ -1,8 +1,9 @@
     1.4  (*  Title:      Pure/Isar/code.ML
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Abstract executable code of theory.  Management of data dependent on
     1.8 -executable code.  Cache assumes non-concurrent processing of a single theory.
     1.9 +Abstract executable ingredients of theory.  Management of data
    1.10 +dependent on executable ingredients as synchronized cache; purged
    1.11 +on any change of underlying executable ingredients.
    1.12  *)
    1.13  
    1.14  signature CODE =
    1.15 @@ -70,13 +71,11 @@
    1.16  sig
    1.17    type T
    1.18    val empty: T
    1.19 -  val purge: theory -> string list -> T -> T
    1.20  end;
    1.21  
    1.22  signature CODE_DATA =
    1.23  sig
    1.24    type T
    1.25 -  val get: theory -> T
    1.26    val change: theory -> (T -> T) -> T
    1.27    val change_yield: theory -> (T -> 'a * T) -> 'a * T
    1.28  end;
    1.29 @@ -84,10 +83,7 @@
    1.30  signature PRIVATE_CODE =
    1.31  sig
    1.32    include CODE
    1.33 -  val declare_data: Object.T -> (theory -> string list -> Object.T -> Object.T)
    1.34 -    -> serial
    1.35 -  val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.36 -    -> theory -> 'a
    1.37 +  val declare_data: Object.T -> serial
    1.38    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.39      -> theory -> ('a -> 'a) -> 'a
    1.40    val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.41 @@ -211,13 +207,9 @@
    1.42  
    1.43  local
    1.44  
    1.45 -type kind = {
    1.46 -  empty: Object.T,
    1.47 -  purge: theory -> string list -> Object.T -> Object.T
    1.48 -};
    1.49 +type kind = { empty: Object.T };
    1.50  
    1.51  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    1.52 -val kind_keys = Unsynchronized.ref ([]: serial list);
    1.53  
    1.54  fun invoke f k = case Datatab.lookup (! kinds) k
    1.55   of SOME kind => f kind
    1.56 @@ -225,20 +217,15 @@
    1.57  
    1.58  in
    1.59  
    1.60 -fun declare_data empty purge =
    1.61 +fun declare_data empty =
    1.62    let
    1.63      val k = serial ();
    1.64 -    val kind = {empty = empty, purge = purge};
    1.65 -    val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
    1.66 -    val _ = Unsynchronized.change kind_keys (cons k);
    1.67 +    val kind = { empty = empty };
    1.68 +    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    1.69    in k end;
    1.70  
    1.71  fun invoke_init k = invoke (fn kind => #empty kind) k;
    1.72  
    1.73 -fun invoke_purge_all thy cs =
    1.74 -  fold (fn k => Datatab.map_entry k
    1.75 -    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
    1.76 -
    1.77  end; (*local*)
    1.78  
    1.79  
    1.80 @@ -247,26 +234,27 @@
    1.81  local
    1.82  
    1.83  type data = Object.T Datatab.table;
    1.84 -val empty_data = Datatab.empty : data;
    1.85 +fun create_data data = Synchronized.var "code data" data;
    1.86 +fun empty_data () = create_data Datatab.empty;
    1.87  
    1.88  structure Code_Data = TheoryDataFun
    1.89  (
    1.90 -  type T = spec * data Unsynchronized.ref;
    1.91 +  type T = spec * data Synchronized.var;
    1.92    val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    1.93 -    (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
    1.94 -  fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
    1.95 +    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
    1.96 +  fun copy (spec, data) = (spec, create_data (Synchronized.value data));
    1.97    val extend = copy;
    1.98    fun merge _ ((spec1, _), (spec2, _)) =
    1.99 -    (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
   1.100 +    (merge_spec (spec1, spec2), empty_data ());
   1.101  );
   1.102  
   1.103  fun thy_data f thy = f ((snd o Code_Data.get) thy);
   1.104  
   1.105 -fun get_ensure_init kind data_ref =
   1.106 -  case Datatab.lookup (! data_ref) kind
   1.107 +fun get_ensure_init kind data =
   1.108 +  case Datatab.lookup (Synchronized.value data) kind
   1.109     of SOME x => x
   1.110      | NONE => let val y = invoke_init kind
   1.111 -        in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
   1.112 +        in (Synchronized.change data (Datatab.update (kind, y)); y) end;
   1.113  
   1.114  in
   1.115  
   1.116 @@ -274,19 +262,12 @@
   1.117  
   1.118  val the_exec = fst o Code_Data.get;
   1.119  
   1.120 -fun complete_class_params thy cs =
   1.121 -  fold (fn c => case AxClass.inst_of_param thy c
   1.122 -   of NONE => insert (op =) c
   1.123 -    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
   1.124 +fun map_exec_purge f =
   1.125 +  Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
   1.126  
   1.127 -fun map_exec_purge touched f thy =
   1.128 -  Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
   1.129 -   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
   1.130 -    | NONE => empty_data))) thy;
   1.131 +val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
   1.132  
   1.133 -val purge_data = (Code_Data.map o apsnd) (fn _ => Unsynchronized.ref empty_data);
   1.134 -
   1.135 -fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   1.136 +fun change_eqns delete c f = (map_exec_purge o map_eqns
   1.137    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
   1.138      o apfst) (fn (_, eqns) => (true, f eqns));
   1.139  
   1.140 @@ -323,15 +304,13 @@
   1.141  
   1.142  (* access to data dependent on abstract executable code *)
   1.143  
   1.144 -fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest);
   1.145 -
   1.146  fun change_data (kind, mk, dest) =
   1.147    let
   1.148      fun chnge data_ref f =
   1.149        let
   1.150          val data = get_ensure_init kind data_ref;
   1.151          val data' = f (dest data);
   1.152 -      in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   1.153 +      in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   1.154    in thy_data chnge end;
   1.155  
   1.156  fun change_yield_data (kind, mk, dest) =
   1.157 @@ -340,7 +319,7 @@
   1.158        let
   1.159          val data = get_ensure_init kind data_ref;
   1.160          val (x, data') = f (dest data);
   1.161 -      in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   1.162 +      in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   1.163    in thy_data chnge end;
   1.164  
   1.165  end; (*local*)
   1.166 @@ -707,7 +686,7 @@
   1.167  fun add_type tyco thy =
   1.168    case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco
   1.169     of SOME (Type.Abbreviation (vs, _, _)) =>
   1.170 -          (map_exec_purge NONE o map_signatures o apfst)
   1.171 +          (map_exec_purge o map_signatures o apfst)
   1.172              (Symtab.update (tyco, length vs)) thy
   1.173      | _ => error ("No such type abbreviation: " ^ quote tyco);
   1.174  
   1.175 @@ -723,7 +702,7 @@
   1.176        error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty);
   1.177    in
   1.178      thy
   1.179 -    |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty))
   1.180 +    |> (map_exec_purge o map_signatures o apsnd) (Symtab.update (c, ty))
   1.181    end;
   1.182  
   1.183  val add_signature = gen_add_signature (K I) cert_signature;
   1.184 @@ -747,7 +726,7 @@
   1.185    in
   1.186      thy
   1.187      |> fold (del_eqns o fst) cs
   1.188 -    |> map_exec_purge NONE
   1.189 +    |> map_exec_purge
   1.190          ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.191          #> (map_cases o apfst) drop_outdated_cases)
   1.192      |> Type_Interpretation.data (tyco, serial ())
   1.193 @@ -838,29 +817,27 @@
   1.194       of [] => ()
   1.195        | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.196      val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.197 -  in (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.198 +  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.199  
   1.200  fun add_undefined c thy =
   1.201 -  (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.202 +  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.203  
   1.204  end; (*struct*)
   1.205  
   1.206  
   1.207  (** type-safe interfaces for data dependent on executable code **)
   1.208  
   1.209 -functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
   1.210 +functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA =
   1.211  struct
   1.212  
   1.213  type T = Data.T;
   1.214  exception Data of T;
   1.215  fun dest (Data x) = x
   1.216  
   1.217 -val kind = Code.declare_data (Data Data.empty)
   1.218 -  (fn thy => fn cs => fn Data x => Data (Data.purge thy cs x));
   1.219 +val kind = Code.declare_data (Data Data.empty);
   1.220  
   1.221  val data_op = (kind, Data, dest);
   1.222  
   1.223 -val get = Code.get_data data_op;
   1.224  val change = Code.change_data data_op;
   1.225  fun change_yield thy = Code.change_yield_data data_op thy;
   1.226  
     2.1 --- a/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:14 2009 +0100
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:15 2009 +0100
     2.3 @@ -445,22 +445,10 @@
     2.4  
     2.5  (** store for preprocessed arities and code equations **)
     2.6  
     2.7 -structure Wellsorted = Code_Data_Fun
     2.8 +structure Wellsorted = Code_Data
     2.9  (
    2.10    type T = ((string * class) * sort list) list * code_graph;
    2.11    val empty = ([], Graph.empty);
    2.12 -  fun purge thy cs (arities, eqngr) =
    2.13 -    let
    2.14 -      val del_cs = ((Graph.all_preds eqngr
    2.15 -        o filter (can (Graph.get_node eqngr))) cs);
    2.16 -      val del_arities = del_cs
    2.17 -        |> map_filter (AxClass.inst_of_param thy)
    2.18 -        |> maps (fn (c, tyco) =>
    2.19 -             (map (rpair tyco) o Sign.complete_sort thy o the_list
    2.20 -               o AxClass.class_of_param thy) c);
    2.21 -      val arities' = fold (AList.delete (op =)) del_arities arities;
    2.22 -      val eqngr' = Graph.del_nodes del_cs eqngr;
    2.23 -    in (arities', eqngr') end;
    2.24  );
    2.25  
    2.26  
     3.1 --- a/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:14 2009 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:15 2009 +0100
     3.3 @@ -356,15 +356,9 @@
     3.4        (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
     3.5    in fold (insert (op =)) cs5 cs1 end;
     3.6  
     3.7 -fun cached_program thy = 
     3.8 -  let
     3.9 -    val (naming, program) = Code_Thingol.cached_program thy;
    3.10 -  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
    3.11 -
    3.12  fun export_code thy cs seris =
    3.13    let
    3.14 -    val (cs', (naming, program)) = if null cs then cached_program thy
    3.15 -      else Code_Thingol.consts_program thy cs;
    3.16 +    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
    3.17      fun mk_seri_dest dest = case dest
    3.18       of NONE => compile
    3.19        | SOME "-" => export
    3.20 @@ -514,7 +508,7 @@
    3.21  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
    3.22  
    3.23  val code_exprP =
    3.24 -  (Scan.repeat P.term_group
    3.25 +  (Scan.repeat1 P.term_group
    3.26    -- Scan.repeat (P.$$$ inK |-- P.name
    3.27       -- Scan.option (P.$$$ module_nameK |-- P.name)
    3.28       -- Scan.option (P.$$$ fileK |-- P.name)
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 23 08:31:14 2009 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 23 08:31:15 2009 +0100
     4.3 @@ -90,7 +90,6 @@
     4.4    val canonize_thms: theory -> thm list -> thm list
     4.5    val read_const_exprs: theory -> string list -> string list * string list
     4.6    val consts_program: theory -> string list -> string list * (naming * program)
     4.7 -  val cached_program: theory -> naming * program
     4.8    val eval_conv: theory
     4.9      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
    4.10      -> cterm -> thm
    4.11 @@ -843,22 +842,12 @@
    4.12  
    4.13  (* store *)
    4.14  
    4.15 -structure Program = Code_Data_Fun
    4.16 +structure Program = Code_Data
    4.17  (
    4.18    type T = naming * program;
    4.19    val empty = (empty_naming, Graph.empty);
    4.20 -  fun purge thy cs (naming, program) =
    4.21 -    let
    4.22 -      val names_delete = cs
    4.23 -        |> map_filter (lookup_const naming)
    4.24 -        |> filter (can (Graph.get_node program))
    4.25 -        |> Graph.all_preds program;
    4.26 -      val program' = Graph.del_nodes names_delete program;
    4.27 -    in (naming, program') end;
    4.28  );
    4.29  
    4.30 -val cached_program = Program.get;
    4.31 -
    4.32  fun invoke_generation thy (algebra, eqngr) f name =
    4.33    Program.change_yield thy (fn naming_program => (NONE, naming_program)
    4.34      |> f thy algebra eqngr name
    4.35 @@ -943,10 +932,10 @@
    4.36  fun code_depgr thy consts =
    4.37    let
    4.38      val (_, eqngr) = Code_Preproc.obtain thy consts [];
    4.39 -    val select = Graph.all_succs eqngr consts;
    4.40 +    val all_consts = Graph.all_succs eqngr consts;
    4.41    in
    4.42      eqngr
    4.43 -    |> not (null consts) ? Graph.subgraph (member (op =) select) 
    4.44 +    |> Graph.subgraph (member (op =) all_consts) 
    4.45      |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
    4.46    end;
    4.47  
    4.48 @@ -983,13 +972,13 @@
    4.49  
    4.50  val _ =
    4.51    OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
    4.52 -    (Scan.repeat P.term_group
    4.53 +    (Scan.repeat1 P.term_group
    4.54        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    4.55          o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
    4.56  
    4.57  val _ =
    4.58    OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
    4.59 -    (Scan.repeat P.term_group
    4.60 +    (Scan.repeat1 P.term_group
    4.61        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    4.62          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
    4.63  
     5.1 --- a/src/Tools/nbe.ML	Wed Dec 23 08:31:14 2009 +0100
     5.2 +++ b/src/Tools/nbe.ML	Wed Dec 23 08:31:15 2009 +0100
     5.3 @@ -505,18 +505,10 @@
     5.4  
     5.5  (* function store *)
     5.6  
     5.7 -structure Nbe_Functions = Code_Data_Fun
     5.8 +structure Nbe_Functions = Code_Data
     5.9  (
    5.10    type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
    5.11    val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
    5.12 -  fun purge thy cs (naming, (gr, (maxidx, idx_tab))) =
    5.13 -    let
    5.14 -      val names_delete = cs
    5.15 -        |> map_filter (Code_Thingol.lookup_const naming)
    5.16 -        |> filter (can (Graph.get_node gr))
    5.17 -        |> Graph.all_preds gr;
    5.18 -      val gr' = Graph.del_nodes names_delete gr;
    5.19 -    in (naming, (gr', (maxidx, idx_tab))) end;
    5.20  );
    5.21  
    5.22  (* compilation, evaluation and reification *)