diff -r 79136ce06bdb -r 2aaf339fb7c1 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Tue Mar 03 17:05:18 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,390 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Introduction}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Introduction\isanewline -\isakeyword{imports}\ Setup\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories% -} -\isamarkuptrue% -% -\isamarkupsection{Introduction and Overview% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This tutorial introduces a generic code generator for the - \isa{Isabelle} system. - Generic in the sense that the - \qn{target language} for which code shall ultimately be - generated is not fixed but may be an arbitrary state-of-the-art - functional programming language (currently, the implementation - supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell} - \cite{haskell-revised-report}). - - Conceptually the code generator framework is part - of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic - \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} - already comes with a reasonable framework setup and thus provides - a good working horse for raising code-generation-driven - applications. So, we assume some familiarity and experience - with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories. - (see also \cite{isa-tutorial}). - - The code generator aims to be usable with no further ado - in most cases while allowing for detailed customisation. - This manifests in the structure of this tutorial: after a short - conceptual introduction with an example (\secref{sec:intro}), - we discuss the generic customisation facilities (\secref{sec:program}). - A further section (\secref{sec:adaption}) is dedicated to the matter of - \qn{adaption} to specific target language environments. After some - further issues (\secref{sec:further}) we conclude with an overview - of some ML programming interfaces (\secref{sec:ml}). - - \begin{warn} - Ultimately, the code generator which this tutorial deals with - is supposed to replace the existing code generator - by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. - So, for the moment, there are two distinct code generators - in Isabelle. In case of ambiguity, we will refer to the framework - described here as \isa{generic\ code\ generator}, to the - other as \isa{SML\ code\ generator}. - Also note that while the framework itself is - object-logic independent, only \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} provides a reasonable - framework setup. - \end{warn}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Code generation via shallow embedding \label{sec:intro}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The key concept for understanding \isa{Isabelle}'s code generation is - \emph{shallow embedding}, i.e.~logical entities like constants, types and - classes are identified with corresponding concepts in the target language. - - Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and - \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form - the core of a functional programming language. The default code generator setup - allows to turn those into functional programs immediately. - This means that \qt{naive} code generation can proceed without further ado. - For example, here a simple \qt{implementation} of amortised queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{datatype}\isamarkupfalse% -\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{fun}\isamarkupfalse% -\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Then we can generate code e.g.~for \isa{SML} as follows:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{export{\isacharunderscore}code}\isamarkupfalse% -\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline -\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent resulting in the following code:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example = \\ -\hspace*{0pt}struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun foldl f a [] = a\\ -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\ -\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\ -\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ -\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\ -\hspace*{0pt} ~~~let\\ -\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\ -\hspace*{0pt} ~~~in\\ -\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\ -\hspace*{0pt} ~~~end;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of - constants for which code shall be generated; anything else needed for those - is added implicitly. Then follows a target language identifier - (\isa{SML}, \isa{OCaml} or \isa{Haskell}) and a freely chosen module name. - A file name denotes the destination to store the generated code. Note that - the semantics of the destination depends on the target language: for - \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} - it denotes a \emph{directory} where a file named as the module name - (with extension \isa{{\isachardot}hs}) is written:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{export{\isacharunderscore}code}\isamarkupfalse% -\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline -\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This is how the corresponding code in \isa{Haskell} looks like:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}\\ -\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\ -\hspace*{0pt}foldla f a [] = a;\\ -\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\ -\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}list{\char95}case ::~forall t a.~t -> (a -> [a] -> t) -> [a] -> t;\\ -\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ -\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Queue a = AQueue [a] [a];\\ -\hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Queue a;\\ -\hspace*{0pt}empty = AQueue [] [];\\ -\hspace*{0pt}\\ -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ -\hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ -\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ -\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command; - for more details see \secref{sec:further}.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Code generator architecture \label{sec:concept}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -What you have seen so far should be already enough in a lot of cases. If you - are content with this, you can quit reading here. Anyway, in order to customise - and adapt the code generator, it is inevitable to gain some understanding - how it works. - - \begin{figure}[h] - \begin{tikzpicture}[x = 4.2cm, y = 1cm] - \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white]; - \tikzstyle process=[ellipse, draw, thick, color = green, fill = white]; - \tikzstyle process_arrow=[->, semithick, color = green]; - \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory}; - \node (eqn) at (2, 2) [style=entity] {code equations}; - \node (iml) at (2, 0) [style=entity] {intermediate language}; - \node (seri) at (1, 0) [style=process] {serialisation}; - \node (SML) at (0, 3) [style=entity] {\isa{SML}}; - \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}}; - \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}}; - \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}}; - \draw [style=process_arrow] (HOL) .. controls (2, 4) .. - node [style=process, near start] {selection} - node [style=process, near end] {preprocessing} - (eqn); - \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml); - \draw [style=process_arrow] (iml) -- (seri); - \draw [style=process_arrow] (seri) -- (SML); - \draw [style=process_arrow] (seri) -- (OCaml); - \draw [style=process_arrow, dashed] (seri) -- (further); - \draw [style=process_arrow] (seri) -- (Haskell); - \end{tikzpicture} - \caption{Code generator architecture} - \label{fig:arch} - \end{figure} - - The code generator employs a notion of executability - for three foundational executable ingredients known - from functional programming: - \emph{code equations}, \emph{datatypes}, and - \emph{type classes}. A code equation as a first approximation - is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} - (an equation headed by a constant \isa{f} with arguments - \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}). - Code generation aims to turn code equations - into a functional program. This is achieved by three major - components which operate sequentially, i.e. the result of one is - the input - of the next in the chain, see diagram \ref{fig:arch}: - - \begin{itemize} - - \item Out of the vast collection of theorems proven in a - \qn{theory}, a reasonable subset modelling - code equations is \qn{selected}. - - \item On those selected theorems, certain - transformations are carried out - (\qn{preprocessing}). Their purpose is to turn theorems - representing non- or badly executable - specifications into equivalent but executable counterparts. - The result is a structured collection of \qn{code theorems}. - - \item Before the selected code equations are continued with, - they can be \qn{preprocessed}, i.e. subjected to theorem - transformations. This \qn{preprocessor} is an interface which - allows to apply - the full expressiveness of ML-based theorem transformations - to code generation; motivating examples are shown below, see - \secref{sec:preproc}. - The result of the preprocessing step is a structured collection - of code equations. - - \item These code equations are \qn{translated} to a program - in an abstract intermediate language. Think of it as a kind - of \qt{Mini-Haskell} with four \qn{statements}: \isa{data} - (for datatypes), \isa{fun} (stemming from code equations), - also \isa{class} and \isa{inst} (for type classes). - - \item Finally, the abstract program is \qn{serialised} into concrete - source code of a target language. - - \end{itemize} - - \noindent From these steps, only the two last are carried out outside the logic; by - keeping this layer as thin as possible, the amount of code to trust is - kept to a minimum.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: