LambdaPi.hs

LambdaPi.hs

-- http://www.andres-loeh.de/LambdaPi/
module LambaPi where

data TermI
  = Ann TermC TermC
  | Star
  | Pi TermC TermC
  | Bound Int
  | Free Name
  | TermI :@: TermC
  deriving (Show,Eq)

data TermC
  = Inf TermI
  | Lam TermC
  deriving (Show,Eq)

data Name
  = Global String
  | Local Int
  | Quote Int
  deriving (Show,Eq)

data Value
  = VLam (Value -> Value)
  | VStar
  | VPi Value (Value -> Value)
  | VNeutral Neutral

type Type = Value
type Context = [(Name,Type)]

data Neutral
  = NFree Name
  | NApp Neutral Value

vfree :: Name -> Value
vfree n = VNeutral (NFree n)

type Env = [Value]

evalI :: TermI -> Env -> Value
evalI (Ann e _) d  = evalC e d
evalI (Free x) d   = vfree x
evalI (Bound i) d  = d !! i
evalI (e :@: e') d = vapp (evalI e d) (evalC e' d)
evalI Star d       = VStar
evalI (Pi tau tau') d = VPi (evalC tau d) (\x -> evalC tau' (x:d))

vapp :: Value -> Value -> Value
vapp (VLam f) v     = f v
vapp (VNeutral n) v = VNeutral (NApp n v)

evalC :: TermC -> Env -> Value
evalC (Inf i) d = evalI i d
evalC (Lam e) d = VLam (\x -> evalC e (x:d))