%

\begin{isabellebody}%

%

\begin{isamarkuptext}%

\noindent

The task is to develop a compiler from a generic type of expressions (built

up from variables, constants and binary operations) to a stack machine.  This

generic type of expressions is a generalization of the boolean expressions in

\S\ref{sec:boolex}.  This time we do not commit ourselves to a particular

type of variables or values but make them type parameters.  Neither is there

a fixed set of binary operations: instead the expression contains the

appropriate function itself.%

\end{isamarkuptext}%

\isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline

\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Bex\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}%

\begin{isamarkuptext}%

\noindent

The three constructors represent constants, variables and the application of

a binary operation to two subexpressions.

The value of an expression w.r.t.\ an environment that maps variables to

values is easily defined:%

\end{isamarkuptext}%

\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline

\isacommand{primrec}\isanewline

{\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline

{\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline

{\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e\isadigit{1}\ env{\isacharparenright}\ {\isacharparenleft}value\ e\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}%

\begin{isamarkuptext}%

The stack machine has three instructions: load a constant value onto the

stack, load the contents of a certain address onto the stack, and apply a

binary operation to the two topmost elements of the stack, replacing them by

the result. As for \isa{expr}, addresses and values are type parameters:%

\end{isamarkuptext}%

\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}%

\begin{isamarkuptext}%

The execution of the stack machine is modelled by a function

\isa{exec} that takes a list of instructions, a store (modelled as a

function from addresses to values, just like the environment for

evaluating expressions), and a stack (modelled as a list) of values,

and returns the stack at the end of the execution---the store remains

unchanged:%

\end{isamarkuptext}%

\isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline

\isacommand{primrec}\isanewline

{\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline

{\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline

\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline

\ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline

\ \ {\isacharbar}\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}f\ {\isacharparenleft}hd\ vs{\isacharparenright}\ {\isacharparenleft}hd{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharhash}{\isacharparenleft}tl{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%

\begin{isamarkuptext}%

\noindent

Recall that \isa{hd} and \isa{tl}

return the first element and the remainder of a list.

Because all functions are total, \isa{hd} is defined even for the empty

list, although we do not know what the result is. Thus our model of the

machine always terminates properly, although the above definition does not

tell us much about the result in situations where \isa{Apply} was executed

with fewer than two elements on the stack.

The compiler is a function from expressions to a list of instructions. Its

definition is pretty much obvious:%

\end{isamarkuptext}%

\isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline

\isacommand{primrec}\isanewline

{\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline

{\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline

{\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e\isadigit{2}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e\isadigit{1}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}%

\begin{isamarkuptext}%

Now we have to prove the correctness of the compiler, i.e.\ that the

execution of a compiled expression results in the value of the expression:%

\end{isamarkuptext}%

\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}%

\begin{isamarkuptext}%

\noindent

This theorem needs to be generalized to%

\end{isamarkuptext}%

\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}%

\begin{isamarkuptxt}%

\noindent

which is proved by induction on \isa{e} followed by simplification, once

we have the following lemma about executing the concatenation of two

instruction sequences:%

\end{isamarkuptxt}%

\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}%

\begin{isamarkuptxt}%

\noindent

This requires induction on \isa{xs} and ordinary simplification for the

base cases. In the induction step, simplification leaves us with a formula

that contains two \isa{case}-expressions over instructions. Thus we add

automatic case splitting as well, which finishes the proof:%

\end{isamarkuptxt}%

\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%

\begin{isamarkuptext}%

\noindent

Note that because \isaindex{auto} performs simplification, it can

also be modified in the same way \isa{simp} can. Thus the proof can be

rewritten as%

\end{isamarkuptext}%

\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%

\begin{isamarkuptext}%

\noindent

Although this is more compact, it is less clear for the reader of the proof.

We could now go back and prove \isa{exec (comp e) s [] = [value e s]}

merely by simplification with the generalized version we just proved.

However, this is unnecessary because the generalized version fully subsumes

its instance.%

\end{isamarkuptext}%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: