(*<*)
theory ex07_2
imports "~~/src/HOL/IMP/Compiler"
begin
(*>*)
text {* \Exercise{Compiler optimization}
A common programming idiom is @{text "IF b THEN c"}, i.e.,
the else-branch consists of a single @{term SKIP} command.
\begin{enumerate}
\item
Look at how the program
@{term "IF Less (V ''x'') (N 5) THEN ''y'' ::= N 3 ELSE SKIP"}
is compiled by @{text ccomp} and identify a possible compiler optimization.
\item
Implement an optimized compiler (by modifying @{term ccomp}) which reduces the number of instructions
for programs of the form @{text "IF b THEN c"}.
\item
Extend the proof
of @{text ccomp_bigstep} to your modified compiler.
\end{enumerate}
*}
(*<*)
value "ccomp (IF Less (V ''x'') (N 5) THEN ''y'' ::= N 3 ELSE SKIP)"
fun ccomp2 :: "com \ instr list" where
"ccomp2 SKIP = []" |
"ccomp2 (x ::= a) = acomp a @ [STORE x]" |
"ccomp2 (c1;; c2) = ccomp2 c1 @ ccomp2 c2" |
"ccomp2 (IF b THEN c1 ELSE c2) =
(if c2 = SKIP
then (let cc1 = ccomp2 c1; cb = bcomp b False (size cc1) in cb @ cc1)
else (let cc1 = ccomp2 c1; cc2 = ccomp2 c2; cb = bcomp b False (size cc1 + 1)
in cb @ cc1 @ JMP (size cc2) # cc2))" |
"ccomp2 (WHILE b DO c) =
(let cc = ccomp2 c; cb = bcomp b False (size cc + 1)
in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
value "ccomp2 (IF Less (V ''x'') (N 5) THEN ''y'' ::= N 3 ELSE SKIP)"
lemma "(c,s) \ t \ ccomp2 c \ (0,s,stk) \* (size(ccomp2 c),t,stk)"
proof(induct arbitrary: stk rule: big_step_induct)
case (Assign x a s)
show ?case by (fastforce simp:fun_upd_def)
next
case (Seq c1 s1 s2 c2 s3)
let ?cc1 = "ccomp2 c1" let ?cc2 = "ccomp2 c2"
have "?cc1 @ ?cc2 \ (0,s1,stk) \* (size ?cc1,s2,stk)"
using Seq.hyps(2) by (fastforce)
moreover
have "?cc1 @ ?cc2 \ (size ?cc1,s2,stk) \* (size(?cc1 @ ?cc2),s3,stk)"
using Seq.hyps(4) by (fastforce)
ultimately show ?case by simp (blast intro: star_trans)
next
case (WhileTrue b s1 c s2 s3)
let ?cc = "ccomp2 c"
let ?cb = "bcomp b False (size ?cc + 1)"
let ?cw = "ccomp2(WHILE b DO c)"
have "?cw \ (0,s1,stk) \* (size ?cb + size ?cc,s2,stk)"
using WhileTrue(1,3) by fastforce
moreover
have "?cw \ (size ?cb + size ?cc,s2,stk) \* (0,s2,stk)"
by (fastforce)
moreover
have "?cw \ (0,s2,stk) \* (size ?cw,s3,stk)" by(rule WhileTrue(5))
ultimately show ?case by(blast intro: star_trans)
qed fastforce+
(*<*)
end
(*>*)