packages feed

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 ()