1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 09:40:11 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 10:04:17 2010 +0200
     1.3 @@ -1012,6 +1012,7 @@
     1.4      \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.5      \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.6      \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.7 +    \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -1084,6 +1085,10 @@
    1.12      'code\_modulename' target ( ( string string ) + )
    1.13      ;
    1.14  
    1.15 +    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
    1.16 +      ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.17 +    ;
    1.18 +
    1.19      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
    1.20      ;
    1.21  
    1.22 @@ -1092,8 +1097,9 @@
    1.23    \begin{description}
    1.24  
    1.25    \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
    1.26 -  of constants in the specified target language(s).  If no serialization
    1.27 -  instruction is given, only abstract code is generated internally.
    1.28 +  of constants in the specified target language(s).  If no
    1.29 +  serialization instruction is given, only abstract code is generated
    1.30 +  internally.
    1.31  
    1.32    Constants may be specified by giving them literally, referring to
    1.33    all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
    1.34 @@ -1104,18 +1110,20 @@
    1.35    after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
    1.36    placed in this module.
    1.37  
    1.38 -  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
    1.39 -  single file; for \emph{Haskell}, it refers to a whole directory,
    1.40 -  where code is generated in multiple files reflecting the module
    1.41 -  hierarchy.  Omitting the file specification denotes standard
    1.42 +  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
    1.43 +  refers to a single file; for \emph{Haskell}, it refers to a whole
    1.44 +  directory, where code is generated in multiple files reflecting the
    1.45 +  module hierarchy.  Omitting the file specification denotes standard
    1.46    output.
    1.47  
    1.48    Serializers take an optional list of arguments in parentheses.  For
    1.49    \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
    1.50    explicit module signatures.
    1.51    
    1.52 -  For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
    1.53 -  declaration.
    1.54 +  For \emph{Haskell} a module name prefix may be given using the
    1.55 +  ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a
    1.56 +  ``\verb|deriving (Read, Show)|'' clause to each appropriate
    1.57 +  datatype declaration.
    1.58  
    1.59    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
    1.60    ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
    1.61 @@ -1125,8 +1133,8 @@
    1.62    code equations on abstract datatype representations respectively.
    1.63  
    1.64    \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
    1.65 -  required to have a definition by means of code equations; if
    1.66 -  needed these are implemented by program abort instead.
    1.67 +  required to have a definition by means of code equations; if needed
    1.68 +  these are implemented by program abort instead.
    1.69  
    1.70    \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
    1.71    for a logical type.
    1.72 @@ -1134,17 +1142,15 @@
    1.73    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    1.74    selected code equations and code generator datatypes.
    1.75  
    1.76 -  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
    1.77 -  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    1.78 -  applied as rewrite rules to any code equation during
    1.79 -  preprocessing.
    1.80 +  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with option
    1.81 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are applied as
    1.82 +  rewrite rules to any code equation during preprocessing.
    1.83  
    1.84 -  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
    1.85 -  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
    1.86 -  applied as rewrite rules to any result of an evaluation.
    1.87 +  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are applied as rewrite rules to any
    1.88 +  result of an evaluation.
    1.89  
    1.90 -  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
    1.91 -  of the code generator preprocessor.
    1.92 +  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
    1.93 +  generator preprocessor.
    1.94  
    1.95    \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
    1.96    representing the corresponding program containing all given
    1.97 @@ -1186,11 +1192,20 @@
    1.98    \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
    1.99    module name onto another.
   1.100  
   1.101 +  \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
   1.102 +  argument compiles code into the system runtime environment and
   1.103 +  modifies the code generator setup that future invocations of system
   1.104 +  runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
   1.105 +  entities.  With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
   1.106 +  is generated into that specified file without modifying the code
   1.107 +  generator setup.
   1.108 +
   1.109    \end{description}
   1.110  
   1.111 -  The other framework generates code from both functional and relational
   1.112 -  programs to SML.  See \cite{isabelle-HOL} for further information
   1.113 -  (this actually covers the new-style theory format as well).
   1.114 +  The other framework generates code from both functional and
   1.115 +  relational programs to SML.  See \cite{isabelle-HOL} for further
   1.116 +  information (this actually covers the new-style theory format as
   1.117 +  well).
   1.118  
   1.119    \begin{matharray}{rcl}
   1.120      \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\