# HG changeset patch # User haftmann # Date 1262610596 -3600 # Node ID 03f8dcab55f33366d16a2d57bce69ef9907e84c4 # Parent 225daff4323b7439602083a4e0be6dbfdfdcbe6f code cache without copy; tuned diff -r 225daff4323b -r 03f8dcab55f3 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sun Jan 03 15:09:02 2010 +0100 +++ b/src/Pure/Isar/code.ML Mon Jan 04 14:09:56 2010 +0100 @@ -76,8 +76,8 @@ signature CODE_DATA = sig type T - val change: theory -> (T -> T) -> T - val change_yield: theory -> (T -> 'a * T) -> 'a * T + val change: theory -> (theory -> T -> T) -> T + val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T end; signature PRIVATE_CODE = @@ -85,9 +85,9 @@ include CODE val declare_data: Object.T -> serial val change_data: serial * ('a -> Object.T) * (Object.T -> 'a) - -> theory -> ('a -> 'a) -> 'a + -> theory -> (theory -> 'a -> 'a) -> 'a val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a) - -> theory -> ('a -> 'b * 'a) -> 'b * 'a + -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a end; structure Code : PRIVATE_CODE = @@ -234,53 +234,35 @@ local type data = Object.T Datatab.table; -fun create_data data = Synchronized.var "code data" data; -fun empty_data () = create_data Datatab.empty : data Synchronized.var; +fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option); -structure Code_Data = TheoryDataFun +structure Code_Data = Theory_Data ( - type T = spec * data Synchronized.var; + type T = spec * (data * theory_ref) option Synchronized.var; val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty), - (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), empty_data ()); + (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); + val extend = I + fun merge ((spec1, _), (spec2, _)) = + (merge_spec (spec1, spec2), empty_dataref ()); ); -fun thy_data f thy = f ((snd o Code_Data.get) thy); - -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 (Synchronized.change data (Datatab.update (kind, y)); y) end; - in (* access to executable code *) val the_exec = fst o Code_Data.get; -fun map_exec_purge f = - Code_Data.map (fn (exec, data) => (f exec, empty_data ())); +fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ())); -val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ()); +val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ()); 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)); -fun del_eqns c = change_eqns true c (K (false, [])); - (* tackling equation history *) -fun get_eqns thy c = - Symtab.lookup ((the_eqns o the_exec) thy) c - |> Option.map (snd o snd o fst) - |> these; - fun continue_history thy = if (history_concluded o the_exec) thy then thy |> (Code_Data.map o apfst o map_history_concluded) (K false) @@ -297,30 +279,26 @@ #> map_history_concluded (K true)) |> SOME; -val _ = Context.>> (Context.map_theory (Code_Data.init - #> Theory.at_begin continue_history - #> Theory.at_end conclude_history)); +val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history)); (* access to data dependent on abstract executable code *) -fun change_data (kind, mk, dest) = +fun change_yield_data (kind, mk, dest) theory f = let - fun chnge data_ref f = - let - val data = get_ensure_init kind data_ref; - val data' = f (dest data); - in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end; - in thy_data chnge end; + val dataref = (snd o Code_Data.get) theory; + val (datatab, thy, thy_ref) = case Synchronized.value dataref + of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref) + | NONE => (Datatab.empty, theory, Theory.check_thy theory) + val data = case Datatab.lookup datatab kind + of SOME data => data + | NONE => invoke_init kind; + val result as (x, data') = f thy (dest data); + val _ = Synchronized.change dataref + ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); + in result 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, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end; - in thy_data chnge end; +fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd; end; (*local*) @@ -574,7 +552,9 @@ in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end; fun these_eqns thy c = - get_eqns thy c + Symtab.lookup ((the_eqns o the_exec) thy) c + |> Option.map (snd o snd o fst) + |> these |> (map o apfst) (Thm.transfer thy) |> burrow_fst (standard_typscheme thy); @@ -709,38 +689,6 @@ val add_signature_cmd = gen_add_signature read_const read_signature; -(* datatypes *) - -structure Type_Interpretation = - Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); - -fun add_datatype raw_cs thy = - let - val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs; - val (tyco, vs_cos) = constrset_of_consts thy cs; - val old_cs = (map fst o snd o get_datatype thy) tyco; - fun drop_outdated_cases cases = fold Symtab.delete_safe - (Symtab.fold (fn (c, (_, (_, cos))) => - if exists (member (op =) old_cs) cos - then insert (op =) c else I) cases []) cases; - in - thy - |> fold (del_eqns o fst) cs - |> 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 ()) - end; - -fun type_interpretation f = Type_Interpretation.interpretation - (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy); - -fun add_datatype_cmd raw_cs thy = - let - val cs = map (read_bare_const thy) raw_cs; - in add_datatype cs thy end; - - (* code equations *) fun gen_add_eqn default (thm, proper) thy = @@ -773,6 +721,56 @@ of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy | NONE => thy; +fun del_eqns c = change_eqns true c (K (false, [])); + + +(* cases *) + +fun add_case thm thy = + let + val (c, (k, case_pats)) = case_cert thm; + val _ = case filter_out (is_constr thy) case_pats + 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 o map_cases o apfst) (Symtab.update (c, entry)) thy end; + +fun add_undefined c thy = + (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy; + + +(* datatypes *) + +structure Type_Interpretation = + Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); + +fun add_datatype raw_cs thy = + let + val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs; + val (tyco, vs_cos) = constrset_of_consts thy cs; + val old_cs = (map fst o snd o get_datatype thy) tyco; + fun drop_outdated_cases cases = fold Symtab.delete_safe + (Symtab.fold (fn (c, (_, (_, cos))) => + if exists (member (op =) old_cs) cos + then insert (op =) c else I) cases []) cases; + in + thy + |> fold (del_eqns o fst) cs + |> 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 ()) + end; + +fun type_interpretation f = Type_Interpretation.interpretation + (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy); + +fun add_datatype_cmd raw_cs thy = + let + val cs = map (read_bare_const thy) raw_cs; + in add_datatype cs thy end; + + (* c.f. src/HOL/Tools/recfun_codegen.ML *) structure Code_Target_Attr = Theory_Data @@ -789,7 +787,6 @@ let val attr = the_default ((K o K) I) (Code_Target_Attr.get thy); in thy |> add_warning_eqn thm |> attr prefix thm end; - (* setup *) val _ = Context.>> (Context.map_theory @@ -807,21 +804,6 @@ "declare theorems for code generation" end)); - -(* cases *) - -fun add_case thm thy = - let - val (c, (k, case_pats)) = case_cert thm; - val _ = case filter_out (is_constr thy) case_pats - 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 o map_cases o apfst) (Symtab.update (c, entry)) thy end; - -fun add_undefined c thy = - (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy; - end; (*struct*) diff -r 225daff4323b -r 03f8dcab55f3 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Sun Jan 03 15:09:02 2010 +0100 +++ b/src/Tools/Code/code_preproc.ML Mon Jan 04 14:09:56 2010 +0100 @@ -454,8 +454,8 @@ (** retrieval and evaluation interfaces **) -fun obtain thy cs ts = apsnd snd - (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); +fun obtain theory cs ts = apsnd snd + (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts)); fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = let diff -r 225daff4323b -r 03f8dcab55f3 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sun Jan 03 15:09:02 2010 +0100 +++ b/src/Tools/Code/code_thingol.ML Mon Jan 04 14:09:56 2010 +0100 @@ -848,8 +848,8 @@ val empty = (empty_naming, Graph.empty); ); -fun invoke_generation thy (algebra, eqngr) f name = - Program.change_yield thy (fn naming_program => (NONE, naming_program) +fun invoke_generation theory (algebra, eqngr) f name = + Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program) |> f thy algebra eqngr name |-> (fn name => fn (_, naming_program) => (name, naming_program))); diff -r 225daff4323b -r 03f8dcab55f3 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun Jan 03 15:09:02 2010 +0100 +++ b/src/Tools/nbe.ML Mon Jan 04 14:09:56 2010 +0100 @@ -513,15 +513,14 @@ (* compilation, evaluation and reification *) -fun compile_eval thy naming program vs_t deps = +fun compile_eval theory naming program vs_t deps = let - val ctxt = ProofContext.init thy; val (_, (gr, (_, idx_tab))) = - Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd); + Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd); in vs_t - |> eval_term ctxt gr deps - |> term_of_univ thy program idx_tab + |> eval_term (ProofContext.init theory) gr deps + |> term_of_univ theory program idx_tab end; (* evaluation with type reconstruction *)