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

Instances details

MonadTrans NamesT Source #
Instance details Defined in Agda.TypeChecking.Names Methods lift :: Monad m => 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 #
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 #
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 #
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 #
MonadFail m => MonadFail (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods fail :: String -> 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 #
MonadIO m => MonadIO (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods liftIO :: IO a -> NamesT m a #
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 # locallyTCState :: Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b Source # withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a Source #
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 #
HasBuiltins m => HasBuiltins (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #
MonadDebug m => MonadDebug (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m () Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source # formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m String Source # getVerbosity :: NamesT m Verbosity Source # isDebugPrinting :: NamesT m Bool Source # nowDebugPrinting :: NamesT m a -> NamesT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source #

type Names = [String] Source #

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

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

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

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

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

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

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

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

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

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

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