# HG changeset patch
# User haftmann
# Date 1177068651 -7200
# Node ID 8b3131eeb509643188e1f6beecb39eeb816c92ff
# Parent  1bfd75c1f232dd211551e3ba8a4ec41b72f8beda
updated code generator

diff -r 1bfd75c1f232 -r 8b3131eeb509 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Fri Apr 20 13:11:47 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Fri Apr 20 13:30:51 2007 +0200
@@ -752,11 +752,14 @@
 (including overloading using type classes) to SML \cite{SML},
 OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}.
 Conceptually, code generation is split up in three steps: \emph{selection}
-of code theorems, \emph{extraction} into an abstract executable view
+of code theorems, \emph{translation} 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-thms}
+\indexisarcmd{code-deps}
+\indexisarcmd{code-datatype}
 \indexisarcmd{code-const}
 \indexisarcmd{code-type}
 \indexisarcmd{code-class}
@@ -767,7 +770,6 @@
 \indexisarcmd{code-moduleprolog}
 \indexisarcmd{code-axioms}
 \indexisarcmd{code-abstype}
-\indexisarcmd{code-thms}
 \indexisarcmd{print-codesetup}
 \indexisaratt{code func}
 \indexisaratt{code nofunc}
@@ -776,6 +778,9 @@
 
 \begin{matharray}{rcl}
   \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_const} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_type} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_class} & : & \isartrans{theory}{theory} \\
@@ -786,7 +791,6 @@
   \isarcmd{code_moduleprolog} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_axioms} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\
-  \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\
   code\ func & : & \isaratt \\
   code\ nofunc & : & \isaratt \\
@@ -795,10 +799,16 @@
 \end{matharray}
 
 \begin{rail}
-'code\_gen' ( ( const | 'name.*' | '*' ) + ) ? ( seri + ) ?;
+'code\_gen' ( constexpr + ) ? ( seri + ) ?;
+
+'code\_thms' ( constexpr + ) ?;
+
+'code\_deps' ( constexpr + ) ?;
 
 const : term;
 
+constexpr : ( const | 'name.*' | '*' );
+
 typeconstructor : nameref;
 
 class : nameref;
@@ -807,6 +817,8 @@
 
 target : 'OCaml' | 'SML' | 'Haskell';
 
+'code\_datatype' const +;
+
 'code\_const' (const + 'and') \\
   ( ( '(' target ( syntax + 'and' ) ')' ) + );
 
@@ -834,8 +846,6 @@
 
 syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string;
 
-'code\_thms' ( const + ) ?;
-
 'print\_codesetup';
 
 ('code\ func' | 'code\ nofunc' | 'code\ inline' | 'code\ noinline');
@@ -851,7 +861,7 @@
 
   Constants may be specified by giving them literally, referring
   to all exeuctable contants within a certain theory named ``name''
-  by giving (``name.*''), or referring to \emph{all} exeuctable
+  by giving (``name.*''), or referring to \emph{all} executable
   constants currently available (``*'').
 
   The \emph{SML} serializer takes either a filename or an ``-'' or ``*''
@@ -870,6 +880,16 @@
   to each appropriate datatype declaration.
   A ``-'' instead of a directory name prints code to standard output.
 
+\item [$\isarcmd{code_thms}$] prints a list of theorems representing the
+  corresponding program containing all given constants; if no constants are
+  given, the current cache of code theorems in printed.
+
+\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the
+  corresponding program containing all given constants; if no constants are
+  given, the current cache os visualized.
+
+\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type.
+
 \item [$\isarcmd{code_const}$] associates a list of constants
   with target-specific serializations.
 
@@ -892,11 +912,11 @@
   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_modulename}$] declares aliasings from one module name
+  onto another.
 
 \item [$\isarcmd{code_moduleprolog}$] adds any content (''prolog``)
-  to a specified module. A ``-'' will remove any already specified prolog.
+  to a specified module. A ``-'' will remove an already given prolog.
 
 \item [$\isarcmd{code_axioms}$] uses the given equations for code generation
   whenever possible. Both sides are required to be constants which are
@@ -908,18 +928,10 @@
 \item [$code\ func$ and $code\ nofunc$] select or deselect explicitly
   a defining equation for code generation.  Usually packages introducing
   defining equations provide a resonable default setup for selection.
-  If no theorem has been selected explicitly
-  for a constant, its primitive definition
-  is used as defining equations if possible.
 
 \item [$code\ inline$ and $code\ noinline$] select or deselect
   inlining theorems which are applied as rewrite rules to any defining equation.
 
-\item [$\isarcmd{code_thms}$] lists currently cached defining equations
-  (i.e.~\emph{after} any preprocessing step has been carried out);
-  when constants are given, it adds the defining equations
-  for those constants, too.
-
 \item [$\isarcmd{print_codesetup}$] gives an overview on selected
   defining equations, code generator datatypes and inlining theorems.