13739
|
1 |
(*<*)
|
|
2 |
theory a3 = Main:
|
|
3 |
(*>*)
|
|
4 |
|
|
5 |
subsection{* Compilation *}
|
|
6 |
|
|
7 |
text {* This exercise deals with the compiler example in section~3.3
|
|
8 |
of \cite{isabelle-tutorial}. The simple side effect free expressions
|
|
9 |
are extended with side effects.
|
|
10 |
\begin{enumerate}
|
|
11 |
|
|
12 |
\item Read sections 3.3 and 8.2 of \cite{isabelle-tutorial}. Study
|
|
13 |
the section about @{text fun_upd} in theory @{text Fun} of HOL:
|
|
14 |
@{text"fun_upd f x y"}, written @{text"f(x:=y)"}, is @{text f}
|
|
15 |
updated at @{text x} with new value @{text y}.
|
|
16 |
|
|
17 |
\item Extend data type @{text "('a, 'v) expr"} with a new alternative
|
|
18 |
@{text "Assign x e"} that shall represent an assignment @{text "x =
|
|
19 |
e"} of the value of the expression @{text e} to the variable @{text x}.
|
|
20 |
The value of an assignment shall be the value of @{text e}.
|
|
21 |
|
|
22 |
\item Modify the evaluation function @{text value} such that it can
|
|
23 |
deal with assignments. Note that since the evaluation of an expression
|
|
24 |
may now change the environment, it no longer suffices to return only
|
|
25 |
the value from the evaluation of an expression.
|
|
26 |
|
|
27 |
Define a function @{text "se_free :: expr \<Rightarrow> bool"} that
|
|
28 |
identifies side effect free expressions. Show that @{text "se_free e"}
|
|
29 |
implies that evaluation of @{text e} does not change the environment.
|
|
30 |
|
|
31 |
\item Extend data type @{text "('a, 'v) instr"} with a new instruction
|
|
32 |
@{text "Store x"} that stores the topmost element on the stack in
|
|
33 |
address/variable @{text x}, without removing it from the stack.
|
|
34 |
Update the machine semantics @{text exec} accordingly. You will face
|
|
35 |
the same problem as in the extension of @{text value}.
|
|
36 |
|
|
37 |
\item Modify the compiler @{text comp} and its correctness proof to
|
|
38 |
accommodate the above changes.
|
|
39 |
\end{enumerate}
|
|
40 |
*}
|
|
41 |
(*<*)
|
|
42 |
end
|
|
43 |
(*>*) |