Evaluate.hs

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

module Evaluate where

import Validate (Index (..))
import qualified Validate as Validated


data Value t where
  Boolean :: Bool -> Value Bool
  Integer :: Integer -> Value Integer
  Closure :: (Value t -> Value t') -> Value (t -> t')

instance Show (Value t) where
  show = \case
    Boolean b -> show b
    Integer i -> show i
    Closure _ -> "<closure>"

data VariableEnvironment env where
  Empty :: VariableEnvironment '[]
  Cons  :: Value t -> VariableEnvironment env -> VariableEnvironment (t : env)

evaluate :: Validated.Expression '[] t -> Value t
evaluate expr = go Empty expr
  where
    go :: VariableEnvironment env -> Validated.Expression env t -> Value t
    go env = \case
      Validated.BooleanLiteral b    -> Boolean b
      Validated.IntegerLiteral i    -> Integer i
      Validated.Abstraction body    -> Closure $ \arg -> go (Cons arg env) body
      Validated.Application fun arg -> let Closure f = go env fun in f (go env arg)
      Validated.Variable idx        -> get idx env
    
    get :: Index env t -> VariableEnvironment env -> Value t
    get Zero       (Cons val _) = val
    get (Succ idx) (Cons _ env) = get idx env