haftmann@20967: % haftmann@20967: \begin{isabellebody}% haftmann@20967: \def\isabellecontext{Codegen}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: \isanewline haftmann@26513: \isanewline haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % haftmann@20967: \isatagtheory wenzelm@21172: % haftmann@20967: \endisatagtheory haftmann@20967: {\isafoldtheory}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML wenzelm@21172: % wenzelm@21172: \isatagML wenzelm@21172: % wenzelm@21172: \endisatagML wenzelm@21172: {\isafoldML}% wenzelm@21172: % wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML wenzelm@21172: % haftmann@20967: \isamarkupchapter{Code generation from Isabelle theories% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsection{Introduction% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \isamarkupsubsection{Motivation% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@20967: \begin{isamarkuptext}% wenzelm@21172: Executing formal specifications as programs is a well-established wenzelm@21172: topic in the theorem proving community. With increasing wenzelm@21172: application of theorem proving systems in the area of wenzelm@21172: software development and verification, its relevance manifests wenzelm@21172: for running test cases and rapid prototyping. In logical wenzelm@21172: calculi like constructive type theory, wenzelm@21172: a notion of executability is implicit due to the nature haftmann@22550: of the calculus. In contrast, specifications in Isabelle wenzelm@21172: can be highly non-executable. In order to bridge wenzelm@21172: the gap between logic and executable specifications, wenzelm@21172: an explicit non-trivial transformation has to be applied: wenzelm@21172: code generation. wenzelm@21172: wenzelm@21172: This tutorial introduces a generic code generator for the wenzelm@21172: Isabelle system \cite{isa-tutorial}. wenzelm@21172: Generic in the sense that the wenzelm@21172: \qn{target language} for which code shall ultimately be wenzelm@21172: generated is not fixed but may be an arbitrary state-of-the-art wenzelm@21172: functional programming language (currently, the implementation haftmann@22550: supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell haftmann@22550: \cite{haskell-revised-report}). wenzelm@21172: We aim to provide a wenzelm@21172: versatile environment wenzelm@21172: suitable for software development and verification, wenzelm@21172: structuring the process wenzelm@21172: of code generation into a small set of orthogonal principles wenzelm@21172: while achieving a big coverage of application areas haftmann@21348: with maximum flexibility. haftmann@21348: haftmann@22550: Conceptually the code generator framework is part haftmann@22550: of Isabelle's \isa{Pure} meta logic; the object logic haftmann@22550: \isa{HOL} which is an extension of \isa{Pure} haftmann@22550: already comes with a reasonable framework setup and thus provides haftmann@22550: a good working horse for raising code-generation-driven haftmann@22550: applications. So, we assume some familiarity and experience haftmann@22550: with the ingredients of the \isa{HOL} \emph{Main} theory haftmann@22550: (see also \cite{isa-tutorial}).% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \isamarkupsubsection{Overview% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: The code generator aims to be usable with no further ado wenzelm@21172: in most cases while allowing for detailed customization. haftmann@22550: This manifests in the structure of this tutorial: haftmann@22550: we start with a generic example \secref{sec:example} haftmann@22550: and introduce code generation concepts \secref{sec:concept}. haftmann@22550: Section wenzelm@21186: \secref{sec:basics} explains how to use the framework naively, wenzelm@21172: presuming a reasonable default setup. Then, section wenzelm@21172: \secref{sec:advanced} deals with advanced topics, wenzelm@21172: introducing further aspects of the code generator framework wenzelm@21172: in a motivation-driven manner. Last, section \secref{sec:ml} wenzelm@21172: introduces the framework's internal programming interfaces. wenzelm@21172: wenzelm@21172: \begin{warn} wenzelm@21172: Ultimately, the code generator which this tutorial deals with wenzelm@21172: is supposed to replace the already established code generator wenzelm@21172: by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. wenzelm@21172: So, for the moment, there are two distinct code generators wenzelm@21172: in Isabelle. haftmann@22916: Also note that while the framework itself is haftmann@22550: object-logic independent, only \isa{HOL} provides a reasonable wenzelm@21172: framework setup. wenzelm@21172: \end{warn}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@22550: \isamarkupsection{An example: a simple theory of search trees \label{sec:example}% haftmann@22479: } haftmann@22479: \isamarkuptrue% haftmann@22550: % haftmann@22550: \begin{isamarkuptext}% haftmann@22916: When writing executable specifications using \isa{HOL}, haftmann@22916: it is convenient to use haftmann@22550: three existing packages: the datatype package for defining haftmann@22550: datatypes, the function package for (recursive) functions, haftmann@22550: and the class package for overloaded definitions. haftmann@22550: haftmann@22550: We develope a small theory of search trees; trees are represented haftmann@22550: as a datatype with key type \isa{{\isacharprime}a} and value type \isa{{\isacharprime}b}:% haftmann@22550: \end{isamarkuptext}% haftmann@22550: \isamarkuptrue% haftmann@22479: \isacommand{datatype}\isamarkupfalse% haftmann@22479: \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline haftmann@22550: \ \ {\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}% haftmann@22550: \begin{isamarkuptext}% haftmann@22550: \noindent Note that we have constrained the type of keys haftmann@22550: to the class of total orders, \isa{linorder}. haftmann@22550: haftmann@22550: We define \isa{find} and \isa{update} functions:% haftmann@22550: \end{isamarkuptext}% haftmann@22550: \isamarkuptrue% haftmann@25870: \isacommand{primrec}\isamarkupfalse% haftmann@22479: \isanewline haftmann@22479: \ \ 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 haftmann@22479: \ \ {\isachardoublequoteopen}find\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isacharequal}\ key\ then\ Some\ val\ else\ None{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@22479: \ \ {\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 haftmann@22479: \isanewline haftmann@22479: \isacommand{fun}\isamarkupfalse% haftmann@22479: \isanewline haftmann@22479: \ \ 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 haftmann@22479: \ \ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline haftmann@22479: \ \ \ \ if\ it\ {\isacharequal}\ key\ then\ Leaf\ key\ entry\isanewline haftmann@22479: \ \ \ \ \ \ else\ if\ it\ {\isasymle}\ key\isanewline haftmann@22479: \ \ \ \ \ \ then\ Branch\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\isanewline haftmann@22479: \ \ \ \ \ \ else\ Branch\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\isanewline haftmann@22479: \ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@22479: \ \ {\isacharbar}\ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline haftmann@22479: \ \ \ \ if\ it\ {\isasymle}\ key\isanewline haftmann@22479: \ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline haftmann@22479: \ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline haftmann@22550: \ \ \ {\isacharparenright}{\isachardoublequoteclose}% haftmann@22550: \begin{isamarkuptext}% haftmann@22550: \noindent For testing purpose, we define a small example haftmann@22550: using natural numbers \isa{nat} (which are a \isa{linorder}) haftmann@23132: as keys and list of nats as values:% haftmann@22550: \end{isamarkuptext}% haftmann@22550: \isamarkuptrue% haftmann@23132: \isacommand{definition}\isamarkupfalse% haftmann@22479: \isanewline haftmann@23132: \ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat{\isacharcomma}\ nat\ list{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline haftmann@23132: \isakeyword{where}\isanewline haftmann@23132: \ \ {\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 haftmann@23132: \ \ \ \ {\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}% haftmann@22550: \begin{isamarkuptext}% haftmann@22550: \noindent Then we generate code% haftmann@22550: \end{isamarkuptext}% haftmann@22550: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}% haftmann@22479: \begin{isamarkuptext}% haftmann@22550: \noindent which looks like: haftmann@22550: \lstsml{Thy/examples/tree.ML}% haftmann@22479: \end{isamarkuptext}% haftmann@22479: \isamarkuptrue% haftmann@22479: % haftmann@22550: \isamarkupsection{Code generation concepts and process \label{sec:concept}% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: \begin{figure}[h] haftmann@21348: \centering haftmann@21348: \includegraphics[width=0.7\textwidth]{codegen_process} haftmann@21348: \caption{code generator -- processing overview} haftmann@21348: \label{fig:process} haftmann@21348: \end{figure} haftmann@21348: haftmann@21348: The code generator employs a notion of executability wenzelm@21172: for three foundational executable ingredients known wenzelm@21172: from functional programming: haftmann@22060: \emph{defining equations}, \emph{datatypes}, and haftmann@22060: \emph{type classes}. A defining equation as a first approximation wenzelm@21172: is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} wenzelm@21172: (an equation headed by a constant \isa{f} with arguments haftmann@22798: \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}). haftmann@22060: Code generation aims to turn defining equations wenzelm@21172: into a functional program by running through wenzelm@21172: a process (see figure \ref{fig:process}): wenzelm@21172: wenzelm@21172: \begin{itemize} wenzelm@21172: wenzelm@21172: \item Out of the vast collection of theorems proven in a wenzelm@21172: \qn{theory}, a reasonable subset modeling haftmann@22060: defining equations is \qn{selected}. wenzelm@21172: wenzelm@21172: \item On those selected theorems, certain wenzelm@21172: transformations are carried out wenzelm@21172: (\qn{preprocessing}). Their purpose is to turn theorems wenzelm@21172: representing non- or badly executable wenzelm@21172: specifications into equivalent but executable counterparts. wenzelm@21172: The result is a structured collection of \qn{code theorems}. wenzelm@21172: haftmann@22479: \item These \qn{code theorems} then are \qn{translated} wenzelm@21172: into an Haskell-like intermediate wenzelm@21172: language. wenzelm@21172: wenzelm@21172: \item Finally, out of the intermediate language the final wenzelm@21172: code in the desired \qn{target language} is \qn{serialized}. wenzelm@21172: wenzelm@21172: \end{itemize} wenzelm@21172: wenzelm@21172: From these steps, only the two last are carried out wenzelm@21172: outside the logic; by keeping this layer as wenzelm@21172: thin as possible, the amount of code to trust is wenzelm@21172: kept to a minimum.% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isamarkupsection{Basics \label{sec:basics}% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsubsection{Invoking the code generator% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \begin{isamarkuptext}% haftmann@22916: Thanks to a reasonable setup of the \isa{HOL} theories, in wenzelm@21172: most cases code generation proceeds without further ado:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@25870: \isacommand{primrec}\isamarkupfalse% wenzelm@21172: \isanewline haftmann@22479: \ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@22479: \ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline haftmann@22479: \ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@22550: \noindent This executable specification is now turned to SML code:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@24379: \noindent The \isa{{\isasymEXPORTCODE}} command takes a space-separated list of wenzelm@21172: constants together with \qn{serialization directives} haftmann@22845: These start with a \qn{target language} haftmann@22845: identifier, followed by a file specification haftmann@22845: where to write the generated code to. wenzelm@21172: haftmann@22060: Internally, the defining equations for all selected wenzelm@21186: constants are taken, including any transitively required wenzelm@21172: constants, datatypes and classes, resulting in the following wenzelm@21172: code: wenzelm@21172: wenzelm@21172: \lstsml{Thy/examples/fac.ML} wenzelm@21172: wenzelm@21172: The code generator will complain when a required haftmann@22550: ingredient does not provide a executable counterpart, haftmann@22550: e.g.~generating code wenzelm@21172: for constants not yielding haftmann@22550: a defining equation (e.g.~the Hilbert choice haftmann@22550: operation \isa{SOME}):% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML wenzelm@21172: % wenzelm@21172: \isatagML wenzelm@21172: % wenzelm@21172: \endisatagML wenzelm@21172: {\isafoldML}% wenzelm@21172: % wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML wenzelm@21172: \isacommand{definition}\isamarkupfalse% wenzelm@21172: \isanewline haftmann@21993: \ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@22798: \ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}% wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML wenzelm@21172: % wenzelm@21172: \isatagML wenzelm@21172: % wenzelm@21172: \endisatagML wenzelm@21172: {\isafoldML}% wenzelm@21172: % wenzelm@21172: \isadelimML wenzelm@21172: % wenzelm@21172: \endisadelimML haftmann@25870: \isanewline haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}% haftmann@22550: \begin{isamarkuptext}% haftmann@22550: \noindent will fail.% haftmann@22550: \end{isamarkuptext}% haftmann@22550: \isamarkuptrue% haftmann@22550: % haftmann@20967: \isamarkupsubsection{Theorem selection% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \begin{isamarkuptext}% haftmann@22060: The list of all defining equations in a theory may be inspected haftmann@22292: using the \isa{{\isasymPRINTCODESETUP}} command:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@22292: \isacommand{print{\isacharunderscore}codesetup}\isamarkupfalse% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \noindent which displays a table of constant with corresponding haftmann@22060: defining equations (the additional stuff displayed haftmann@22751: shall not bother us for the moment). wenzelm@21172: haftmann@22916: The typical \isa{HOL} tools are already set up in a way that haftmann@22751: function definitions introduced by \isa{{\isasymDEFINITION}}, haftmann@25870: \isa{{\isasymPRIMREC}}, \isa{{\isasymFUN}}, haftmann@25870: \isa{{\isasymFUNCTION}}, \isa{{\isasymCONSTDEFS}}, haftmann@21348: \isa{{\isasymRECDEF}} are implicitly propagated haftmann@22060: to this defining equation table. Specific theorems may be wenzelm@21172: selected using an attribute: \emph{code func}. As example, wenzelm@21172: a weight selector function:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{primrec}\isamarkupfalse% wenzelm@21172: \isanewline haftmann@25870: \ \ pick\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline wenzelm@21172: \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline wenzelm@21172: \ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@22798: \noindent We want to eliminate the explicit destruction wenzelm@21172: of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{lemma}\isamarkupfalse% wenzelm@21172: \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline wenzelm@21172: \ \ {\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 wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: \ \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{by}\isamarkupfalse% wenzelm@21172: \ simp% wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: \isanewline wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: \isanewline haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@22798: \noindent This theorem now is used for generating code: wenzelm@21172: wenzelm@21172: \lstsml{Thy/examples/pick1.ML} wenzelm@21172: haftmann@22798: \noindent It might be convenient to remove the pointless original haftmann@22845: equation, using the \emph{func del} attribute:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{lemmas}\isamarkupfalse% haftmann@22845: \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline wenzelm@21172: \isanewline haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \lstsml{Thy/examples/pick2.ML} wenzelm@21172: haftmann@22798: \noindent Syntactic redundancies are implicitly dropped. For example, wenzelm@21172: using a modified version of the \isa{fac} function haftmann@22060: as defining equation, the then redundant (since haftmann@22060: syntactically subsumed) original defining equations wenzelm@21172: are dropped, resulting in a warning:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{lemma}\isamarkupfalse% wenzelm@21172: \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline wenzelm@21172: \ \ {\isachardoublequoteopen}fac\ n\ {\isacharequal}\ {\isacharparenleft}case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ n\ {\isacharasterisk}\ fac\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: \ \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{by}\isamarkupfalse% wenzelm@21172: \ {\isacharparenleft}cases\ n{\isacharparenright}\ simp{\isacharunderscore}all% wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: \isanewline wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: \isanewline haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \lstsml{Thy/examples/fac_case.ML} wenzelm@21172: wenzelm@21172: \begin{warn} haftmann@22292: The attributes \emph{code} and \emph{code del} wenzelm@21172: associated with the existing code generator also apply to wenzelm@21172: the new one: \emph{code} implies \emph{code func}, haftmann@22845: and \emph{code del} implies \emph{code func del}. wenzelm@21172: \end{warn}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@20967: \isamarkupsubsection{Type classes% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: Type classes enter the game via the Isar class package. wenzelm@21172: For a short introduction how to use it, see \cite{isabelle-classes}; wenzelm@21172: here we just illustrate its impact on code generation. wenzelm@21172: wenzelm@21172: In a target language, type classes may be represented haftmann@22798: natively (as in the case of Haskell). For languages wenzelm@21172: like SML, they are implemented using \emph{dictionaries}. wenzelm@21186: Our following example specifies a class \qt{null}, wenzelm@21172: assigning to each of its inhabitants a \qt{null} value:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{class}\isamarkupfalse% haftmann@22479: \ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline wenzelm@21172: \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline wenzelm@21172: \isanewline haftmann@25870: \isacommand{primrec}\isamarkupfalse% wenzelm@21172: \isanewline haftmann@25870: \ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline wenzelm@21172: \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline haftmann@22798: \ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% wenzelm@25731: \noindent We provide some instances for our \isa{null}:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@25533: \isacommand{instantiation}\isamarkupfalse% haftmann@25533: \ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline haftmann@25533: \isakeyword{begin}\isanewline haftmann@25533: \isanewline haftmann@25533: \isacommand{definition}\isamarkupfalse% haftmann@25533: \isanewline haftmann@25533: \ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline haftmann@25533: \isanewline haftmann@25533: \isacommand{definition}\isamarkupfalse% haftmann@25533: \isanewline wenzelm@25731: \ \ {\isachardoublequoteopen}null\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline haftmann@25533: \isanewline wenzelm@21172: \isacommand{instance}\isamarkupfalse% haftmann@25533: % wenzelm@21172: \isadelimproof wenzelm@21172: \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% wenzelm@21172: % wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: \isanewline wenzelm@21172: \isanewline haftmann@25533: \isacommand{end}\isamarkupfalse% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@25731: \noindent Constructing a dummy example:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: \isacommand{definition}\isamarkupfalse% wenzelm@21172: \isanewline wenzelm@21172: \ \ {\isachardoublequoteopen}dummy\ {\isacharequal}\ head\ {\isacharbrackleft}Some\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ None{\isacharbrackright}{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% wenzelm@21186: Type classes offer a suitable occasion to introduce wenzelm@21172: the Haskell serializer. Its usage is almost the same wenzelm@21172: as SML, but, in accordance with conventions wenzelm@21172: some Haskell systems enforce, each module ends wenzelm@21172: up in a single file. The module hierarchy is reflected in haftmann@22845: the file system, with root directory given as file specification.% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \lsthaskell{Thy/examples/Codegen.hs} haftmann@22798: \noindent (we have left out all other modules). wenzelm@21172: haftmann@22798: \medskip wenzelm@21172: wenzelm@21172: The whole code in SML with explicit dictionary passing:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@22798: \lstsml{Thy/examples/class.ML} haftmann@22798: haftmann@22798: \medskip haftmann@22798: haftmann@22798: \noindent or in OCaml:% haftmann@22292: \end{isamarkuptext}% haftmann@22292: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}% haftmann@22292: \begin{isamarkuptext}% haftmann@22798: \lstsml{Thy/examples/class.ocaml} wenzelm@21172: haftmann@22798: \medskip The explicit association of constants haftmann@22845: to classes can be inspected using the \isa{{\isasymPRINTCLASSES}} haftmann@22845: command.% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isamarkupsection{Recipes and advanced topics \label{sec:advanced}% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: In this tutorial, we do not attempt to give an exhaustive wenzelm@21172: description of the code generator framework; instead, wenzelm@21172: we cast a light on advanced topics by introducing wenzelm@21172: them together with practically motivated examples. Concerning wenzelm@21172: further reading, see wenzelm@21172: wenzelm@21172: \begin{itemize} wenzelm@21172: wenzelm@21172: \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} wenzelm@21172: for exhaustive syntax diagrams. haftmann@24193: \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues wenzelm@21172: of the code generator framework. wenzelm@21172: wenzelm@21172: \end{itemize}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@22798: \isamarkupsubsection{Library theories \label{sec:library}% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% haftmann@22916: The \isa{HOL} \isa{Main} theory already provides a code haftmann@22916: generator setup wenzelm@21172: which should be suitable for most applications. Common extensions haftmann@22916: and modifications are available by certain theories of the \isa{HOL} wenzelm@21172: library; beside being useful in applications, they may serve wenzelm@21186: as a tutorial for customizing the code generator setup. wenzelm@21172: wenzelm@21172: \begin{description} wenzelm@21172: wenzelm@25370: \item[\isa{Code{\isacharunderscore}Integer}] represents \isa{HOL} integers by big haftmann@22798: integer literals in target languages. wenzelm@25370: \item[\isa{Code{\isacharunderscore}Char}] represents \isa{HOL} characters by haftmann@22798: character literals in target languages. wenzelm@25370: \item[\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Code{\isacharunderscore}Char}, haftmann@22798: but also offers treatment of character codes; includes wenzelm@25370: \isa{Code{\isacharunderscore}Integer}. haftmann@23850: \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers, wenzelm@21186: which in general will result in higher efficency; pattern wenzelm@21172: matching with \isa{{\isadigit{0}}} / \isa{Suc} wenzelm@25370: is eliminated; includes \isa{Code{\isacharunderscore}Integer}. wenzelm@25370: \item[\isa{Code{\isacharunderscore}Index}] provides an additional datatype wenzelm@25370: \isa{index} which is mapped to target-language built-in integers. wenzelm@25370: Useful for code setups which involve e.g. indexing of wenzelm@25370: target-language arrays. wenzelm@25370: \item[\isa{Code{\isacharunderscore}Message}] provides an additional datatype wenzelm@25370: \isa{message{\isacharunderscore}string} which is isomorphic to strings; wenzelm@25370: \isa{message{\isacharunderscore}string}s are mapped to target-language strings. wenzelm@25370: Useful for code setups which involve e.g. printing (error) messages. wenzelm@21172: haftmann@22916: \end{description} haftmann@22916: haftmann@22916: \begin{warn} haftmann@22916: When importing any of these theories, they should form the last haftmann@22916: items in an import list. Since these theories adapt the haftmann@22916: code generator setup in a non-conservative fashion, haftmann@22916: strange effects may occur otherwise. haftmann@22916: \end{warn}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isamarkupsubsection{Preprocessing% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: Before selected function theorems are turned into abstract wenzelm@21172: code, a chain of definitional transformation steps is carried haftmann@27609: out: \emph{preprocessing}. In essence, the preprocessor haftmann@27609: consists of two components: a \emph{simpset} and \emph{function transformers}. wenzelm@21172: haftmann@27557: The \emph{simpset} allows to employ the full generality of the Isabelle haftmann@27557: simplifier. Due to the interpretation of theorems haftmann@22060: of defining equations, rewrites are applied to the right wenzelm@21172: hand side and the arguments of the left hand side of an wenzelm@21172: equation, but never to the constant heading the left hand side. haftmann@27557: An important special case are \emph{inline theorems} which may be haftmann@27557: declared an undeclared using the haftmann@22845: \emph{code inline} or \emph{code inline del} attribute respectively. wenzelm@21172: Some common applications:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{itemize} haftmann@22845: % haftmann@22845: \begin{isamarkuptext}% haftmann@22845: \item replacing non-executable constructs by executable ones:% haftmann@22845: \end{isamarkuptext}% haftmann@22845: \isamarkuptrue% haftmann@22845: \ \ \isacommand{lemma}\isamarkupfalse% wenzelm@21172: \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22845: \ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}% wenzelm@21172: \isadelimproof wenzelm@21172: \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{by}\isamarkupfalse% wenzelm@21172: \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: % haftmann@22845: \begin{isamarkuptext}% haftmann@22845: \item eliminating superfluous constants:% haftmann@22845: \end{isamarkuptext}% haftmann@22845: \isamarkuptrue% haftmann@22845: \ \ \isacommand{lemma}\isamarkupfalse% wenzelm@21172: \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22845: \ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}% wenzelm@21172: \isadelimproof wenzelm@21172: \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{by}\isamarkupfalse% wenzelm@21172: \ simp% wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: % haftmann@22845: \begin{isamarkuptext}% haftmann@22845: \item replacing executable but inconvenient constructs:% haftmann@22845: \end{isamarkuptext}% haftmann@22845: \isamarkuptrue% haftmann@22845: \ \ \isacommand{lemma}\isamarkupfalse% wenzelm@21172: \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22845: \ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}% wenzelm@21172: \isadelimproof wenzelm@21172: \ % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \isatagproof wenzelm@21172: \isacommand{by}\isamarkupfalse% wenzelm@21172: \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% wenzelm@21172: \endisatagproof wenzelm@21172: {\isafoldproof}% wenzelm@21172: % wenzelm@21172: \isadelimproof wenzelm@21172: % wenzelm@21172: \endisadelimproof wenzelm@21172: % wenzelm@21172: \end{itemize} wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% haftmann@27609: \emph{Function transformers} provide a very general interface, wenzelm@21172: transforming a list of function theorems to another wenzelm@21172: list of function theorems, provided that neither the heading wenzelm@21172: constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} haftmann@21348: pattern elimination implemented in haftmann@27609: theory \isa{Efficient{\isacharunderscore}Nat} (\secref{eff_nat}) uses this wenzelm@21172: interface. wenzelm@21172: haftmann@27557: \noindent The current setup of the preprocessor may be inspected using haftmann@27557: the \isa{{\isasymPRINTCODESETUP}} command. haftmann@27557: wenzelm@21172: \begin{warn} haftmann@27609: The attribute \emph{code unfold} wenzelm@21172: associated with the existing code generator also applies to wenzelm@21172: the new one: \emph{code unfold} implies \emph{code inline}. wenzelm@21172: \end{warn}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@22798: \isamarkupsubsection{Concerning operational equality% haftmann@22798: } haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: Surely you have already noticed how equality is treated haftmann@22798: by the code generator:% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@25870: \isacommand{primrec}\isamarkupfalse% haftmann@22798: \isanewline haftmann@22798: \ \ 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 haftmann@22798: \ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline haftmann@22798: \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline haftmann@22798: \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline haftmann@22798: \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline haftmann@22798: \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline haftmann@22798: \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% haftmann@22798: \begin{isamarkuptext}% haftmann@22798: The membership test during preprocessing is rewritten, haftmann@22798: resulting in \isa{op\ mem}, which itself haftmann@22798: performs an explicit equality check.% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}% haftmann@22798: \begin{isamarkuptext}% haftmann@22798: \lstsml{Thy/examples/collect_duplicates.ML}% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: Obviously, polymorphic equality is implemented the Haskell haftmann@26513: way using a type class. How is this achieved? HOL introduces haftmann@26513: an explicit class \isa{eq} with a corresponding operation haftmann@26513: \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}. haftmann@26513: The preprocessing framework does the rest. haftmann@22798: For datatypes, instances of \isa{eq} are implicitly derived haftmann@26513: when possible. For other types, you may instantiate \isa{eq} haftmann@26513: manually like any other type class. haftmann@22798: haftmann@22798: Though this \isa{eq} class is designed to get rarely in haftmann@22798: the way, a subtlety haftmann@22798: enters the stage when definitions of overloaded constants haftmann@22798: are dependent on operational equality. For example, let haftmann@22798: us define a lexicographic ordering on tuples:% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@25870: \isacommand{instantiation}\isamarkupfalse% haftmann@22798: \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline haftmann@25870: \isakeyword{begin}\isanewline haftmann@25870: \isanewline haftmann@25870: \isacommand{definition}\isamarkupfalse% haftmann@25870: \isanewline haftmann@25870: \ \ {\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 haftmann@25870: \ \ \ \ 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 haftmann@25870: \isanewline haftmann@25870: \isacommand{definition}\isamarkupfalse% haftmann@25870: \isanewline haftmann@25870: \ \ {\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 haftmann@25870: \ \ \ \ 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 haftmann@25870: \isanewline haftmann@25870: \isacommand{instance}\isamarkupfalse% haftmann@25870: % haftmann@22798: \isadelimproof haftmann@22798: \ % haftmann@22798: \endisadelimproof haftmann@22798: % haftmann@22798: \isatagproof haftmann@22798: \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% haftmann@22798: % haftmann@22798: \endisatagproof haftmann@22798: {\isafoldproof}% haftmann@22798: % haftmann@22798: \isadelimproof haftmann@22798: % haftmann@22798: \endisadelimproof haftmann@22798: \isanewline haftmann@22798: \isanewline haftmann@25870: \isacommand{end}\isamarkupfalse% haftmann@25870: \isanewline haftmann@22798: \isanewline haftmann@22798: \isacommand{lemma}\isamarkupfalse% haftmann@22798: \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22798: \ \ {\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 haftmann@22798: \ \ {\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 haftmann@22798: % haftmann@22798: \isadelimproof haftmann@22798: \ \ % haftmann@22798: \endisadelimproof haftmann@22798: % haftmann@22798: \isatagproof haftmann@22798: \isacommand{unfolding}\isamarkupfalse% haftmann@22798: \ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@22798: \ simp{\isacharunderscore}all% haftmann@22798: \endisatagproof haftmann@22798: {\isafoldproof}% haftmann@22798: % haftmann@22798: \isadelimproof haftmann@22798: % haftmann@22798: \endisadelimproof haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: Then code generation will fail. Why? The definition haftmann@22798: of \isa{op\ {\isasymle}} depends on equality on both arguments, haftmann@22798: which are polymorphic and impose an additional \isa{eq} haftmann@22798: class constraint, thus violating the type discipline haftmann@22798: for class operations. haftmann@22798: haftmann@22798: The solution is to add \isa{eq} explicitly to the first sort arguments in the haftmann@22798: code theorems:% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: \isacommand{lemma}\isamarkupfalse% haftmann@22798: \ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22798: \ \ {\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 haftmann@22798: \ \ \ \ 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 haftmann@22798: \ \ {\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 haftmann@22798: \ \ \ \ 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 haftmann@22798: % haftmann@22798: \isadelimproof haftmann@22798: \ \ % haftmann@22798: \endisadelimproof haftmann@22798: % haftmann@22798: \isatagproof haftmann@22798: \isacommand{unfolding}\isamarkupfalse% haftmann@22798: \ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse% haftmann@22798: \ rule{\isacharplus}% haftmann@22798: \endisatagproof haftmann@22798: {\isafoldproof}% haftmann@22798: % haftmann@22798: \isadelimproof haftmann@22798: % haftmann@22798: \endisadelimproof haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: \noindent Then code generation succeeds:% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22798: \ {\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 haftmann@22845: \ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}% haftmann@22798: \begin{isamarkuptext}% haftmann@22798: \lstsml{Thy/examples/lexicographic.ML}% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: In general, code theorems for overloaded constants may have more haftmann@22798: restrictive sort constraints than the underlying instance relation haftmann@22798: between class and type constructor as long as the whole system of haftmann@22798: constraints is coregular; code theorems violating coregularity haftmann@22798: are rejected immediately. Consequently, it might be necessary haftmann@22798: to delete disturbing theorems in the code theorem table, haftmann@22798: as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def} haftmann@22885: and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}. haftmann@22885: haftmann@22885: In some cases, the automatically derived defining equations haftmann@22885: for equality on a particular type may not be appropriate. haftmann@22885: As example, watch the following datatype representing haftmann@23132: monomorphic parametric types (where type constructors haftmann@23132: are referred to by natural numbers):% haftmann@22885: \end{isamarkuptext}% haftmann@22885: \isamarkuptrue% haftmann@22885: \isacommand{datatype}\isamarkupfalse% haftmann@23132: \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}% haftmann@22885: \isadelimproof haftmann@22885: % haftmann@22885: \endisadelimproof haftmann@22885: % haftmann@22885: \isatagproof haftmann@22885: % haftmann@22885: \endisatagproof haftmann@22885: {\isafoldproof}% haftmann@22885: % haftmann@22885: \isadelimproof haftmann@22885: % haftmann@22885: \endisadelimproof haftmann@22885: % haftmann@22885: \begin{isamarkuptext}% haftmann@22885: Then code generation for SML would fail with a message haftmann@22885: that the generated code conains illegal mutual dependencies: haftmann@23132: 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 haftmann@22885: instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires haftmann@23132: \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 haftmann@22885: recursive \isa{instance} and \isa{function} definitions, haftmann@22885: but the SML serializer does not support this. haftmann@22885: haftmann@22885: In such cases, you have to provide you own equality equations haftmann@22885: involving auxiliary constants. In our case, haftmann@22885: \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:% haftmann@22885: \end{isamarkuptext}% haftmann@22885: \isamarkuptrue% haftmann@22885: \isacommand{lemma}\isamarkupfalse% haftmann@22885: \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline haftmann@22885: \ \ {\isachardoublequoteopen}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymlongleftrightarrow}\isanewline haftmann@22885: \ \ \ \ \ 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 haftmann@22885: % haftmann@22885: \isadelimproof haftmann@22885: \ \ % haftmann@22885: \endisadelimproof haftmann@22885: % haftmann@22885: \isatagproof haftmann@22885: \isacommand{by}\isamarkupfalse% haftmann@22885: \ {\isacharparenleft}simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}% haftmann@22885: \endisatagproof haftmann@22885: {\isafoldproof}% haftmann@22885: % haftmann@22885: \isadelimproof haftmann@22885: % haftmann@22885: \endisadelimproof haftmann@22885: % haftmann@22885: \begin{isamarkuptext}% haftmann@22885: does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:% haftmann@22885: \end{isamarkuptext}% haftmann@22885: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22885: \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isacharcolon}{\isacharcolon}\ monotype\ {\isasymRightarrow}\ monotype\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline haftmann@22885: \ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}monotype{\isachardot}ML{\isachardoublequoteclose}% haftmann@22885: \begin{isamarkuptext}% haftmann@22885: \lstsml{Thy/examples/monotype.ML}% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \isamarkupsubsection{Programs as sets of theorems% haftmann@22798: } haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: As told in \secref{sec:concept}, code generation is based haftmann@22798: on a structured collection of code theorems. haftmann@22798: For explorative purpose, this collection haftmann@22798: may be inspected using the \isa{{\isasymCODETHMS}} command:% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: \isacommand{code{\isacharunderscore}thms}\isamarkupfalse% haftmann@22798: \ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}% haftmann@22798: \begin{isamarkuptext}% haftmann@22798: \noindent prints a table with \emph{all} defining equations haftmann@22798: for \isa{op\ mod}, including haftmann@22798: \emph{all} defining equations those equations depend haftmann@22798: on recursivly. \isa{{\isasymCODETHMS}} provides a convenient haftmann@22798: mechanism to inspect the impact of a preprocessor setup haftmann@22798: on defining equations. haftmann@22798: haftmann@22798: Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph haftmann@22798: visualizing dependencies between defining equations.% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@25411: \isamarkupsubsection{Constructor sets for datatypes% haftmann@25411: } haftmann@25411: \isamarkuptrue% haftmann@25411: % haftmann@25411: \begin{isamarkuptext}% haftmann@25411: Conceptually, any datatype is spanned by a set of haftmann@25411: \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} haftmann@25411: where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all} haftmann@25411: type variables in \isa{{\isasymtau}}. The HOL datatype package haftmann@25411: by default registers any new datatype in the table haftmann@25411: of datatypes, which may be inspected using haftmann@25411: the \isa{{\isasymPRINTCODESETUP}} command. haftmann@25411: haftmann@25411: In some cases, it may be convenient to alter or haftmann@26999: extend this table; as an example, we will develope an alternative haftmann@26999: representation of natural numbers as binary digits, whose haftmann@26999: size does increase logarithmically with its value, not linear haftmann@26999: \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat} haftmann@26999: does something similar}. First, the digit representation:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{definition}\isamarkupfalse% haftmann@26999: \ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline haftmann@26999: \isanewline haftmann@26999: \isacommand{definition}\isamarkupfalse% haftmann@26999: \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}% haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \noindent We will use these two ">digits"< to represent natural numbers haftmann@26999: in binary digits, e.g.:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{lemma}\isamarkupfalse% haftmann@26999: \ {\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 haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: \ \ % haftmann@26999: \endisadelimproof haftmann@26999: % haftmann@26999: \isatagproof haftmann@26999: \isacommand{by}\isamarkupfalse% haftmann@26999: \ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% haftmann@26999: \endisatagproof haftmann@26999: {\isafoldproof}% haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: % haftmann@26999: \endisadelimproof haftmann@26999: % haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \noindent Of course we also have to provide proper code equations for haftmann@26999: the operations, e.g. \isa{op\ {\isacharplus}}:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{lemma}\isamarkupfalse% haftmann@26999: \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: \ \ % haftmann@26999: \endisadelimproof haftmann@26999: % haftmann@26999: \isatagproof haftmann@26999: \isacommand{by}\isamarkupfalse% haftmann@26999: \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% haftmann@26999: \endisatagproof haftmann@26999: {\isafoldproof}% haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: % haftmann@26999: \endisadelimproof haftmann@26999: % haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \noindent We then instruct the code generator to view \isa{{\isadigit{0}}}, haftmann@26999: \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as haftmann@26999: datatype constructors:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% haftmann@26999: \ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}% haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \noindent For the former constructor \isa{Suc}, we provide a code haftmann@26999: equation and remove some parts of the default code generator setup haftmann@26999: which are an obstacle here:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{lemma}\isamarkupfalse% haftmann@26999: \ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline haftmann@26999: \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: \ \ % haftmann@26999: \endisadelimproof haftmann@26999: % haftmann@26999: \isatagproof haftmann@26999: \isacommand{by}\isamarkupfalse% haftmann@26999: \ simp% haftmann@26999: \endisatagproof haftmann@26999: {\isafoldproof}% haftmann@26999: % haftmann@26999: \isadelimproof haftmann@26999: \isanewline haftmann@26999: % haftmann@26999: \endisadelimproof haftmann@26999: \isanewline haftmann@26999: \isacommand{declare}\isamarkupfalse% haftmann@26999: \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline haftmann@26999: \isacommand{declare}\isamarkupfalse% haftmann@26999: \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}% haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \noindent This yields the following code:% haftmann@26999: \end{isamarkuptext}% haftmann@26999: \isamarkuptrue% haftmann@26999: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@26999: \ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}nat{\isacharunderscore}binary{\isachardot}ML{\isachardoublequoteclose}% haftmann@26999: \begin{isamarkuptext}% haftmann@26999: \lstsml{Thy/examples/nat_binary.ML}% haftmann@25411: \end{isamarkuptext}% haftmann@25411: \isamarkuptrue% haftmann@25411: % haftmann@25411: \begin{isamarkuptext}% haftmann@26973: \medskip haftmann@25411: haftmann@26999: From this example, it can be easily glimpsed that using own constructor sets haftmann@26999: is a little delicate since it changes the set of valid patterns for values haftmann@26999: of that type. Without going into much detail, here some practical hints: haftmann@26999: haftmann@26999: \begin{itemize} haftmann@26999: \item When changing the constuctor set for datatypes, take care to haftmann@26999: provide an alternative for the \isa{case} combinator (e.g. by replacing haftmann@26999: it using the preprocessor). haftmann@26999: \item Values in the target language need not to be normalized -- different haftmann@26999: values in the target language may represent the same value in the haftmann@26999: logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}). haftmann@26999: \item Usually, a good methodology to deal with the subleties of pattern haftmann@26999: matching is to see the type as an abstract type: provide a set haftmann@26999: of operations which operate on the concrete representation of the type, haftmann@26999: and derive further operations by combinations of these primitive ones, haftmann@26999: without relying on a particular representation. haftmann@26999: \end{itemize}% haftmann@25411: \end{isamarkuptext}% haftmann@25411: \isamarkuptrue% haftmann@25411: % haftmann@26999: \isadeliminvisible haftmann@26999: % haftmann@26999: \endisadeliminvisible haftmann@26999: % haftmann@26999: \isataginvisible haftmann@26999: \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% haftmann@26999: \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline haftmann@26999: \isacommand{declare}\isamarkupfalse% haftmann@26999: \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline haftmann@26999: \isacommand{declare}\isamarkupfalse% haftmann@26999: \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline haftmann@26999: \isacommand{declare}\isamarkupfalse% haftmann@26999: \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline haftmann@26999: \isacommand{lemma}\isamarkupfalse% haftmann@26999: \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@26999: \ simp% haftmann@26999: \endisataginvisible haftmann@26999: {\isafoldinvisible}% haftmann@26999: % haftmann@26999: \isadeliminvisible haftmann@26999: % haftmann@26999: \endisadeliminvisible haftmann@26999: % wenzelm@21172: \isamarkupsubsection{Customizing serialization% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@22798: \isamarkupsubsubsection{Basics% haftmann@22798: } haftmann@22798: \isamarkuptrue% haftmann@22798: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: Consider the following function and its corresponding wenzelm@21172: SML code:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@25870: \isacommand{primrec}\isamarkupfalse% wenzelm@21172: \isanewline wenzelm@21172: \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@22798: \ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% haftmann@21348: \isadelimtt wenzelm@21172: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21172: % haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt wenzelm@21172: % haftmann@21348: \endisadelimtt haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ in{\isacharunderscore}interval\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: \lstsml{Thy/examples/bool_literal.ML} wenzelm@21172: haftmann@22798: \noindent Though this is correct code, it is a little bit unsatisfactory: wenzelm@21172: boolean values and operators are materialized as distinguished wenzelm@21172: entities with have nothing to do with the SML-builtin notion wenzelm@21172: of \qt{bool}. This results in less readable code; wenzelm@21172: additionally, eager evaluation may cause programs to wenzelm@21172: loop or break which would perfectly terminate when wenzelm@21172: the existing SML \qt{bool} would be used. To map wenzelm@21172: the HOL \qt{bool} on SML \qt{bool}, we may use wenzelm@21172: \qn{custom serializations}:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21172: \isacommand{code{\isacharunderscore}type}\isamarkupfalse% wenzelm@21172: \ bool\isanewline wenzelm@21172: \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline wenzelm@21172: \isacommand{code{\isacharunderscore}const}\isamarkupfalse% wenzelm@21172: \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline wenzelm@21172: \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: The \isa{{\isasymCODETYPE}} commad takes a type constructor wenzelm@21172: as arguments together with a list of custom serializations. wenzelm@21172: Each custom serialization starts with a target language wenzelm@21172: identifier followed by an expression, which during wenzelm@21172: code serialization is inserted whenever the type constructor haftmann@21348: would occur. For constants, \isa{{\isasymCODECONST}} implements haftmann@21348: the corresponding mechanism. Each ``\verb|_|'' in wenzelm@21172: a serialization expression is treated as a placeholder wenzelm@21172: for the type constructor's (the constant's) arguments.% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: \lstsml{Thy/examples/bool_mlbool.ML} wenzelm@21172: haftmann@22798: \noindent This still is not perfect: the parentheses haftmann@21348: around the \qt{andalso} expression are superfluous. haftmann@21348: Though the serializer wenzelm@21172: by no means attempts to imitate the rich Isabelle syntax wenzelm@21172: framework, it provides some common idioms, notably wenzelm@21172: associative infixes with precedences which may be used here:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21172: \isacommand{code{\isacharunderscore}const}\isamarkupfalse% wenzelm@21172: \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline haftmann@21348: \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: \isanewline wenzelm@21172: \isanewline haftmann@24379: \isacommand{export{\isacharunderscore}code}\isamarkupfalse% haftmann@22845: \ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}% wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: \lstsml{Thy/examples/bool_infix.ML} wenzelm@21172: haftmann@22798: \medskip haftmann@22798: wenzelm@21172: Next, we try to map HOL pairs to SML pairs, using the haftmann@21348: infix ``\verb|*|'' type constructor and parentheses:% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21172: \isacommand{code{\isacharunderscore}type}\isamarkupfalse% wenzelm@21172: \ {\isacharasterisk}\isanewline wenzelm@21172: \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline wenzelm@21172: \isacommand{code{\isacharunderscore}const}\isamarkupfalse% wenzelm@21172: \ Pair\isanewline wenzelm@21172: \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: The initial bang ``\verb|!|'' tells the serializer to never put wenzelm@21172: parentheses around the whole expression (they are already present), wenzelm@21172: while the parentheses around argument place holders wenzelm@21172: tell not to put parentheses around the arguments. haftmann@21348: The slash ``\verb|/|'' (followed by arbitrary white space) wenzelm@21172: inserts a space which may be used as a break if necessary wenzelm@21172: during pretty printing. wenzelm@21172: haftmann@22798: These examples give a glimpse what mechanisms wenzelm@21186: custom serializations provide; however their usage wenzelm@21186: requires careful thinking in order not to introduce wenzelm@21186: inconsistencies -- or, in other words: wenzelm@21186: custom serializations are completely axiomatic. wenzelm@21186: wenzelm@21186: A further noteworthy details is that any special wenzelm@21186: character in a custom serialization may be quoted haftmann@21348: using ``\verb|'|''; thus, in haftmann@21348: ``\verb|fn '_ => _|'' the first haftmann@21348: ``\verb|_|'' is a proper underscore while the haftmann@21348: second ``\verb|_|'' is a placeholder. wenzelm@21186: wenzelm@21186: The HOL theories provide further haftmann@25411: examples for custom serializations.% wenzelm@21186: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21186: \isamarkupsubsubsection{Haskell serialization% wenzelm@21186: } wenzelm@21186: \isamarkuptrue% wenzelm@21186: % wenzelm@21186: \begin{isamarkuptext}% wenzelm@21186: For convenience, the default wenzelm@21186: HOL setup for Haskell maps the \isa{eq} class to wenzelm@21186: its counterpart in Haskell, giving custom serializations haftmann@21348: for the class (\isa{{\isasymCODECLASS}}) and its operation:% wenzelm@21186: \end{isamarkuptext}% wenzelm@21186: \isamarkuptrue% wenzelm@21186: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21186: \isacommand{code{\isacharunderscore}class}\isamarkupfalse% wenzelm@21186: \ eq\isanewline haftmann@22798: \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline wenzelm@21186: \isanewline wenzelm@21186: \isacommand{code{\isacharunderscore}const}\isamarkupfalse% haftmann@22798: \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline haftmann@22798: \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % wenzelm@21186: \begin{isamarkuptext}% wenzelm@21186: A problem now occurs whenever a type which wenzelm@21186: is an instance of \isa{eq} in HOL is mapped wenzelm@21186: on a Haskell-builtin type which is also an instance wenzelm@21186: of Haskell \isa{Eq}:% wenzelm@21186: \end{isamarkuptext}% wenzelm@21186: \isamarkuptrue% wenzelm@21186: \isacommand{typedecl}\isamarkupfalse% wenzelm@21186: \ bar\isanewline wenzelm@21186: \isanewline haftmann@26513: \isacommand{instantiation}\isamarkupfalse% haftmann@26513: \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline haftmann@26513: \isakeyword{begin}\isanewline haftmann@26513: \isanewline haftmann@26513: \isacommand{definition}\isamarkupfalse% haftmann@26732: \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline haftmann@26513: \isanewline wenzelm@21186: \isacommand{instance}\isamarkupfalse% haftmann@26513: % wenzelm@21186: \isadelimproof wenzelm@21186: \ % wenzelm@21186: \endisadelimproof wenzelm@21186: % wenzelm@21186: \isatagproof haftmann@26513: \isacommand{by}\isamarkupfalse% haftmann@26513: \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}% wenzelm@21186: \endisatagproof wenzelm@21186: {\isafoldproof}% wenzelm@21186: % wenzelm@21186: \isadelimproof wenzelm@21172: % wenzelm@21186: \endisadelimproof wenzelm@21186: \isanewline haftmann@26513: \isanewline haftmann@26513: \isacommand{end}\isamarkupfalse% haftmann@26513: \isanewline haftmann@21348: % haftmann@21348: \isadelimtt wenzelm@21186: \isanewline haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21186: \isacommand{code{\isacharunderscore}type}\isamarkupfalse% wenzelm@21186: \ bar\isanewline wenzelm@21186: \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % wenzelm@21186: \begin{isamarkuptext}% wenzelm@21186: The code generator would produce haftmann@22188: an additional instance, which of course is rejected. haftmann@22188: To suppress this additional instance, use haftmann@22188: \isa{{\isasymCODEINSTANCE}}:% wenzelm@21186: \end{isamarkuptext}% wenzelm@21186: \isamarkuptrue% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@21348: \isatagtt wenzelm@21186: \isacommand{code{\isacharunderscore}instance}\isamarkupfalse% wenzelm@21186: \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline wenzelm@21186: \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% haftmann@21348: \endisatagtt haftmann@21348: {\isafoldtt}% haftmann@21348: % haftmann@21348: \isadelimtt haftmann@21348: % haftmann@21348: \endisadelimtt haftmann@21348: % haftmann@22798: \isamarkupsubsubsection{Pretty printing% haftmann@22798: } haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: The serializer provides ML interfaces to set up haftmann@22798: pretty serializations for expressions like lists, numerals haftmann@22798: and characters; these are haftmann@22798: monolithic stubs and should only be used with the haftmann@22798: theories introduces in \secref{sec:library}.% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@21348: \isamarkupsubsection{Cyclic module dependencies% haftmann@21348: } haftmann@21348: \isamarkuptrue% haftmann@21348: % haftmann@21348: \begin{isamarkuptext}% haftmann@21348: Sometimes the awkward situation occurs that dependencies haftmann@21348: between definitions introduce cyclic dependencies haftmann@21348: between modules, which in the Haskell world leaves haftmann@21348: you to the mercy of the Haskell implementation you are using, haftmann@21348: while for SML code generation is not possible. haftmann@21348: haftmann@21348: A solution is to declare module names explicitly. haftmann@21348: Let use assume the three cyclically dependent haftmann@21348: modules are named \emph{A}, \emph{B} and \emph{C}. haftmann@21348: Then, by stating% haftmann@21348: \end{isamarkuptext}% haftmann@21348: \isamarkuptrue% haftmann@21348: \isacommand{code{\isacharunderscore}modulename}\isamarkupfalse% haftmann@21348: \ SML\isanewline haftmann@21348: \ \ A\ ABC\isanewline haftmann@21348: \ \ B\ ABC\isanewline haftmann@21348: \ \ C\ ABC% haftmann@21348: \begin{isamarkuptext}% haftmann@21348: we explicitly map all those modules on \emph{ABC}, haftmann@21348: resulting in an ad-hoc merge of this three modules haftmann@21348: at serialization time.% haftmann@21348: \end{isamarkuptext}% haftmann@21348: \isamarkuptrue% haftmann@21348: % haftmann@22798: \isamarkupsubsection{Incremental code generation% haftmann@22798: } haftmann@22798: \isamarkuptrue% haftmann@22798: % haftmann@22798: \begin{isamarkuptext}% haftmann@22798: Code generation is \emph{incremental}: theorems haftmann@22798: and abstract intermediate code are cached and extended on demand. haftmann@22798: The cache may be partially or fully dropped if the underlying haftmann@22798: executable content of the theory changes. haftmann@22798: Implementation of caching is supposed to transparently haftmann@22798: hid away the details from the user. Anyway, caching haftmann@22798: reaches the surface by using a slightly more general form haftmann@22798: of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}} haftmann@24379: and \isa{{\isasymEXPORTCODE}} commands: the list of constants haftmann@22798: may be omitted. Then, all constants with code theorems haftmann@22798: in the current cache are referred to.% haftmann@22798: \end{isamarkuptext}% haftmann@22798: \isamarkuptrue% haftmann@22798: % wenzelm@21172: \isamarkupsection{ML interfaces \label{sec:ml}% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@21348: \begin{isamarkuptext}% haftmann@21348: Since the code generator framework not only aims to provide haftmann@21348: a nice Isar interface but also to form a base for haftmann@21348: code-generation-based applications, here a short haftmann@21348: description of the most important ML interfaces.% haftmann@21348: \end{isamarkuptext}% haftmann@21348: \isamarkuptrue% haftmann@21348: % haftmann@24217: \isamarkupsubsection{Executable theory content: \isa{Code}% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: This Pure module implements the core notions of wenzelm@21172: executable content of a theory.% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@22292: \isamarkupsubsubsection{Managing executable content% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \isadelimmlref wenzelm@21172: % wenzelm@21172: \endisadelimmlref wenzelm@21172: % wenzelm@21172: \isatagmlref wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \begin{mldecls} wenzelm@26856: \indexml{Code.add\_func}\verb|Code.add_func: thm -> theory -> theory| \\ wenzelm@26856: \indexml{Code.del\_func}\verb|Code.del_func: thm -> theory -> theory| \\ wenzelm@26856: \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\ haftmann@27557: \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ haftmann@27557: \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ haftmann@27609: \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list option)|\isasep\isanewline% haftmann@21348: \verb| -> theory -> theory| \\ haftmann@27557: \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\ wenzelm@26856: \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ wenzelm@26856: \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline% haftmann@22479: \verb| -> (string * sort) list * (string * typ list) list| \\ wenzelm@26856: \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option| wenzelm@21172: \end{mldecls} wenzelm@21172: wenzelm@21172: \begin{description} wenzelm@21172: haftmann@24217: \item \verb|Code.add_func|~\isa{thm}~\isa{thy} adds function haftmann@21348: theorem \isa{thm} to executable content. haftmann@21348: haftmann@24217: \item \verb|Code.del_func|~\isa{thm}~\isa{thy} removes function haftmann@21348: theorem \isa{thm} from executable content, if present. haftmann@21348: haftmann@24217: \item \verb|Code.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds haftmann@22060: suspended defining equations \isa{lthms} for constant haftmann@21348: \isa{const} to executable content. haftmann@21348: haftmann@27557: \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes haftmann@27557: the preprocessor simpset. haftmann@21348: haftmann@27557: \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds haftmann@27609: function transformer \isa{f} (named \isa{name}) to executable content; haftmann@27609: \isa{f} is a transformer of the defining equations belonging haftmann@21348: to a certain function definition, depending on the haftmann@27609: current theory context. Returning \isa{NONE} indicates that no haftmann@27609: transformation took place; otherwise, the whole process will be iterated haftmann@27609: with the new defining equations. haftmann@21348: haftmann@27557: \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes haftmann@27609: function transformer named \isa{name} from executable content. haftmann@22060: haftmann@24421: \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds haftmann@24421: a datatype to executable content, with generation haftmann@24421: set \isa{cs}. haftmann@21348: haftmann@24217: \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const} haftmann@21348: returns type constructor corresponding to haftmann@21348: constructor \isa{const}; returns \isa{NONE} haftmann@21348: if \isa{const} is no constructor. haftmann@21348: haftmann@21348: \end{description}% haftmann@21348: \end{isamarkuptext}% haftmann@21348: \isamarkuptrue% haftmann@21348: % haftmann@21348: \endisatagmlref haftmann@21348: {\isafoldmlref}% haftmann@21348: % haftmann@21348: \isadelimmlref haftmann@21348: % haftmann@21348: \endisadelimmlref haftmann@21348: % haftmann@22292: \isamarkupsubsection{Auxiliary% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isadelimmlref wenzelm@21172: % wenzelm@21172: \endisadelimmlref wenzelm@21172: % wenzelm@21172: \isatagmlref wenzelm@21172: % wenzelm@21172: \begin{isamarkuptext}% wenzelm@21172: \begin{mldecls} wenzelm@26856: \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\ haftmann@26973: \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * ((string * sort) list * typ)| \\ haftmann@27557: \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\ haftmann@21348: \end{mldecls} haftmann@21348: haftmann@21348: \begin{description} haftmann@21348: haftmann@24217: \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s} haftmann@21348: reads a constant as a concrete term expression \isa{s}. haftmann@21348: haftmann@24217: \item \verb|CodeUnit.head_func|~\isa{thm} haftmann@22751: extracts the constant and its type from a defining equation \isa{thm}. haftmann@21348: haftmann@27557: \item \verb|CodeUnit.rewrite_func|~\isa{ss}~\isa{thm} haftmann@27557: rewrites a defining equation \isa{thm} with a simpset \isa{ss}; haftmann@27557: only arguments and right hand side are rewritten, haftmann@22060: not the head of the defining equation. haftmann@21348: haftmann@21348: \end{description}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \endisatagmlref wenzelm@21172: {\isafoldmlref}% wenzelm@21172: % wenzelm@21172: \isadelimmlref wenzelm@21172: % wenzelm@21172: \endisadelimmlref wenzelm@21172: % haftmann@20967: \isamarkupsubsection{Implementing code generator applications% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % wenzelm@21172: \begin{isamarkuptext}% haftmann@21348: Implementing code generator applications on top haftmann@21348: of the framework set out so far usually not only haftmann@21348: involves using those primitive interfaces haftmann@21348: but also storing code-dependent data and various haftmann@21348: other things. haftmann@21348: haftmann@21348: \begin{warn} wenzelm@21172: Some interfaces discussed here have not reached wenzelm@21172: a final state yet. wenzelm@21172: Changes likely to occur in future. haftmann@21452: \end{warn}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % wenzelm@21172: \isamarkupsubsubsection{Data depending on the theory's executable content% wenzelm@21172: } wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@21348: \begin{isamarkuptext}% haftmann@21452: Due to incrementality of code generation, changes in the haftmann@21452: theory's executable content have to be propagated in a haftmann@21452: certain fashion. Additionally, such changes may occur haftmann@21452: not only during theory extension but also during theory haftmann@21452: merge, which is a little bit nasty from an implementation haftmann@21452: point of view. The framework provides a solution haftmann@21452: to this technical challenge by providing a functorial haftmann@21452: data slot \verb|CodeDataFun|; on instantiation haftmann@21452: of this functor, the following types and operations haftmann@21452: are required: haftmann@21452: haftmann@21452: \medskip haftmann@21348: \begin{tabular}{l} haftmann@21348: \isa{type\ T} \\ haftmann@21348: \isa{val\ empty{\isacharcolon}\ T} \\ haftmann@21348: \isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\ haftmann@24217: \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T} haftmann@21348: \end{tabular} haftmann@21348: haftmann@21452: \begin{description} haftmann@21452: haftmann@21452: \item \isa{T} the type of data to store. haftmann@21452: haftmann@21452: \item \isa{empty} initial (empty) data. haftmann@21452: haftmann@21452: \item \isa{merge} merging two data slots. haftmann@21452: haftmann@22798: \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content; haftmann@21452: if possible, the current theory context is handed over haftmann@21452: as argument \isa{thy} (if there is no current theory context (e.g.~during haftmann@22798: theory merge, \verb|NONE|); \isa{consts} indicates the kind haftmann@21452: of change: \verb|NONE| stands for a fundamental change haftmann@22798: which invalidates any existing code, \isa{SOME\ consts} haftmann@22798: hints that executable content for constants \isa{consts} haftmann@21452: has changed. haftmann@21452: haftmann@21452: \end{description} haftmann@21452: haftmann@21452: An instance of \verb|CodeDataFun| provides the following haftmann@21452: interface: haftmann@21452: haftmann@21348: \medskip haftmann@21348: \begin{tabular}{l} haftmann@21348: \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\ haftmann@21348: \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ haftmann@21348: \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} haftmann@21452: \end{tabular} haftmann@21452: haftmann@21452: \begin{description} haftmann@21452: haftmann@21452: \item \isa{get} retrieval of the current data. haftmann@21452: haftmann@21452: \item \isa{change} update of current data (cached!) haftmann@21452: by giving a continuation. haftmann@21452: haftmann@21452: \item \isa{change{\isacharunderscore}yield} update with side result. haftmann@21452: haftmann@21452: \end{description}% haftmann@21452: \end{isamarkuptext}% haftmann@21452: \isamarkuptrue% haftmann@21452: % haftmann@21452: \begin{isamarkuptext}% haftmann@24628: \emph{Happy proving, happy hacking!}% wenzelm@21172: \end{isamarkuptext}% wenzelm@21172: \isamarkuptrue% wenzelm@21172: % haftmann@20967: \isadelimtheory haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % haftmann@20967: \isatagtheory haftmann@20967: \isacommand{end}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagtheory haftmann@20967: {\isafoldtheory}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: \isanewline haftmann@20967: \end{isabellebody}% haftmann@20967: %%% Local Variables: haftmann@20967: %%% mode: latex haftmann@20967: %%% TeX-master: "root" haftmann@20967: %%% End: