%

\begin{isabellebody}%

\def\isabellecontext{Codegen}%

%

\isadelimtheory

\isanewline

\isanewline

%

\endisadelimtheory

%

\isatagtheory

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupchapter{Code generation from Isabelle theories%

}

\isamarkuptrue%

%

\isamarkupsection{Introduction%

}

\isamarkuptrue%

%

\isamarkupsubsection{Motivation%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Executing formal specifications as programs is a well-established

  topic in the theorem proving community.  With increasing

  application of theorem proving systems in the area of

  software development and verification, its relevance manifests

  for running test cases and rapid prototyping.  In logical

  calculi like constructive type theory,

  a notion of executability is implicit due to the nature

  of the calculus.  In contrast, specifications in Isabelle

  can be highly non-executable.  In order to bridge

  the gap between logic and executable specifications,

  an explicit non-trivial transformation has to be applied:

  code generation.

  This tutorial introduces a generic code generator for the

  Isabelle system \cite{isa-tutorial}.

  Generic in the sense that the

  \qn{target language} for which code shall ultimately be

  generated is not fixed but may be an arbitrary state-of-the-art

  functional programming language (currently, the implementation

  supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell

  \cite{haskell-revised-report}).

  We aim to provide a

  versatile environment

  suitable for software development and verification,

  structuring the process

  of code generation into a small set of orthogonal principles

  while achieving a big coverage of application areas

  with maximum flexibility.

  Conceptually the code generator framework is part

  of Isabelle's \isa{Pure} meta logic; the object logic

  \isa{HOL} which is an extension of \isa{Pure}

  already comes with a reasonable framework setup and thus provides

  a good working horse for raising code-generation-driven

  applications.  So, we assume some familiarity and experience

  with the ingredients of the \isa{HOL} \emph{Main} theory

  (see also \cite{isa-tutorial}).%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Overview%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The code generator aims to be usable with no further ado

  in most cases while allowing for detailed customization.

  This manifests in the structure of this tutorial:

  we start with a generic example \secref{sec:example}

  and introduce code generation concepts \secref{sec:concept}.

  Section

  \secref{sec:basics} explains how to use the framework naively,

  presuming a reasonable default setup.  Then, section

  \secref{sec:advanced} deals with advanced topics,

  introducing further aspects of the code generator framework

  in a motivation-driven manner.  Last, section \secref{sec:ml}

  introduces the framework's internal programming interfaces.

  \begin{warn}

    Ultimately, the code generator which this tutorial deals with

    is supposed to replace the already established code generator

    by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.

    So, for the moment, there are two distinct code generators

    in Isabelle.

    Also note that while the framework itself is

    object-logic independent, only \isa{HOL} provides a reasonable

    framework setup.    

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{An example: a simple theory of search trees \label{sec:example}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

When writing executable specifications using \isa{HOL},

  it is convenient to use

  three existing packages: the datatype package for defining

  datatypes, the function package for (recursive) functions,

  and the class package for overloaded definitions.

  We develope a small theory of search trees; trees are represented

  as a datatype with key type \isa{{\isacharprime}a} and value type \isa{{\isacharprime}b}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{datatype}\isamarkupfalse%

\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline

\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent Note that we have constrained the type of keys

  to the class of total orders, \isa{linorder}.

  We define \isa{find} and \isa{update} functions:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{primrec}\isamarkupfalse%

\isanewline

\ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}find\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isacharequal}\ key\ then\ Some\ val\ else\ None{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}find\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isasymle}\ key\ then\ find\ t{\isadigit{1}}\ it\ else\ find\ t{\isadigit{2}}\ it{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{fun}\isamarkupfalse%

\isanewline

\ \ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline

\ \ \ \ if\ it\ {\isacharequal}\ key\ then\ Leaf\ key\ entry\isanewline

\ \ \ \ \ \ else\ if\ it\ {\isasymle}\ key\isanewline

\ \ \ \ \ \ then\ Branch\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\isanewline

\ \ \ \ \ \ else\ Branch\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\isanewline

\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline

\ \ \ \ if\ it\ {\isasymle}\ key\isanewline

\ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline

\ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline

\ \ \ {\isacharparenright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent For testing purpose, we define a small example

  using natural numbers \isa{nat} (which are a \isa{linorder})

  as keys and list of nats as values:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat{\isacharcomma}\ nat\ list{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline

\isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline

\ \ \ \ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent Then we generate code%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent which looks like:

  \lstsml{Thy/examples/tree.ML}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{Code generation concepts and process \label{sec:concept}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\begin{figure}[h]

  \centering

  \includegraphics[width=0.7\textwidth]{codegen_process}

  \caption{code generator -- processing overview}

  \label{fig:process}

  \end{figure}

  The code generator employs a notion of executability

  for three foundational executable ingredients known

  from functional programming:

  \emph{defining equations}, \emph{datatypes}, and

  \emph{type classes}. A defining equation as a first approximation

  is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}

  (an equation headed by a constant \isa{f} with arguments

  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).

  Code generation aims to turn defining equations

  into a functional program by running through

  a process (see figure \ref{fig:process}):

  \begin{itemize}

    \item Out of the vast collection of theorems proven in a

      \qn{theory}, a reasonable subset modeling

      defining equations is \qn{selected}.

    \item On those selected theorems, certain

      transformations are carried out

      (\qn{preprocessing}).  Their purpose is to turn theorems

      representing non- or badly executable

      specifications into equivalent but executable counterparts.

      The result is a structured collection of \qn{code theorems}.

    \item These \qn{code theorems} then are \qn{translated}

      into an Haskell-like intermediate

      language.

    \item Finally, out of the intermediate language the final

      code in the desired \qn{target language} is \qn{serialized}.

  \end{itemize}

  From these steps, only the two last are carried out

  outside the logic; by keeping this layer as

  thin as possible, the amount of code to trust is

  kept to a minimum.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{Basics \label{sec:basics}%

}

\isamarkuptrue%

%

\isamarkupsubsection{Invoking the code generator%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Thanks to a reasonable setup of the \isa{HOL} theories, in

  most cases code generation proceeds without further ado:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{primrec}\isamarkupfalse%

\isanewline

\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent This executable specification is now turned to SML code:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent  The \isa{{\isasymEXPORTCODE}} command takes a space-separated list of

  constants together with \qn{serialization directives}

  These start with a \qn{target language}

  identifier, followed by a file specification

  where to write the generated code to.

  Internally, the defining equations for all selected

  constants are taken, including any transitively required

  constants, datatypes and classes, resulting in the following

  code:

  \lstsml{Thy/examples/fac.ML}

  The code generator will complain when a required

  ingredient does not provide a executable counterpart,

  e.g.~generating code

  for constants not yielding

  a defining equation (e.g.~the Hilbert choice

  operation \isa{SOME}):%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

\isanewline

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent will fail.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Theorem selection%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The list of all defining equations in a theory may be inspected

  using the \isa{{\isasymPRINTCODESETUP}} command:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{print{\isacharunderscore}codesetup}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent which displays a table of constant with corresponding

  defining equations (the additional stuff displayed

  shall not bother us for the moment).

  The typical \isa{HOL} tools are already set up in a way that

  function definitions introduced by \isa{{\isasymDEFINITION}},

  \isa{{\isasymPRIMREC}}, \isa{{\isasymFUN}},

  \isa{{\isasymFUNCTION}}, \isa{{\isasymCONSTDEFS}},

  \isa{{\isasymRECDEF}} are implicitly propagated

  to this defining equation table. Specific theorems may be

  selected using an attribute: \emph{code func}. As example,

  a weight selector function:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{primrec}\isamarkupfalse%

\isanewline

\ \ pick\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline

\ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent We want to eliminate the explicit destruction

  of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ simp%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent This theorem now is used for generating code:

  \lstsml{Thy/examples/pick1.ML}

  \noindent The policy is that \emph{default equations} stemming from

  \isa{{\isasymDEFINITION}},

  \isa{{\isasymPRIMREC}}, \isa{{\isasymFUN}},

  \isa{{\isasymFUNCTION}}, \isa{{\isasymCONSTDEFS}},

  \isa{{\isasymRECDEF}} statements are discarded as soon as an

  equation is explicitly selected by means of \emph{code func}.

  Further applications of \emph{code func} add theorems incrementally,

  but syntactic redundancies are implicitly dropped.  For example,

  using a modified version of the \isa{fac} function

  as defining equation, the then redundant (since

  syntactically subsumed) original defining equations

  are dropped.

  \begin{warn}

    The attributes \emph{code} and \emph{code del}

    associated with the existing code generator also apply to

    the new one: \emph{code} implies \emph{code func},

    and \emph{code del} implies \emph{code func del}.

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Type classes%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Type classes enter the game via the Isar class package.

  For a short introduction how to use it, see \cite{isabelle-classes};

  here we just illustrate its impact on code generation.

  In a target language, type classes may be represented

  natively (as in the case of Haskell).  For languages

  like SML, they are implemented using \emph{dictionaries}.

  Our following example specifies a class \qt{null},

  assigning to each of its inhabitants a \qt{null} value:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{class}\isamarkupfalse%

\ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline

\ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline

\isanewline

\isacommand{primrec}\isamarkupfalse%

\isanewline

\ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline

\ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent  We provide some instances for our \isa{null}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{instantiation}\isamarkupfalse%

\ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{instance}\isamarkupfalse%

%

\isadelimproof

\ %

\endisadelimproof

%

\isatagproof

\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

\isanewline

\isanewline

\isacommand{end}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent Constructing a dummy example:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ {\isachardoublequoteopen}dummy\ {\isacharequal}\ head\ {\isacharbrackleft}Some\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ None{\isacharbrackright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

Type classes offer a suitable occasion to introduce

  the Haskell serializer.  Its usage is almost the same

  as SML, but, in accordance with conventions

  some Haskell systems enforce, each module ends

  up in a single file. The module hierarchy is reflected in

  the file system, with root directory given as file specification.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lsthaskell{Thy/examples/Codegen.hs}

  \noindent (we have left out all other modules).

  \medskip

  The whole code in SML with explicit dictionary passing:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lstsml{Thy/examples/class.ML}

  \medskip

  \noindent or in OCaml:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lstsml{Thy/examples/class.ocaml}

  \medskip The explicit association of constants

  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}

  command.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{Recipes and advanced topics \label{sec:advanced}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

In this tutorial, we do not attempt to give an exhaustive

  description of the code generator framework; instead,

  we cast a light on advanced topics by introducing

  them together with practically motivated examples.  Concerning

  further reading, see

  \begin{itemize}

  \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}

    for exhaustive syntax diagrams.

  \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues

    of the code generator framework.

  \end{itemize}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Library theories \label{sec:library}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The \isa{HOL} \isa{Main} theory already provides a code

  generator setup

  which should be suitable for most applications. Common extensions

  and modifications are available by certain theories of the \isa{HOL}

  library; beside being useful in applications, they may serve

  as a tutorial for customizing the code generator setup.

  \begin{description}

    \item[\isa{Code{\isacharunderscore}Integer}] represents \isa{HOL} integers by big

       integer literals in target languages.

    \item[\isa{Code{\isacharunderscore}Char}] represents \isa{HOL} characters by 

       character literals in target languages.

    \item[\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Code{\isacharunderscore}Char},

       but also offers treatment of character codes; includes

       \isa{Code{\isacharunderscore}Integer}.

    \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,

       which in general will result in higher efficency; pattern

       matching with \isa{{\isadigit{0}}} / \isa{Suc}

       is eliminated;  includes \isa{Code{\isacharunderscore}Integer}.

    \item[\isa{Code{\isacharunderscore}Index}] provides an additional datatype

       \isa{index} which is mapped to target-language built-in integers.

       Useful for code setups which involve e.g. indexing of

       target-language arrays.

    \item[\isa{Code{\isacharunderscore}Message}] provides an additional datatype

       \isa{message{\isacharunderscore}string} which is isomorphic to strings;

       \isa{message{\isacharunderscore}string}s are mapped to target-language strings.

       Useful for code setups which involve e.g. printing (error) messages.

  \end{description}

  \begin{warn}

    When importing any of these theories, they should form the last

    items in an import list.  Since these theories adapt the

    code generator setup in a non-conservative fashion,

    strange effects may occur otherwise.

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Preprocessing%

}

\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 defining 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 an 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%

\ \ \isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%

\isadelimproof

\ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\item eliminating superfluous constants:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%

\isadelimproof

\ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ simp%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\item replacing executable but inconvenient constructs:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \isacommand{lemma}\isamarkupfalse%

\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline

\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%

\isadelimproof

\ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\end{itemize}

%

\begin{isamarkuptext}%

\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 \isa{{\isasymPRINTCODESETUP}} command.

  \begin{warn}

    The attribute \emph{code unfold}

    associated with the existing code generator also applies to

    the new one: \emph{code unfold} implies \emph{code inline}.

  \end{warn}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Concerning operational equality%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Surely you have already noticed how equality is treated

  by the code generator:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{primrec}\isamarkupfalse%

\isanewline

\ \ 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}%

\begin{isamarkuptext}%

The membership test during preprocessing is rewritten,

  resulting in \isa{op\ mem}, which itself

  performs an explicit equality check.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lstsml{Thy/examples/collect_duplicates.ML}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\begin{isamarkuptext}%

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\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}.

  The preprocessing framework does the rest.

  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:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{instantiation}\isamarkupfalse%

\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline

\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline

\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{instance}\isamarkupfalse%

%

\isadelimproof

\ %

\endisadelimproof

%

\isatagproof

\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

\isanewline

\isanewline

\isacommand{end}\isamarkupfalse%

\isanewline

\isanewline

\isacommand{lemma}\isamarkupfalse%

\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{unfolding}\isamarkupfalse%

\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp{\isacharunderscore}all%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

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, thus violating the type discipline

  for class operations.

  The solution is to add \isa{eq} explicitly to the first sort arguments in the

  code theorems:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\isamarkupfalse%

\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline

\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline

\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{unfolding}\isamarkupfalse%

\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%

\ rule{\isacharplus}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Then code generation succeeds:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lstsml{Thy/examples/lexicographic.ML}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\begin{isamarkuptext}%

In general, code theorems for overloaded constants may have more

  restrictive sort constraints than the underlying instance relation

  between class and type constructor as long as the whole system of

  constraints is coregular; code theorems violating coregularity

  are rejected immediately.  Consequently, it might be necessary

  to delete disturbing theorems in the code theorem table,

  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}

  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.

  In some cases, the automatically derived defining 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%

\isacommand{datatype}\isamarkupfalse%

\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

Then code generation for SML would fail with a message

  that the generated code conains illegal mutual dependencies:

  the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the

  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires

  \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually

  recursive \isa{instance} and \isa{function} definitions,

  but the SML serializer does not support this.

  In such cases, you have to provide you own equality equations

  involving auxiliary constants.  In our case,

  \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\isamarkupfalse%

\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequoteopen}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymlongleftrightarrow}\isanewline

\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{export{\isacharunderscore}code}\isamarkupfalse%

\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isacharcolon}{\isacharcolon}\ monotype\ {\isasymRightarrow}\ monotype\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}monotype{\isachardot}ML{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\lstsml{Thy/examples/monotype.ML}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Programs as sets of theorems%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

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 \isa{{\isasymCODETHMS}} command:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%

\ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent prints a table with \emph{all} defining equations

  for \isa{op\ mod}, including

  \emph{all} defining equations those equations depend

  on recursivly.  \isa{{\isasymCODETHMS}} provides a convenient

  mechanism to inspect the impact of a preprocessor setup

  on defining equations.

  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph

  visualizing dependencies between defining equations.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Constructor sets for 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 excactly 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 \isa{{\isasymPRINTCODESETUP}} command.

  In some cases, it may be convenient to alter or

  extend this table;  as an example, we will develope an alternative

  representation of natural numbers as binary digits, whose

  size does increase logarithmically with its value, not linear

  \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory (see \ref{eff_nat})

    does something similar}.  First, the digit representation:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{definition}\isamarkupfalse%

\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent We will use these two ">digits"< to represent natural numbers

  in binary digits, e.g.:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\isamarkupfalse%

\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Of course we also have to provide proper code equations for

  the operations, e.g. \isa{op\ {\isacharplus}}:%

\end{isamarkuptext}%