untyped-lambda.hs

{-# LANGUAGE LambdaCase #-}

data Term
    = TmVar Integer
    | TmAbs String Term
    | TmApp Term Term
    deriving (Show, Eq)

termShift :: Integer -> Term -> Term
termShift d = walk 0
  where
    walk :: Integer -> Term -> Term
    walk c = \case
      TmVar x -> if x > c then TmVar (x + d) else TmVar x
      TmAbs x t1 -> TmAbs x (walk (succ c) t1)
      TmApp t1 t2 -> TmApp (walk c t1) (walk c t2)

termSubst :: Integer -> Term -> Term -> Term
termSubst j s = walk 0
  where
    walk :: Integer -> Term -> Term
    walk c = \case
      TmVar x -> if x == j + c then termShift c s else TmVar x
      TmAbs x t1 -> TmAbs x (walk (succ c) t1)
      TmApp t1 t2 -> TmApp (walk c t1) (walk c t2)

termSubstTop :: Term -> Term -> Term
termSubstTop s t = termShift (-1) $ termSubst 0 (termShift 1 s) t

isval :: Term -> Bool
isval t = case t of
    TmAbs _ _ -> True
    _ -> False


eval :: Term -> Term
eval = \case
  TmApp t1 t2 -> case eval t1 of
                   TmAbs x t1' -> let v2' = eval t2 in
                                    if isval v2'
                                    then eval (termSubstTop v2' t1')
                                    else TmApp t1' t2
                   t1'' -> TmApp t1'' t2 -- or t
  t -> t