NbE.hs

NbE.hs

module NbE where

data Term
    = Var Int
    -- ^ DeBruijin Indicies (count outwards)
    | Lam Term
    | App Term Term
    | Pair Term Term
    | Fst Term
    | Snd Term
    deriving (Show, Eq)

data Value
    = VNeu Head [Frame]
    | VLam Clo
    | VPair Value Value
    deriving Show

data Clo = Clo [Value] Term
    deriving Show

data Head
    = Local Int
    -- ^ DeBruijin Levels (count inwards)
    deriving Show

-- Frames = Elimination Forms
data Frame
    = KApp Value
    | KFst
    | KSnd
    deriving Show

vlocal :: Int -> Value
vlocal lvl = VNeu (Local lvl) []

--------------------------------------------------------------------------------
-- Eval

eval :: Term -> ([Value] -> Value)
eval (Var ix) env = env !! ix
eval (Lam tm) env = VLam (Clo env tm)
eval (App fn arg) env = doAp (eval fn env) (eval arg env)
eval (Pair l r) env = VPair (eval l env) (eval r env)
eval (Fst tm) env = doFst (eval tm env)
eval (Snd tm) env = doSnd (eval tm env)

doAp :: Value -> Value -> Value
doAp (VLam clo) arg = instClo clo arg
doAp (VNeu hd spine) arg = VNeu hd (KApp arg : spine)
doAp _ _ = error "Bad doAp"

doFst :: Value -> Value
doFst (VPair l _) = l
doFst (VNeu hd spine) = VNeu hd (KFst : spine)
doFst _ = error "Bad doFst"

doSnd :: Value -> Value
doSnd (VPair _ r) = r
doSnd (VNeu hd spine) = VNeu hd (KFst : spine)
doSnd _ = error "Bad doSnd"

instClo :: Clo -> Value -> Value
instClo (Clo env tm) v = eval tm (v : env)

--------------------------------------------------------------------------------
-- Quote

quote :: Int -> Value -> Term
quote size (VLam clo) = Lam $ quoteClo size clo
quote size (VNeu hd spine) = foldr (quoteFrame size) (quoteHead size hd) spine
quote size (VPair l r) = Pair (quote size l) (quote size r)

quoteHead :: Int -> Head -> Term
quoteHead size (Local lvl) = quoteVar size lvl

quoteFrame :: Int -> Frame -> Term -> Term
quoteFrame size (KApp v) tm = App tm (quote size v)
quoteFrame size KFst tm = Fst tm
quoteFrame size KSnd tm = Snd tm

quoteVar :: Int -> Int -> Term
quoteVar size lvl = Var (size - lvl - 1)

quoteClo :: Int -> Clo -> Term
quoteClo size (Clo env tm) = quote (size + 1) $ eval tm (vlocal size : env)

--------------------------------------------------------------------------------
-- Normalization

nf :: Term -> Term
nf tm = quote 0 $ eval tm []

nf' :: [Value] -> Term -> Term
nf' env tm = quote (length env) $ eval tm env

example :: Term
example = Lam (App (Lam $ Var 0) (Var 0))

idtm :: Term
idtm = Lam $ Var 0

equate :: Term -> Term -> Bool
equate tm0 tm1 = (nf tm0) == (nf tm1)