author haftmann Tue Jul 15 16:02:07 2008 +0200 (2008-07-15) changeset 27609 b23c9ad0fe7d parent 27608 8fd5662ccd97 child 27610 8882d47e075f
tuned code theorem bookkeeping
 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy file | annotate | diff | revisions doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex file | annotate | diff | revisions src/HOL/Library/Efficient_Nat.thy file | annotate | diff | revisions src/Pure/Isar/code.ML file | annotate | diff | revisions src/Tools/code/code_funcgr.ML file | annotate | diff | revisions src/Tools/code/code_name.ML file | annotate | diff | revisions src/Tools/code/code_thingol.ML file | annotate | diff | revisions src/Tools/nbe.ML file | annotate | diff | revisions
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 15:59:49 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 16:02:07 2008 +0200
1.3 @@ -501,8 +501,8 @@
1.4  text {*
1.5    Before selected function theorems are turned into abstract
1.6    code, a chain of definitional transformation steps is carried
1.7 -  out: \emph{preprocessing}.  In essence, the preprocessort
1.8 -  consists of two components: a \emph{simpset} and \emph{function transformators}.
1.9 +  out: \emph{preprocessing}.  In essence, the preprocessor
1.10 +  consists of two components: a \emph{simpset} and \emph{function transformers}.
1.11
1.12    The \emph{simpset} allows to employ the full generality of the Isabelle
1.13    simplifier.  Due to the interpretation of theorems
1.14 @@ -546,22 +546,19 @@
1.15
1.16  text {*
1.17
1.18 -  \emph{Function transformators} provide a most general interface,
1.19 +  \emph{Function transformers} provide a very general interface,
1.20    transforming a list of function theorems to another
1.21    list of function theorems, provided that neither the heading
1.22    constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
1.23    pattern elimination implemented in
1.24 -  theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
1.25 +  theory @{text "Efficient_Nat"} (\secref{eff_nat}) uses this
1.26    interface.
1.27
1.28    \noindent The current setup of the preprocessor may be inspected using
1.29    the @{text "\<PRINTCODESETUP>"} command.
1.30
1.31    \begin{warn}
1.32 -    Preprocessing is \emph{no} fix point process.  Keep this in mind when
1.33 -    setting up the preprocessor.
1.34 -
1.35 -    Further, the attribute \emph{code unfold}
1.36 +    The attribute \emph{code unfold}
1.37      associated with the existing code generator also applies to
1.38      the new one: \emph{code unfold} implies \emph{code inline}.
1.39    \end{warn}
1.40 @@ -1096,7 +1093,7 @@
1.41    @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
1.42    @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
1.43    @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
1.44 -  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list)
1.45 +  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list option)
1.46      -> theory -> theory"} \\
1.47    @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
1.48    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
1.49 @@ -1120,14 +1117,16 @@
1.50    \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
1.51       the preprocessor simpset.
1.52
1.54 -     function transformator @{text f} (named @{text name}) to executable content;
1.55 -     @{text f} is a transformation of the defining equations belonging
1.57 +     function transformer @{text f} (named @{text name}) to executable content;
1.58 +     @{text f} is a transformer of the defining equations belonging
1.59       to a certain function definition, depending on the
1.60 -     current theory context.
1.61 +     current theory context.  Returning @{text NONE} indicates that no
1.62 +     transformation took place;  otherwise, the whole process will be iterated
1.63 +     with the new defining equations.
1.64
1.65    \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
1.66 -     function transformator named @{text name} from executable content.
1.67 +     function transformer named @{text name} from executable content.
1.68
1.70       a datatype to executable content, with generation

     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Jul 15 15:59:49 2008 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Jul 15 16:02:07 2008 +0200
2.3 @@ -615,8 +615,8 @@
2.4  \begin{isamarkuptext}%
2.5  Before selected function theorems are turned into abstract
2.6    code, a chain of definitional transformation steps is carried
2.7 -  out: \emph{preprocessing}.  In essence, the preprocessort
2.8 -  consists of two components: a \emph{simpset} and \emph{function transformators}.
2.9 +  out: \emph{preprocessing}.  In essence, the preprocessor
2.10 +  consists of two components: a \emph{simpset} and \emph{function transformers}.
2.11
2.12    The \emph{simpset} allows to employ the full generality of the Isabelle
2.13    simplifier.  Due to the interpretation of theorems
2.14 @@ -698,22 +698,19 @@
2.15  \end{itemize}
2.16  %
2.17  \begin{isamarkuptext}%
2.18 -\emph{Function transformators} provide a most general interface,
2.19 +\emph{Function transformers} provide a very general interface,
2.20    transforming a list of function theorems to another
2.21    list of function theorems, provided that neither the heading
2.22    constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
2.23    pattern elimination implemented in
2.24 -  theory \isa{EfficientNat} (\secref{eff_nat}) uses this
2.25 +  theory \isa{Efficient{\isacharunderscore}Nat} (\secref{eff_nat}) uses this
2.26    interface.
2.27
2.28    \noindent The current setup of the preprocessor may be inspected using
2.29    the \isa{{\isasymPRINTCODESETUP}} command.
2.30
2.31    \begin{warn}
2.32 -    Preprocessing is \emph{no} fix point process.  Keep this in mind when
2.33 -    setting up the preprocessor.
2.34 -
2.35 -    Further, the attribute \emph{code unfold}
2.36 +    The attribute \emph{code unfold}
2.37      associated with the existing code generator also applies to
2.38      the new one: \emph{code unfold} implies \emph{code inline}.
2.39    \end{warn}%
2.40 @@ -1516,7 +1513,7 @@
2.41    \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
2.42    \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
2.43    \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
2.44 -  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list)|\isasep\isanewline%
2.45 +  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list option)|\isasep\isanewline%
2.46  \verb|    -> theory -> theory| \\
2.47    \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
2.49 @@ -1541,13 +1538,15 @@
2.50       the preprocessor simpset.
2.51
2.53 -     function transformator \isa{f} (named \isa{name}) to executable content;
2.54 -     \isa{f} is a transformation of the defining equations belonging
2.55 +     function transformer \isa{f} (named \isa{name}) to executable content;
2.56 +     \isa{f} is a transformer of the defining equations belonging
2.57       to a certain function definition, depending on the
2.58 -     current theory context.
2.59 +     current theory context.  Returning \isa{NONE} indicates that no
2.60 +     transformation took place;  otherwise, the whole process will be iterated
2.61 +     with the new defining equations.
2.62
2.63    \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
2.64 -     function transformator named \isa{name} from executable content.
2.65 +     function transformer named \isa{name} from executable content.
2.66
2.68       a datatype to executable content, with generation

     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 15:59:49 2008 +0200
3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 16:02:07 2008 +0200
3.3 @@ -119,8 +119,9 @@
3.4  *}
3.5
3.6  (*<*)
3.7 +setup {*
3.8 +let
3.9
3.10 -ML {*
3.11  fun remove_suc thy thms =
3.12    let
3.13      val vname = Name.variant (map fst
3.14 @@ -159,8 +160,7 @@
3.15                let val (ths1, ths2) = split_list thps
3.16                in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
3.17        end
3.18 -  in
3.19 -    case get_first mk_thms eqs of
3.20 +  in case get_first mk_thms eqs of
3.21        NONE => thms
3.22      | SOME x => remove_suc thy x
3.23    end;
3.24 @@ -215,24 +215,31 @@
3.25      then remove_suc_clause thy ths else ths
3.26    end;
3.27
3.28 -fun lift_obj_eq f thy thms =
3.29 -  thms
3.30 -  |> try (
3.31 -    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
3.32 -    #> f thy
3.33 -    #> map (fn thm => thm RS @{thm eq_reflection})
3.34 -    #> map (Conv.fconv_rule Drule.beta_eta_conversion))
3.35 -  |> the_default thms
3.36 -*}
3.37 +fun lift f thy thms1 =
3.38 +  let
3.39 +    val thms2 = Drule.zero_var_indexes_list thms1;
3.40 +    val thms3 = try (map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
3.41 +      #> f thy
3.42 +      #> map (fn thm => thm RS @{thm eq_reflection})
3.43 +      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) thms2;
3.44 +    val thms4 = Option.map Drule.zero_var_indexes_list thms3;
3.45 +  in case thms4
3.46 +   of NONE => NONE
3.47 +    | SOME thms4 => if Thm.eq_thms (thms2, thms4) then NONE else SOME thms4
3.48 +  end
3.49
3.50 -setup {*
3.51 +in
3.52 +
3.55 -  #> Code.add_functrans ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
3.56 -  #> Code.add_functrans ("clause_Suc", lift_obj_eq clause_suc_preproc)
3.57 +  #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
3.58 +  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
3.59 +
3.60 +end;
3.61  *}
3.62  (*>*)
3.63
3.64 +
3.65  subsection {* Target language setup *}
3.66
3.67  text {*

     4.1 --- a/src/Pure/Isar/code.ML	Tue Jul 15 15:59:49 2008 +0200
4.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 15 16:02:07 2008 +0200
4.3 @@ -21,7 +21,7 @@
4.4    val del_inline: thm -> theory -> theory
4.5    val add_post: thm -> theory -> theory
4.6    val del_post: thm -> theory -> theory
4.7 -  val add_functrans: string * (theory -> thm list -> thm list) -> theory -> theory
4.8 +  val add_functrans: string * (theory -> thm list -> thm list option) -> theory -> theory
4.9    val del_functrans: string -> theory -> theory
4.10    val add_datatype: (string * typ) list -> theory -> theory
4.11    val add_datatype_cmd: string list -> theory -> theory
4.12 @@ -54,8 +54,7 @@
4.13  sig
4.14    type T
4.15    val empty: T
4.16 -  val merge: Pretty.pp -> T * T -> T
4.17 -  val purge: theory option -> string list option -> T -> T
4.18 +  val purge: theory -> string list -> T -> T
4.19  end;
4.20
4.21  signature CODE_DATA =
4.22 @@ -69,8 +68,8 @@
4.23  signature PRIVATE_CODE =
4.24  sig
4.25    include CODE
4.26 -  val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
4.27 -    -> (theory option -> string list option -> Object.T -> Object.T) -> serial
4.28 +  val declare_data: Object.T -> (theory -> string list -> Object.T -> Object.T)
4.29 +    -> serial
4.30    val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
4.31      -> theory -> 'a
4.32    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
4.33 @@ -171,10 +170,6 @@
4.34
4.35  fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
4.36
4.37 -
4.38 -(* fundamental melting operations *)
4.39 -(*FIXME delete*)
4.40 -
4.41  fun melt _ ([], []) = (false, [])
4.42    | melt _ ([], ys) = (true, ys)
4.43    | melt eq (xs, ys) = fold_rev
4.44 @@ -200,17 +195,15 @@
4.45          (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
4.46        val (_, dels) = melt_thms
4.47          (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
4.48 -    in (true, ((Susp.delay o K) sels, dels)) end
4.49 +    in ((Susp.delay o K) sels, dels) end
4.50      else let
4.51 -      val (sels_t, sels) = melt_lthms (sels1, sels2);
4.52 -    in (sels_t, (sels, dels)) end
4.53 +      val (_, sels) = melt_lthms (sels1, sels2);
4.54 +    in (sels, dels) end
4.55    end;
4.56
4.57
4.58  (* specification data *)
4.59
4.60 -val merge_funcs = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b));
4.61 -
4.62  val eq_string = op = : string * string -> bool;
4.63  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) =
4.64    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
4.65 @@ -220,11 +213,8 @@
4.66      fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2;
4.67    in Symtab.join join tabs end;
4.68
4.69 -fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
4.70 -  (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2));
4.71 -
4.72  datatype spec = Spec of {
4.73 -  funcs: (bool * sdthms) Symtab.table,
4.74 +  funcs: sdthms Symtab.table,
4.75    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
4.76    cases: (int * string list) Symtab.table * unit Symtab.table
4.77  };
4.78 @@ -233,12 +223,13 @@
4.79    Spec { funcs = funcs, dtyps = dtyps, cases = cases };
4.80  fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
4.81    mk_spec (f (funcs, (dtyps, cases)));
4.82 -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
4.83 -  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
4.84 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) },
4.85 +  Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
4.86    let
4.87 -    val funcs = merge_funcs (funcs1, funcs2);
4.88 +    val funcs = Symtab.join (K melt_sdthms) (funcs1, funcs2);
4.89      val dtyps = merge_dtyps (dtyps1, dtyps2);
4.90 -    val cases = merge_cases (cases1, cases2);
4.91 +    val cases = (Symtab.merge (K true) (cases1, cases2),
4.92 +      Symtab.merge (K true) (undefs1, undefs2));
4.93    in mk_spec (funcs, (dtyps, cases)) end;
4.94
4.95
4.96 @@ -247,7 +238,7 @@
4.97  datatype thmproc = Thmproc of {
4.98    pre: MetaSimplifier.simpset,
4.99    post: MetaSimplifier.simpset,
4.100 -  functrans: (string * (serial * (theory -> thm list -> thm list))) list
4.101 +  functrans: (string * (serial * (theory -> thm list -> thm list option))) list
4.102  };
4.103
4.104  fun mk_thmproc ((pre, post), functrans) =
4.105 @@ -300,8 +291,7 @@
4.106
4.107  type kind = {
4.108    empty: Object.T,
4.109 -  merge: Pretty.pp -> Object.T * Object.T -> Object.T,
4.110 -  purge: theory option -> string list option -> Object.T -> Object.T
4.111 +  purge: theory -> string list -> Object.T -> Object.T
4.112  };
4.113
4.114  val kinds = ref (Datatab.empty: kind Datatab.table);
4.115 @@ -313,22 +303,19 @@
4.116
4.117  in
4.118
4.119 -fun declare_data empty merge purge =
4.120 +fun declare_data empty purge =
4.121    let
4.122      val k = serial ();
4.123 -    val kind = {empty = empty, merge = merge, purge = purge};
4.124 +    val kind = {empty = empty, purge = purge};
4.125      val _ = change kinds (Datatab.update (k, kind));
4.126      val _ = change kind_keys (cons k);
4.127    in k end;
4.128
4.129 -fun invoke_empty k = invoke (fn kind => #empty kind) k;
4.130 +fun invoke_init k = invoke (fn kind => #empty kind) k;
4.131
4.132 -fun invoke_merge_all pp = Datatab.join
4.133 -  (invoke (fn kind => #merge kind pp));
4.134 -
4.135 -fun invoke_purge_all thy_opt cs =
4.136 +fun invoke_purge_all thy cs =
4.137    fold (fn k => Datatab.map_entry k
4.138 -    (invoke (fn kind => #purge kind thy_opt cs) k)) (! kind_keys);
4.139 +    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
4.140
4.141  end; (*local*)
4.142
4.143 @@ -338,20 +325,16 @@
4.144  local
4.145
4.146  type data = Object.T Datatab.table;
4.147 +val empty_data = Datatab.empty : data;
4.148
4.149  structure CodeData = TheoryDataFun
4.150  (
4.151    type T = exec * data ref;
4.152 -  val empty = (empty_exec, ref Datatab.empty : data ref);
4.153 +  val empty = (empty_exec, ref empty_data);
4.154    fun copy (exec, data) = (exec, ref (! data));
4.155    val extend = copy;
4.156    fun merge pp ((exec1, data1), (exec2, data2)) =
4.157 -    let
4.158 -      val exec = merge_exec (exec1, exec2);
4.159 -      val data1' = invoke_purge_all NONE NONE (! data1);
4.160 -      val data2' = invoke_purge_all NONE NONE (! data2);
4.161 -      val data = invoke_merge_all pp (data1', data2');
4.162 -    in (exec, ref data) end;
4.163 +    (merge_exec (exec1, exec2), ref empty_data);
4.164  );
4.165
4.166  val _ = Context.>> (Context.map_theory CodeData.init);
4.167 @@ -361,7 +344,7 @@
4.168  fun get_ensure_init kind data_ref =
4.169    case Datatab.lookup (! data_ref) kind
4.170     of SOME x => x
4.171 -    | NONE => let val y = invoke_empty kind
4.172 +    | NONE => let val y = invoke_init kind
4.173          in (change data_ref (Datatab.update (kind, y)); y) end;
4.174
4.175  in
4.176 @@ -371,8 +354,9 @@
4.177  val the_exec = fst o CodeData.get;
4.178
4.179  fun map_exec_purge touched f thy =
4.180 -  CodeData.map (fn (exec, data) =>
4.181 -    (f exec, ref (invoke_purge_all (SOME thy) touched (! data)))) thy;
4.182 +  CodeData.map (fn (exec, data) => (f exec, ref (case touched
4.183 +   of SOME cs => invoke_purge_all thy cs (! data)
4.184 +    | NONE => empty_data))) thy;
4.185
4.186
4.188 @@ -426,9 +410,8 @@
4.189      val pre = (#pre o the_thmproc) exec;
4.190      val post = (#post o the_thmproc) exec;
4.191      val functrans = (map fst o #functrans o the_thmproc) exec;
4.192 -    val funs = the_funcs exec
4.193 +    val funcs = the_funcs exec
4.194        |> Symtab.dest
4.195 -      |> (map o apsnd) snd
4.196        |> (map o apfst) (CodeUnit.string_of_const thy)
4.197        |> sort (string_ord o pairself fst);
4.198      val dtyps = the_dtyps exec
4.199 @@ -441,7 +424,7 @@
4.200        Pretty.block (
4.201          Pretty.str "defining equations:"
4.202          :: Pretty.fbrk
4.203 -        :: (Pretty.fbreaks o map pretty_func) funs
4.204 +        :: (Pretty.fbreaks o map pretty_func) funcs
4.205        ),
4.206        Pretty.block [
4.207          Pretty.str "preprocessing simpset:",
4.208 @@ -454,7 +437,7 @@
4.209          MetaSimplifier.pretty_ss post
4.210        ],
4.211        Pretty.block (
4.212 -        Pretty.str "function transformators:"
4.213 +        Pretty.str "function transformers:"
4.214          :: Pretty.fbrk
4.215          :: (Pretty.fbreaks o map Pretty.str) functrans
4.216        ),
4.217 @@ -527,7 +510,7 @@
4.218      val funcs = classparams
4.219        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
4.220        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
4.221 -      |> (map o Option.map) (Susp.force o fst o snd)
4.222 +      |> (map o Option.map) (Susp.force o fst)
4.223        |> maps these
4.224        |> map (Thm.transfer thy)
4.225      fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
4.226 @@ -704,7 +687,7 @@
4.227        else ();
4.228    in
4.229      (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
4.230 -      (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
4.231 +      (c, (Susp.value [], [])) (add_thm func)) thy
4.232    end;
4.233
4.234  fun add_liberal_func thm thy =
4.235 @@ -716,7 +699,7 @@
4.236            then thy
4.237            else map_exec_purge (SOME [c]) (map_funcs
4.238              (Symtab.map_default
4.239 -              (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
4.240 +              (c, (Susp.value [], [])) (add_thm func))) thy
4.241          end
4.242      | NONE => thy;
4.243
4.244 @@ -729,7 +712,7 @@
4.245            then thy
4.246            else map_exec_purge (SOME [c]) (map_funcs
4.247            (Symtab.map_default
4.248 -            (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
4.249 +            (c, (Susp.value [], [])) (add_thm func))) thy
4.250          end
4.251      | NONE => thy;
4.252
4.253 @@ -738,12 +721,12 @@
4.254     of SOME func => let
4.255            val c = const_of_func thy func;
4.256          in map_exec_purge (SOME [c]) (map_funcs
4.257 -          (Symtab.map_entry c (apsnd (del_thm func)))) thy
4.258 +          (Symtab.map_entry c (del_thm func))) thy
4.259          end
4.260      | NONE => thy;
4.261
4.262  fun del_funcs const = map_exec_purge (SOME [const])
4.263 -  (map_funcs (Symtab.map_entry const (apsnd del_thms)));
4.264 +  (map_funcs (Symtab.map_entry const del_thms));
4.265
4.266  fun add_funcl (const, lthms) thy =
4.267    let
4.268 @@ -752,8 +735,8 @@
4.269          alas, naive checking results in non-termination!*)
4.270    in
4.271      map_exec_purge (SOME [const])
4.272 -      (map_funcs (Symtab.map_default (const, (false, (Susp.value [], [])))
4.273 -      (apsnd (add_lthms lthms')))) thy
4.274 +      (map_funcs (Symtab.map_default (const, (Susp.value [], []))
4.276    end;
4.277
4.278  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
4.279 @@ -819,7 +802,7 @@
4.280
4.281  fun del_functrans name =
4.282    (map_exec_purge NONE o map_thmproc o apsnd)
4.283 -    (delete_force "function transformator" name);
4.284 +    (delete_force "function transformer" name);
4.285
4.286  val _ = Context.>> (Context.map_theory
4.287    (let
4.288 @@ -841,11 +824,13 @@
4.289
4.290  local
4.291
4.292 -fun apply_functrans thy f [] = []
4.293 -  | apply_functrans thy f (thms as (thm :: _)) =
4.294 +fun apply_functrans thy [] = []
4.295 +  | apply_functrans thy (thms as thm :: _) =
4.296        let
4.297          val const = const_of_func thy thm;
4.298 -        val thms' = f thy thms;
4.299 +        val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
4.300 +          o the_thmproc o the_exec) thy;
4.301 +        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) thms;
4.302        in certify_const thy const thms' end;
4.303
4.304  fun rhs_conv conv thm =
4.305 @@ -867,7 +852,7 @@
4.306      val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
4.307    in
4.308      thms
4.309 -    |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy)
4.310 +    |> apply_functrans thy
4.311      |> map (CodeUnit.rewrite_func pre)
4.312      (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
4.314 @@ -913,7 +898,7 @@
4.315
4.316  fun get_funcs thy const =
4.317    Symtab.lookup ((the_funcs o the_exec) thy) const
4.318 -  |> Option.map (Susp.force o fst o snd)
4.319 +  |> Option.map (Susp.force o fst)
4.320    |> these
4.321    |> map (Thm.transfer thy);
4.322
4.323 @@ -950,8 +935,7 @@
4.324  fun dest (Data x) = x
4.325
4.326  val kind = Code.declare_data (Data Data.empty)
4.327 -  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
4.328 -  (fn thy_opt => fn cs => fn Data x => Data (Data.purge thy_opt cs x));
4.329 +  (fn thy => fn cs => fn Data x => Data (Data.purge thy cs x));
4.330
4.331  val data_op = (kind, Data, dest);
4.332

     5.1 --- a/src/Tools/code/code_funcgr.ML	Tue Jul 15 15:59:49 2008 +0200
5.2 +++ b/src/Tools/code/code_funcgr.ML	Tue Jul 15 16:02:07 2008 +0200
5.3 @@ -261,11 +261,9 @@
5.4  (
5.5    type T = T;
5.6    val empty = Graph.empty;
5.7 -  fun merge _ _ = Graph.empty;
5.8 -  fun purge _ NONE _ = Graph.empty
5.9 -    | purge _ (SOME cs) funcgr =
5.10 -        Graph.del_nodes ((Graph.all_preds funcgr
5.11 -          o filter (can (Graph.get_node funcgr))) cs) funcgr;
5.12 +  fun purge _ cs funcgr =
5.13 +    Graph.del_nodes ((Graph.all_preds funcgr
5.14 +      o filter (can (Graph.get_node funcgr))) cs) funcgr;
5.15  );
5.16
5.17  fun make thy =

     6.1 --- a/src/Tools/code/code_name.ML	Tue Jul 15 15:59:49 2008 +0200
6.2 +++ b/src/Tools/code/code_name.ML	Tue Jul 15 16:02:07 2008 +0200
6.3 @@ -303,12 +303,8 @@
6.4  (
6.5    type T = const Symtab.table * string Symtab.table;
6.6    val empty = (Symtab.empty, Symtab.empty);
6.7 -  fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
6.8 -    (Symtab.merge (op =) (const1, const2),
6.9 -      Symtab.merge (op =) (constrev1, constrev2));
6.10 -  fun purge _ NONE _ = empty
6.11 -    | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
6.12 -        fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
6.13 +  fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
6.14 +    fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
6.15  );
6.16
6.17  val setup = CodeName.init;

     7.1 --- a/src/Tools/code/code_thingol.ML	Tue Jul 15 15:59:49 2008 +0200
7.2 +++ b/src/Tools/code/code_thingol.ML	Tue Jul 15 16:02:07 2008 +0200
7.3 @@ -569,18 +569,15 @@
7.4  (
7.5    type T = program;
7.6    val empty = Graph.empty;
7.7 -  fun merge _ = Graph.merge (K true);
7.8 -  fun purge _ NONE _ = Graph.empty
7.9 -    | purge NONE _ _ = Graph.empty
7.10 -    | purge (SOME thy) (SOME cs) program =
7.11 -        let
7.12 -          val cs_exisiting =
7.13 -            map_filter (CodeName.const_rev thy) (Graph.keys program);
7.14 -          val dels = (Graph.all_preds program
7.15 -              o map (CodeName.const thy)
7.16 -              o filter (member (op =) cs_exisiting)
7.17 -            ) cs;
7.18 -        in Graph.del_nodes dels program end;
7.19 +  fun purge thy cs program =
7.20 +    let
7.21 +      val cs_exisiting =
7.22 +        map_filter (CodeName.const_rev thy) (Graph.keys program);
7.23 +      val dels = (Graph.all_preds program
7.24 +          o map (CodeName.const thy)
7.25 +          o filter (member (op =) cs_exisiting)
7.26 +        ) cs;
7.27 +    in Graph.del_nodes dels program end;
7.28  );
7.29
7.30  val cached_program = Program.get;

     8.1 --- a/src/Tools/nbe.ML	Tue Jul 15 15:59:49 2008 +0200
8.2 +++ b/src/Tools/nbe.ML	Tue Jul 15 16:02:07 2008 +0200
8.3 @@ -346,20 +346,15 @@
8.4  (
8.5    type T = (Univ option * int) Graph.T * (int * string Inttab.table);
8.6    val empty = (Graph.empty, (0, Inttab.empty));
8.7 -  fun merge _ ((gr1, (maxidx1, idx_tab1)), (gr2, (maxidx2, idx_tab2))) =
8.8 -    (Graph.merge (K true) (gr1, gr2), (IntInf.max (maxidx1, maxidx2),
8.9 -      Inttab.merge (K true) (idx_tab1, idx_tab2)));
8.10 -  fun purge _ NONE _ = empty
8.11 -    | purge NONE _ _ = empty
8.12 -    | purge (SOME thy) (SOME cs) (gr, (maxidx, idx_tab)) =
8.13 -        let
8.14 -          val cs_exisiting =
8.15 -            map_filter (CodeName.const_rev thy) (Graph.keys gr);
8.16 -          val dels = (Graph.all_preds gr
8.17 -              o map (CodeName.const thy)
8.18 -              o filter (member (op =) cs_exisiting)
8.19 -            ) cs;
8.20 -        in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
8.21 +  fun purge thy cs (gr, (maxidx, idx_tab)) =
8.22 +    let
8.23 +      val cs_exisiting =
8.24 +        map_filter (CodeName.const_rev thy) (Graph.keys gr);
8.25 +      val dels = (Graph.all_preds gr
8.26 +          o map (CodeName.const thy)
8.27 +          o filter (member (op =) cs_exisiting)
8.28 +        ) cs;
8.29 +    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
8.30  );
8.31
8.32  (* compilation, evaluation and reification *)