13. Making Append Vanish (2)

23/03/23

data Tree = Leaf Int | Node Tree Tree
flatten :: Tree -> [Int]
flatten (Leaf n) = [n]
flatten (Node l r) = flatten l ++ flatten r

flatten' t ns = flatten t ++ ns

Base Case:

flatten' (Leaf n) ns
=
flatten (Leaf n) ++ ns
=
[n] ++ ns
= 
n : ns

flatten' (Leaf n) ns = n : ns

Inductive Case:

flatten' (Node l r) ns
= flatten (Node l r) ++ ns
= (flatten l ++ flatten r) ++ ns
= flatten l ++ (flatten r ++ ns)
= flatten l ++ (flatten' r ns)
= flatten' l (flatten' r ns)

flatten' :: Tree -> [Int] -> [Int]
flatten' (Leaf n) ns = n : ns
flatten' (Node l r) ns = flatten' l (flatten' r ns)

flatten :: Tree -> [Int]
flatten t = flatten' t []

Compiler

Source Language

data Expr = Val Int | Add Expr Expr

Semantics/Meaning

Correctness of our compiler.

eval :: Exp -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval

Target Language (Virtual Machine)

type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD

Semantics

exec :: Code -> Stack -> Stack
exec [] s = s
exec (PUSH n : c) s = exec c (n : s)
exec (ADD : c) (m:n:s) = exec c (n+m : s)

Compiler

comp :: Expr -> Code
comp (Val n) = [PUSH n]
comp (Add x y) = comp x ++ comp y ++ [ADD]

Compiler Correctness

exec (comp e) s = (eval e) : s