Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Names

Description

EDSL to construct terms without touching De Bruijn indices.

e.g. if given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this:

runNames [] $ do -- open binds t and u to computations that know how to weaken themselves in -- an extended context

t,u: <- mapM open [t,u]

- lam gives the illusion of HOAS by providing f as a computation
- It also extends the internal context with the name "f", so that
- t and u will get weakened in the body.
- Then we finish the job using the (@) combinator from Agda.TypeChecking.Primitive

lam "f" $ f -> f @ t @ u

Documentation

newtype NamesT m a Source #

Constructors

NamesT
Fields unName :: ReaderT Names m a

Instances

MonadTrans NamesT Source #
Instance details Defined in Agda.TypeChecking.Names Methods lift :: Monad m => m a -> NamesT m a Source #
MonadState s m => MonadState s (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods get :: NamesT m s Source # put :: s -> NamesT m () Source # state :: (s -> (a, s)) -> NamesT m a Source #
Monad m => Monad (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods (>>=) :: NamesT m a -> (a -> NamesT m b) -> NamesT m b Source # (>>) :: NamesT m a -> NamesT m b -> NamesT m b Source # return :: a -> NamesT m a Source # fail :: String -> NamesT m a Source #
Functor m => Functor (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods fmap :: (a -> b) -> NamesT m a -> NamesT m b Source # (<$) :: a -> NamesT m b -> NamesT m a Source #
MonadFail m => MonadFail (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods fail :: String -> NamesT m a Source #
Applicative m => Applicative (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods pure :: a -> NamesT m a Source # (<>) :: NamesT m (a -> b) -> NamesT m a -> NamesT m b Source # liftA2 :: (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c Source # (>) :: NamesT m a -> NamesT m b -> NamesT m b Source # (<*) :: NamesT m a -> NamesT m b -> NamesT m a Source #
MonadIO m => MonadIO (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods liftIO :: IO a -> NamesT m a Source #
MonadTCM m => MonadTCM (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods liftTCM :: TCM a -> NamesT m a Source #
MonadTCState m => MonadTCState (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods getTC :: NamesT m TCState Source # putTC :: TCState -> NamesT m () Source # modifyTC :: (TCState -> TCState) -> NamesT m () Source #
MonadTCEnv m => MonadTCEnv (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods askTC :: NamesT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a Source #
MonadReduce m => MonadReduce (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods liftReduce :: ReduceM a -> NamesT m a Source #
HasOptions m => HasOptions (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods pragmaOptions :: NamesT m PragmaOptions Source # commandLineOptions :: NamesT m CommandLineOptions Source #
ReadTCState m => ReadTCState (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods getTCState :: NamesT m TCState Source # withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a Source #
MonadDebug m => MonadDebug (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods displayDebugMessage :: Int -> String -> NamesT m () Source # traceDebugMessage :: Int -> String -> NamesT m a -> NamesT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> NamesT m String Source #
HasBuiltins m => HasBuiltins (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #

type Names = [String] Source #

runNamesT :: Names -> NamesT m a -> m a Source #

runNames :: Names -> NamesT Identity a -> a Source #

currentCxt :: Monad m => NamesT m Names Source #

cxtSubst :: Monad m => Names -> NamesT m (Substitution' a) Source #

inCxt :: (Monad m, Subst t a) => Names -> a -> NamesT m a Source #

cl' :: Applicative m => a -> NamesT m a Source #

cl :: Monad m => m a -> NamesT m a Source #

open :: (Monad m, Subst t a) => a -> NamesT m (NamesT m a) Source #

bind' :: (Monad m, Subst t' b, DeBruijn b, Subst t a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a Source #

bind :: (Monad m, Subst t' b, DeBruijn b, Subst t a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a) Source #

glam :: Monad m => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #

glamN :: (Functor m, Monad m) => [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term Source #

lam :: Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #

ilam :: Monad m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #