# HG changeset patch
# User haftmann
# Date 1285142657 -7200
# Node ID 76bc7e4999f87a24dd13bceeb8eeceb866125911
# Parent  564448a92ae03c6159d966cbe810fbe02e7fe747
formal syntax diagram for code_reflect

diff -r 564448a92ae0 -r 76bc7e4999f8 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 09:40:11 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 10:04:17 2010 +0200
@@ -996,6 +996,7 @@
     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
   \begin{rail}
@@ -1068,6 +1069,10 @@
     'code\_modulename' target ( ( string string ) + )
     ;
 
+    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+      ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+    ;
+
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
@@ -1076,8 +1081,9 @@
   \begin{description}
 
   \item @{command (HOL) "export_code"} generates code for a given list
-  of constants in the specified target language(s).  If no serialization
-  instruction is given, only abstract code is generated internally.
+  of constants in the specified target language(s).  If no
+  serialization instruction is given, only abstract code is generated
+  internally.
 
   Constants may be specified by giving them literally, referring to
   all executable contants within a certain theory by giving @{text
@@ -1089,20 +1095,20 @@
   after the @{keyword "module_name"} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
-  single file; for \emph{Haskell}, it refers to a whole directory,
-  where code is generated in multiple files reflecting the module
-  hierarchy.  Omitting the file specification denotes standard
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+  refers to a single file; for \emph{Haskell}, it refers to a whole
+  directory, where code is generated in multiple files reflecting the
+  module hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
   explicit module signatures.
   
-  For \emph{Haskell} a module name prefix may be given using the ``@{text
-  "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
-  "deriving (Read, Show)"}'' clause to each appropriate datatype
-  declaration.
+  For \emph{Haskell} a module name prefix may be given using the
+  ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
+  ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
+  datatype declaration.
 
   \item @{attribute (HOL) code} explicitly selects (or with option
   ``@{text "del"}'' deselects) a code equation for code generation.
@@ -1112,8 +1118,8 @@
   code equations on abstract datatype representations respectively.
 
   \item @{command (HOL) "code_abort"} declares constants which are not
-  required to have a definition by means of code equations; if
-  needed these are implemented by program abort instead.
+  required to have a definition by means of code equations; if needed
+  these are implemented by program abort instead.
 
   \item @{command (HOL) "code_datatype"} specifies a constructor set
   for a logical type.
@@ -1121,17 +1127,16 @@
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
-  \item @{attribute (HOL) code_inline} declares (or with
-  option ``@{text "del"}'' removes) inlining theorems which are
-  applied as rewrite rules to any code equation during
-  preprocessing.
+  \item @{attribute (HOL) code_inline} declares (or with option
+  ``@{text "del"}'' removes) inlining theorems which are applied as
+  rewrite rules to any code equation during preprocessing.
 
-  \item @{attribute (HOL) code_post} declares (or with
-  option ``@{text "del"}'' removes) theorems which are
-  applied as rewrite rules to any result of an evaluation.
+  \item @{attribute (HOL) code_post} declares (or with option ``@{text
+  "del"}'' removes) theorems which are applied as rewrite rules to any
+  result of an evaluation.
 
-  \item @{command (HOL) "print_codeproc"} prints the setup
-  of the code generator preprocessor.
+  \item @{command (HOL) "print_codeproc"} prints the setup of the code
+  generator preprocessor.
 
   \item @{command (HOL) "code_thms"} prints a list of theorems
   representing the corresponding program containing all given
@@ -1173,11 +1178,21 @@
   \item @{command (HOL) "code_modulename"} declares aliasings from one
   module name onto another.
 
+  \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
+  argument compiles code into the system runtime environment and
+  modifies the code generator setup that future invocations of system
+  runtime code generation referring to one of the ``@{text
+  "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
+  entities.  With a ``@{text "file"}'' argument, the corresponding code
+  is generated into that specified file without modifying the code
+  generator setup.
+
   \end{description}
 
-  The other 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).
+  The other 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).
 
   \begin{matharray}{rcl}
     @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
diff -r 564448a92ae0 -r 76bc7e4999f8 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 09:40:11 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 10:04:17 2010 +0200
@@ -1012,6 +1012,7 @@
     \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}} \\
     \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}} \\
     \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}} \\
+    \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}}
   \end{matharray}
 
   \begin{rail}
@@ -1084,6 +1085,10 @@
     'code\_modulename' target ( ( string string ) + )
     ;
 
+    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+      ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+    ;
+
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
@@ -1092,8 +1097,9 @@
   \begin{description}
 
   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
-  of constants in the specified target language(s).  If no serialization
-  instruction is given, only abstract code is generated internally.
+  of constants in the specified target language(s).  If no
+  serialization instruction is given, only abstract code is generated
+  internally.
 
   Constants may be specified by giving them literally, referring to
   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
@@ -1104,18 +1110,20 @@
   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
-  single file; for \emph{Haskell}, it refers to a whole directory,
-  where code is generated in multiple files reflecting the module
-  hierarchy.  Omitting the file specification denotes standard
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+  refers to a single file; for \emph{Haskell}, it refers to a whole
+  directory, where code is generated in multiple files reflecting the
+  module hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
   explicit module signatures.
   
-  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
-  declaration.
+  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 declaration.
 
   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
@@ -1125,8 +1133,8 @@
   code equations on abstract datatype representations respectively.
 
   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
-  required to have a definition by means of code equations; if
-  needed these are implemented by program abort instead.
+  required to have a definition by means of code equations; if needed
+  these are implemented by program abort instead.
 
   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
   for a logical type.
@@ -1134,17 +1142,15 @@
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
   selected code equations and code generator datatypes.
 
-  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
-  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
-  applied as rewrite rules to any code equation during
-  preprocessing.
+  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with option
+  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are applied as
+  rewrite rules to any code equation during preprocessing.
 
-  \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 result of an evaluation.
+  \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
+  result of an evaluation.
 
-  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
-  of the code generator preprocessor.
+  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
+  generator preprocessor.
 
   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
   representing the corresponding program containing all given
@@ -1186,11 +1192,20 @@
   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
   module name onto another.
 
+  \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
+  argument compiles code into the system runtime environment and
+  modifies the code generator setup that future invocations of system
+  runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
+  entities.  With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
+  is generated into that specified file without modifying the code
+  generator setup.
+
   \end{description}
 
-  The other 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).
+  The other 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).
 
   \begin{matharray}{rcl}
     \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}} \\