# HG changeset patch
# User haftmann
# Date 1527068234 0
# Node ID 3a7f257dcac70306620cfcbe66f91cf6fbabc933
# Parent  a8660a39e304ce64919680f025006ed973b19517
more complete and more correct documentation on code generation

diff -r a8660a39e304 -r 3a7f257dcac7 src/Doc/Codegen/Foundations.thy
--- 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>
 
 
diff -r a8660a39e304 -r 3a7f257dcac7 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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.