1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 14 10:38:29 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 14 10:50:49 2010 +0200
1.3 @@ -965,7 +965,214 @@
1.4 instantiates these mechanisms in a way that is amenable to end-user
1.5 applications.
1.6
1.7 - One framework generates code from both functional and relational
1.8 + \medskip One framework generates code from functional programs
1.9 + (including overloading using type classes) to SML \cite{SML}, OCaml
1.10 + \cite{OCaml} and Haskell \cite{haskell-revised-report}.
1.11 + Conceptually, code generation is split up in three steps:
1.12 + \emph{selection} of code theorems, \emph{translation} into an
1.13 + abstract executable view and \emph{serialization} to a specific
1.14 + \emph{target language}. Inductive specifications can be executed
1.15 + using the predicate compiler which operates within HOL.
1.16 + See \cite{isabelle-codegen} for an introduction.
1.17 +
1.18 + \begin{matharray}{rcl}
1.19 + @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.20 + @{attribute_def (HOL) code} & : & @{text attribute} \\
1.21 + @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
1.22 + @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
1.23 + @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.24 + @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
1.25 + @{attribute_def (HOL) code_post} & : & @{text attribute} \\
1.26 + @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.27 + @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.28 + @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.29 + @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
1.30 + @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
1.31 + @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
1.32 + @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
1.33 + @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
1.34 + @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
1.35 + @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
1.36 + @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
1.37 + \end{matharray}
1.38 +
1.39 + \begin{rail}
1.40 + 'export\_code' ( constexpr + ) \\
1.41 + ( ( 'in' target ( 'module\_name' string ) ? \\
1.42 + ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1.43 + ;
1.44 +
1.45 + const: term
1.46 + ;
1.47 +
1.48 + constexpr: ( const | 'name.*' | '*' )
1.49 + ;
1.50 +
1.51 + typeconstructor: nameref
1.52 + ;
1.53 +
1.54 + class: nameref
1.55 + ;
1.56 +
1.57 + target: 'OCaml' | 'SML' | 'Haskell'
1.58 + ;
1.59 +
1.60 + 'code' ( 'del' ) ?
1.61 + ;
1.62 +
1.63 + 'code\_abort' ( const + )
1.64 + ;
1.65 +
1.66 + 'code\_datatype' ( const + )
1.67 + ;
1.68 +
1.69 + 'code_inline' ( 'del' ) ?
1.70 + ;
1.71 +
1.72 + 'code_post' ( 'del' ) ?
1.73 + ;
1.74 +
1.75 + 'code\_thms' ( constexpr + ) ?
1.76 + ;
1.77 +
1.78 + 'code\_deps' ( constexpr + ) ?
1.79 + ;
1.80 +
1.81 + 'code\_const' (const + 'and') \\
1.82 + ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.83 + ;
1.84 +
1.85 + 'code\_type' (typeconstructor + 'and') \\
1.86 + ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.87 + ;
1.88 +
1.89 + 'code\_class' (class + 'and') \\
1.90 + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
1.91 + ;
1.92 +
1.93 + 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
1.94 + ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1.95 + ;
1.96 +
1.97 + 'code\_reserved' target ( string + )
1.98 + ;
1.99 +
1.100 + 'code\_monad' const const target
1.101 + ;
1.102 +
1.103 + 'code\_include' target ( string ( string | '-') )
1.104 + ;
1.105 +
1.106 + 'code\_modulename' target ( ( string string ) + )
1.107 + ;
1.108 +
1.109 + syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
1.110 + ;
1.111 +
1.112 + \end{rail}
1.113 +
1.114 + \begin{description}
1.115 +
1.116 + \item @{command (HOL) "export_code"} generates code for a given list
1.117 + of constants in the specified target language(s). If no serialization
1.118 + instruction is given, only abstract code is generated internally.
1.119 +
1.120 + Constants may be specified by giving them literally, referring to
1.121 + all executable contants within a certain theory by giving @{text
1.122 + "name.*"}, or referring to \emph{all} executable constants currently
1.123 + available by giving @{text "*"}.
1.124 +
1.125 + By default, for each involved theory one corresponding name space
1.126 + module is generated. Alternativly, a module name may be specified
1.127 + after the @{keyword "module_name"} keyword; then \emph{all} code is
1.128 + placed in this module.
1.129 +
1.130 + For \emph{SML} and \emph{OCaml}, the file specification refers to a
1.131 + single file; for \emph{Haskell}, it refers to a whole directory,
1.132 + where code is generated in multiple files reflecting the module
1.133 + hierarchy. The file specification ``@{text "-"}'' denotes standard
1.134 + output. For \emph{SML}, omitting the file specification compiles
1.135 + code internally in the context of the current ML session.
1.136 +
1.137 + Serializers take an optional list of arguments in parentheses. For
1.138 + \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
1.139 + explicit module signatures.
1.140 +
1.141 + For \emph{Haskell} a module name prefix may be given using the ``@{text
1.142 + "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
1.143 + "deriving (Read, Show)"}'' clause to each appropriate datatype
1.144 + declaration.
1.145 +
1.146 + \item @{attribute (HOL) code} explicitly selects (or with option
1.147 + ``@{text "del"}'' deselects) a code equation for code
1.148 + generation. Usually packages introducing code equations provide
1.149 + a reasonable default setup for selection.
1.150 +
1.151 + \item @{command (HOL) "code_abort"} declares constants which are not
1.152 + required to have a definition by means of code equations; if
1.153 + needed these are implemented by program abort instead.
1.154 +
1.155 + \item @{command (HOL) "code_datatype"} specifies a constructor set
1.156 + for a logical type.
1.157 +
1.158 + \item @{command (HOL) "print_codesetup"} gives an overview on
1.159 + selected code equations and code generator datatypes.
1.160 +
1.161 + \item @{attribute (HOL) code_inline} declares (or with
1.162 + option ``@{text "del"}'' removes) inlining theorems which are
1.163 + applied as rewrite rules to any code equation during
1.164 + preprocessing.
1.165 +
1.166 + \item @{attribute (HOL) code_post} declares (or with
1.167 + option ``@{text "del"}'' removes) theorems which are
1.168 + applied as rewrite rules to any result of an evaluation.
1.169 +
1.170 + \item @{command (HOL) "print_codeproc"} prints the setup
1.171 + of the code generator preprocessor.
1.172 +
1.173 + \item @{command (HOL) "code_thms"} prints a list of theorems
1.174 + representing the corresponding program containing all given
1.175 + constants after preprocessing.
1.176 +
1.177 + \item @{command (HOL) "code_deps"} visualizes dependencies of
1.178 + theorems representing the corresponding program containing all given
1.179 + constants after preprocessing.
1.180 +
1.181 + \item @{command (HOL) "code_const"} associates a list of constants
1.182 + with target-specific serializations; omitting a serialization
1.183 + deletes an existing serialization.
1.184 +
1.185 + \item @{command (HOL) "code_type"} associates a list of type
1.186 + constructors with target-specific serializations; omitting a
1.187 + serialization deletes an existing serialization.
1.188 +
1.189 + \item @{command (HOL) "code_class"} associates a list of classes
1.190 + with target-specific class names; omitting a serialization deletes
1.191 + an existing serialization. This applies only to \emph{Haskell}.
1.192 +
1.193 + \item @{command (HOL) "code_instance"} declares a list of type
1.194 + constructor / class instance relations as ``already present'' for a
1.195 + given target. Omitting a ``@{text "-"}'' deletes an existing
1.196 + ``already present'' declaration. This applies only to
1.197 + \emph{Haskell}.
1.198 +
1.199 + \item @{command (HOL) "code_reserved"} declares a list of names as
1.200 + reserved for a given target, preventing it to be shadowed by any
1.201 + generated code.
1.202 +
1.203 + \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1.204 + to generate monadic code for Haskell.
1.205 +
1.206 + \item @{command (HOL) "code_include"} adds arbitrary named content
1.207 + (``include'') to generated code. A ``@{text "-"}'' as last argument
1.208 + will remove an already added ``include''.
1.209 +
1.210 + \item @{command (HOL) "code_modulename"} declares aliasings from one
1.211 + module name onto another.
1.212 +
1.213 + \end{description}
1.214 +
1.215 + The other framework generates code from both functional and relational
1.216 programs to SML. See \cite{isabelle-HOL} for further information
1.217 (this actually covers the new-style theory format as well).
1.218
1.219 @@ -1011,209 +1218,6 @@
1.220 ;
1.221 \end{rail}
1.222
1.223 - \medskip The other framework generates code from functional programs
1.224 - (including overloading using type classes) to SML \cite{SML}, OCaml
1.225 - \cite{OCaml} and Haskell \cite{haskell-revised-report}.
1.226 - Conceptually, code generation is split up in three steps:
1.227 - \emph{selection} of code theorems, \emph{translation} into an
1.228 - abstract executable view and \emph{serialization} to a specific
1.229 - \emph{target language}. See \cite{isabelle-codegen} for an
1.230 - introduction on how to use it.
1.231 -
1.232 - \begin{matharray}{rcl}
1.233 - @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.234 - @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.235 - @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.236 - @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
1.237 - @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
1.238 - @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
1.239 - @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
1.240 - @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
1.241 - @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
1.242 - @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
1.243 - @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
1.244 - @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
1.245 - @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
1.246 - @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.247 - @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.248 - @{attribute_def (HOL) code} & : & @{text attribute} \\
1.249 - \end{matharray}
1.250 -
1.251 - \begin{rail}
1.252 - 'export\_code' ( constexpr + ) \\
1.253 - ( ( 'in' target ( 'module\_name' string ) ? \\
1.254 - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1.255 - ;
1.256 -
1.257 - 'code\_thms' ( constexpr + ) ?
1.258 - ;
1.259 -
1.260 - 'code\_deps' ( constexpr + ) ?
1.261 - ;
1.262 -
1.263 - const: term
1.264 - ;
1.265 -
1.266 - constexpr: ( const | 'name.*' | '*' )
1.267 - ;
1.268 -
1.269 - typeconstructor: nameref
1.270 - ;
1.271 -
1.272 - class: nameref
1.273 - ;
1.274 -
1.275 - target: 'OCaml' | 'SML' | 'Haskell'
1.276 - ;
1.277 -
1.278 - 'code\_datatype' ( const + )
1.279 - ;
1.280 -
1.281 - 'code\_const' (const + 'and') \\
1.282 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.283 - ;
1.284 -
1.285 - 'code\_type' (typeconstructor + 'and') \\
1.286 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.287 - ;
1.288 -
1.289 - 'code\_class' (class + 'and') \\
1.290 - ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
1.291 - ;
1.292 -
1.293 - 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
1.294 - ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1.295 - ;
1.296 -
1.297 - 'code\_monad' const const target
1.298 - ;
1.299 -
1.300 - 'code\_reserved' target ( string + )
1.301 - ;
1.302 -
1.303 - 'code\_include' target ( string ( string | '-') )
1.304 - ;
1.305 -
1.306 - 'code\_modulename' target ( ( string string ) + )
1.307 - ;
1.308 -
1.309 - 'code\_abort' ( const + )
1.310 - ;
1.311 -
1.312 - syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
1.313 - ;
1.314 -
1.315 - 'code' ( 'del' ) ?
1.316 - ;
1.317 -
1.318 - 'code_unfold' ( 'del' ) ?
1.319 - ;
1.320 -
1.321 - 'code_post' ( 'del' ) ?
1.322 - ;
1.323 - \end{rail}
1.324 -
1.325 - \begin{description}
1.326 -
1.327 - \item @{command (HOL) "export_code"} is the canonical interface for
1.328 - generating and serializing code: for a given list of constants, code
1.329 - is generated for the specified target languages. If no serialization
1.330 - instruction is given, only abstract code is generated internally.
1.331 -
1.332 - Constants may be specified by giving them literally, referring to
1.333 - all executable contants within a certain theory by giving @{text
1.334 - "name.*"}, or referring to \emph{all} executable constants currently
1.335 - available by giving @{text "*"}.
1.336 -
1.337 - By default, for each involved theory one corresponding name space
1.338 - module is generated. Alternativly, a module name may be specified
1.339 - after the @{keyword "module_name"} keyword; then \emph{all} code is
1.340 - placed in this module.
1.341 -
1.342 - For \emph{SML} and \emph{OCaml}, the file specification refers to a
1.343 - single file; for \emph{Haskell}, it refers to a whole directory,
1.344 - where code is generated in multiple files reflecting the module
1.345 - hierarchy. The file specification ``@{text "-"}'' denotes standard
1.346 - output. For \emph{SML}, omitting the file specification compiles
1.347 - code internally in the context of the current ML session.
1.348 -
1.349 - Serializers take an optional list of arguments in parentheses. For
1.350 - \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
1.351 - explicit module signatures.
1.352 -
1.353 - For \emph{Haskell} a module name prefix may be given using the ``@{text
1.354 - "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
1.355 - "deriving (Read, Show)"}'' clause to each appropriate datatype
1.356 - declaration.
1.357 -
1.358 - \item @{command (HOL) "code_thms"} prints a list of theorems
1.359 - representing the corresponding program containing all given
1.360 - constants.
1.361 -
1.362 - \item @{command (HOL) "code_deps"} visualizes dependencies of
1.363 - theorems representing the corresponding program containing all given
1.364 - constants.
1.365 -
1.366 - \item @{command (HOL) "code_datatype"} specifies a constructor set
1.367 - for a logical type.
1.368 -
1.369 - \item @{command (HOL) "code_const"} associates a list of constants
1.370 - with target-specific serializations; omitting a serialization
1.371 - deletes an existing serialization.
1.372 -
1.373 - \item @{command (HOL) "code_type"} associates a list of type
1.374 - constructors with target-specific serializations; omitting a
1.375 - serialization deletes an existing serialization.
1.376 -
1.377 - \item @{command (HOL) "code_class"} associates a list of classes
1.378 - with target-specific class names; omitting a serialization deletes
1.379 - an existing serialization. This applies only to \emph{Haskell}.
1.380 -
1.381 - \item @{command (HOL) "code_instance"} declares a list of type
1.382 - constructor / class instance relations as ``already present'' for a
1.383 - given target. Omitting a ``@{text "-"}'' deletes an existing
1.384 - ``already present'' declaration. This applies only to
1.385 - \emph{Haskell}.
1.386 -
1.387 - \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1.388 - to generate monadic code for Haskell.
1.389 -
1.390 - \item @{command (HOL) "code_reserved"} declares a list of names as
1.391 - reserved for a given target, preventing it to be shadowed by any
1.392 - generated code.
1.393 -
1.394 - \item @{command (HOL) "code_include"} adds arbitrary named content
1.395 - (``include'') to generated code. A ``@{text "-"}'' as last argument
1.396 - will remove an already added ``include''.
1.397 -
1.398 - \item @{command (HOL) "code_modulename"} declares aliasings from one
1.399 - module name onto another.
1.400 -
1.401 - \item @{command (HOL) "code_abort"} declares constants which are not
1.402 - required to have a definition by means of code equations; if
1.403 - needed these are implemented by program abort instead.
1.404 -
1.405 - \item @{attribute (HOL) code} explicitly selects (or with option
1.406 - ``@{text "del"}'' deselects) a code equation for code
1.407 - generation. Usually packages introducing code equations provide
1.408 - a reasonable default setup for selection.
1.409 -
1.410 - \item @{attribute (HOL) code_inline} declares (or with
1.411 - option ``@{text "del"}'' removes) inlining theorems which are
1.412 - applied as rewrite rules to any code equation during
1.413 - preprocessing.
1.414 -
1.415 - \item @{attribute (HOL) code_post} declares (or with
1.416 - option ``@{text "del"}'' removes) theorems which are
1.417 - applied as rewrite rules to any result of an evaluation.
1.418 -
1.419 - \item @{command (HOL) "print_codesetup"} gives an overview on
1.420 - selected code equations and code generator datatypes.
1.421 -
1.422 - \item @{command (HOL) "print_codeproc"} prints the setup
1.423 - of the code generator preprocessor.
1.424 -
1.425 - \end{description}
1.426 *}
1.427
1.428
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 14 10:38:29 2010 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 14 10:50:49 2010 +0200
2.3 @@ -981,7 +981,211 @@
2.4 instantiates these mechanisms in a way that is amenable to end-user
2.5 applications.
2.6
2.7 - One framework generates code from both functional and relational
2.8 + \medskip One framework generates code from functional programs
2.9 + (including overloading using type classes) to SML \cite{SML}, OCaml
2.10 + \cite{OCaml} and Haskell \cite{haskell-revised-report}.
2.11 + Conceptually, code generation is split up in three steps:
2.12 + \emph{selection} of code theorems, \emph{translation} into an
2.13 + abstract executable view and \emph{serialization} to a specific
2.14 + \emph{target language}. Inductive specifications can be executed
2.15 + using the predicate compiler which operates within HOL.
2.16 + See \cite{isabelle-codegen} for an introduction.
2.17 +
2.18 + \begin{matharray}{rcl}
2.19 + \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.20 + \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
2.21 + \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.22 + \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.23 + \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.24 + \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}}} & : & \isa{attribute} \\
2.25 + \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}}} & : & \isa{attribute} \\
2.26 + \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.27 + \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.28 + \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.29 + \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.30 + \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.31 + \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.32 + \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.33 + \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.34 + \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}} \\
2.35 + \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}} \\
2.36 + \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}} \\
2.37 + \end{matharray}
2.38 +
2.39 + \begin{rail}
2.40 + 'export\_code' ( constexpr + ) \\
2.41 + ( ( 'in' target ( 'module\_name' string ) ? \\
2.42 + ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
2.43 + ;
2.44 +
2.45 + const: term
2.46 + ;
2.47 +
2.48 + constexpr: ( const | 'name.*' | '*' )
2.49 + ;
2.50 +
2.51 + typeconstructor: nameref
2.52 + ;
2.53 +
2.54 + class: nameref
2.55 + ;
2.56 +
2.57 + target: 'OCaml' | 'SML' | 'Haskell'
2.58 + ;
2.59 +
2.60 + 'code' ( 'del' ) ?
2.61 + ;
2.62 +
2.63 + 'code\_abort' ( const + )
2.64 + ;
2.65 +
2.66 + 'code\_datatype' ( const + )
2.67 + ;
2.68 +
2.69 + 'code_inline' ( 'del' ) ?
2.70 + ;
2.71 +
2.72 + 'code_post' ( 'del' ) ?
2.73 + ;
2.74 +
2.75 + 'code\_thms' ( constexpr + ) ?
2.76 + ;
2.77 +
2.78 + 'code\_deps' ( constexpr + ) ?
2.79 + ;
2.80 +
2.81 + 'code\_const' (const + 'and') \\
2.82 + ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
2.83 + ;
2.84 +
2.85 + 'code\_type' (typeconstructor + 'and') \\
2.86 + ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
2.87 + ;
2.88 +
2.89 + 'code\_class' (class + 'and') \\
2.90 + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
2.91 + ;
2.92 +
2.93 + 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
2.94 + ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
2.95 + ;
2.96 +
2.97 + 'code\_reserved' target ( string + )
2.98 + ;
2.99 +
2.100 + 'code\_monad' const const target
2.101 + ;
2.102 +
2.103 + 'code\_include' target ( string ( string | '-') )
2.104 + ;
2.105 +
2.106 + 'code\_modulename' target ( ( string string ) + )
2.107 + ;
2.108 +
2.109 + syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
2.110 + ;
2.111 +
2.112 + \end{rail}
2.113 +
2.114 + \begin{description}
2.115 +
2.116 + \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
2.117 + of constants in the specified target language(s). If no serialization
2.118 + instruction is given, only abstract code is generated internally.
2.119 +
2.120 + Constants may be specified by giving them literally, referring to
2.121 + all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
2.122 + available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
2.123 +
2.124 + By default, for each involved theory one corresponding name space
2.125 + module is generated. Alternativly, a module name may be specified
2.126 + after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
2.127 + placed in this module.
2.128 +
2.129 + For \emph{SML} and \emph{OCaml}, the file specification refers to a
2.130 + single file; for \emph{Haskell}, it refers to a whole directory,
2.131 + where code is generated in multiple files reflecting the module
2.132 + hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
2.133 + output. For \emph{SML}, omitting the file specification compiles
2.134 + code internally in the context of the current ML session.
2.135 +
2.136 + Serializers take an optional list of arguments in parentheses. For
2.137 + \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
2.138 + explicit module signatures.
2.139 +
2.140 + 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
2.141 + declaration.
2.142 +
2.143 + \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
2.144 + ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
2.145 + generation. Usually packages introducing code equations provide
2.146 + a reasonable default setup for selection.
2.147 +
2.148 + \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
2.149 + required to have a definition by means of code equations; if
2.150 + needed these are implemented by program abort instead.
2.151 +
2.152 + \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
2.153 + for a logical type.
2.154 +
2.155 + \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
2.156 + selected code equations and code generator datatypes.
2.157 +
2.158 + \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
2.159 + option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
2.160 + applied as rewrite rules to any code equation during
2.161 + preprocessing.
2.162 +
2.163 + \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
2.164 + option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
2.165 + applied as rewrite rules to any result of an evaluation.
2.166 +
2.167 + \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
2.168 + of the code generator preprocessor.
2.169 +
2.170 + \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
2.171 + representing the corresponding program containing all given
2.172 + constants after preprocessing.
2.173 +
2.174 + \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
2.175 + theorems representing the corresponding program containing all given
2.176 + constants after preprocessing.
2.177 +
2.178 + \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
2.179 + with target-specific serializations; omitting a serialization
2.180 + deletes an existing serialization.
2.181 +
2.182 + \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
2.183 + constructors with target-specific serializations; omitting a
2.184 + serialization deletes an existing serialization.
2.185 +
2.186 + \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
2.187 + with target-specific class names; omitting a serialization deletes
2.188 + an existing serialization. This applies only to \emph{Haskell}.
2.189 +
2.190 + \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
2.191 + constructor / class instance relations as ``already present'' for a
2.192 + given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
2.193 + ``already present'' declaration. This applies only to
2.194 + \emph{Haskell}.
2.195 +
2.196 + \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
2.197 + reserved for a given target, preventing it to be shadowed by any
2.198 + generated code.
2.199 +
2.200 + \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
2.201 + to generate monadic code for Haskell.
2.202 +
2.203 + \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
2.204 + (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
2.205 + will remove an already added ``include''.
2.206 +
2.207 + \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
2.208 + module name onto another.
2.209 +
2.210 + \end{description}
2.211 +
2.212 + The other framework generates code from both functional and relational
2.213 programs to SML. See \cite{isabelle-HOL} for further information
2.214 (this actually covers the new-style theory format as well).
2.215
2.216 @@ -1025,208 +1229,7 @@
2.217
2.218 'code' (name)?
2.219 ;
2.220 - \end{rail}
2.221 -
2.222 - \medskip The other framework generates code from functional programs
2.223 - (including overloading using type classes) to SML \cite{SML}, OCaml
2.224 - \cite{OCaml} and Haskell \cite{haskell-revised-report}.
2.225 - Conceptually, code generation is split up in three steps:
2.226 - \emph{selection} of code theorems, \emph{translation} into an
2.227 - abstract executable view and \emph{serialization} to a specific
2.228 - \emph{target language}. See \cite{isabelle-codegen} for an
2.229 - introduction on how to use it.
2.230 -
2.231 - \begin{matharray}{rcl}
2.232 - \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.233 - \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.234 - \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.235 - \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.236 - \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.237 - \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.238 - \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.239 - \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.240 - \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}} \\
2.241 - \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.242 - \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}} \\
2.243 - \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}} \\
2.244 - \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
2.245 - \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.246 - \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.247 - \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
2.248 - \end{matharray}
2.249 -
2.250 - \begin{rail}
2.251 - 'export\_code' ( constexpr + ) \\
2.252 - ( ( 'in' target ( 'module\_name' string ) ? \\
2.253 - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
2.254 - ;
2.255 -
2.256 - 'code\_thms' ( constexpr + ) ?
2.257 - ;
2.258 -
2.259 - 'code\_deps' ( constexpr + ) ?
2.260 - ;
2.261 -
2.262 - const: term
2.263 - ;
2.264 -
2.265 - constexpr: ( const | 'name.*' | '*' )
2.266 - ;
2.267 -
2.268 - typeconstructor: nameref
2.269 - ;
2.270 -
2.271 - class: nameref
2.272 - ;
2.273 -
2.274 - target: 'OCaml' | 'SML' | 'Haskell'
2.275 - ;
2.276 -
2.277 - 'code\_datatype' ( const + )
2.278 - ;
2.279 -
2.280 - 'code\_const' (const + 'and') \\
2.281 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
2.282 - ;
2.283 -
2.284 - 'code\_type' (typeconstructor + 'and') \\
2.285 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
2.286 - ;
2.287 -
2.288 - 'code\_class' (class + 'and') \\
2.289 - ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
2.290 - ;
2.291 -
2.292 - 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
2.293 - ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
2.294 - ;
2.295 -
2.296 - 'code\_monad' const const target
2.297 - ;
2.298 -
2.299 - 'code\_reserved' target ( string + )
2.300 - ;
2.301 -
2.302 - 'code\_include' target ( string ( string | '-') )
2.303 - ;
2.304 -
2.305 - 'code\_modulename' target ( ( string string ) + )
2.306 - ;
2.307 -
2.308 - 'code\_abort' ( const + )
2.309 - ;
2.310 -
2.311 - syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
2.312 - ;
2.313 -
2.314 - 'code' ( 'del' ) ?
2.315 - ;
2.316 -
2.317 - 'code_unfold' ( 'del' ) ?
2.318 - ;
2.319 -
2.320 - 'code_post' ( 'del' ) ?
2.321 - ;
2.322 - \end{rail}
2.323 -
2.324 - \begin{description}
2.325 -
2.326 - \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for
2.327 - generating and serializing code: for a given list of constants, code
2.328 - is generated for the specified target languages. If no serialization
2.329 - instruction is given, only abstract code is generated internally.
2.330 -
2.331 - Constants may be specified by giving them literally, referring to
2.332 - all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
2.333 - available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
2.334 -
2.335 - By default, for each involved theory one corresponding name space
2.336 - module is generated. Alternativly, a module name may be specified
2.337 - after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
2.338 - placed in this module.
2.339 -
2.340 - For \emph{SML} and \emph{OCaml}, the file specification refers to a
2.341 - single file; for \emph{Haskell}, it refers to a whole directory,
2.342 - where code is generated in multiple files reflecting the module
2.343 - hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
2.344 - output. For \emph{SML}, omitting the file specification compiles
2.345 - code internally in the context of the current ML session.
2.346 -
2.347 - Serializers take an optional list of arguments in parentheses. For
2.348 - \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
2.349 - explicit module signatures.
2.350 -
2.351 - 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
2.352 - declaration.
2.353 -
2.354 - \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
2.355 - representing the corresponding program containing all given
2.356 - constants.
2.357 -
2.358 - \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
2.359 - theorems representing the corresponding program containing all given
2.360 - constants.
2.361 -
2.362 - \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
2.363 - for a logical type.
2.364 -
2.365 - \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
2.366 - with target-specific serializations; omitting a serialization
2.367 - deletes an existing serialization.
2.368 -
2.369 - \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
2.370 - constructors with target-specific serializations; omitting a
2.371 - serialization deletes an existing serialization.
2.372 -
2.373 - \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
2.374 - with target-specific class names; omitting a serialization deletes
2.375 - an existing serialization. This applies only to \emph{Haskell}.
2.376 -
2.377 - \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
2.378 - constructor / class instance relations as ``already present'' for a
2.379 - given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
2.380 - ``already present'' declaration. This applies only to
2.381 - \emph{Haskell}.
2.382 -
2.383 - \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
2.384 - to generate monadic code for Haskell.
2.385 -
2.386 - \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
2.387 - reserved for a given target, preventing it to be shadowed by any
2.388 - generated code.
2.389 -
2.390 - \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
2.391 - (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
2.392 - will remove an already added ``include''.
2.393 -
2.394 - \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
2.395 - module name onto another.
2.396 -
2.397 - \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
2.398 - required to have a definition by means of code equations; if
2.399 - needed these are implemented by program abort instead.
2.400 -
2.401 - \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
2.402 - ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
2.403 - generation. Usually packages introducing code equations provide
2.404 - a reasonable default setup for selection.
2.405 -
2.406 - \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
2.407 - option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
2.408 - applied as rewrite rules to any code equation during
2.409 - preprocessing.
2.410 -
2.411 - \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
2.412 - option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
2.413 - applied as rewrite rules to any result of an evaluation.
2.414 -
2.415 - \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
2.416 - selected code equations and code generator datatypes.
2.417 -
2.418 - \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
2.419 - of the code generator preprocessor.
2.420 -
2.421 - \end{description}%
2.422 + \end{rail}%
2.423 \end{isamarkuptext}%
2.424 \isamarkuptrue%
2.425 %