Aidan Ewart
Viewing eval.hs
The source for this file is available here.
data Term
= Var Int
| Lam Term
| App Term Term
lift :: (Int, Term) -> Term
lift (i, Var v) | v < i = Var v
lift (i, Var v) | v >= i = Var (v+1)
lift (i, Lam b) =
let c = lift (i+1, b) in Lam c
lift (i, App f a) =
let g = lift (i, f)
b = lift (i, a)
in App g b
lower :: (Int, Term) -> Term
lower (i, Var v) | v < i = Var v
lower (i, Var v) | v >= i = Var (v-1)
lower (i, App f a) =
let g = lower (i, f)
b = lower (i, a)
in App g b
lower (i, Lam b) =
let c = lower (i+1, b)
in Lam c
subst :: (Int, Term, Term) -> Term
subst (i, st, Var v) | i == v = st
subst (i, st, Var v) | i /= v = Var v
subst (i, st, App f a) =
let g = subst (i, st, f)
b = subst (i, st, a)
in App g b
subst (i, st, Lam b) =
let c = subst (i+1, lift (0, st), b)
in Lam c
eval :: Term -> Term
eval (Lam b) = Lam b
eval (App f a) =
let (Lam b) = eval f
sb = subst (0, a, b)
lb = lower (0, sb)
vb = eval lb
in vb