1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Codegen/Thy/document/Program.tex Tue Mar 03 11:00:51 2009 +0100
1.3 @@ -0,0 +1,1250 @@
1.4 +%
1.5 +\begin{isabellebody}%
1.6 +\def\isabellecontext{Program}%
1.7 +%
1.8 +\isadelimtheory
1.9 +%
1.10 +\endisadelimtheory
1.11 +%
1.12 +\isatagtheory
1.13 +\isacommand{theory}\isamarkupfalse%
1.14 +\ Program\isanewline
1.15 +\isakeyword{imports}\ Introduction\isanewline
1.16 +\isakeyword{begin}%
1.17 +\endisatagtheory
1.18 +{\isafoldtheory}%
1.19 +%
1.20 +\isadelimtheory
1.21 +%
1.22 +\endisadelimtheory
1.23 +%
1.24 +\isamarkupsection{Turning Theories into Programs \label{sec:program}%
1.25 +}
1.26 +\isamarkuptrue%
1.27 +%
1.28 +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
1.29 +}
1.30 +\isamarkuptrue%
1.31 +%
1.32 +\begin{isamarkuptext}%
1.33 +We have already seen how by default equations stemming from
1.34 + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
1.35 + statements are used for code generation. This default behaviour
1.36 + can be changed, e.g. by providing different code equations.
1.37 + All kinds of customisation shown in this section is \emph{safe}
1.38 + in the sense that the user does not have to worry about
1.39 + correctness -- all programs generatable that way are partially
1.40 + correct.%
1.41 +\end{isamarkuptext}%
1.42 +\isamarkuptrue%
1.43 +%
1.44 +\isamarkupsubsection{Selecting code equations%
1.45 +}
1.46 +\isamarkuptrue%
1.47 +%
1.48 +\begin{isamarkuptext}%
1.49 +Coming back to our introductory example, we
1.50 + could provide an alternative code equations for \isa{dequeue}
1.51 + explicitly:%
1.52 +\end{isamarkuptext}%
1.53 +\isamarkuptrue%
1.54 +%
1.55 +\isadelimquote
1.56 +%
1.57 +\endisadelimquote
1.58 +%
1.59 +\isatagquote
1.60 +\isacommand{lemma}\isamarkupfalse%
1.61 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.62 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.63 +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
1.64 +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.65 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
1.66 +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.67 +\ \ \isacommand{by}\isamarkupfalse%
1.68 +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
1.69 +\endisatagquote
1.70 +{\isafoldquote}%
1.71 +%
1.72 +\isadelimquote
1.73 +%
1.74 +\endisadelimquote
1.75 +%
1.76 +\begin{isamarkuptext}%
1.77 +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
1.78 + \isa{attribute} which states that the given theorems should be
1.79 + considered as code equations for a \isa{fun} statement --
1.80 + the corresponding constant is determined syntactically. The resulting code:%
1.81 +\end{isamarkuptext}%
1.82 +\isamarkuptrue%
1.83 +%
1.84 +\isadelimquote
1.85 +%
1.86 +\endisadelimquote
1.87 +%
1.88 +\isatagquote
1.89 +%
1.90 +\begin{isamarkuptext}%
1.91 +\isatypewriter%
1.92 +\noindent%
1.93 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
1.94 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
1.95 +\hspace*{0pt}dequeue (AQueue xs []) =\\
1.96 +\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
1.97 +\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
1.98 +\end{isamarkuptext}%
1.99 +\isamarkuptrue%
1.100 +%
1.101 +\endisatagquote
1.102 +{\isafoldquote}%
1.103 +%
1.104 +\isadelimquote
1.105 +%
1.106 +\endisadelimquote
1.107 +%
1.108 +\begin{isamarkuptext}%
1.109 +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
1.110 + replaced by the predicate \isa{null\ xs}. This is due to the default
1.111 + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
1.112 +
1.113 + Changing the default constructor set of datatypes is also
1.114 + possible. See \secref{sec:datatypes} for an example.
1.115 +
1.116 + As told in \secref{sec:concept}, code generation is based
1.117 + on a structured collection of code theorems.
1.118 + For explorative purpose, this collection
1.119 + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
1.120 +\end{isamarkuptext}%
1.121 +\isamarkuptrue%
1.122 +%
1.123 +\isadelimquote
1.124 +%
1.125 +\endisadelimquote
1.126 +%
1.127 +\isatagquote
1.128 +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
1.129 +\ dequeue%
1.130 +\endisatagquote
1.131 +{\isafoldquote}%
1.132 +%
1.133 +\isadelimquote
1.134 +%
1.135 +\endisadelimquote
1.136 +%
1.137 +\begin{isamarkuptext}%
1.138 +\noindent prints a table with \emph{all} code equations
1.139 + for \isa{dequeue}, including
1.140 + \emph{all} code equations those equations depend
1.141 + on recursively.
1.142 +
1.143 + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
1.144 + visualising dependencies between code equations.%
1.145 +\end{isamarkuptext}%
1.146 +\isamarkuptrue%
1.147 +%
1.148 +\isamarkupsubsection{\isa{class} and \isa{instantiation}%
1.149 +}
1.150 +\isamarkuptrue%
1.151 +%
1.152 +\begin{isamarkuptext}%
1.153 +Concerning type classes and code generation, let us examine an example
1.154 + from abstract algebra:%
1.155 +\end{isamarkuptext}%
1.156 +\isamarkuptrue%
1.157 +%
1.158 +\isadelimquote
1.159 +%
1.160 +\endisadelimquote
1.161 +%
1.162 +\isatagquote
1.163 +\isacommand{class}\isamarkupfalse%
1.164 +\ semigroup\ {\isacharequal}\isanewline
1.165 +\ \ \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
1.166 +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.167 +\isanewline
1.168 +\isacommand{class}\isamarkupfalse%
1.169 +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
1.170 +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
1.171 +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
1.172 +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
1.173 +\isanewline
1.174 +\isacommand{instantiation}\isamarkupfalse%
1.175 +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
1.176 +\isakeyword{begin}\isanewline
1.177 +\isanewline
1.178 +\isacommand{primrec}\isamarkupfalse%
1.179 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
1.180 +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.181 +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
1.182 +\isanewline
1.183 +\isacommand{definition}\isamarkupfalse%
1.184 +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
1.185 +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
1.186 +\isanewline
1.187 +\isacommand{lemma}\isamarkupfalse%
1.188 +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
1.189 +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1.190 +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
1.191 +\ \ \isacommand{by}\isamarkupfalse%
1.192 +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
1.193 +\isanewline
1.194 +\isacommand{instance}\isamarkupfalse%
1.195 +\ \isacommand{proof}\isamarkupfalse%
1.196 +\isanewline
1.197 +\ \ \isacommand{fix}\isamarkupfalse%
1.198 +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1.199 +\ \ \isacommand{show}\isamarkupfalse%
1.200 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.201 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.202 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
1.203 +\ \ \isacommand{show}\isamarkupfalse%
1.204 +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
1.205 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.206 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
1.207 +\ \ \isacommand{show}\isamarkupfalse%
1.208 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
1.209 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.210 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
1.211 +\isacommand{qed}\isamarkupfalse%
1.212 +\isanewline
1.213 +\isanewline
1.214 +\isacommand{end}\isamarkupfalse%
1.215 +%
1.216 +\endisatagquote
1.217 +{\isafoldquote}%
1.218 +%
1.219 +\isadelimquote
1.220 +%
1.221 +\endisadelimquote
1.222 +%
1.223 +\begin{isamarkuptext}%
1.224 +\noindent We define the natural operation of the natural numbers
1.225 + on monoids:%
1.226 +\end{isamarkuptext}%
1.227 +\isamarkuptrue%
1.228 +%
1.229 +\isadelimquote
1.230 +%
1.231 +\endisadelimquote
1.232 +%
1.233 +\isatagquote
1.234 +\isacommand{primrec}\isamarkupfalse%
1.235 +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.236 +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
1.237 +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
1.238 +\endisatagquote
1.239 +{\isafoldquote}%
1.240 +%
1.241 +\isadelimquote
1.242 +%
1.243 +\endisadelimquote
1.244 +%
1.245 +\begin{isamarkuptext}%
1.246 +\noindent This we use to define the discrete exponentiation function:%
1.247 +\end{isamarkuptext}%
1.248 +\isamarkuptrue%
1.249 +%
1.250 +\isadelimquote
1.251 +%
1.252 +\endisadelimquote
1.253 +%
1.254 +\isatagquote
1.255 +\isacommand{definition}\isamarkupfalse%
1.256 +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.257 +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
1.258 +\endisatagquote
1.259 +{\isafoldquote}%
1.260 +%
1.261 +\isadelimquote
1.262 +%
1.263 +\endisadelimquote
1.264 +%
1.265 +\begin{isamarkuptext}%
1.266 +\noindent The corresponding code:%
1.267 +\end{isamarkuptext}%
1.268 +\isamarkuptrue%
1.269 +%
1.270 +\isadelimquote
1.271 +%
1.272 +\endisadelimquote
1.273 +%
1.274 +\isatagquote
1.275 +%
1.276 +\begin{isamarkuptext}%
1.277 +\isatypewriter%
1.278 +\noindent%
1.279 +\hspace*{0pt}module Example where {\char123}\\
1.280 +\hspace*{0pt}\\
1.281 +\hspace*{0pt}\\
1.282 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1.283 +\hspace*{0pt}\\
1.284 +\hspace*{0pt}class Semigroup a where {\char123}\\
1.285 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
1.286 +\hspace*{0pt}{\char125};\\
1.287 +\hspace*{0pt}\\
1.288 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
1.289 +\hspace*{0pt} ~neutral ::~a;\\
1.290 +\hspace*{0pt}{\char125};\\
1.291 +\hspace*{0pt}\\
1.292 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1.293 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
1.294 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
1.295 +\hspace*{0pt}\\
1.296 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
1.297 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
1.298 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
1.299 +\hspace*{0pt}\\
1.300 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
1.301 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
1.302 +\hspace*{0pt}\\
1.303 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
1.304 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
1.305 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
1.306 +\hspace*{0pt}\\
1.307 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
1.308 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
1.309 +\hspace*{0pt}{\char125};\\
1.310 +\hspace*{0pt}\\
1.311 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
1.312 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
1.313 +\hspace*{0pt}{\char125};\\
1.314 +\hspace*{0pt}\\
1.315 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
1.316 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
1.317 +\hspace*{0pt}\\
1.318 +\hspace*{0pt}{\char125}%
1.319 +\end{isamarkuptext}%
1.320 +\isamarkuptrue%
1.321 +%
1.322 +\endisatagquote
1.323 +{\isafoldquote}%
1.324 +%
1.325 +\isadelimquote
1.326 +%
1.327 +\endisadelimquote
1.328 +%
1.329 +\begin{isamarkuptext}%
1.330 +\noindent This is a convenient place to show how explicit dictionary construction
1.331 + manifests in generated code (here, the same example in \isa{SML}):%
1.332 +\end{isamarkuptext}%
1.333 +\isamarkuptrue%
1.334 +%
1.335 +\isadelimquote
1.336 +%
1.337 +\endisadelimquote
1.338 +%
1.339 +\isatagquote
1.340 +%
1.341 +\begin{isamarkuptext}%
1.342 +\isatypewriter%
1.343 +\noindent%
1.344 +\hspace*{0pt}structure Example = \\
1.345 +\hspace*{0pt}struct\\
1.346 +\hspace*{0pt}\\
1.347 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.348 +\hspace*{0pt}\\
1.349 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1.350 +\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
1.351 +\hspace*{0pt}\\
1.352 +\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
1.353 +\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
1.354 +\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
1.355 +\hspace*{0pt}\\
1.356 +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
1.357 +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
1.358 +\hspace*{0pt}\\
1.359 +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
1.360 +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
1.361 +\hspace*{0pt}\\
1.362 +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
1.363 +\hspace*{0pt}\\
1.364 +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
1.365 +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
1.366 +\hspace*{0pt}\\
1.367 +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
1.368 +\hspace*{0pt}\\
1.369 +\hspace*{0pt}val monoid{\char95}nat =\\
1.370 +\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\
1.371 +\hspace*{0pt} ~nat monoid;\\
1.372 +\hspace*{0pt}\\
1.373 +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
1.374 +\hspace*{0pt}\\
1.375 +\hspace*{0pt}end;~(*struct Example*)%
1.376 +\end{isamarkuptext}%
1.377 +\isamarkuptrue%
1.378 +%
1.379 +\endisatagquote
1.380 +{\isafoldquote}%
1.381 +%
1.382 +\isadelimquote
1.383 +%
1.384 +\endisadelimquote
1.385 +%
1.386 +\begin{isamarkuptext}%
1.387 +\noindent Note the parameters with trailing underscore (\verb|A_|)
1.388 + which are the dictionary parameters.%
1.389 +\end{isamarkuptext}%
1.390 +\isamarkuptrue%
1.391 +%
1.392 +\isamarkupsubsection{The preprocessor \label{sec:preproc}%
1.393 +}
1.394 +\isamarkuptrue%
1.395 +%
1.396 +\begin{isamarkuptext}%
1.397 +Before selected function theorems are turned into abstract
1.398 + code, a chain of definitional transformation steps is carried
1.399 + out: \emph{preprocessing}. In essence, the preprocessor
1.400 + consists of two components: a \emph{simpset} and \emph{function transformers}.
1.401 +
1.402 + The \emph{simpset} allows to employ the full generality of the Isabelle
1.403 + simplifier. Due to the interpretation of theorems
1.404 + as code equations, rewrites are applied to the right
1.405 + hand side and the arguments of the left hand side of an
1.406 + equation, but never to the constant heading the left hand side.
1.407 + An important special case are \emph{inline theorems} which may be
1.408 + declared and undeclared using the
1.409 + \emph{code inline} or \emph{code inline del} attribute respectively.
1.410 +
1.411 + Some common applications:%
1.412 +\end{isamarkuptext}%
1.413 +\isamarkuptrue%
1.414 +%
1.415 +\begin{itemize}
1.416 +%
1.417 +\begin{isamarkuptext}%
1.418 +\item replacing non-executable constructs by executable ones:%
1.419 +\end{isamarkuptext}%
1.420 +\isamarkuptrue%
1.421 +%
1.422 +\isadelimquote
1.423 +%
1.424 +\endisadelimquote
1.425 +%
1.426 +\isatagquote
1.427 +\isacommand{lemma}\isamarkupfalse%
1.428 +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
1.429 +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.430 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
1.431 +\endisatagquote
1.432 +{\isafoldquote}%
1.433 +%
1.434 +\isadelimquote
1.435 +%
1.436 +\endisadelimquote
1.437 +%
1.438 +\begin{isamarkuptext}%
1.439 +\item eliminating superfluous constants:%
1.440 +\end{isamarkuptext}%
1.441 +\isamarkuptrue%
1.442 +%
1.443 +\isadelimquote
1.444 +%
1.445 +\endisadelimquote
1.446 +%
1.447 +\isatagquote
1.448 +\isacommand{lemma}\isamarkupfalse%
1.449 +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
1.450 +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.451 +\ simp%
1.452 +\endisatagquote
1.453 +{\isafoldquote}%
1.454 +%
1.455 +\isadelimquote
1.456 +%
1.457 +\endisadelimquote
1.458 +%
1.459 +\begin{isamarkuptext}%
1.460 +\item replacing executable but inconvenient constructs:%
1.461 +\end{isamarkuptext}%
1.462 +\isamarkuptrue%
1.463 +%
1.464 +\isadelimquote
1.465 +%
1.466 +\endisadelimquote
1.467 +%
1.468 +\isatagquote
1.469 +\isacommand{lemma}\isamarkupfalse%
1.470 +\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
1.471 +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.472 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
1.473 +\endisatagquote
1.474 +{\isafoldquote}%
1.475 +%
1.476 +\isadelimquote
1.477 +%
1.478 +\endisadelimquote
1.479 +%
1.480 +\end{itemize}
1.481 +%
1.482 +\begin{isamarkuptext}%
1.483 +\noindent \emph{Function transformers} provide a very general interface,
1.484 + transforming a list of function theorems to another
1.485 + list of function theorems, provided that neither the heading
1.486 + constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
1.487 + pattern elimination implemented in
1.488 + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
1.489 + interface.
1.490 +
1.491 + \noindent The current setup of the preprocessor may be inspected using
1.492 + the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
1.493 + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
1.494 + mechanism to inspect the impact of a preprocessor setup
1.495 + on code equations.
1.496 +
1.497 + \begin{warn}
1.498 + The attribute \emph{code unfold}
1.499 + associated with the \isa{SML\ code\ generator} also applies to
1.500 + the \isa{generic\ code\ generator}:
1.501 + \emph{code unfold} implies \emph{code inline}.
1.502 + \end{warn}%
1.503 +\end{isamarkuptext}%
1.504 +\isamarkuptrue%
1.505 +%
1.506 +\isamarkupsubsection{Datatypes \label{sec:datatypes}%
1.507 +}
1.508 +\isamarkuptrue%
1.509 +%
1.510 +\begin{isamarkuptext}%
1.511 +Conceptually, any datatype is spanned by a set of
1.512 + \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
1.513 + \isa{{\isasymtau}}. The HOL datatype package by default registers any new
1.514 + datatype in the table of datatypes, which may be inspected using the
1.515 + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
1.516 +
1.517 + In some cases, it is appropriate to alter or extend this table. As
1.518 + an example, we will develop an alternative representation of the
1.519 + queue example given in \secref{sec:intro}. The amortised
1.520 + representation is convenient for generating code but exposes its
1.521 + \qt{implementation} details, which may be cumbersome when proving
1.522 + theorems about it. Therefore, here a simple, straightforward
1.523 + representation of queues:%
1.524 +\end{isamarkuptext}%
1.525 +\isamarkuptrue%
1.526 +%
1.527 +\isadelimquote
1.528 +%
1.529 +\endisadelimquote
1.530 +%
1.531 +\isatagquote
1.532 +\isacommand{datatype}\isamarkupfalse%
1.533 +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
1.534 +\isanewline
1.535 +\isacommand{definition}\isamarkupfalse%
1.536 +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.537 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
1.538 +\isanewline
1.539 +\isacommand{primrec}\isamarkupfalse%
1.540 +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.541 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.542 +\isanewline
1.543 +\isacommand{fun}\isamarkupfalse%
1.544 +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.545 +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.546 +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
1.547 +\endisatagquote
1.548 +{\isafoldquote}%
1.549 +%
1.550 +\isadelimquote
1.551 +%
1.552 +\endisadelimquote
1.553 +%
1.554 +\begin{isamarkuptext}%
1.555 +\noindent This we can use directly for proving; for executing,
1.556 + we provide an alternative characterisation:%
1.557 +\end{isamarkuptext}%
1.558 +\isamarkuptrue%
1.559 +%
1.560 +\isadelimquote
1.561 +%
1.562 +\endisadelimquote
1.563 +%
1.564 +\isatagquote
1.565 +\isacommand{definition}\isamarkupfalse%
1.566 +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.567 +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.568 +\isanewline
1.569 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
1.570 +\ AQueue%
1.571 +\endisatagquote
1.572 +{\isafoldquote}%
1.573 +%
1.574 +\isadelimquote
1.575 +%
1.576 +\endisadelimquote
1.577 +%
1.578 +\begin{isamarkuptext}%
1.579 +\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which
1.580 + is defined in terms of \isa{Queue} and interprets its arguments
1.581 + according to what the \emph{content} of an amortised queue is supposed
1.582 + to be. Equipped with this, we are able to prove the following equations
1.583 + for our primitive queue operations which \qt{implement} the simple
1.584 + queues in an amortised fashion:%
1.585 +\end{isamarkuptext}%
1.586 +\isamarkuptrue%
1.587 +%
1.588 +\isadelimquote
1.589 +%
1.590 +\endisadelimquote
1.591 +%
1.592 +\isatagquote
1.593 +\isacommand{lemma}\isamarkupfalse%
1.594 +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.595 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
1.596 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.597 +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.598 +\ simp\isanewline
1.599 +\isanewline
1.600 +\isacommand{lemma}\isamarkupfalse%
1.601 +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.602 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
1.603 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.604 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.605 +\ simp\isanewline
1.606 +\isanewline
1.607 +\isacommand{lemma}\isamarkupfalse%
1.608 +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.609 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.610 +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
1.611 +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.612 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.613 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.614 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.615 +\ simp{\isacharunderscore}all%
1.616 +\endisatagquote
1.617 +{\isafoldquote}%
1.618 +%
1.619 +\isadelimquote
1.620 +%
1.621 +\endisadelimquote
1.622 +%
1.623 +\begin{isamarkuptext}%
1.624 +\noindent For completeness, we provide a substitute for the
1.625 + \isa{case} combinator on queues:%
1.626 +\end{isamarkuptext}%
1.627 +\isamarkuptrue%
1.628 +%
1.629 +\isadelimquote
1.630 +%
1.631 +\endisadelimquote
1.632 +%
1.633 +\isatagquote
1.634 +\isacommand{definition}\isamarkupfalse%
1.635 +\isanewline
1.636 +\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
1.637 +\isanewline
1.638 +\isacommand{lemma}\isamarkupfalse%
1.639 +\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
1.640 +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
1.641 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.642 +\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
1.643 +\isanewline
1.644 +\isanewline
1.645 +\isacommand{lemma}\isamarkupfalse%
1.646 +\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.647 +\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.648 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.649 +\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.650 +\ simp%
1.651 +\endisatagquote
1.652 +{\isafoldquote}%
1.653 +%
1.654 +\isadelimquote
1.655 +%
1.656 +\endisadelimquote
1.657 +%
1.658 +\begin{isamarkuptext}%
1.659 +\noindent The resulting code looks as expected:%
1.660 +\end{isamarkuptext}%
1.661 +\isamarkuptrue%
1.662 +%
1.663 +\isadelimquote
1.664 +%
1.665 +\endisadelimquote
1.666 +%
1.667 +\isatagquote
1.668 +%
1.669 +\begin{isamarkuptext}%
1.670 +\isatypewriter%
1.671 +\noindent%
1.672 +\hspace*{0pt}structure Example = \\
1.673 +\hspace*{0pt}struct\\
1.674 +\hspace*{0pt}\\
1.675 +\hspace*{0pt}fun foldl f a [] = a\\
1.676 +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
1.677 +\hspace*{0pt}\\
1.678 +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
1.679 +\hspace*{0pt}\\
1.680 +\hspace*{0pt}fun null [] = true\\
1.681 +\hspace*{0pt} ~| null (x ::~xs) = false;\\
1.682 +\hspace*{0pt}\\
1.683 +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
1.684 +\hspace*{0pt}\\
1.685 +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
1.686 +\hspace*{0pt}\\
1.687 +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
1.688 +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
1.689 +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
1.690 +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
1.691 +\hspace*{0pt}\\
1.692 +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
1.693 +\hspace*{0pt}\\
1.694 +\hspace*{0pt}end;~(*struct Example*)%
1.695 +\end{isamarkuptext}%
1.696 +\isamarkuptrue%
1.697 +%
1.698 +\endisatagquote
1.699 +{\isafoldquote}%
1.700 +%
1.701 +\isadelimquote
1.702 +%
1.703 +\endisadelimquote
1.704 +%
1.705 +\begin{isamarkuptext}%
1.706 +\noindent From this example, it can be glimpsed that using own
1.707 + constructor sets is a little delicate since it changes the set of
1.708 + valid patterns for values of that type. Without going into much
1.709 + detail, here some practical hints:
1.710 +
1.711 + \begin{itemize}
1.712 +
1.713 + \item When changing the constructor set for datatypes, take care
1.714 + to provide an alternative for the \isa{case} combinator
1.715 + (e.g.~by replacing it using the preprocessor).
1.716 +
1.717 + \item Values in the target language need not to be normalised --
1.718 + different values in the target language may represent the same
1.719 + value in the logic.
1.720 +
1.721 + \item Usually, a good methodology to deal with the subtleties of
1.722 + pattern matching is to see the type as an abstract type: provide
1.723 + a set of operations which operate on the concrete representation
1.724 + of the type, and derive further operations by combinations of
1.725 + these primitive ones, without relying on a particular
1.726 + representation.
1.727 +
1.728 + \end{itemize}%
1.729 +\end{isamarkuptext}%
1.730 +\isamarkuptrue%
1.731 +%
1.732 +\isamarkupsubsection{Equality and wellsortedness%
1.733 +}
1.734 +\isamarkuptrue%
1.735 +%
1.736 +\begin{isamarkuptext}%
1.737 +Surely you have already noticed how equality is treated
1.738 + by the code generator:%
1.739 +\end{isamarkuptext}%
1.740 +\isamarkuptrue%
1.741 +%
1.742 +\isadelimquote
1.743 +%
1.744 +\endisadelimquote
1.745 +%
1.746 +\isatagquote
1.747 +\isacommand{primrec}\isamarkupfalse%
1.748 +\ 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
1.749 +\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
1.750 +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
1.751 +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
1.752 +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
1.753 +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
1.754 +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
1.755 +\endisatagquote
1.756 +{\isafoldquote}%
1.757 +%
1.758 +\isadelimquote
1.759 +%
1.760 +\endisadelimquote
1.761 +%
1.762 +\begin{isamarkuptext}%
1.763 +\noindent The membership test during preprocessing is rewritten,
1.764 + resulting in \isa{op\ mem}, which itself
1.765 + performs an explicit equality check.%
1.766 +\end{isamarkuptext}%
1.767 +\isamarkuptrue%
1.768 +%
1.769 +\isadelimquote
1.770 +%
1.771 +\endisadelimquote
1.772 +%
1.773 +\isatagquote
1.774 +%
1.775 +\begin{isamarkuptext}%
1.776 +\isatypewriter%
1.777 +\noindent%
1.778 +\hspace*{0pt}structure Example = \\
1.779 +\hspace*{0pt}struct\\
1.780 +\hspace*{0pt}\\
1.781 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
1.782 +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
1.783 +\hspace*{0pt}\\
1.784 +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
1.785 +\hspace*{0pt}\\
1.786 +\hspace*{0pt}fun member A{\char95}~x [] = false\\
1.787 +\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\
1.788 +\hspace*{0pt}\\
1.789 +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
1.790 +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
1.791 +\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
1.792 +\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
1.793 +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
1.794 +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
1.795 +\hspace*{0pt}\\
1.796 +\hspace*{0pt}end;~(*struct Example*)%
1.797 +\end{isamarkuptext}%
1.798 +\isamarkuptrue%
1.799 +%
1.800 +\endisatagquote
1.801 +{\isafoldquote}%
1.802 +%
1.803 +\isadelimquote
1.804 +%
1.805 +\endisadelimquote
1.806 +%
1.807 +\begin{isamarkuptext}%
1.808 +\noindent Obviously, polymorphic equality is implemented the Haskell
1.809 + way using a type class. How is this achieved? HOL introduces
1.810 + an explicit class \isa{eq} with a corresponding operation
1.811 + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
1.812 + The preprocessing framework does the rest by propagating the
1.813 + \isa{eq} constraints through all dependent code equations.
1.814 + For datatypes, instances of \isa{eq} are implicitly derived
1.815 + when possible. For other types, you may instantiate \isa{eq}
1.816 + manually like any other type class.
1.817 +
1.818 + Though this \isa{eq} class is designed to get rarely in
1.819 + the way, a subtlety
1.820 + enters the stage when definitions of overloaded constants
1.821 + are dependent on operational equality. For example, let
1.822 + us define a lexicographic ordering on tuples
1.823 + (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
1.824 +\end{isamarkuptext}%
1.825 +\isamarkuptrue%
1.826 +%
1.827 +\isadelimquote
1.828 +%
1.829 +\endisadelimquote
1.830 +%
1.831 +\isatagquote
1.832 +\isacommand{instantiation}\isamarkupfalse%
1.833 +\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
1.834 +\isakeyword{begin}\isanewline
1.835 +\isanewline
1.836 +\isacommand{definition}\isamarkupfalse%
1.837 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
1.838 +\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
1.839 +\isanewline
1.840 +\isacommand{definition}\isamarkupfalse%
1.841 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
1.842 +\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
1.843 +\isanewline
1.844 +\isacommand{instance}\isamarkupfalse%
1.845 +\ \isacommand{proof}\isamarkupfalse%
1.846 +\isanewline
1.847 +\isacommand{qed}\isamarkupfalse%
1.848 +\ {\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
1.849 +\isanewline
1.850 +\isacommand{end}\isamarkupfalse%
1.851 +\isanewline
1.852 +\isanewline
1.853 +\isacommand{lemma}\isamarkupfalse%
1.854 +\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.855 +\ \ {\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
1.856 +\ \ \ \ \ 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
1.857 +\ \ {\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
1.858 +\ \ \ \ \ 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
1.859 +\ \ \isacommand{by}\isamarkupfalse%
1.860 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
1.861 +\endisatagquote
1.862 +{\isafoldquote}%
1.863 +%
1.864 +\isadelimquote
1.865 +%
1.866 +\endisadelimquote
1.867 +%
1.868 +\begin{isamarkuptext}%
1.869 +\noindent Then code generation will fail. Why? The definition
1.870 + of \isa{op\ {\isasymle}} depends on equality on both arguments,
1.871 + which are polymorphic and impose an additional \isa{eq}
1.872 + class constraint, which the preprocessor does not propagate
1.873 + (for technical reasons).
1.874 +
1.875 + The solution is to add \isa{eq} explicitly to the first sort arguments in the
1.876 + code theorems:%
1.877 +\end{isamarkuptext}%
1.878 +\isamarkuptrue%
1.879 +%
1.880 +\isadelimquote
1.881 +%
1.882 +\endisadelimquote
1.883 +%
1.884 +\isatagquote
1.885 +\isacommand{lemma}\isamarkupfalse%
1.886 +\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.887 +\ \ {\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
1.888 +\ \ \ \ \ 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
1.889 +\ \ {\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
1.890 +\ \ \ \ \ 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
1.891 +\ \ \isacommand{by}\isamarkupfalse%
1.892 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
1.893 +\endisatagquote
1.894 +{\isafoldquote}%
1.895 +%
1.896 +\isadelimquote
1.897 +%
1.898 +\endisadelimquote
1.899 +%
1.900 +\begin{isamarkuptext}%
1.901 +\noindent Then code generation succeeds:%
1.902 +\end{isamarkuptext}%
1.903 +\isamarkuptrue%
1.904 +%
1.905 +\isadelimquote
1.906 +%
1.907 +\endisadelimquote
1.908 +%
1.909 +\isatagquote
1.910 +%
1.911 +\begin{isamarkuptext}%
1.912 +\isatypewriter%
1.913 +\noindent%
1.914 +\hspace*{0pt}structure Example = \\
1.915 +\hspace*{0pt}struct\\
1.916 +\hspace*{0pt}\\
1.917 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
1.918 +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
1.919 +\hspace*{0pt}\\
1.920 +\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\
1.921 +\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
1.922 +\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
1.923 +\hspace*{0pt}\\
1.924 +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
1.925 +\hspace*{0pt}\\
1.926 +\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
1.927 +\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
1.928 +\hspace*{0pt}\\
1.929 +\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
1.930 +\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
1.931 +\hspace*{0pt}\\
1.932 +\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
1.933 +\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
1.934 +\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
1.935 +\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
1.936 +\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
1.937 +\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
1.938 +\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
1.939 +\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
1.940 +\hspace*{0pt}\\
1.941 +\hspace*{0pt}end;~(*struct Example*)%
1.942 +\end{isamarkuptext}%
1.943 +\isamarkuptrue%
1.944 +%
1.945 +\endisatagquote
1.946 +{\isafoldquote}%
1.947 +%
1.948 +\isadelimquote
1.949 +%
1.950 +\endisadelimquote
1.951 +%
1.952 +\begin{isamarkuptext}%
1.953 +In some cases, the automatically derived code equations
1.954 + for equality on a particular type may not be appropriate.
1.955 + As example, watch the following datatype representing
1.956 + monomorphic parametric types (where type constructors
1.957 + are referred to by natural numbers):%
1.958 +\end{isamarkuptext}%
1.959 +\isamarkuptrue%
1.960 +%
1.961 +\isadelimquote
1.962 +%
1.963 +\endisadelimquote
1.964 +%
1.965 +\isatagquote
1.966 +\isacommand{datatype}\isamarkupfalse%
1.967 +\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
1.968 +\endisatagquote
1.969 +{\isafoldquote}%
1.970 +%
1.971 +\isadelimquote
1.972 +%
1.973 +\endisadelimquote
1.974 +%
1.975 +\isadelimproof
1.976 +%
1.977 +\endisadelimproof
1.978 +%
1.979 +\isatagproof
1.980 +%
1.981 +\endisatagproof
1.982 +{\isafoldproof}%
1.983 +%
1.984 +\isadelimproof
1.985 +%
1.986 +\endisadelimproof
1.987 +%
1.988 +\begin{isamarkuptext}%
1.989 +\noindent Then code generation for SML would fail with a message
1.990 + that the generated code contains illegal mutual dependencies:
1.991 + 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
1.992 + instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
1.993 + \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
1.994 + recursive \isa{instance} and \isa{function} definitions,
1.995 + but the SML serialiser does not support this.
1.996 +
1.997 + In such cases, you have to provide your own equality equations
1.998 + involving auxiliary constants. In our case,
1.999 + \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
1.1000 +\end{isamarkuptext}%
1.1001 +\isamarkuptrue%
1.1002 +%
1.1003 +\isadelimquote
1.1004 +%
1.1005 +\endisadelimquote
1.1006 +%
1.1007 +\isatagquote
1.1008 +\isacommand{lemma}\isamarkupfalse%
1.1009 +\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.1010 +\ \ {\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
1.1011 +\ \ \ \ \ 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
1.1012 +\ \ \isacommand{by}\isamarkupfalse%
1.1013 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
1.1014 +\endisatagquote
1.1015 +{\isafoldquote}%
1.1016 +%
1.1017 +\isadelimquote
1.1018 +%
1.1019 +\endisadelimquote
1.1020 +%
1.1021 +\begin{isamarkuptext}%
1.1022 +\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
1.1023 +\end{isamarkuptext}%
1.1024 +\isamarkuptrue%
1.1025 +%
1.1026 +\isadelimquote
1.1027 +%
1.1028 +\endisadelimquote
1.1029 +%
1.1030 +\isatagquote
1.1031 +%
1.1032 +\begin{isamarkuptext}%
1.1033 +\isatypewriter%
1.1034 +\noindent%
1.1035 +\hspace*{0pt}structure Example = \\
1.1036 +\hspace*{0pt}struct\\
1.1037 +\hspace*{0pt}\\
1.1038 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.1039 +\hspace*{0pt}\\
1.1040 +\hspace*{0pt}fun null [] = true\\
1.1041 +\hspace*{0pt} ~| null (x ::~xs) = false;\\
1.1042 +\hspace*{0pt}\\
1.1043 +\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\
1.1044 +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\
1.1045 +\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
1.1046 +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
1.1047 +\hspace*{0pt}\\
1.1048 +\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
1.1049 +\hspace*{0pt}\\
1.1050 +\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
1.1051 +\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
1.1052 +\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
1.1053 +\hspace*{0pt}\\
1.1054 +\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
1.1055 +\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
1.1056 +\hspace*{0pt}\\
1.1057 +\hspace*{0pt}end;~(*struct Example*)%
1.1058 +\end{isamarkuptext}%
1.1059 +\isamarkuptrue%
1.1060 +%
1.1061 +\endisatagquote
1.1062 +{\isafoldquote}%
1.1063 +%
1.1064 +\isadelimquote
1.1065 +%
1.1066 +\endisadelimquote
1.1067 +%
1.1068 +\isamarkupsubsection{Explicit partiality%
1.1069 +}
1.1070 +\isamarkuptrue%
1.1071 +%
1.1072 +\begin{isamarkuptext}%
1.1073 +Partiality usually enters the game by partial patterns, as
1.1074 + in the following example, again for amortised queues:%
1.1075 +\end{isamarkuptext}%
1.1076 +\isamarkuptrue%
1.1077 +%
1.1078 +\isadelimquote
1.1079 +%
1.1080 +\endisadelimquote
1.1081 +%
1.1082 +\isatagquote
1.1083 +\isacommand{definition}\isamarkupfalse%
1.1084 +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.1085 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
1.1086 +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.1087 +\isanewline
1.1088 +\isacommand{lemma}\isamarkupfalse%
1.1089 +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.1090 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.1091 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.1092 +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.1093 +\ \ \isacommand{by}\isamarkupfalse%
1.1094 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
1.1095 +\endisatagquote
1.1096 +{\isafoldquote}%
1.1097 +%
1.1098 +\isadelimquote
1.1099 +%
1.1100 +\endisadelimquote
1.1101 +%
1.1102 +\begin{isamarkuptext}%
1.1103 +\noindent In the corresponding code, there is no equation
1.1104 + for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
1.1105 +\end{isamarkuptext}%
1.1106 +\isamarkuptrue%
1.1107 +%
1.1108 +\isadelimquote
1.1109 +%
1.1110 +\endisadelimquote
1.1111 +%
1.1112 +\isatagquote
1.1113 +%
1.1114 +\begin{isamarkuptext}%
1.1115 +\isatypewriter%
1.1116 +\noindent%
1.1117 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
1.1118 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
1.1119 +\hspace*{0pt} ~let {\char123}\\
1.1120 +\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
1.1121 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
1.1122 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
1.1123 +\end{isamarkuptext}%
1.1124 +\isamarkuptrue%
1.1125 +%
1.1126 +\endisatagquote
1.1127 +{\isafoldquote}%
1.1128 +%
1.1129 +\isadelimquote
1.1130 +%
1.1131 +\endisadelimquote
1.1132 +%
1.1133 +\begin{isamarkuptext}%
1.1134 +\noindent In some cases it is desirable to have this
1.1135 + pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
1.1136 +\end{isamarkuptext}%
1.1137 +\isamarkuptrue%
1.1138 +%
1.1139 +\isadelimquote
1.1140 +%
1.1141 +\endisadelimquote
1.1142 +%
1.1143 +\isatagquote
1.1144 +\isacommand{axiomatization}\isamarkupfalse%
1.1145 +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
1.1146 +\isanewline
1.1147 +\isacommand{definition}\isamarkupfalse%
1.1148 +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.1149 +\ \ {\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
1.1150 +\isanewline
1.1151 +\isacommand{lemma}\isamarkupfalse%
1.1152 +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.1153 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
1.1154 +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.1155 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
1.1156 +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.1157 +\ \ \isacommand{by}\isamarkupfalse%
1.1158 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
1.1159 +\endisatagquote
1.1160 +{\isafoldquote}%
1.1161 +%
1.1162 +\isadelimquote
1.1163 +%
1.1164 +\endisadelimquote
1.1165 +%
1.1166 +\begin{isamarkuptext}%
1.1167 +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
1.1168 + which is unspecified.
1.1169 +
1.1170 + Normally, if constants without any code equations occur in a
1.1171 + program, the code generator complains (since in most cases this is
1.1172 + not what the user expects). But such constants can also be thought
1.1173 + of as function definitions with no equations which always fail,
1.1174 + since there is never a successful pattern match on the left hand
1.1175 + side. In order to categorise a constant into that category
1.1176 + explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
1.1177 +\end{isamarkuptext}%
1.1178 +\isamarkuptrue%
1.1179 +%
1.1180 +\isadelimquote
1.1181 +%
1.1182 +\endisadelimquote
1.1183 +%
1.1184 +\isatagquote
1.1185 +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
1.1186 +\ empty{\isacharunderscore}queue%
1.1187 +\endisatagquote
1.1188 +{\isafoldquote}%
1.1189 +%
1.1190 +\isadelimquote
1.1191 +%
1.1192 +\endisadelimquote
1.1193 +%
1.1194 +\begin{isamarkuptext}%
1.1195 +\noindent Then the code generator will just insert an error or
1.1196 + exception at the appropriate position:%
1.1197 +\end{isamarkuptext}%
1.1198 +\isamarkuptrue%
1.1199 +%
1.1200 +\isadelimquote
1.1201 +%
1.1202 +\endisadelimquote
1.1203 +%
1.1204 +\isatagquote
1.1205 +%
1.1206 +\begin{isamarkuptext}%
1.1207 +\isatypewriter%
1.1208 +\noindent%
1.1209 +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
1.1210 +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
1.1211 +\hspace*{0pt}\\
1.1212 +\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
1.1213 +\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
1.1214 +\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
1.1215 +\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
1.1216 +\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
1.1217 +\end{isamarkuptext}%
1.1218 +\isamarkuptrue%
1.1219 +%
1.1220 +\endisatagquote
1.1221 +{\isafoldquote}%
1.1222 +%
1.1223 +\isadelimquote
1.1224 +%
1.1225 +\endisadelimquote
1.1226 +%
1.1227 +\begin{isamarkuptext}%
1.1228 +\noindent This feature however is rarely needed in practice.
1.1229 + Note also that the \isa{HOL} default setup already declares
1.1230 + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
1.1231 + likely to be used in such situations.%
1.1232 +\end{isamarkuptext}%
1.1233 +\isamarkuptrue%
1.1234 +%
1.1235 +\isadelimtheory
1.1236 +%
1.1237 +\endisadelimtheory
1.1238 +%
1.1239 +\isatagtheory
1.1240 +\isacommand{end}\isamarkupfalse%
1.1241 +%
1.1242 +\endisatagtheory
1.1243 +{\isafoldtheory}%
1.1244 +%
1.1245 +\isadelimtheory
1.1246 +%
1.1247 +\endisadelimtheory
1.1248 +\isanewline
1.1249 +\ \end{isabellebody}%
1.1250 +%%% Local Variables:
1.1251 +%%% mode: latex
1.1252 +%%% TeX-master: "root"
1.1253 +%%% End: