6 The task is to develop a compiler from a generic type of expressions (built
7 up from variables, constants and binary operations) to a stack machine. This
8 generic type of expressions is a generalization of the boolean expressions in
9 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular
10 type of variables or values but make them type parameters. Neither is there
11 a fixed set of binary operations: instead the expression contains the
12 appropriate function itself.%
14 \isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline
15 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline
16 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline
17 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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}%
18 \begin{isamarkuptext}%
20 The three constructors represent constants, variables and the application of
21 a binary operation to two subexpressions.
23 The value of an expression w.r.t.\ an environment that maps variables to
24 values is easily defined:%
26 \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
27 \isacommand{primrec}\isanewline
28 {\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline
29 {\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline
30 {\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}%
31 \begin{isamarkuptext}%
32 The stack machine has three instructions: load a constant value onto the
33 stack, load the contents of a certain address onto the stack, and apply a
34 binary operation to the two topmost elements of the stack, replacing them by
35 the result. As for \isa{expr}, addresses and values are type parameters:%
37 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline
39 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}%
40 \begin{isamarkuptext}%
41 The execution of the stack machine is modelled by a function
42 \isa{exec} that takes a list of instructions, a store (modelled as a
43 function from addresses to values, just like the environment for
44 evaluating expressions), and a stack (modelled as a list) of values,
45 and returns the stack at the end of the execution---the store remains
48 \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
49 \isacommand{primrec}\isanewline
50 {\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline
51 {\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline
52 \ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline
53 \ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline
54 \ \ {\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}%
55 \begin{isamarkuptext}%
57 Recall that \isa{hd} and \isa{tl}
58 return the first element and the remainder of a list.
59 Because all functions are total, \isa{hd} is defined even for the empty
60 list, although we do not know what the result is. Thus our model of the
61 machine always terminates properly, although the above definition does not
62 tell us much about the result in situations where \isa{Apply} was executed
63 with fewer than two elements on the stack.
65 The compiler is a function from expressions to a list of instructions. Its
66 definition is pretty much obvious:%
68 \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
69 \isacommand{primrec}\isanewline
70 {\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline
71 {\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline
72 {\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}%
73 \begin{isamarkuptext}%
74 Now we have to prove the correctness of the compiler, i.e.\ that the
75 execution of a compiled expression results in the value of the expression:%
77 \isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}%
78 \begin{isamarkuptext}%
80 This theorem needs to be generalized to%
82 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}%
85 which is proved by induction on \isa{e} followed by simplification, once
86 we have the following lemma about executing the concatenation of two
87 instruction sequences:%
89 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
90 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}%
93 This requires induction on \isa{xs} and ordinary simplification for the
94 base cases. In the induction step, simplification leaves us with a formula
95 that contains two \isa{case}-expressions over instructions. Thus we add
96 automatic case splitting as well, which finishes the proof:%
98 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
99 \begin{isamarkuptext}%
101 Note that because \isaindex{auto} performs simplification, it can
102 also be modified in the same way \isa{simp} can. Thus the proof can be
105 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
106 \begin{isamarkuptext}%
108 Although this is more compact, it is less clear for the reader of the proof.
110 We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
111 merely by simplification with the generalized version we just proved.
112 However, this is unnecessary because the generalized version fully subsumes
118 %%% TeX-master: "root"