doc-src/IsarRef/logics.tex

 \end{descr}
 
 
 \subsection{Executable code}
 
-Isabelle/Pure provides a generic infrastructure to support code
-generation from executable specifications, both functional and
-relational programs.  Isabelle/HOL instantiates these mechanisms in a
-way that is amenable to end-user applications.  See
+Isabelle/Pure provides two generic frameworks to support code
+generation from executable specifications. Isabelle/HOL
+instantiates these mechanisms in a
+way that is amenable to end-user applications
+
+One framework generates code from both functional and
+relational programs to SML.  See
 \cite{isabelle-HOL} for further information (this actually covers the
 new-style theory format as well).
 
 \indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library}
 \indexisarcmd{consts-code}\indexisarcmd{types-code}

 \begin{descr}
 \item [$\isarkeyword{value}~t$] reads, evaluates and prints a term
   using the code generator.
 \end{descr}
 
+The other framework generates code from functional programs
+(including overloading using type classes) to SML and Haskell.
+Conceptually, code generation is split up in three steps: \emph{selection}
+of code theorems, \emph{extraction} into an abstract executable view
+and \emph{serialization} to a specific \emph{target language}.
+
+\indexisarcmd{code-gen}
+\indexisarcmd{code-const}\indexisarcmd{code-type}
+\indexisarcmd{code-class}\indexisarcmd{code-instance}
+\indexisarcmd{print-codethms}
+\indexisaratt{code func}
+\indexisaratt{code nofunc}
+\indexisaratt{code inline}
+\indexisaratt{code noinline}
+
+\begin{matharray}{rcl}
+  \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{code_const} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_type} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_class} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\
+  \isarcmd{print_codethms}^* & : & \isarkeep{theory~|~proof} \\
+  code\ func & : & \isaratt \\
+  code\ nofunc & : & \isaratt \\
+  code\ inline & : & \isaratt \\
+  code\ noinline & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+'code\_gen' ( ( const + ) ( seri + ) | ( const + ) | ( seri + ) );
+
+const : term;
+
+typeconstructor : nameref;
+
+class : nameref;
+
+seri : target | 'SML' ( string | '-' | ()) | 'Haskell' (string | ());
+
+target : 'SML' | 'Haskell';
+
+'code\_const' (const + 'and') \\
+  ( ( '(' target ( syntax + 'and' ) ')' ) + );
+
+'code\_type' (typeconstructor + 'and') \\
+  ( ( '(' target ( syntax + 'and' ) ')' ) + );
+
+'code\_class' (class + 'and') \\
+  ( ( '(' target \\
+    ( ( string ('where' ( const ( '==' | equiv ) string ) + ) ? ) + 'and' ) ')' ) + );
+
+'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+  ( ( '(' target ( '-' + 'and' ) ')' ) + );
+
+syntax : ( 'target\_atom' ? string ) | ( 'infix' | 'infixl' | 'infixr' ) nat string;
+
+'print\_codethms' ( '(' ( const + ) ? ')' ) ?;
+
+('code\ func' | 'code\ nofunc' | 'code\ inline' | 'code\ noinline');
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarcmd{code_gen}$] is the canonical interface for generating and
+  serializing code: for a given list of constants, code is generated for the specified
+  target language(s).  Abstract code is cached incrementally.  If no constant is given,
+  the whole current cache is serialized.  If no serialization instruction
+  is given, only abstract code is cached.
+
+  The \emph{SML} serializer takes either a filename or an ``-'' as argument.
+  In the first case, code is written to the specified file, in the latter
+  it is compiled internally in the context of the current ML session.
+
+  For \emph{Haskell}, also a filename is specified; different modules
+  are serialized to different files in the directory of the specified file, or
+  subdirectories.
+
+\item [$\isarcmd{code_const}$] associates a list of constants
+  with target-specific serializations.
+
+\item [$\isarcmd{code_type}$] associates a list of type constructors
+  with target-specific serializations.
+
+\item [$\isarcmd{code_class}$] associates a list of classes
+  with target-specific class names; in addition, constants associated
+  with this class may be given target-specific names used for instance
+  declarations.  Applies only to \emph{Haskell}.
+
+\item [$\isarcmd{code_instance}$] declares a list of type constructor / class
+  instance relations as ``already present'' for a given target.
+  Applies only to \emph{Haskell}.
+
+\item [$code\ func$ and $code\ nofunc$] select or deselect explicitly
+  a function theorem for code generation.  Usually packages introducing
+  function theorems provide a resonable default setup for selection.
+  If no theorem has been selected for a constant, its definition
+  is used as function theorem if possible.
+
+\item [$code\ inline$ and $code\ noinline$] select or deselect
+  inlining theorems which are applied as rewrite rules to any function theorem.
+
+\item [$\isarcmd{print_thms}$] gives an overview on selected
+  function theorems, code generator datatypes and inlining theorems.
+  When constants are given, it displays the function theorems
+  for those constants \emph{after} any preprocessing step has been carried out.
+
+\end{descr}
 
 \section{HOLCF}
 
 \subsection{Mixfix syntax for continuous operations}