# HG changeset patch # User blanchet # Date 1409870461 -7200 # Node ID 89034dc402476e2e7e8b8ddeb8dc722fc37fa1d8 # Parent 9d714be4f02827e8462b89d3d873b10cf3d56212 updated docs diff -r 9d714be4f028 -r 89034dc40247 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 05 00:41:01 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 05 00:41:01 2014 +0200 @@ -128,9 +128,9 @@ %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,'' %describes the package's programmatic interface. -%\item Section \ref{sec:interoperability}, ``Interoperability,'' -%is concerned with the packages' interaction with other Isabelle packages and -%tools, such as the code generator and the counterexample generators. +\item Section \ref{sec:plugins}, ``Plugins,'' +is concerned with the package's interoperability with other Isabelle packages +and tools, such as Transfer, Lifting, and Quickcheck. %\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and %Limitations,'' concludes with known open issues at the time of writing. @@ -482,7 +482,9 @@ (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \ @{syntax map_rel}? (@'where' (prop + '|'))? + @'and') ; - @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')' + @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +) + ; + @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels' | 'no_code') + ',') ')' ; @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +) \} @@ -497,13 +499,17 @@ context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}), and \synt{prop} denotes a HOL proposition. -The optional target is optionally followed by one or both of the following +The optional target is optionally followed by a combination of the following options: \begin{itemize} \setlength{\itemsep}{0pt} \item +The @{text "plugins"} option indicates which plugins should be enabled +(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. + +\item The @{text "discs_sels"} option indicates that discriminators and selectors should be generated. The option is implicitly enabled if names are specified for discriminators or selectors. @@ -536,7 +542,7 @@ The optional names preceding the type variables allow to override the default names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type -arguments can be marked as dead by entering ``@{text dead}'' in front of the +arguments can be marked as dead by entering @{text dead} in front of the type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead (and a set function is generated or not) depending on where they occur in the right-hand sides of the definition. Declaring a type argument as dead can speed @@ -659,9 +665,7 @@ Relator: & @{text t.rel_t} \\ Recursor: & - @{text t.rec_t} \\ -Size function: & - @{text t.size_t} + @{text t.rec_t} \end{tabular} \medskip @@ -670,9 +674,6 @@ The case combinator, discriminators, and selectors are collectively called \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the names and is normally hidden. - -In addition to the above, the @{class size} class is instantiated to overload the -@{const size} function based on @{text t.size_t}. *} @@ -1012,18 +1013,6 @@ @{thm list.rec(1)[no_vars]} \\ @{thm list.rec(2)[no_vars]} -\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\ -@{thm list.rec_o_map[no_vars]} - -\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\ -@{thm list.size(1)[no_vars]} \\ -@{thm list.size(2)[no_vars]} \\ -@{thm list.size(3)[no_vars]} \\ -@{thm list.size(4)[no_vars]} - -\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\ -@{thm list.size_o_map[no_vars]} - \end{description} \end{indentblock} @@ -1054,12 +1043,9 @@ \item \emph{The Standard ML interfaces are different.} Tools and extensions written to call the old ML interfaces will need to be adapted to the new -interfaces. This concerns Quickcheck in particular. Whenever possible, it is -recommended to use @{command datatype_compat} to register new-style datatypes -as old-style datatypes. - -\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are -now called @{text case_t}, @{text rec_t}, and @{text size_t}.} +interfaces. Whenever possible, it is recommended to use +@{command datatype_compat} to register new-style datatypes as old-style +datatypes. \item \emph{The recursor @{text rec_t} has a different signature for nested recursive datatypes.} In the old package, nested recursion through non-functions @@ -1739,7 +1725,7 @@ with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the -recursor is replaced by a dual concept and no size function is produced: +recursor is replaced by a dual concept: \medskip @@ -2622,7 +2608,8 @@ @{rail \ @@{command bnf} target? (name ':')? type \ 'map:' term ('sets:' (term +))? 'bd:' term \ - ('wits:' (term +))? ('rel:' term)? + ('wits:' (term +))? ('rel:' term)? \ + @{syntax plugins}? \} \medskip @@ -2650,8 +2637,9 @@ \end{matharray} @{rail \ - @@{command bnf_axiomatization} target? @{syntax tyargs}? name \ - @{syntax wit_types}? mixfix? @{syntax map_rel}? + @@{command bnf_axiomatization} target? @{syntax plugins}? \ + @{syntax tyargs}? name @{syntax wit_types}? \ + mixfix? @{syntax map_rel}? ; @{syntax_def wit_types}: '[' 'wits' ':' types ']' \} @@ -2669,7 +2657,7 @@ parenthesized mixfix notation \cite{isabelle-isar-ref}. Type arguments are live by default; they can be marked as dead by entering -``@{text dead}'' in front of the type variable (e.g., ``@{text "(dead 'a)"}'') +@{text dead} in front of the type variable (e.g., ``@{text "(dead 'a)"}'') instead of an identifier for the corresponding set function. Witnesses can be specified by their types. Otherwise, the syntax of @{command bnf_axiomatization} is identical to the left-hand side of a @{command datatype_new} or @@ -2779,35 +2767,78 @@ *) -(* -section {* Interoperability - \label{sec:interoperability} *} +section {* Plugins + \label{sec:plugins} *} + +text {* +Plugins extend the (co)datatype package to interoperate with other Isabelle +packages and tools, such as Transfer, Lifting, and Quickcheck. They can be +enabled or disabled individually using the @{syntax plugins} option to +@{command datatype_new}, @{command codatatype}, @{command free_constructors}, +@{command bnf}, and @{command bnf_axiomatization}. For example: +*} + + datatype_new (plugins del: size) color = Red | Black + + +subsection {* Size + \label{ssec:size} *} text {* -The package's interaction with other Isabelle packages and tools, such as the -code generator and the counterexample generators. +For each datatype, the @{text size} plugin generates a parameterized size +function @{text "t.size_t"} as well as a specific instance +@{text "size \ t \ bool"} belonging to the @{text size} type +class. The \keyw{fun} command relies on @{const size} to prove termination of +recursive functions on datatypes. + +The plugin derives the following properties: + +\begin{indentblock} +\begin{description} + +\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\ +@{thm list.size(1)[no_vars]} \\ +@{thm list.size(2)[no_vars]} \\ +@{thm list.size(3)[no_vars]} \\ +@{thm list.size(4)[no_vars]} + +\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\ +@{thm list.rec_o_map[no_vars]} + +\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\ +@{thm list.size_o_map[no_vars]} +(This property is not generated for all datatypes.) + +\end{description} +\end{indentblock} *} -subsection {* Transfer and Lifting - \label{ssec:transfer-and-lifting} *} - - -subsection {* Code Generator - \label{ssec:code-generator} *} +subsection {* Transfer + \label{ssec:transfer} *} + +text {* +The @{text transfer} plugin generates properties and attributes that guide the +Transfer tool. +*} + + +subsection {* Lifting + \label{ssec:lifting} *} + +text {* +The @{text lifting} plugin generates properties that guide the Lifting tool. +*} subsection {* Quickcheck \label{ssec:quickcheck} *} - -subsection {* Nitpick - \label{ssec:nitpick} *} - - -subsection {* Nominal Isabelle - \label{ssec:nominal-isabelle} *} -*) +text {* +The integration with Quickcheck is accomplished by a number of plugins that +instantiate specific type classes: @{text random}, @{text exhaustive}, +@{text bounded_forall}, @{text full_exhaustive}, @{text narrowing}. +*} (* @@ -2821,8 +2852,6 @@ text {* %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) % -%* partial documentation -% %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them % (for @{command datatype_compat} and prim(co)rec) %