Agda.TypeChecking.Names

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

Constructors

NamesT

Fields

• unName :: ReaderT Names m a

Instances

MonadTrans NamesT

Defined in Agda.TypeChecking.Names

Methods

lift :: Monad m => m a -> NamesT m a

MonadState s m => MonadState s (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

get :: NamesT m s

put :: s -> NamesT m ()

state :: (s -> (a, s)) -> NamesT m a

MonadError e m => MonadError e (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

throwError :: e -> NamesT m a

catchError :: NamesT m a -> (e -> NamesT m a) -> NamesT m a

Monad m => Monad (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

(>>=) :: NamesT m a -> (a -> NamesT m b) -> NamesT m b

(>>) :: NamesT m a -> NamesT m b -> NamesT m b

return :: a -> NamesT m a

fail :: String -> NamesT m a

Functor m => Functor (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

fmap :: (a -> b) -> NamesT m a -> NamesT m b

(<$) :: a -> NamesT m b -> NamesT m a

MonadFail m => MonadFail (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

fail :: String -> NamesT m a

Applicative m => Applicative (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

pure :: a -> NamesT m a

(<*>) :: NamesT m (a -> b) -> NamesT m a -> NamesT m b

liftA2 :: (a -> b -> c) -> NamesT m a -> NamesT m b -> NamesT m c

(*>) :: NamesT m a -> NamesT m b -> NamesT m b

(<*) :: NamesT m a -> NamesT m b -> NamesT m a

MonadIO m => MonadIO (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

liftIO :: IO a -> NamesT m a

MonadTCM m => MonadTCM (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

liftTCM :: TCM a -> NamesT m a

MonadTCState m => MonadTCState (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getTC :: NamesT m TCState

putTC :: TCState -> NamesT m ()

modifyTC :: (TCState -> TCState) -> NamesT m ()

MonadTCEnv m => MonadTCEnv (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

askTC :: NamesT m TCEnv

localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a

MonadReduce m => MonadReduce (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

liftReduce :: ReduceM a -> NamesT m a

HasOptions m => HasOptions (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

pragmaOptions :: NamesT m PragmaOptions

commandLineOptions :: NamesT m CommandLineOptions

ReadTCState m => ReadTCState (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState

locallyTCState :: Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b

withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a

MonadAddContext m => MonadAddContext (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a

addLetBinding' :: Name -> Term -> Dom Type -> NamesT m a -> NamesT m a

updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a

withFreshName :: Range -> ArgName -> (Name -> NamesT m a) -> NamesT m a

HasBuiltins m => HasBuiltins (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))

MonadDebug m => MonadDebug (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m ()

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m String

getVerbosity :: NamesT m Verbosity

isDebugPrinting :: NamesT m Bool

nowDebugPrinting :: NamesT m a -> NamesT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a

type Names = [String]

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

runNames :: Names -> NamesT Fail a -> a

currentCxt :: Monad m => NamesT m Names

cxtSubst :: MonadFail m => Names -> NamesT m (Substitution' a)

inCxt :: (MonadFail m, Subst t a) => Names -> a -> NamesT m a

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

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

open :: (MonadFail m, Subst t a) => a -> NamesT m (NamesT m a)

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

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

glam :: MonadFail m => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term

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

lam :: MonadFail m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term

ilam :: MonadFail m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term