{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE LambdaCase #-}

module Minilang.Lambda.Eval where

import Data.Aeson (FromJSON, ToJSON)
import Data.String (IsString (..))
import Data.Text (Text, pack)
import GHC.Generics (Generic)

data Term
  = Var Text
  | Lam Text Term
  | App Term Term
  | Num Int
  deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)

instance IsString Term where
  fromString = Var . pack

data Value = Clos EnvValue Text Term | VNeut Neutral | VNum Int
  deriving (Show, Read, Eq)

data Neutral = NVar Text | NNum Int | NApp Neutral Value
  deriving (Show, Read, Eq)

type Env = [(Text, Term)]

type EnvValue = [(Text, Value)]

newEnv :: Env
newEnv = []

normalise :: Term -> Term
normalise term = readBack (eval [] term)

-- call-by-value evaluator
-- from https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-eval%29
eval :: EnvValue -> Term -> Value
eval env = \case
  Var x -> case lookup x env of
    Just term -> term
    Nothing -> VNeut (NVar x)
  Lam x body -> Clos env x body
  App f a ->
    let f' = eval env f
        a' = eval env a
     in f' `seq` a' `seq` apply f' a'
  Num n -> VNum n

apply :: Value -> Value -> Value
apply f a =
  case f of
    Clos closureEnv x body ->
      let env' = (x, a) : closureEnv
       in eval env' body
    VNeut f' -> VNeut (NApp f' a)
    VNum n -> VNeut (NApp (NNum n) a)

readBack :: Value -> Term
readBack = go []
  where
    go names = \case
      Clos env x body ->
        let name = freshName x names
            names' = name : names
            val' = eval ((x, VNeut (NVar name)) : env) body
         in Lam name (go names' val')
      VNeut (NVar n) -> Var n
      VNeut (NNum n) -> Num n
      VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
      VNum n -> Num n

freshName :: Text -> [Text] -> Text
freshName x names
  | x `elem` names = freshName (x <> "'") names
  | otherwise = x