Agda.TypeChecking.Names

EDSL to construct terms without touching De Bruijn indices.

e.g. 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.
• - We apply f with the (@) combinator from Agda.TypeChecking.Primitive.

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

Documentation

newtype NamesT (m :: Type -> Type) 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

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

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

HasOptions m => HasOptions (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

pragmaOptions :: NamesT m PragmaOptions

commandLineOptions :: NamesT m CommandLineOptions

MonadReduce m => MonadReduce (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

liftReduce :: ReduceM a -> NamesT m a

MonadTCEnv m => MonadTCEnv (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

askTC :: NamesT m TCEnv

localTC :: (TCEnv -> TCEnv) -> NamesT m 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 ()

ReadTCState m => ReadTCState (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState

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

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

HasBuiltins m => HasBuiltins (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

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

MonadAddContext m => MonadAddContext (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

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

addLetBinding' :: Origin -> 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

MonadDebug m => MonadDebug (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

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

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

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

getVerbosity :: NamesT m Verbosity

getProfileOptions :: NamesT m ProfileOptions

isDebugPrinting :: NamesT m Bool

nowDebugPrinting :: NamesT m a -> NamesT m a

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m)

Defined in Agda.TypeChecking.Names

HasConstInfo m => HasConstInfo (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getConstInfo :: QName -> NamesT m Definition

getConstInfo' :: QName -> NamesT m (Either SigError Definition)

getRewriteRulesFor :: QName -> NamesT m RewriteRules

MonadFail m => MonadFail (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

fail :: String -> NamesT m a

MonadIO m => MonadIO (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

liftIO :: IO a -> 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

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

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

type Names = [String]

A list of variable names from a context.

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

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

currentCxt :: forall (m :: Type -> Type). Monad m => NamesT m Names

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

cxtSubst Γ returns the substitution needed to go from Γ to the current context.

Fails if Γ is not a subcontext of the current one.

inCxt :: forall (m :: Type -> Type) a. (MonadFail m, Subst a) => Names -> a -> NamesT m a

inCxt Γ t takes a t in context Γ and produce an action that will return t weakened to the current context.

Fails whenever cxtSubst Γ would.

cl' :: forall (m :: Type -> Type) a. Applicative m => a -> NamesT m a

Closed terms

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

open :: forall (m :: Type -> Type) a. (MonadFail m, Subst a) => a -> NamesT m (NamesT m a)

Open terms in the current context.

type Var (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => NamesT m b

Monadic actions standing for variables.

b is quantified over so the same variable can be used e.g. both as a pattern and as an expression.

bind :: forall (m :: Type -> Type) a. MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m (Abs a)

bind n f provides f with a fresh variable, which can be used in any extended context.

Returns an Abs which binds the extra variable.

bind' :: forall (m :: Type -> Type) a. MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a

Like bind but returns a bare term.

Helpers to build lambda abstractions.

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

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

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

Combinators for n-ary binders.

data AbsN a

Constructors

AbsN

Fields

• absNName :: [ArgName]
• unAbsN :: a

Instances

Foldable AbsN

Defined in Agda.TypeChecking.Names

Methods

fold :: Monoid m => AbsN m -> m

foldMap :: Monoid m => (a -> m) -> AbsN a -> m

foldMap' :: Monoid m => (a -> m) -> AbsN a -> m

foldr :: (a -> b -> b) -> b -> AbsN a -> b

foldr' :: (a -> b -> b) -> b -> AbsN a -> b

foldl :: (b -> a -> b) -> b -> AbsN a -> b

foldl' :: (b -> a -> b) -> b -> AbsN a -> b

foldr1 :: (a -> a -> a) -> AbsN a -> a

foldl1 :: (a -> a -> a) -> AbsN a -> a

toList :: AbsN a -> [a]

null :: AbsN a -> Bool

length :: AbsN a -> Int

elem :: Eq a => a -> AbsN a -> Bool

maximum :: Ord a => AbsN a -> a

minimum :: Ord a => AbsN a -> a

sum :: Num a => AbsN a -> a

product :: Num a => AbsN a -> a

Traversable AbsN

Defined in Agda.TypeChecking.Names

Methods

traverse :: Applicative f => (a -> f b) -> AbsN a -> f (AbsN b)

sequenceA :: Applicative f => AbsN (f a) -> f (AbsN a)

mapM :: Monad m => (a -> m b) -> AbsN a -> m (AbsN b)

sequence :: Monad m => AbsN (m a) -> m (AbsN a)

Functor AbsN

Defined in Agda.TypeChecking.Names

Methods

fmap :: (a -> b) -> AbsN a -> AbsN b

(<$) :: a -> AbsN b -> AbsN a

Subst a => Subst (AbsN a)

Defined in Agda.TypeChecking.Names

Associated Types

type SubstArg (AbsN a)

Defined in Agda.TypeChecking.Names

type SubstArg (AbsN a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a

type SubstArg (AbsN a)

Defined in Agda.TypeChecking.Names

type SubstArg (AbsN a) = SubstArg a

toAbsN :: Abs (AbsN a) -> AbsN a

Will crash on NoAbs

absAppN :: Subst a => AbsN a -> [SubstArg a] -> a

type ArgVars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m (Arg b)]

type Vars (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => [NamesT m b]

bindN :: forall (m :: Type -> Type) a. MonadFail m => [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)

bindNArg :: forall (m :: Type -> Type) a. MonadFail m => [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a)

type Vars1 (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => List1 (NamesT m b)

bindN1 :: forall (m :: Type -> Type) a. MonadFail m => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a)

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

applyN :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a

applyN' :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a

abstractN :: forall (m :: Type -> Type) a. (MonadFail m, Abstract a) => NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a

abstractT :: forall (m :: Type -> Type) a. (MonadFail m, Abstract a) => String -> NamesT m Type -> (Var m -> NamesT m a) -> NamesT m a

lamTel :: forall (m :: Type -> Type). Monad m => NamesT m (Abs [Term]) -> NamesT m [Term]

appTel :: forall (m :: Type -> Type). Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term]