content: {-# LANGUAGE RankNTypes, TypeOperators, ScopedTypeVariables,
               DataKinds, TypeFamilies, PolyKinds,
               GADTs #-}
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Language.Glambda.Eval
  -- Copyright   :  (C) 2015 Richard Eisenberg
  -- License     :  BSD-style (see LICENSE)
  -- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
  -- Stability   :  experimental
  --
  -- Glambda expression evaluators for checked expressions.
  --
  ----------------------------------------------------------------------------
  
  module Language.Glambda.Eval ( eval, step ) where
  
  import Language.Glambda.Exp
  import Language.Glambda.Token
  import Language.Glambda.Shift
  
  -- | Given a lambda and an expression, beta-reduce.
  apply :: Val (arg -> res) -> Exp '[] arg -> Exp '[] res
  apply (LamVal body) arg = subst arg body
  
  -- | Apply an arithmetic operator to two values.
  arith :: Val Int -> ArithOp ty -> Val Int -> Exp '[] ty
  arith (IntVal n1) Plus     (IntVal n2) = IntE (n1 + n2)
  arith (IntVal n1) Minus    (IntVal n2) = IntE (n1 - n2)
  arith (IntVal n1) Times    (IntVal n2) = IntE (n1 * n2)
  arith (IntVal n1) Divide   (IntVal n2) = IntE (n1 `div` n2)
  arith (IntVal n1) Mod      (IntVal n2) = IntE (n1 `mod` n2)
  arith (IntVal n1) Less     (IntVal n2) = BoolE (n1 < n2)
  arith (IntVal n1) LessE    (IntVal n2) = BoolE (n1 <= n2)
  arith (IntVal n1) Greater  (IntVal n2) = BoolE (n1 > n2)
  arith (IntVal n1) GreaterE (IntVal n2) = BoolE (n1 >= n2)
  arith (IntVal n1) Equals   (IntVal n2) = BoolE (n1 == n2)
  
  -- | Conditionally choose between two expressions
  cond :: Val Bool -> Exp '[] t -> Exp '[] t -> Exp '[] t
  cond (BoolVal True)  e _ = e
  cond (BoolVal False) _ e = e
  
  -- | Unroll a `fix` one level
  unfix :: Val (ty -> ty) -> Exp '[] ty
  unfix (LamVal body) = subst (Fix (Lam body)) body
  
  -- | A well-typed variable in an empty context is impossible.
  impossibleVar :: Elem '[] x -> a
  impossibleVar _ = error "GHC's typechecker failed"
    -- GHC 7.8+ supports EmptyCase for this, but the warnings for that
    -- construct don't work yet.
  
  -- | Evaluate an expression, using big-step semantics.
  eval :: Exp '[] t -> Val t
  eval (Var v)          = impossibleVar v
  eval (Lam body)       = LamVal body
  eval (App e1 e2)      = eval (apply (eval e1) e2)
  eval (Arith e1 op e2) = eval (arith (eval e1) op (eval e2))
  eval (Cond e1 e2 e3)  = eval (cond (eval e1) e2 e3)
  eval (Fix e)          = eval (unfix (eval e))
  eval (IntE n)         = IntVal n
  eval (BoolE b)        = BoolVal b
  
  -- | Step an expression, either to another expression or to a value.
  step :: Exp '[] t -> Either (Exp '[] t) (Val t)
  step (Var v)          = impossibleVar v
  step (Lam body)       = Right (LamVal body)
  step (App e1 e2)      = case step e1 of
                            Left e1' -> Left (App e1' e2)
                            Right (LamVal body) -> Left (subst e2 body)
  step (Arith e1 op e2) = case step e1 of
                            Left e1' -> Left (Arith e1' op e2)
                            Right v1 -> case step e2 of
                              Left e2' -> Left (Arith (val v1) op e2')
                              Right v2 -> Left (arith v1 op v2)
  step (Cond e1 e2 e3)  = case step e1 of
                            Left e1' -> Left (Cond e1' e2 e3)
                            Right v1 -> Left (cond v1 e2 e3)
  step (Fix e)          = case step e of
                            Left e' -> Left (Fix e')
                            Right v -> Left (unfix v)
  step (IntE n)         = Right (IntVal n)
  step (BoolE b)        = Right (BoolVal b)
  