more complete and more correct documentation on code generation
authorhaftmann
Wed May 23 09:37:14 2018 +0000 (21 months ago)
changeset 682543a7f257dcac7
parent 68253 a8660a39e304
child 68258 4e7937704843
more complete and more correct documentation on code generation
src/Doc/Codegen/Foundations.thy
src/Doc/Isar_Ref/HOL_Specific.thy
     1.1 --- a/src/Doc/Codegen/Foundations.thy	Wed May 23 07:13:11 2018 +0000
     1.2 +++ b/src/Doc/Codegen/Foundations.thy	Wed May 23 09:37:14 2018 +0000
     1.3 @@ -152,9 +152,16 @@
     1.4    using the @{command_def print_codeproc} command.  @{command_def
     1.5    code_thms} (see \secref{sec:equations}) provides a convenient
     1.6    mechanism to inspect the impact of a preprocessor setup on code
     1.7 -  equations.
     1.8 +  equations.  Attribute @{attribute code_preproc_trace} allows
     1.9 +  for low-level tracing:
    1.10  \<close>
    1.11  
    1.12 +declare %quote [[code_preproc_trace]]
    1.13 +
    1.14 +declare %quote [[code_preproc_trace only: distinct remdups]]
    1.15 +
    1.16 +declare %quote [[code_preproc_trace off]]
    1.17 +
    1.18  
    1.19  subsection \<open>Understanding code equations \label{sec:equations}\<close>
    1.20  
    1.21 @@ -282,14 +289,15 @@
    1.22  \<close>
    1.23  
    1.24  text \<open>
    1.25 -  \noindent In some cases it is desirable to have this
    1.26 +  \noindent In some cases it is desirable to state this
    1.27    pseudo-\qt{partiality} more explicitly, e.g.~as follows:
    1.28  \<close>
    1.29  
    1.30  axiomatization %quote empty_queue :: 'a
    1.31  
    1.32  definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
    1.33 -  "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
    1.34 +  "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q')
    1.35 +    | _ \<Rightarrow> empty_queue)"
    1.36  
    1.37  lemma %quote strict_dequeue'_AQueue [code]:
    1.38    "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
    1.39 @@ -301,11 +309,11 @@
    1.40  text \<open>
    1.41    Observe that on the right hand side of the definition of @{const
    1.42    "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
    1.43 -
    1.44 -  Normally, if constants without any code equations occur in a
    1.45 -  program, the code generator complains (since in most cases this is
    1.46 -  indeed an error).  But such constants can also be thought
    1.47 -  of as function definitions which always fail,
    1.48 +  An attempt to generate code for @{const strict_dequeue'} would
    1.49 +  make the code generator complain that @{const empty_queue} has
    1.50 +  no associated code equations.  In most situations unimplemented
    1.51 +  constants indeed indicated a broken program; however such
    1.52 +  constants can also be thought of as function definitions which always fail,
    1.53    since there is never a successful pattern match on the left hand
    1.54    side.  In order to categorise a constant into that category
    1.55    explicitly, use the @{attribute code} attribute with
    1.56 @@ -325,9 +333,14 @@
    1.57  
    1.58  text \<open>
    1.59    \noindent This feature however is rarely needed in practice.  Note
    1.60 -  also that the HOL default setup already declares @{const undefined},
    1.61 -  which is most likely to be used in such situations, as
    1.62 -  @{text "code abort"}.
    1.63 +  that the HOL default setup already includes
    1.64 +\<close>
    1.65 +
    1.66 +declare %quote [[code abort: undefined]]
    1.67 +
    1.68 +text \<open>
    1.69 +  \noindent -- hence @{const undefined} can always be used in such
    1.70 +  situations.
    1.71  \<close>
    1.72  
    1.73  
     2.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed May 23 07:13:11 2018 +0000
     2.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed May 23 09:37:14 2018 +0000
     2.3 @@ -2307,8 +2307,8 @@
     2.4      ;
     2.5      target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     2.6      ;
     2.7 -    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
     2.8 -      | 'drop:' ( const + ) | 'abort:' ( const + ) )?
     2.9 +    @@{attribute (HOL) code} ( 'equation' | 'nbe' | 'abstype' | 'abstract'
    2.10 +      | 'del' | 'drop:' ( const + ) | 'abort:' ( const + ) )?
    2.11      ;
    2.12      @@{command (HOL) code_datatype} ( const + )
    2.13      ;
    2.14 @@ -2316,7 +2316,7 @@
    2.15      ;
    2.16      @@{attribute (HOL) code_post} ( 'del' ) ?
    2.17      ;
    2.18 -    @@{attribute (HOL) code_abbrev}
    2.19 +    @@{attribute (HOL) code_abbrev} ( 'del' ) ?
    2.20      ;
    2.21      @@{command (HOL) code_thms} ( constexpr + ) ?
    2.22      ;
    2.23 @@ -2401,29 +2401,37 @@
    2.24  
    2.25    Serializers take an optional list of arguments in parentheses.
    2.26  
    2.27 -  For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
    2.28 -  argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause 
    2.29 -  to each appropriate datatype declaration.
    2.30 -
    2.31 -  For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
    2.32 -  case-insensitive file systems.
    2.33 -
    2.34 -  \<^descr> @{attribute (HOL) code} declare code equations for code generation.
    2.35 +      \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
    2.36 +      argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause 
    2.37 +      to each appropriate datatype declaration.
    2.38 +
    2.39 +      \<^item> For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
    2.40 +      case-insensitive file systems.
    2.41 +
    2.42 +  \<^descr> @{attribute (HOL) code} declares code equations for code generation.
    2.43 +
    2.44    Variant \<open>code equation\<close> declares a conventional equation as code equation.
    2.45 +
    2.46    Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
    2.47    certificates or code equations on abstract datatype representations
    2.48 -  respectively. Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstype\<close>
    2.49 -  depending on the syntactic shape of the underlying equation. Variant \<open>code
    2.50 -  del\<close> deselects a code equation for code generation.
    2.51 +  respectively.
    2.52 +
    2.53 +  Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstract\<close>
    2.54 +  depending on the syntactic shape of the underlying equation.
    2.55 +
    2.56 +  Variant \<open>code del\<close> deselects a code equation for code generation.
    2.57 +
    2.58 +  Variant \<open>code nbe\<close> accepts also non-left-linear equations for
    2.59 +  \<^emph>\<open>normalization by evaluation\<close> only.
    2.60  
    2.61    Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
    2.62 -  and drop all code equations declared for them. In the case of {text abort},
    2.63 -  these constants then are are not required to have a definition by means of
    2.64 +  and drop all code equations declared for them. In the case of \<open>abort\<close>,
    2.65 +  these constants then do not require to a specification by means of
    2.66    code equations; if needed these are implemented by program abort (exception)
    2.67    instead.
    2.68  
    2.69 -  Usually packages introducing code equations provide a reasonable default
    2.70 -  setup for selection.
    2.71 +  Packages declaring code equations usually provide a reasonable default
    2.72 +  setup.
    2.73  
    2.74    \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
    2.75    type.