{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Eval where

import AST
import ASTfunc


eval :: Expr '[] t -> t
eval = eval'Expr VZ

eval'Expr :: Val env -> Expr env t -> t
eval'Expr v (Expr e) = eval' eval'Expr v e

eval' :: (forall env' t'. Val env' -> expr env' t' -> t')
      -> Val env -> PExpr expr env t -> t
eval' _ _ (Const _ x) = x
eval' f v (Pair x y) = (f v x, f v y)
eval' _ _ Nil = ()
eval' f v (Prim op x) = applyOper op (f v x)
eval' _ v (Var (V _ i)) = prjV v i
eval' f v (Let lhs rhs e) = f (vpush lhs (f v rhs) v) e

applyOper :: Oper (t -> t') -> t -> t'
applyOper (Add t) (x, y) | NumDict <- reifyNum t = x + y
applyOper (Mul t) (x, y) | NumDict <- reifyNum t = x * y
applyOper Round x = round x