1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Jul 14 11:04:42 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Jul 14 11:04:46 2008 +0200
     1.3 @@ -501,16 +501,16 @@
     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}. There are three possibilities
     1.8 -  to customize preprocessing: \emph{inline theorems},
     1.9 -  \emph{inline procedures} and \emph{generic preprocessors}.
    1.10 +  out: \emph{preprocessing}.  In essence, the preprocessort
    1.11 +  consists of two components: a \emph{simpset} and \emph{function transformators}.
    1.12  
    1.13 -  \emph{Inline theorems} are rewriting rules applied to each
    1.14 -  defining equation.  Due to the interpretation of theorems
    1.15 +  The \emph{simpset} allows to employ the full generality of the Isabelle
    1.16 +  simplifier.  Due to the interpretation of theorems
    1.17    of defining equations, rewrites are applied to the right
    1.18    hand side and the arguments of the left hand side of an
    1.19    equation, but never to the constant heading the left hand side.
    1.20 -  Inline theorems may be declared an undeclared using the
    1.21 +  An important special case are \emph{inline theorems} which may be
    1.22 +  declared an undeclared using the
    1.23    \emph{code inline} or \emph{code inline del} attribute respectively.
    1.24    Some common applications:
    1.25  *}
    1.26 @@ -545,17 +545,8 @@
    1.27  *}
    1.28  
    1.29  text {*
    1.30 -  \noindent The current set of inline theorems may be inspected using
    1.31 -  the @{text "\<PRINTCODESETUP>"} command.
    1.32  
    1.33 -  \emph{Inline procedures} are a generalized version of inline
    1.34 -  theorems written in ML -- rewrite rules are generated dependent
    1.35 -  on the function theorems for a certain function.  One
    1.36 -  application is the implicit expanding of @{typ nat} numerals
    1.37 -  to @{term "0\<Colon>nat"} / @{const Suc} representation.  See further
    1.38 -  \secref{sec:ml}
    1.39 -
    1.40 -  \emph{Generic preprocessors} provide a most general interface,
    1.41 +  \emph{Function transformators} provide a most general interface,
    1.42    transforming a list of function theorems to another
    1.43    list of function theorems, provided that neither the heading
    1.44    constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
    1.45 @@ -563,10 +554,11 @@
    1.46    theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
    1.47    interface.
    1.48  
    1.49 +  \noindent The current setup of the preprocessor may be inspected using
    1.50 +  the @{text "\<PRINTCODESETUP>"} command.
    1.51 +
    1.52    \begin{warn}
    1.53 -    The order in which single preprocessing steps are carried
    1.54 -    out currently is not specified; in particular, preprocessing
    1.55 -    is \emph{no} fix point process.  Keep this in mind when
    1.56 +    Preprocessing is \emph{no} fix point process.  Keep this in mind when
    1.57      setting up the preprocessor.
    1.58  
    1.59      Further, the attribute \emph{code unfold}
    1.60 @@ -1102,14 +1094,11 @@
    1.61    @{index_ML Code.add_func: "thm -> theory -> theory"} \\
    1.62    @{index_ML Code.del_func: "thm -> theory -> theory"} \\
    1.63    @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
    1.64 -  @{index_ML Code.add_inline: "thm -> theory -> theory"} \\
    1.65 -  @{index_ML Code.del_inline: "thm -> theory -> theory"} \\
    1.66 -  @{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list)
    1.67 +  @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.68 +  @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.69 +  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list)
    1.70      -> theory -> theory"} \\
    1.71 -  @{index_ML Code.del_inline_proc: "string -> theory -> theory"} \\
    1.72 -  @{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list)
    1.73 -    -> theory -> theory"} \\
    1.74 -  @{index_ML Code.del_preproc: "string -> theory -> theory"} \\
    1.75 +  @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
    1.76    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.77    @{index_ML Code.get_datatype: "theory -> string
    1.78      -> (string * sort) list * (string * typ list) list"} \\
    1.79 @@ -1128,30 +1117,17 @@
    1.80       suspended defining equations @{text lthms} for constant
    1.81       @{text const} to executable content.
    1.82  
    1.83 -  \item @{ML Code.add_inline}~@{text "thm"}~@{text "thy"} adds
    1.84 -     inlining theorem @{text thm} to executable content.
    1.85 +  \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
    1.86 +     the preprocessor simpset.
    1.87  
    1.88 -  \item @{ML Code.del_inline}~@{text "thm"}~@{text "thy"} remove
    1.89 -     inlining theorem @{text thm} from executable content, if present.
    1.90 -
    1.91 -  \item @{ML Code.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
    1.92 -     inline procedure @{text f} (named @{text name}) to executable content;
    1.93 -     @{text f} is a computation of rewrite rules dependent on
    1.94 -     the current theory context and the list of all arguments
    1.95 -     and right hand sides of the defining equations belonging
    1.96 -     to a certain function definition.
    1.97 -
    1.98 -  \item @{ML Code.del_inline_proc}~@{text "name"}~@{text "thy"} removes
    1.99 -     inline procedure named @{text name} from executable content.
   1.100 -
   1.101 -  \item @{ML Code.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
   1.102 -     generic preprocessor @{text f} (named @{text name}) to executable content;
   1.103 +    \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
   1.104 +     function transformator @{text f} (named @{text name}) to executable content;
   1.105       @{text f} is a transformation of the defining equations belonging
   1.106       to a certain function definition, depending on the
   1.107       current theory context.
   1.108  
   1.109 -  \item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes
   1.110 -     generic preprcoessor named @{text name} from executable content.
   1.111 +  \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
   1.112 +     function transformator named @{text name} from executable content.
   1.113  
   1.114    \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
   1.115       a datatype to executable content, with generation
   1.116 @@ -1171,7 +1147,7 @@
   1.117    \begin{mldecls}
   1.118    @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\
   1.119    @{index_ML CodeUnit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
   1.120 -  @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\
   1.121 +  @{index_ML CodeUnit.rewrite_func: "MetaSimplifier.simpset -> thm -> thm"} \\
   1.122    \end{mldecls}
   1.123  
   1.124    \begin{description}
   1.125 @@ -1182,9 +1158,9 @@
   1.126    \item @{ML CodeUnit.head_func}~@{text thm}
   1.127       extracts the constant and its type from a defining equation @{text thm}.
   1.128  
   1.129 -  \item @{ML CodeUnit.rewrite_func}~@{text rews}~@{text thm}
   1.130 -     rewrites a defining equation @{text thm} with a set of rewrite
   1.131 -     rules @{text rews}; only arguments and right hand side are rewritten,
   1.132 +  \item @{ML CodeUnit.rewrite_func}~@{text ss}~@{text thm}
   1.133 +     rewrites a defining equation @{text thm} with a simpset @{text ss};
   1.134 +     only arguments and right hand side are rewritten,
   1.135       not the head of the defining equation.
   1.136  
   1.137    \end{description}

     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Jul 14 11:04:42 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Jul 14 11:04:46 2008 +0200
     2.3 @@ -615,16 +615,16 @@
     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}. There are three possibilities
     2.8 -  to customize preprocessing: \emph{inline theorems},
     2.9 -  \emph{inline procedures} and \emph{generic preprocessors}.
    2.10 +  out: \emph{preprocessing}.  In essence, the preprocessort
    2.11 +  consists of two components: a \emph{simpset} and \emph{function transformators}.
    2.12  
    2.13 -  \emph{Inline theorems} are rewriting rules applied to each
    2.14 -  defining equation.  Due to the interpretation of theorems
    2.15 +  The \emph{simpset} allows to employ the full generality of the Isabelle
    2.16 +  simplifier.  Due to the interpretation of theorems
    2.17    of defining equations, rewrites are applied to the right
    2.18    hand side and the arguments of the left hand side of an
    2.19    equation, but never to the constant heading the left hand side.
    2.20 -  Inline theorems may be declared an undeclared using the
    2.21 +  An important special case are \emph{inline theorems} which may be
    2.22 +  declared an undeclared using the
    2.23    \emph{code inline} or \emph{code inline del} attribute respectively.
    2.24    Some common applications:%
    2.25  \end{isamarkuptext}%
    2.26 @@ -698,17 +698,7 @@
    2.27  \end{itemize}
    2.28  %
    2.29  \begin{isamarkuptext}%
    2.30 -\noindent The current set of inline theorems may be inspected using
    2.31 -  the \isa{{\isasymPRINTCODESETUP}} command.
    2.32 -
    2.33 -  \emph{Inline procedures} are a generalized version of inline
    2.34 -  theorems written in ML -- rewrite rules are generated dependent
    2.35 -  on the function theorems for a certain function.  One
    2.36 -  application is the implicit expanding of \isa{nat} numerals
    2.37 -  to \isa{{\isadigit{0}}} / \isa{Suc} representation.  See further
    2.38 -  \secref{sec:ml}
    2.39 -
    2.40 -  \emph{Generic preprocessors} provide a most general interface,
    2.41 +\emph{Function transformators} provide a most general interface,
    2.42    transforming a list of function theorems to another
    2.43    list of function theorems, provided that neither the heading
    2.44    constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
    2.45 @@ -716,10 +706,11 @@
    2.46    theory \isa{EfficientNat} (\secref{eff_nat}) uses this
    2.47    interface.
    2.48  
    2.49 +  \noindent The current setup of the preprocessor may be inspected using
    2.50 +  the \isa{{\isasymPRINTCODESETUP}} command.
    2.51 +
    2.52    \begin{warn}
    2.53 -    The order in which single preprocessing steps are carried
    2.54 -    out currently is not specified; in particular, preprocessing
    2.55 -    is \emph{no} fix point process.  Keep this in mind when
    2.56 +    Preprocessing is \emph{no} fix point process.  Keep this in mind when
    2.57      setting up the preprocessor.
    2.58  
    2.59      Further, the attribute \emph{code unfold}
    2.60 @@ -1523,14 +1514,11 @@
    2.61    \indexml{Code.add\_func}\verb|Code.add_func: thm -> theory -> theory| \\
    2.62    \indexml{Code.del\_func}\verb|Code.del_func: thm -> theory -> theory| \\
    2.63    \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
    2.64 -  \indexml{Code.add\_inline}\verb|Code.add_inline: thm -> theory -> theory| \\
    2.65 -  \indexml{Code.del\_inline}\verb|Code.del_inline: thm -> theory -> theory| \\
    2.66 -  \indexml{Code.add\_inline\_proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
    2.67 +  \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
    2.68 +  \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
    2.69 +  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list)|\isasep\isanewline%
    2.70  \verb|    -> theory -> theory| \\
    2.71 -  \indexml{Code.del\_inline\_proc}\verb|Code.del_inline_proc: string -> theory -> theory| \\
    2.72 -  \indexml{Code.add\_preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
    2.73 -\verb|    -> theory -> theory| \\
    2.74 -  \indexml{Code.del\_preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
    2.75 +  \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
    2.76    \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    2.77    \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
    2.78  \verb|    -> (string * sort) list * (string * typ list) list| \\
    2.79 @@ -1549,30 +1537,17 @@
    2.80       suspended defining equations \isa{lthms} for constant
    2.81       \isa{const} to executable content.
    2.82  
    2.83 -  \item \verb|Code.add_inline|~\isa{thm}~\isa{thy} adds
    2.84 -     inlining theorem \isa{thm} to executable content.
    2.85 +  \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
    2.86 +     the preprocessor simpset.
    2.87  
    2.88 -  \item \verb|Code.del_inline|~\isa{thm}~\isa{thy} remove
    2.89 -     inlining theorem \isa{thm} from executable content, if present.
    2.90 -
    2.91 -  \item \verb|Code.add_inline_proc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
    2.92 -     inline procedure \isa{f} (named \isa{name}) to executable content;
    2.93 -     \isa{f} is a computation of rewrite rules dependent on
    2.94 -     the current theory context and the list of all arguments
    2.95 -     and right hand sides of the defining equations belonging
    2.96 -     to a certain function definition.
    2.97 -
    2.98 -  \item \verb|Code.del_inline_proc|~\isa{name}~\isa{thy} removes
    2.99 -     inline procedure named \isa{name} from executable content.
   2.100 -
   2.101 -  \item \verb|Code.add_preproc|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.102 -     generic preprocessor \isa{f} (named \isa{name}) to executable content;
   2.103 +    \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
   2.104 +     function transformator \isa{f} (named \isa{name}) to executable content;
   2.105       \isa{f} is a transformation of the defining equations belonging
   2.106       to a certain function definition, depending on the
   2.107       current theory context.
   2.108  
   2.109 -  \item \verb|Code.del_preproc|~\isa{name}~\isa{thy} removes
   2.110 -     generic preprcoessor named \isa{name} from executable content.
   2.111 +  \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
   2.112 +     function transformator named \isa{name} from executable content.
   2.113  
   2.114    \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
   2.115       a datatype to executable content, with generation
   2.116 @@ -1608,7 +1583,7 @@
   2.117  \begin{mldecls}
   2.118    \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\
   2.119    \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * ((string * sort) list * typ)| \\
   2.120 -  \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
   2.121 +  \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\
   2.122    \end{mldecls}
   2.123  
   2.124    \begin{description}
   2.125 @@ -1619,9 +1594,9 @@
   2.126    \item \verb|CodeUnit.head_func|~\isa{thm}
   2.127       extracts the constant and its type from a defining equation \isa{thm}.
   2.128  
   2.129 -  \item \verb|CodeUnit.rewrite_func|~\isa{rews}~\isa{thm}
   2.130 -     rewrites a defining equation \isa{thm} with a set of rewrite
   2.131 -     rules \isa{rews}; only arguments and right hand side are rewritten,
   2.132 +  \item \verb|CodeUnit.rewrite_func|~\isa{ss}~\isa{thm}
   2.133 +     rewrites a defining equation \isa{thm} with a simpset \isa{ss};
   2.134 +     only arguments and right hand side are rewritten,
   2.135       not the head of the defining equation.
   2.136  
   2.137    \end{description}%

     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 14 11:04:42 2008 +0200
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 14 11:04:46 2008 +0200
     3.3 @@ -228,8 +228,8 @@
     3.4  setup {*
     3.5    Codegen.add_preprocessor eqn_suc_preproc
     3.6    #> Codegen.add_preprocessor clause_suc_preproc
     3.7 -  #> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
     3.8 -  #> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
     3.9 +  #> Code.add_functrans ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
    3.10 +  #> Code.add_functrans ("clause_Suc", lift_obj_eq clause_suc_preproc)
    3.11  *}
    3.12  (*>*)
    3.13  

     4.1 --- a/src/Pure/Isar/code.ML	Mon Jul 14 11:04:42 2008 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Mon Jul 14 11:04:46 2008 +0200
     4.3 @@ -15,14 +15,14 @@
     4.4    val del_func: thm -> theory -> theory
     4.5    val del_funcs: string -> theory -> theory
     4.6    val add_funcl: string * thm list Susp.T -> theory -> theory
     4.7 +  val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
     4.8 +  val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
     4.9    val add_inline: thm -> theory -> theory
    4.10    val del_inline: thm -> theory -> theory
    4.11 -  val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
    4.12 -  val del_inline_proc: string -> theory -> theory
    4.13 -  val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
    4.14 -  val del_preproc: string -> theory -> theory
    4.15    val add_post: thm -> theory -> theory
    4.16    val del_post: thm -> theory -> theory
    4.17 +  val add_functrans: string * (theory -> thm list -> thm list) -> theory -> theory
    4.18 +  val del_functrans: string -> theory -> theory
    4.19    val add_datatype: (string * typ) list -> theory -> theory
    4.20    val add_datatype_cmd: string list -> theory -> theory
    4.21    val type_interpretation:
    4.22 @@ -173,6 +173,7 @@
    4.23  
    4.24  
    4.25  (* fundamental melting operations *)
    4.26 +(*FIXME delete*)
    4.27  
    4.28  fun melt _ ([], []) = (false, [])
    4.29    | melt _ ([], ys) = (true, ys)
    4.30 @@ -258,42 +259,34 @@
    4.31    Spec { funcs = funcs, dtyps = dtyps, cases = cases };
    4.32  fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
    4.33    mk_spec (f (funcs, (dtyps, cases)));
    4.34 -fun melt_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    4.35 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    4.36    Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
    4.37    let
    4.38 -    val (touched_funcs, funcs) = melt_funcs (funcs1, funcs2);
    4.39 -    val (touched_dtyps, dtyps) = melt_dtyps (dtyps1, dtyps2);
    4.40 -    val (touched_cases, cases) = melt_cases (cases1, cases2);
    4.41 -    val touched = if touched_dtyps then NONE else
    4.42 -      SOME (fold (insert (op =)) touched_cases touched_funcs);
    4.43 -  in (touched, mk_spec (funcs, (dtyps, cases))) end;
    4.44 +    val (_, funcs) = melt_funcs (funcs1, funcs2);
    4.45 +    val (_, dtyps) = melt_dtyps (dtyps1, dtyps2);
    4.46 +    val (_, cases) = melt_cases (cases1, cases2);
    4.47 +  in mk_spec (funcs, (dtyps, cases)) end;
    4.48  
    4.49  
    4.50  (* pre- and postprocessor *)
    4.51  
    4.52  datatype thmproc = Thmproc of {
    4.53 -  inlines: thm list,
    4.54 -  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
    4.55 -  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
    4.56 -  posts: thm list
    4.57 +  pre: MetaSimplifier.simpset,
    4.58 +  post: MetaSimplifier.simpset,
    4.59 +  functrans: (string * (serial * (theory -> thm list -> thm list))) list
    4.60  };
    4.61  
    4.62 -fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
    4.63 -  Thmproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
    4.64 -    posts = posts };
    4.65 -fun map_thmproc f (Thmproc { inlines, inline_procs, preprocs, posts }) =
    4.66 -  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
    4.67 -fun melt_thmproc (Thmproc { inlines = inlines1, inline_procs = inline_procs1,
    4.68 -    preprocs = preprocs1, posts = posts1 },
    4.69 -  Thmproc { inlines = inlines2, inline_procs = inline_procs2,
    4.70 -      preprocs = preprocs2, posts= posts2 }) =
    4.71 +fun mk_thmproc ((pre, post), functrans) =
    4.72 +  Thmproc { pre = pre, post = post, functrans = functrans };
    4.73 +fun map_thmproc f (Thmproc { pre, post, functrans }) =
    4.74 +  mk_thmproc (f ((pre, post), functrans));
    4.75 +fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    4.76 +  Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    4.77      let
    4.78 -      val (touched1, inlines) = melt_thms (inlines1, inlines2);
    4.79 -      val (touched2, inline_procs) = melt_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
    4.80 -      val (touched3, preprocs) = melt_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
    4.81 -      val (_, posts) = melt_thms (posts1, posts2);
    4.82 -    in (touched1 orelse touched2 orelse touched3,
    4.83 -      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
    4.84 +      val pre = MetaSimplifier.merge_ss (pre1, pre2);
    4.85 +      val post = MetaSimplifier.merge_ss (post1, post2);
    4.86 +      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    4.87 +    in mk_thmproc ((pre, post), functrans) end;
    4.88  
    4.89  datatype exec = Exec of {
    4.90    thmproc: thmproc,
    4.91 @@ -304,14 +297,13 @@
    4.92    Exec { thmproc = thmproc, spec = spec };
    4.93  fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
    4.94    mk_exec (f (thmproc, spec));
    4.95 -fun melt_exec (Exec { thmproc = thmproc1, spec = spec1 },
    4.96 +fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
    4.97    Exec { thmproc = thmproc2, spec = spec2 }) =
    4.98    let
    4.99 -    val (touched', thmproc) = melt_thmproc (thmproc1, thmproc2);
   4.100 -    val (touched_cs, spec) = melt_spec (spec1, spec2);
   4.101 -    val touched = if touched' then NONE else touched_cs;
   4.102 -  in (touched, mk_exec (thmproc, spec)) end;
   4.103 -val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   4.104 +    val thmproc = merge_thmproc (thmproc1, thmproc2);
   4.105 +    val spec = merge_spec (spec1, spec2);
   4.106 +  in mk_exec (thmproc, spec) end;
   4.107 +val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []),
   4.108    mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
   4.109  
   4.110  fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
   4.111 @@ -381,9 +373,9 @@
   4.112    val extend = copy;
   4.113    fun merge pp ((exec1, data1), (exec2, data2)) =
   4.114      let
   4.115 -      val (touched, exec) = melt_exec (exec1, exec2);
   4.116 -      val data1' = invoke_purge_all NONE touched (! data1);
   4.117 -      val data2' = invoke_purge_all NONE touched (! data2);
   4.118 +      val exec = merge_exec (exec1, exec2);
   4.119 +      val data1' = invoke_purge_all NONE NONE (! data1);
   4.120 +      val data2' = invoke_purge_all NONE NONE (! data2);
   4.121        val data = invoke_merge_all pp (data1', data2');
   4.122      in (exec, ref data) end;
   4.123  );
   4.124 @@ -457,10 +449,9 @@
   4.125                            :: Pretty.str "of"
   4.126                            :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   4.127            );
   4.128 -    val inlines = (#inlines o the_thmproc) exec;
   4.129 -    val posts = (#posts o the_thmproc) exec;
   4.130 -    val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
   4.131 -    val preprocs = (map fst o #preprocs o the_thmproc) exec;
   4.132 +    val pre = (#pre o the_thmproc) exec;
   4.133 +    val post = (#post o the_thmproc) exec;
   4.134 +    val functrans = (map fst o #functrans o the_thmproc) exec;
   4.135      val funs = the_funcs exec
   4.136        |> Symtab.dest
   4.137        |> (map o apsnd) snd
   4.138 @@ -478,25 +469,20 @@
   4.139          :: Pretty.fbrk
   4.140          :: (Pretty.fbreaks o map pretty_func) funs
   4.141        ),
   4.142 +      Pretty.block [
   4.143 +        Pretty.str "preprocessing simpset:",
   4.144 +        Pretty.fbrk,
   4.145 +        MetaSimplifier.pretty_ss pre
   4.146 +      ],
   4.147 +      Pretty.block [
   4.148 +        Pretty.str "postprocessing simpset:",
   4.149 +        Pretty.fbrk,
   4.150 +        MetaSimplifier.pretty_ss post
   4.151 +      ],
   4.152        Pretty.block (
   4.153 -        Pretty.str "inlining theorems:"
   4.154 +        Pretty.str "function transformators:"
   4.155          :: Pretty.fbrk
   4.156 -        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
   4.157 -      ),
   4.158 -      Pretty.block (
   4.159 -        Pretty.str "inlining procedures:"
   4.160 -        :: Pretty.fbrk
   4.161 -        :: (Pretty.fbreaks o map Pretty.str) inline_procs
   4.162 -      ),
   4.163 -      Pretty.block (
   4.164 -        Pretty.str "preprocessors:"
   4.165 -        :: Pretty.fbrk
   4.166 -        :: (Pretty.fbreaks o map Pretty.str) preprocs
   4.167 -      ),
   4.168 -      Pretty.block (
   4.169 -        Pretty.str "postprocessor theorems:"
   4.170 -        :: Pretty.fbrk
   4.171 -        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) posts
   4.172 +        :: (Pretty.fbreaks o map Pretty.str) functrans
   4.173        ),
   4.174        Pretty.block (
   4.175          Pretty.str "datatypes:"
   4.176 @@ -834,41 +820,32 @@
   4.177  fun add_undefined c thy =
   4.178    (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   4.179  
   4.180 -fun add_inline thm thy =
   4.181 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   4.182 -    (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   4.183 -        (*fully applied in order to get right context for mk_rew!*)
   4.184 +val map_pre = map_exec_purge NONE o map_thmproc o apfst o apfst;
   4.185 +val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
   4.186  
   4.187 -fun del_inline thm thy =
   4.188 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   4.189 -    (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   4.190 -        (*fully applied in order to get right context for mk_rew!*)
   4.191 +fun add_inline thm thy = (map_pre o MetaSimplifier.add_simp)
   4.192 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   4.193 +    (*fully applied in order to get right context for mk_rew!*)
   4.194  
   4.195 -fun add_inline_proc (name, f) =
   4.196 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
   4.197 +fun del_inline thm thy = (map_pre o MetaSimplifier.del_simp)
   4.198 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   4.199 +    (*fully applied in order to get right context for mk_rew!*)
   4.200 +
   4.201 +fun add_post thm thy = (map_post o MetaSimplifier.add_simp)
   4.202 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   4.203 +    (*fully applied in order to get right context for mk_rew!*)
   4.204 +
   4.205 +fun del_post thm thy = (map_post o MetaSimplifier.del_simp)
   4.206 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   4.207 +    (*fully applied in order to get right context for mk_rew!*)
   4.208 +  
   4.209 +fun add_functrans (name, f) =
   4.210 +  (map_exec_purge NONE o map_thmproc o apsnd)
   4.211      (AList.update (op =) (name, (serial (), f)));
   4.212  
   4.213 -fun del_inline_proc name =
   4.214 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
   4.215 -    (delete_force "inline procedure" name);
   4.216 -
   4.217 -fun add_preproc (name, f) =
   4.218 -  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
   4.219 -    (AList.update (op =) (name, (serial (), f)));
   4.220 -
   4.221 -fun del_preproc name =
   4.222 -  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
   4.223 -    (delete_force "preprocessor" name);
   4.224 -
   4.225 -fun add_post thm thy =
   4.226 +fun del_functrans name =
   4.227    (map_exec_purge NONE o map_thmproc o apsnd)
   4.228 -    (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   4.229 -        (*fully applied in order to get right context for mk_rew!*)
   4.230 -
   4.231 -fun del_post thm thy =
   4.232 -  (map_exec_purge NONE o map_thmproc o apsnd)
   4.233 -    (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   4.234 -        (*fully applied in order to get right context for mk_rew!*)
   4.235 +    (delete_force "function transformator" name);
   4.236  
   4.237  val _ = Context.>> (Context.map_theory
   4.238    (let
   4.239 @@ -890,20 +867,8 @@
   4.240  
   4.241  local
   4.242  
   4.243 -fun gen_apply_inline_proc prep post thy f x =
   4.244 -  let
   4.245 -    val cts = prep x;
   4.246 -    val rews = map CodeUnit.assert_rew (f thy cts);
   4.247 -  in post rews x end;
   4.248 -
   4.249 -val apply_inline_proc = gen_apply_inline_proc (maps
   4.250 -  ((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
   4.251 -  (fn rews => map (CodeUnit.rewrite_func rews));
   4.252 -val apply_inline_proc_cterm = gen_apply_inline_proc single
   4.253 -  (MetaSimplifier.rewrite false);
   4.254 -
   4.255 -fun apply_preproc thy f [] = []
   4.256 -  | apply_preproc thy f (thms as (thm :: _)) =
   4.257 +fun apply_functrans thy f [] = []
   4.258 +  | apply_functrans thy f (thms as (thm :: _)) =
   4.259        let
   4.260          val const = const_of_func thy thm;
   4.261          val thms' = f thy thms;
   4.262 @@ -925,10 +890,9 @@
   4.263  
   4.264  fun preprocess thy thms =
   4.265    thms
   4.266 -  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy)
   4.267 -  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy))
   4.268 -  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
   4.269 -(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   4.270 +  |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy)
   4.271 +  |> map (CodeUnit.rewrite_func ((#pre o the_thmproc o the_exec) thy))
   4.272 +  (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
   4.273    |> map (AxClass.unoverload thy)
   4.274    |> common_typ_funcs;
   4.275  
   4.276 @@ -938,9 +902,7 @@
   4.277      val thy = Thm.theory_of_cterm ct;
   4.278    in
   4.279      ct
   4.280 -    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
   4.281 -    |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
   4.282 -        ((#inline_procs o the_thmproc o the_exec) thy)
   4.283 +    |> MetaSimplifier.rewrite' (ProofContext.init thy) false ((#pre o the_thmproc o the_exec) thy)
   4.284      |> rhs_conv (AxClass.unoverload_conv thy)
   4.285    end;
   4.286  
   4.287 @@ -952,7 +914,8 @@
   4.288    in
   4.289      ct
   4.290      |> AxClass.overload_conv thy
   4.291 -    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   4.292 +    |> rhs_conv (MetaSimplifier.rewrite' (ProofContext.init thy) false 
   4.293 +          ((#post o the_thmproc o the_exec) thy))
   4.294    end;
   4.295  
   4.296  fun postprocess_term thy = term_of_conv thy postprocess_conv;