{-# language LambdaCase #-}

import Data.String
import Data.HashMap.Strict (HashMap, (!))
import qualified Data.HashMap.Lazy as M

data Term = Var !String | !Term :$ !Term | Lam !String !Term deriving (Show)

instance IsString Term where
  fromString = Var . fromString
infixl 8 :$


-- NBE
--------------------------------------------------------------------------------

data Val = VVar !String | VApp !Val Val | VLam (Val -> Val)

eval :: HashMap String Val -> Term -> Val
eval e = \case
  Var v  -> e ! v
  f :$ x -> case (eval e f, eval e x) of
    (VLam t, x) -> t x
    (f     , x) -> VApp f x
  Lam v t -> VLam $ \val -> eval (M.insert v val e) t


-- Eval-apply environment machine
--------------------------------------------------------------------------------

type Env  = HashMap String Whnf
data Whnf = WVar !String | WApp !Whnf Whnf | WLam !String !Env !Term

eval' :: Env -> Term -> Whnf
eval' e = \case
  Var v  -> e ! v
  f :$ x -> case (eval' e f, eval' e x) of
    (WLam v e' t, x) -> eval' (M.insert v x e') t
    (f          , x) -> WApp f x
  Lam v t -> WLam v e t