Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Instances

Instances details
MonadTrans NamesT Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

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

MonadError e m => MonadError e (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

throwError :: e -> NamesT m a

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

MonadState s m => MonadState s (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

get :: NamesT m s

put :: s -> NamesT m ()

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

HasOptions m => HasOptions (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadReduce m => MonadReduce (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftReduce :: ReduceM a -> NamesT m a 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 #

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

ReadTCState m => ReadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState Source #

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

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

HasBuiltins m => HasBuiltins (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadAddContext m => MonadAddContext (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

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

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

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

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

MonadDebug m => MonadDebug (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

HasConstInfo m => HasConstInfo (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadFail m => MonadFail (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

fail :: String -> NamesT m a #

MonadIO m => MonadIO (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftIO :: IO a -> NamesT m a #

Applicative m => Applicative (NamesT m) Source # 
Instance details

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 #

Functor m => Functor (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

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

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

Monad m => Monad (NamesT m) Source # 
Instance details

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 #

type Names = [String] Source #

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

inCxt :: (MonadFail m, Subst 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 :: (MonadFail m, Subst a) => a -> NamesT m (NamesT m a) Source #

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

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