untyped-lambda.hs

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 t = case t of
      TmVar x -> if x > c then TmVar (x + d) else t
      TmAbs x t1 -> TmAbs x (walk (c+1) 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 t = case t of
      TmVar x -> if x == j + c then termShift c s else t
      TmAbs x t1 -> TmAbs x (walk (c+1) 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 t = case t of
    TmApp t1 t2 -> let t1'' = eval t1 in
                       case t1'' of
                            TmAbs x t1' -> let v2' = eval t2 in
                                           if isval v2'
                                              then eval (termSubstTop v2' t1')
                                              else TmApp t1' t2
                            _ -> TmApp t1'' t2 -- or t
    _ -> t