Agda-2.3.2.2: src/prototyping/termrep/Terms/None.hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, StandaloneDeriving #-}
module Terms.None where
import Control.Applicative
import Types.Monad
data None = None
instance Functor (TermMonad None) where
fmap f (TMNone x) = TMNone (f x)
instance Applicative (TermMonad None) where
pure = TMNone
TMNone f <*> TMNone x = TMNone (f x)
-- deriving instance Applicative (TermMonad None)
instance Monad (TermMonad None) where
return = TMNone
TMNone x >>= f = f x
instance TermRep None where
type Var None = ()
type Term None = ()
type Type None = ()
type Context None = ()
newtype TermMonad None a = TMNone { unTMNone :: a }
type TermState None = ()
liftTC (TMNone x) = return x
initialTermState = return ()
emptyCxt = return ()
lookupCxt x cxt = return ((), TypedVar x ())
extendCxt e cxt = return ()
updateCxt x e cxt = return ()