|
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 (*>*) |