--- a/src/Doc/Codegen/Foundations.thy Wed May 23 07:13:11 2018 +0000
+++ b/src/Doc/Codegen/Foundations.thy Wed May 23 09:37:14 2018 +0000
@@ -152,9 +152,16 @@
using the @{command_def print_codeproc} command. @{command_def
code_thms} (see \secref{sec:equations}) provides a convenient
mechanism to inspect the impact of a preprocessor setup on code
- equations.
+ equations. Attribute @{attribute code_preproc_trace} allows
+ for low-level tracing:
\<close>
+declare %quote [[code_preproc_trace]]
+
+declare %quote [[code_preproc_trace only: distinct remdups]]
+
+declare %quote [[code_preproc_trace off]]
+
subsection \<open>Understanding code equations \label{sec:equations}\<close>
@@ -282,14 +289,15 @@
\<close>
text \<open>
- \noindent In some cases it is desirable to have this
+ \noindent In some cases it is desirable to state this
pseudo-\qt{partiality} more explicitly, e.g.~as follows:
\<close>
axiomatization %quote empty_queue :: 'a
definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
+ "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q')
+ | _ \<Rightarrow> empty_queue)"
lemma %quote strict_dequeue'_AQueue [code]:
"strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
@@ -301,11 +309,11 @@
text \<open>
Observe that on the right hand side of the definition of @{const
"strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
-
- Normally, if constants without any code equations occur in a
- program, the code generator complains (since in most cases this is
- indeed an error). But such constants can also be thought
- of as function definitions which always fail,
+ An attempt to generate code for @{const strict_dequeue'} would
+ make the code generator complain that @{const empty_queue} has
+ no associated code equations. In most situations unimplemented
+ constants indeed indicated a broken program; however such
+ constants can also be thought of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use the @{attribute code} attribute with
@@ -325,9 +333,14 @@
text \<open>
\noindent This feature however is rarely needed in practice. Note
- also that the HOL default setup already declares @{const undefined},
- which is most likely to be used in such situations, as
- @{text "code abort"}.
+ that the HOL default setup already includes
+\<close>
+
+declare %quote [[code abort: undefined]]
+
+text \<open>
+ \noindent -- hence @{const undefined} can always be used in such
+ situations.
\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed May 23 07:13:11 2018 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed May 23 09:37:14 2018 +0000
@@ -2307,8 +2307,8 @@
;
target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
;
- @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
- | 'drop:' ( const + ) | 'abort:' ( const + ) )?
+ @@{attribute (HOL) code} ( 'equation' | 'nbe' | 'abstype' | 'abstract'
+ | 'del' | 'drop:' ( const + ) | 'abort:' ( const + ) )?
;
@@{command (HOL) code_datatype} ( const + )
;
@@ -2316,7 +2316,7 @@
;
@@{attribute (HOL) code_post} ( 'del' ) ?
;
- @@{attribute (HOL) code_abbrev}
+ @@{attribute (HOL) code_abbrev} ( 'del' ) ?
;
@@{command (HOL) code_thms} ( constexpr + ) ?
;
@@ -2401,29 +2401,37 @@
Serializers take an optional list of arguments in parentheses.
- For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
- argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause
- to each appropriate datatype declaration.
-
- For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
- case-insensitive file systems.
-
- \<^descr> @{attribute (HOL) code} declare code equations for code generation.
+ \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
+ argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause
+ to each appropriate datatype declaration.
+
+ \<^item> For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
+ case-insensitive file systems.
+
+ \<^descr> @{attribute (HOL) code} declares code equations for code generation.
+
Variant \<open>code equation\<close> declares a conventional equation as code equation.
+
Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
certificates or code equations on abstract datatype representations
- respectively. Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstype\<close>
- depending on the syntactic shape of the underlying equation. Variant \<open>code
- del\<close> deselects a code equation for code generation.
+ respectively.
+
+ Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstract\<close>
+ depending on the syntactic shape of the underlying equation.
+
+ Variant \<open>code del\<close> deselects a code equation for code generation.
+
+ Variant \<open>code nbe\<close> accepts also non-left-linear equations for
+ \<^emph>\<open>normalization by evaluation\<close> only.
Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
- and drop all code equations declared for them. In the case of {text abort},
- these constants then are are not required to have a definition by means of
+ and drop all code equations declared for them. In the case of \<open>abort\<close>,
+ these constants then do not require to a specification by means of
code equations; if needed these are implemented by program abort (exception)
instead.
- Usually packages introducing code equations provide a reasonable default
- setup for selection.
+ Packages declaring code equations usually provide a reasonable default
+ setup.
\<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
type.