module Minilang.Lambda.Eval where

import Data.Text (Text, unpack)
import Debug.Trace (trace)

data Term
  = Var Text
  | Lam Text Term
  | App Term Term
  deriving (Show, Read, Eq)

type Env = [(Text, Value)]

data Value
  = V Text
  | Abs Text Term Env -- a closure, ie. lambda with its captured environment
  | Ap Value Value
  deriving (Show, Read, Eq)

-- call-by-value evaluator
eval :: Term -> Env -> Value
eval (Var x) env = case lookup x env of
  Just v -> v -- we do not need to eval v again
  Nothing -> V x -- x is not bound in env
eval (Lam x body) env = Abs x body env
eval (App f a) env =
  -- we need to force evaluation of the argument
  -- because haskell's default semantics is non-strict
  -- so if a' is never used, it will not be evaluated!
  let a' = eval a env
   in seq a' $ case eval f env of
        Abs x body env' -> eval body ((x, a') : env')
        f' -> Ap f' a'

evalNeed :: Term -> Env -> Value
evalNeed (Var x) env = case lookup x env of
  Just v -> v
  Nothing -> V x
evalNeed (Lam x body) env = Abs x body env
evalNeed (App f a) env =
  let a' = eval a env
   in case evalNeed f env of
        Abs x body env' -> evalNeed body ((x, a') : env')
        f' -> Ap f' a'

x =
  App
    ( App
        ( App
            ( App
                ( App
                    ( App
                        ( App
                            ( App
                                ( App
                                    (Lam "False" (Lam "True" (Lam "If" (Lam "Zero" (Lam "Succ" (Lam "One" (Lam "Two" (Lam "Three" (Lam "IsZero" (App (Var "IsZero") (Var "Two")))))))))))
                                    (Lam "f" (Lam "t" (Var "f")))
                                )
                                (Lam "f" (Lam "t" (Var "t")))
                            )
                            (Lam "b" (Lam "x" (Lam "y" (App (App (Var "b") (Var "x")) (Var "y")))))
                        )
                        (Lam "z" (Lam "s" (Var "z")))
                    )
                    (Lam "n" (Lam "z" (Lam "s" (App (Var "s") (Var "n")))))
                )
                (App (Var "Succ") (Var "Zero"))
            )
            (App (Var "Succ") (Var "One"))
        )
        (App (Var "Succ") (Var "Two"))
    )
    (Lam "n" (App (App (Var "n") (Var "True")) (Lam "m" (Var "False"))))