1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | betaReduce = untilStable betaReduce1
betaReduce1 = everywhere' (mkT f)
where
f (AppE (LamE [VarP x] e) z) = subst x z e
f (AppE (LamE (VarP x:ps) e) z) = subst x z (LamE ps e)
f a = a
subst x replacement = everywhere (mkT f)
where
f (VarE x1) | x1 == x = replacement
f a = a
untilStable f x = go x where
go x = case f x of
x1 | x1 == x -> x
x1 -> go (f x)
|