code cache without copy; tuned
authorhaftmann
Mon Jan 04 14:09:56 2010 +0100 (2010-01-04)
changeset 3424403f8dcab55f3
parent 34237 225daff4323b
child 34245 25bd3ed2ac9f
code cache without copy; tuned
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/code.ML	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Jan 04 14:09:56 2010 +0100
     1.3 @@ -76,8 +76,8 @@
     1.4  signature CODE_DATA =
     1.5  sig
     1.6    type T
     1.7 -  val change: theory -> (T -> T) -> T
     1.8 -  val change_yield: theory -> (T -> 'a * T) -> 'a * T
     1.9 +  val change: theory -> (theory -> T -> T) -> T
    1.10 +  val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
    1.11  end;
    1.12  
    1.13  signature PRIVATE_CODE =
    1.14 @@ -85,9 +85,9 @@
    1.15    include CODE
    1.16    val declare_data: Object.T -> serial
    1.17    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.18 -    -> theory -> ('a -> 'a) -> 'a
    1.19 +    -> theory -> (theory -> 'a -> 'a) -> 'a
    1.20    val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.21 -    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
    1.22 +    -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
    1.23  end;
    1.24  
    1.25  structure Code : PRIVATE_CODE =
    1.26 @@ -234,53 +234,35 @@
    1.27  local
    1.28  
    1.29  type data = Object.T Datatab.table;
    1.30 -fun create_data data = Synchronized.var "code data" data;
    1.31 -fun empty_data () = create_data Datatab.empty : data Synchronized.var;
    1.32 +fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
    1.33  
    1.34 -structure Code_Data = TheoryDataFun
    1.35 +structure Code_Data = Theory_Data
    1.36  (
    1.37 -  type T = spec * data Synchronized.var;
    1.38 +  type T = spec * (data * theory_ref) option Synchronized.var;
    1.39    val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    1.40 -    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
    1.41 -  fun copy (spec, data) = (spec, create_data (Synchronized.value data));
    1.42 -  val extend = copy;
    1.43 -  fun merge _ ((spec1, _), (spec2, _)) =
    1.44 -    (merge_spec (spec1, spec2), empty_data ());
    1.45 +    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
    1.46 +  val extend = I
    1.47 +  fun merge ((spec1, _), (spec2, _)) =
    1.48 +    (merge_spec (spec1, spec2), empty_dataref ());
    1.49  );
    1.50  
    1.51 -fun thy_data f thy = f ((snd o Code_Data.get) thy);
    1.52 -
    1.53 -fun get_ensure_init kind data =
    1.54 -  case Datatab.lookup (Synchronized.value data) kind
    1.55 -   of SOME x => x
    1.56 -    | NONE => let val y = invoke_init kind
    1.57 -        in (Synchronized.change data (Datatab.update (kind, y)); y) end;
    1.58 -
    1.59  in
    1.60  
    1.61  (* access to executable code *)
    1.62  
    1.63  val the_exec = fst o Code_Data.get;
    1.64  
    1.65 -fun map_exec_purge f =
    1.66 -  Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
    1.67 +fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
    1.68  
    1.69 -val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
    1.70 +val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
    1.71  
    1.72  fun change_eqns delete c f = (map_exec_purge o map_eqns
    1.73    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
    1.74      o apfst) (fn (_, eqns) => (true, f eqns));
    1.75  
    1.76 -fun del_eqns c = change_eqns true c (K (false, []));
    1.77 -
    1.78  
    1.79  (* tackling equation history *)
    1.80  
    1.81 -fun get_eqns thy c =
    1.82 -  Symtab.lookup ((the_eqns o the_exec) thy) c
    1.83 -  |> Option.map (snd o snd o fst)
    1.84 -  |> these;
    1.85 -
    1.86  fun continue_history thy = if (history_concluded o the_exec) thy
    1.87    then thy
    1.88      |> (Code_Data.map o apfst o map_history_concluded) (K false)
    1.89 @@ -297,30 +279,26 @@
    1.90          #> map_history_concluded (K true))
    1.91      |> SOME;
    1.92  
    1.93 -val _ = Context.>> (Context.map_theory (Code_Data.init
    1.94 -  #> Theory.at_begin continue_history
    1.95 -  #> Theory.at_end conclude_history));
    1.96 +val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history));
    1.97  
    1.98  
    1.99  (* access to data dependent on abstract executable code *)
   1.100  
   1.101 -fun change_data (kind, mk, dest) =
   1.102 +fun change_yield_data (kind, mk, dest) theory f =
   1.103    let
   1.104 -    fun chnge data_ref f =
   1.105 -      let
   1.106 -        val data = get_ensure_init kind data_ref;
   1.107 -        val data' = f (dest data);
   1.108 -      in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   1.109 -  in thy_data chnge end;
   1.110 +    val dataref = (snd o Code_Data.get) theory;
   1.111 +    val (datatab, thy, thy_ref) = case Synchronized.value dataref
   1.112 +     of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
   1.113 +      | NONE => (Datatab.empty, theory, Theory.check_thy theory)
   1.114 +    val data = case Datatab.lookup datatab kind
   1.115 +     of SOME data => data
   1.116 +      | NONE => invoke_init kind;
   1.117 +    val result as (x, data') = f thy (dest data);
   1.118 +    val _ = Synchronized.change dataref
   1.119 +      ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
   1.120 +  in result end;
   1.121  
   1.122 -fun change_yield_data (kind, mk, dest) =
   1.123 -  let
   1.124 -    fun chnge data_ref f =
   1.125 -      let
   1.126 -        val data = get_ensure_init kind data_ref;
   1.127 -        val (x, data') = f (dest data);
   1.128 -      in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   1.129 -  in thy_data chnge end;
   1.130 +fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
   1.131  
   1.132  end; (*local*)
   1.133  
   1.134 @@ -574,7 +552,9 @@
   1.135    in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
   1.136  
   1.137  fun these_eqns thy c =
   1.138 -  get_eqns thy c
   1.139 +  Symtab.lookup ((the_eqns o the_exec) thy) c
   1.140 +  |> Option.map (snd o snd o fst)
   1.141 +  |> these
   1.142    |> (map o apfst) (Thm.transfer thy)
   1.143    |> burrow_fst (standard_typscheme thy);
   1.144  
   1.145 @@ -709,38 +689,6 @@
   1.146  val add_signature_cmd = gen_add_signature read_const read_signature;
   1.147  
   1.148  
   1.149 -(* datatypes *)
   1.150 -
   1.151 -structure Type_Interpretation =
   1.152 -  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   1.153 -
   1.154 -fun add_datatype raw_cs thy =
   1.155 -  let
   1.156 -    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
   1.157 -    val (tyco, vs_cos) = constrset_of_consts thy cs;
   1.158 -    val old_cs = (map fst o snd o get_datatype thy) tyco;
   1.159 -    fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.160 -      (Symtab.fold (fn (c, (_, (_, cos))) =>
   1.161 -        if exists (member (op =) old_cs) cos
   1.162 -          then insert (op =) c else I) cases []) cases;
   1.163 -  in
   1.164 -    thy
   1.165 -    |> fold (del_eqns o fst) cs
   1.166 -    |> map_exec_purge
   1.167 -        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.168 -        #> (map_cases o apfst) drop_outdated_cases)
   1.169 -    |> Type_Interpretation.data (tyco, serial ())
   1.170 -  end;
   1.171 -
   1.172 -fun type_interpretation f =  Type_Interpretation.interpretation
   1.173 -  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   1.174 -
   1.175 -fun add_datatype_cmd raw_cs thy =
   1.176 -  let
   1.177 -    val cs = map (read_bare_const thy) raw_cs;
   1.178 -  in add_datatype cs thy end;
   1.179 -
   1.180 -
   1.181  (* code equations *)
   1.182  
   1.183  fun gen_add_eqn default (thm, proper) thy =
   1.184 @@ -773,6 +721,56 @@
   1.185   of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   1.186    | NONE => thy;
   1.187  
   1.188 +fun del_eqns c = change_eqns true c (K (false, []));
   1.189 +
   1.190 +
   1.191 +(* cases *)
   1.192 +
   1.193 +fun add_case thm thy =
   1.194 +  let
   1.195 +    val (c, (k, case_pats)) = case_cert thm;
   1.196 +    val _ = case filter_out (is_constr thy) case_pats
   1.197 +     of [] => ()
   1.198 +      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.199 +    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.200 +  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.201 +
   1.202 +fun add_undefined c thy =
   1.203 +  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.204 +
   1.205 +
   1.206 +(* datatypes *)
   1.207 +
   1.208 +structure Type_Interpretation =
   1.209 +  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   1.210 +
   1.211 +fun add_datatype raw_cs thy =
   1.212 +  let
   1.213 +    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
   1.214 +    val (tyco, vs_cos) = constrset_of_consts thy cs;
   1.215 +    val old_cs = (map fst o snd o get_datatype thy) tyco;
   1.216 +    fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.217 +      (Symtab.fold (fn (c, (_, (_, cos))) =>
   1.218 +        if exists (member (op =) old_cs) cos
   1.219 +          then insert (op =) c else I) cases []) cases;
   1.220 +  in
   1.221 +    thy
   1.222 +    |> fold (del_eqns o fst) cs
   1.223 +    |> map_exec_purge
   1.224 +        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.225 +        #> (map_cases o apfst) drop_outdated_cases)
   1.226 +    |> Type_Interpretation.data (tyco, serial ())
   1.227 +  end;
   1.228 +
   1.229 +fun type_interpretation f =  Type_Interpretation.interpretation
   1.230 +  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   1.231 +
   1.232 +fun add_datatype_cmd raw_cs thy =
   1.233 +  let
   1.234 +    val cs = map (read_bare_const thy) raw_cs;
   1.235 +  in add_datatype cs thy end;
   1.236 +
   1.237 +
   1.238  (* c.f. src/HOL/Tools/recfun_codegen.ML *)
   1.239  
   1.240  structure Code_Target_Attr = Theory_Data
   1.241 @@ -789,7 +787,6 @@
   1.242    let
   1.243      val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
   1.244    in thy |> add_warning_eqn thm |> attr prefix thm end;
   1.245 -
   1.246  (* setup *)
   1.247  
   1.248  val _ = Context.>> (Context.map_theory
   1.249 @@ -807,21 +804,6 @@
   1.250          "declare theorems for code generation"
   1.251    end));
   1.252  
   1.253 -
   1.254 -(* cases *)
   1.255 -
   1.256 -fun add_case thm thy =
   1.257 -  let
   1.258 -    val (c, (k, case_pats)) = case_cert thm;
   1.259 -    val _ = case filter_out (is_constr thy) case_pats
   1.260 -     of [] => ()
   1.261 -      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.262 -    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.263 -  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.264 -
   1.265 -fun add_undefined c thy =
   1.266 -  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.267 -
   1.268  end; (*struct*)
   1.269  
   1.270  
     2.1 --- a/src/Tools/Code/code_preproc.ML	Sun Jan 03 15:09:02 2010 +0100
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Jan 04 14:09:56 2010 +0100
     2.3 @@ -454,8 +454,8 @@
     2.4  
     2.5  (** retrieval and evaluation interfaces **)
     2.6  
     2.7 -fun obtain thy cs ts = apsnd snd
     2.8 -  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
     2.9 +fun obtain theory cs ts = apsnd snd
    2.10 +  (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
    2.11  
    2.12  fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    2.13    let
     3.1 --- a/src/Tools/Code/code_thingol.ML	Sun Jan 03 15:09:02 2010 +0100
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jan 04 14:09:56 2010 +0100
     3.3 @@ -848,8 +848,8 @@
     3.4    val empty = (empty_naming, Graph.empty);
     3.5  );
     3.6  
     3.7 -fun invoke_generation thy (algebra, eqngr) f name =
     3.8 -  Program.change_yield thy (fn naming_program => (NONE, naming_program)
     3.9 +fun invoke_generation theory (algebra, eqngr) f name =
    3.10 +  Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
    3.11      |> f thy algebra eqngr name
    3.12      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
    3.13  
     4.1 --- a/src/Tools/nbe.ML	Sun Jan 03 15:09:02 2010 +0100
     4.2 +++ b/src/Tools/nbe.ML	Mon Jan 04 14:09:56 2010 +0100
     4.3 @@ -513,15 +513,14 @@
     4.4  
     4.5  (* compilation, evaluation and reification *)
     4.6  
     4.7 -fun compile_eval thy naming program vs_t deps =
     4.8 +fun compile_eval theory naming program vs_t deps =
     4.9    let
    4.10 -    val ctxt = ProofContext.init thy;
    4.11      val (_, (gr, (_, idx_tab))) =
    4.12 -      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
    4.13 +      Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
    4.14    in
    4.15      vs_t
    4.16 -    |> eval_term ctxt gr deps
    4.17 -    |> term_of_univ thy program idx_tab
    4.18 +    |> eval_term (ProofContext.init theory) gr deps
    4.19 +    |> term_of_univ theory program idx_tab
    4.20    end;
    4.21  
    4.22  (* evaluation with type reconstruction *)