Unique.lhs

The Unique module implements the Normal Form function by
using Barendregt's variable convention, i.e., all bound
variables are unique.

> module Unique(nf) where
> import Lambda
> import qualified Data.Map as M
> import Control.Monad.State
> import IdInt

The first step is to make all variables unique.
Then normal form is computed by repeatedly performing
substitution (beta reduction) on the leftmost redex.
Normalization is run in a State monad with the next free variable.


> nf :: LC IdInt -> LC IdInt
> nf e = evalState (nf' e') i
>   where (e', (i, _)) = runState (unique e) (firstBoundId, M.empty)

> type N a = State IdInt a

> nf' :: LC IdInt -> N (LC IdInt)
> nf' e@(Var _) = return e
> nf' (Lam x e) = liftM (Lam x) (nf' e)
> nf' (App f a) = do
>     f' <- whnf f
>     case f' of
>         Lam x b -> subst x a b >>= nf'
>         _ -> liftM2 App (nf' f') (nf' a)

Compute the weak head normal form.

> whnf :: LC IdInt -> N (LC IdInt)
> whnf e@(Var _) = return e
> whnf e@(Lam _ _) = return e
> whnf (App f a) = do
>     f' <- whnf f
>     case f' of
>         Lam x b -> subst x a b >>= whnf
>         _ -> return $ App f' a

Substitution proceeds by cloning the term that is inserted
at every place it is put.

(TODO: No need to clone $\lambda$-free terms.)

> subst :: IdInt -> LC IdInt -> LC IdInt -> N (LC IdInt)
> subst x s b = sub b
>  where sub e@(Var v) | v == x = clone M.empty s
>                      | otherwise = return e
>        sub (Lam v e) = liftM (Lam v) (sub e)
>        sub (App f a) = liftM2 App (sub f) (sub a)
>
>        clone m e@(Var v) = return $ maybe e Var (M.lookup v m)
>        clone m (Lam v e) = do v' <- newVar; liftM (Lam v') (clone (M.insert v v' m) e)
>        clone m (App f a) = liftM2 App (clone m f) (clone m a)

Create a fresh variable.

> newVar :: N IdInt
> newVar = do
>     i <- get
>     put (succ i)
>     return i

Do the actual translation of the term to unique variables.
We keep mapping of old variable names to new variable name.
Free variables are just left alone since they are already
uniquely named.

> type U a = State (IdInt, M.Map IdInt IdInt) a

> unique :: LC IdInt -> U (LC IdInt)
> unique (Var v) = liftM Var (getVar v)
> unique (Lam v e) = liftM2 Lam (addVar v) (unique e)
> unique (App f a) = liftM2 App (unique f) (unique a)

Add a variable to the mapping.

> addVar :: IdInt -> U IdInt
> addVar v = do
>    (i, m) <- get
>    put (succ i, M.insert v i m)
>    return i

Find an existing variable in the mapping.

> getVar :: IdInt -> U IdInt
> getVar v = do
>     (_, m) <- get
>     return $ maybe v id (M.lookup v m)