diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/Codegen/Thy/document/Program.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Program.tex Tue Mar 03 11:00:51 2009 +0100 @@ -0,0 +1,1250 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Program}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Program\isanewline +\isakeyword{imports}\ Introduction\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Turning Theories into Programs \label{sec:program}% +} +\isamarkuptrue% +% +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +We have already seen how by default equations stemming from + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} + statements are used for code generation. This default behaviour + can be changed, e.g. by providing different code equations. + All kinds of customisation shown in this section is \emph{safe} + in the sense that the user does not have to worry about + correctness -- all programs generatable that way are partially + correct.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Selecting code equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Coming back to our introductory example, we + could provide an alternative code equations for \isa{dequeue} + explicitly:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} + \isa{attribute} which states that the given theorems should be + considered as code equations for a \isa{fun} statement -- + the corresponding constant is determined syntactically. The resulting code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ +\hspace*{0pt}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been + replaced by the predicate \isa{null\ xs}. This is due to the default + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). + + Changing the default constructor set of datatypes is also + possible. See \secref{sec:datatypes} for an example. + + As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + For explorative purpose, this collection + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% +\ dequeue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent prints a table with \emph{all} code equations + for \isa{dequeue}, including + \emph{all} code equations those equations depend + on recursively. + + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph + visualising dependencies between code equations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{\isa{class} and \isa{instantiation}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Concerning type classes and code generation, let us examine an example + from abstract algebra:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{class}\isamarkupfalse% +\ semigroup\ {\isacharequal}\isanewline +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{class}\isamarkupfalse% +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instantiation}\isamarkupfalse% +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent We define the natural operation of the natural numbers + on monoids:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we use to define the discrete exponentiation function:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The corresponding code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}module Example where {\char123}\\ +\hspace*{0pt}\\ +\hspace*{0pt}\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}class Semigroup a where {\char123}\\ +\hspace*{0pt} ~mult ::~a -> a -> a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ +\hspace*{0pt} ~neutral ::~a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Semigroup Nat where {\char123}\\ +\hspace*{0pt} ~mult = mult{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Monoid Nat where {\char123}\\ +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}bexp ::~Nat -> Nat;\\ +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}{\char125}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This is a convenient place to show how explicit dictionary construction + manifests in generated code (here, the same example in \isa{SML}):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ +\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ +\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\ +\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val monoid{\char95}nat =\\ +\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\ +\hspace*{0pt} ~nat monoid;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Note the parameters with trailing underscore (\verb|A_|) + which are the dictionary parameters.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The preprocessor \label{sec:preproc}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Before selected function theorems are turned into abstract + code, a chain of definitional transformation steps is carried + out: \emph{preprocessing}. In essence, the preprocessor + consists of two components: a \emph{simpset} and \emph{function transformers}. + + The \emph{simpset} allows to employ the full generality of the Isabelle + simplifier. Due to the interpretation of theorems + as code equations, rewrites are applied to the right + hand side and the arguments of the left hand side of an + equation, but never to the constant heading the left hand side. + An important special case are \emph{inline theorems} which may be + declared and undeclared using the + \emph{code inline} or \emph{code inline del} attribute respectively. + + Some common applications:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{itemize} +% +\begin{isamarkuptext}% +\item replacing non-executable constructs by executable ones:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item eliminating superfluous constants:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item replacing executable but inconvenient constructs:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\end{itemize} +% +\begin{isamarkuptext}% +\noindent \emph{Function transformers} provide a very general interface, + transforming a list of function theorems to another + list of function theorems, provided that neither the heading + constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} + pattern elimination implemented in + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this + interface. + + \noindent The current setup of the preprocessor may be inspected using + the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on code equations. + + \begin{warn} + The attribute \emph{code unfold} + associated with the \isa{SML\ code\ generator} also applies to + the \isa{generic\ code\ generator}: + \emph{code unfold} implies \emph{code inline}. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Datatypes \label{sec:datatypes}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Conceptually, any datatype is spanned by a set of + \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in + \isa{{\isasymtau}}. The HOL datatype package by default registers any new + datatype in the table of datatypes, which may be inspected using the + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. + + In some cases, it is appropriate to alter or extend this table. As + an example, we will develop an alternative representation of the + queue example given in \secref{sec:intro}. The amortised + representation is convenient for generating code but exposes its + \qt{implementation} details, which may be cumbersome when proving + theorems about it. Therefore, here a simple, straightforward + representation of queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we can use directly for proving; for executing, + we provide an alternative characterisation:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% +\ AQueue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which + is defined in terms of \isa{Queue} and interprets its arguments + according to what the \emph{content} of an amortised queue is supposed + to be. Equipped with this, we are able to prove the following equations + for our primitive queue operations which \qt{implement} the simple + queues in an amortised fashion:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp{\isacharunderscore}all% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent For completeness, we provide a substitute for the + \isa{case} combinator on queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\isanewline +\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The resulting code looks as expected:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun foldl f a [] = a\\ +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun null [] = true\\ +\hspace*{0pt} ~| null (x ::~xs) = false;\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent From this example, it can be glimpsed that using own + constructor sets is a little delicate since it changes the set of + valid patterns for values of that type. Without going into much + detail, here some practical hints: + + \begin{itemize} + + \item When changing the constructor set for datatypes, take care + to provide an alternative for the \isa{case} combinator + (e.g.~by replacing it using the preprocessor). + + \item Values in the target language need not to be normalised -- + different values in the target language may represent the same + value in the logic. + + \item Usually, a good methodology to deal with the subtleties of + pattern matching is to see the type as an abstract type: provide + a set of operations which operate on the concrete representation + of the type, and derive further operations by combinations of + these primitive ones, without relying on a particular + representation. + + \end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Equality and wellsortedness% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Surely you have already noticed how equality is treated + by the code generator:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The membership test during preprocessing is rewritten, + resulting in \isa{op\ mem}, which itself + performs an explicit equality check.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun member A{\char95}~x [] = false\\ +\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ +\hspace*{0pt} ~~~(if member A{\char95}~z xs\\ +\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\ +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Obviously, polymorphic equality is implemented the Haskell + way using a type class. How is this achieved? HOL introduces + an explicit class \isa{eq} with a corresponding operation + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. + The preprocessing framework does the rest by propagating the + \isa{eq} constraints through all dependent code equations. + For datatypes, instances of \isa{eq} are implicitly derived + when possible. For other types, you may instantiate \isa{eq} + manually like any other type class. + + Though this \isa{eq} class is designed to get rarely in + the way, a subtlety + enters the stage when definitions of overloaded constants + are dependent on operational equality. For example, let + us define a lexicographic ordering on tuples + (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{instantiation}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{proof}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +\ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Then code generation will fail. Why? The definition + of \isa{op\ {\isasymle}} depends on equality on both arguments, + which are polymorphic and impose an additional \isa{eq} + class constraint, which the preprocessor does not propagate + (for technical reasons). + + The solution is to add \isa{eq} explicitly to the first sort arguments in the + code theorems:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Then code generation succeeds:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\ +\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\ +\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\ +\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ +\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ +\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\ +\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\ +\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ +\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ +\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\ +\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +In some cases, the automatically derived code equations + for equality on a particular type may not be appropriate. + As example, watch the following datatype representing + monomorphic parametric types (where type constructors + are referred to by natural numbers):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{datatype}\isamarkupfalse% +\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent Then code generation for SML would fail with a message + that the generated code contains illegal mutual dependencies: + the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the + instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires + \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually + recursive \isa{instance} and \isa{function} definitions, + but the SML serialiser does not support this. + + In such cases, you have to provide your own equality equations + involving auxiliary constants. In our case, + \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline +\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example = \\ +\hspace*{0pt}struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun null [] = true\\ +\hspace*{0pt} ~| null (x ::~xs) = false;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\ +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\ +\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\ +\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\ +\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\ +\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\isamarkupsubsection{Explicit partiality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Partiality usually enters the game by partial patterns, as + in the following example, again for amortised queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In the corresponding code, there is no equation + for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~let {\char123}\\ +\hspace*{0pt} ~~~(y :~ys) = rev xs;\\ +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In some cases it is desirable to have this + pseudo-\qt{partiality} more explicitly, e.g.~as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{axiomatization}\isamarkupfalse% +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs + which is unspecified. + + Normally, if constants without any code equations occur in a + program, the code generator complains (since in most cases this is + not what the user expects). But such constants can also be thought + of as function definitions with no equations 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 \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% +\ empty{\isacharunderscore}queue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Then the code generator will just insert an error or + exception at the appropriate position:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ +\hspace*{0pt}\\ +\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\ +\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This feature however is rarely needed in practice. + Note also that the \isa{HOL} default setup already declares + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most + likely to be used in such situations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\ \end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: