5 \isamarkupsection{Case Study: Compiling Expressions% |
5 \isamarkupsection{Case Study: Compiling Expressions% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:ExprCompiler} |
9 \label{sec:ExprCompiler} |
|
10 \index{compiling expressions example|(}% |
10 The task is to develop a compiler from a generic type of expressions (built |
11 The task is to develop a compiler from a generic type of expressions (built |
11 from variables, constants and binary operations) to a stack machine. This |
12 from variables, constants and binary operations) to a stack machine. This |
12 generic type of expressions is a generalization of the boolean expressions in |
13 generic type of expressions is a generalization of the boolean expressions in |
13 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
14 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
14 type of variables or values but make them type parameters. Neither is there |
15 type of variables or values but make them type parameters. Neither is there |
58 \ \ {\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}% |
59 \ \ {\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}% |
59 \begin{isamarkuptext}% |
60 \begin{isamarkuptext}% |
60 \noindent |
61 \noindent |
61 Recall that \isa{hd} and \isa{tl} |
62 Recall that \isa{hd} and \isa{tl} |
62 return the first element and the remainder of a list. |
63 return the first element and the remainder of a list. |
63 Because all functions are total, \isa{hd} is defined even for the empty |
64 Because all functions are total, \cdx{hd} is defined even for the empty |
64 list, although we do not know what the result is. Thus our model of the |
65 list, although we do not know what the result is. Thus our model of the |
65 machine always terminates properly, although the definition above does not |
66 machine always terminates properly, although the definition above does not |
66 tell us much about the result in situations where \isa{Apply} was executed |
67 tell us much about the result in situations where \isa{Apply} was executed |
67 with fewer than two elements on the stack. |
68 with fewer than two elements on the stack. |
68 |
69 |
79 execution of a compiled expression results in the value of the expression:% |
80 execution of a compiled expression results in the value of the expression:% |
80 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |
81 \isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}% |
82 \isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}% |
82 \begin{isamarkuptext}% |
83 \begin{isamarkuptext}% |
83 \noindent |
84 \noindent |
84 This theorem needs to be generalized to% |
85 This theorem needs to be generalized:% |
85 \end{isamarkuptext}% |
86 \end{isamarkuptext}% |
86 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}% |
87 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}% |
87 \begin{isamarkuptxt}% |
88 \begin{isamarkuptxt}% |
88 \noindent |
89 \noindent |
89 which is proved by induction on \isa{e} followed by simplification, once |
90 It will be proved by induction on \isa{e} followed by simplification. |
90 we have the following lemma about executing the concatenation of two |
91 First, we must prove a lemma about executing the concatenation of two |
91 instruction sequences:% |
92 instruction sequences:% |
92 \end{isamarkuptxt}% |
93 \end{isamarkuptxt}% |
93 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
94 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
94 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}% |
95 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}% |
95 \begin{isamarkuptxt}% |
96 \begin{isamarkuptxt}% |
96 \noindent |
97 \noindent |
97 This requires induction on \isa{xs} and ordinary simplification for the |
98 This requires induction on \isa{xs} and ordinary simplification for the |
98 base cases. In the induction step, simplification leaves us with a formula |
99 base cases. In the induction step, simplification leaves us with a formula |
99 that contains two \isa{case}-expressions over instructions. Thus we add |
100 that contains two \isa{case}-expressions over instructions. Thus we add |
100 automatic case splitting as well, which finishes the proof:% |
101 automatic case splitting, which finishes the proof:% |
101 \end{isamarkuptxt}% |
102 \end{isamarkuptxt}% |
102 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
103 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
103 \begin{isamarkuptext}% |
104 \begin{isamarkuptext}% |
104 \noindent |
105 \noindent |
105 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can |
106 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can |
113 |
114 |
114 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
115 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
115 merely by simplification with the generalized version we just proved. |
116 merely by simplification with the generalized version we just proved. |
116 However, this is unnecessary because the generalized version fully subsumes |
117 However, this is unnecessary because the generalized version fully subsumes |
117 its instance.% |
118 its instance.% |
|
119 \index{compiling expressions example|)}% |
118 \end{isamarkuptext}% |
120 \end{isamarkuptext}% |
119 \end{isabellebody}% |
121 \end{isabellebody}% |
120 %%% Local Variables: |
122 %%% Local Variables: |
121 %%% mode: latex |
123 %%% mode: latex |
122 %%% TeX-master: "root" |
124 %%% TeX-master: "root" |