tuned code theorem bookkeeping
authorhaftmann
Tue Jul 15 16:02:07 2008 +0200 (2008-07-15)
changeset 27609b23c9ad0fe7d
parent 27608 8fd5662ccd97
child 27610 8882d47e075f
tuned code theorem bookkeeping
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
src/HOL/Library/Efficient_Nat.thy
src/Pure/Isar/code.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_name.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     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.53 -    \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    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.56 +  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    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.69    \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    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.48    \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    2.49 @@ -1541,13 +1538,15 @@
    2.50       the preprocessor simpset.
    2.51  
    2.52      \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
    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.67    \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
    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.53    Codegen.add_preprocessor eqn_suc_preproc
    3.54    #> Codegen.add_preprocessor clause_suc_preproc
    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.187  (* access to data dependent on abstract executable content *)
   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.275 +      (add_lthms lthms'))) thy
   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.313      |> map (AxClass.unoverload thy)
   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 *)