# HG changeset patch
# User haftmann
# Date 1161356845 -7200
# Node ID d6c141871b29a7956bffc03dc640bf01fdc58bd8
# Parent  22ae82f77c5e8a49ef3e2cf6df7dc5cadb5d6e90
extended section on code generator

diff -r 22ae82f77c5e -r d6c141871b29 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Fri Oct 20 17:07:24 2006 +0200
+++ b/doc-src/IsarRef/logics.tex	Fri Oct 20 17:07:25 2006 +0200
@@ -753,10 +753,18 @@
 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}.
+See \cite{isabelle-codegen} for an introduction on how to use it.
 
 \indexisarcmd{code-gen}
-\indexisarcmd{code-const}\indexisarcmd{code-type}
-\indexisarcmd{code-class}\indexisarcmd{code-instance}
+\indexisarcmd{code-const}
+\indexisarcmd{code-type}
+\indexisarcmd{code-class}
+\indexisarcmd{code-instance}
+\indexisarcmd{code-reserved}
+\indexisarcmd{code-modulename}
+\indexisarcmd{code-moduleprolog}
+\indexisarcmd{code-axioms}
+\indexisarcmd{code-abstype}
 \indexisarcmd{print-codethms}
 \indexisaratt{code func}
 \indexisaratt{code nofunc}
@@ -769,6 +777,11 @@
   \isarcmd{code_type} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_class} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_moduleprolog} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_axioms} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\
   \isarcmd{print_codethms}^* & : & \isarkeep{theory~|~proof} \\
   code\ func & : & \isaratt \\
   code\ nofunc & : & \isaratt \\
@@ -802,6 +815,16 @@
 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
   ( ( '(' target ( '-' + 'and' ) ')' ) + );
 
+'code\_reserved' target ( string + );
+
+'code\_modulename' target ( ( string string ) + );
+
+'code\_moduleprolog' target ( ( string ( string | '-') ) + );
+
+'code\_axioms' ( const ( '==' | equiv ) const + );
+
+'code\_abstype' typ typ 'where' ( const ( '==' | equiv ) const + );
+
 syntax : ( 'target\_atom' ? string ) | ( 'infix' | 'infixl' | 'infixr' ) nat string;
 
 'print\_codethms' ( '(' ( const + ) ? ')' ) ?;
@@ -821,9 +844,9 @@
   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.
+  For \emph{Haskell}, a directory name is specified; different modules
+  are serialized to different files in this directory or
+  subdirectories, reflecting the module hierarchy.
 
 \item [$\isarcmd{code_const}$] associates a list of constants
   with target-specific serializations.
@@ -840,6 +863,23 @@
   instance relations as ``already present'' for a given target.
   Applies only to \emph{Haskell}.
 
+\item [$\isarcmd{code_reserved}$] declares a list of names
+  as reserved for a given target, preventing it to be shadowed
+  by any generated code.
+
+\item [$\isarcmd{code_modulename}$] declares aliassings a module name
+  to another.
+
+\item [$\isarcmd{code_moduleprolog}$] adds any content (''prolog``)
+  to a specified module. A ``-'' will remove any already specified prolog.
+
+\item [$\isarcmd{code_axioms}$] uses the given equations for code generation
+  whenever possible. Both sides are required to be constants which are
+  mapped on functions in generated code.
+
+\item [$\isarcmd{code_abstype}$] offers an interface for implementing
+  an abstract type plus operations by executable counterparts.
+
 \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.