Is this a push/enter interpreter?

Main.hs

module Main where

data Term = Var Int          -- variable
          | App Term Term    -- f x
          | Abs Term         -- λbody
          | Let Term Term    -- x:body
          | Con Int          -- k[n]
          | Case Term [Term] -- case expression

-- The eval/apply evaluator for contrast.
-- data Value = Closure [Value] Term
--            | Data Int [Value]
-- 
-- eval :: [Value] -> Term -> Maybe Value
-- eval env (Var n)          =    index env n
-- eval env (App f x)        = do f' <- eval env f
--                                x' <- eval env x
--                                apply f' x'
-- eval env (Abs body)       =    pure (Closure env body)
-- eval env (Let x body)     = do x' <- eval env x
--                                eval (x' : env) body
-- eval env (Con n)          =    pure (Data n [])
-- eval env (Case body alts) = do b <- eval env body
--                                case b of
--                                  (Data n args) -> do
--                                      alt <- index alts n
--                                      foldr (\arg f -> do f' <- f
--                                                          apply f' arg)
--                                         (eval env alt) args
--                                  _             -> Nothing
-- 
-- apply :: Value -> Value -> Maybe Value
-- apply (Closure env body) x = eval (x:env) body
-- apply (Data n xs)        x = pure (Data n (x:xs))

data Thunk = Closure [Thunk] Term
data Value = Index Int [Thunk]

enter :: Thunk -> [Thunk] -> Maybe Value
enter (Closure env body) args = eval env body args

eval :: [Thunk] -> Term -> [Thunk] -> Maybe Value
eval env (Var n)           args     = do x <- index env n
                                         enter x args
eval env (App f x)         args     =    eval env f (Closure env x : args)
eval env (Abs body)        (x:args) =    eval (x:env) body args
eval env (Abs body)        _        =    Nothing
eval env (Let x body)      args     =    eval (Closure env x:env) body args
eval env (Con n)           args     =    pure (Index n args)
eval env (Case body alts)  args     = do (Index n xs) <- eval env body []
                                         alt <- index alts n
                                         eval env alt (xs ++ args)

main :: IO ()
main = do
    putStrLn "Hello, Haskell!"

index :: [a] -> Int -> Maybe a
index (_:xs) n | (n > 0)  = index xs (n-1)
index (x:_)  n | (n == 0) = Just x
index _      _            = Nothing