--- 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.