doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 39608 76bc7e4999f8
parent 38814 4d575fbfc920
child 40170 751121d5ca35
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 09:40:11 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 10:04:17 2010 +0200
     1.3 @@ -996,6 +996,7 @@
     1.4      @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
     1.5      @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     1.7 +    @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -1068,6 +1069,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 @@ -1076,8 +1081,9 @@
    1.23    \begin{description}
    1.24  
    1.25    \item @{command (HOL) "export_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 @{text
    1.34 @@ -1089,20 +1095,20 @@
    1.35    after the @{keyword "module_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}, ``@{text no_signatures}`` omits
    1.50    explicit module signatures.
    1.51    
    1.52 -  For \emph{Haskell} a module name prefix may be given using the ``@{text
    1.53 -  "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
    1.54 -  "deriving (Read, Show)"}'' clause to each appropriate datatype
    1.55 -  declaration.
    1.56 +  For \emph{Haskell} a module name prefix may be given using the
    1.57 +  ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
    1.58 +  ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
    1.59 +  datatype declaration.
    1.60  
    1.61    \item @{attribute (HOL) code} explicitly selects (or with option
    1.62    ``@{text "del"}'' deselects) a code equation for code generation.
    1.63 @@ -1112,8 +1118,8 @@
    1.64    code equations on abstract datatype representations respectively.
    1.65  
    1.66    \item @{command (HOL) "code_abort"} declares constants which are not
    1.67 -  required to have a definition by means of code equations; if
    1.68 -  needed these are implemented by program abort instead.
    1.69 +  required to have a definition by means of code equations; if needed
    1.70 +  these are implemented by program abort instead.
    1.71  
    1.72    \item @{command (HOL) "code_datatype"} specifies a constructor set
    1.73    for a logical type.
    1.74 @@ -1121,17 +1127,16 @@
    1.75    \item @{command (HOL) "print_codesetup"} gives an overview on
    1.76    selected code equations and code generator datatypes.
    1.77  
    1.78 -  \item @{attribute (HOL) code_inline} declares (or with
    1.79 -  option ``@{text "del"}'' removes) inlining theorems which are
    1.80 -  applied as rewrite rules to any code equation during
    1.81 -  preprocessing.
    1.82 +  \item @{attribute (HOL) code_inline} declares (or with option
    1.83 +  ``@{text "del"}'' removes) inlining theorems which are applied as
    1.84 +  rewrite rules to any code equation during preprocessing.
    1.85  
    1.86 -  \item @{attribute (HOL) code_post} declares (or with
    1.87 -  option ``@{text "del"}'' removes) theorems which are
    1.88 -  applied as rewrite rules to any result of an evaluation.
    1.89 +  \item @{attribute (HOL) code_post} declares (or with option ``@{text
    1.90 +  "del"}'' removes) theorems which are applied as rewrite rules to any
    1.91 +  result of an evaluation.
    1.92  
    1.93 -  \item @{command (HOL) "print_codeproc"} prints the setup
    1.94 -  of the code generator preprocessor.
    1.95 +  \item @{command (HOL) "print_codeproc"} prints the setup of the code
    1.96 +  generator preprocessor.
    1.97  
    1.98    \item @{command (HOL) "code_thms"} prints a list of theorems
    1.99    representing the corresponding program containing all given
   1.100 @@ -1173,11 +1178,21 @@
   1.101    \item @{command (HOL) "code_modulename"} declares aliasings from one
   1.102    module name onto another.
   1.103  
   1.104 +  \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
   1.105 +  argument compiles code into the system runtime environment and
   1.106 +  modifies the code generator setup that future invocations of system
   1.107 +  runtime code generation referring to one of the ``@{text
   1.108 +  "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
   1.109 +  entities.  With a ``@{text "file"}'' argument, the corresponding code
   1.110 +  is generated into that specified file without modifying the code
   1.111 +  generator setup.
   1.112 +
   1.113    \end{description}
   1.114  
   1.115 -  The other framework generates code from both functional and relational
   1.116 -  programs to SML.  See \cite{isabelle-HOL} for further information
   1.117 -  (this actually covers the new-style theory format as well).
   1.118 +  The other framework generates code from both functional and
   1.119 +  relational programs to SML.  See \cite{isabelle-HOL} for further
   1.120 +  information (this actually covers the new-style theory format as
   1.121 +  well).
   1.122  
   1.123    \begin{matharray}{rcl}
   1.124      @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\