ModuleAgda-2.8.0.2Haskell2010

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

Contents

Helpers to build lambda abstractions.
Combinators for n-ary binders.

Synopsis

newtype NamesT
type Names
value runNamesT
value runNames
value currentCxt
value cxtSubst
value inCxt
value cl'
value cl
value open
type Var
value bind
value bind'
value glam
value lam
value ilam
data AbsN
value toAbsN
value absAppN
type ArgVars
type Vars
value bindN
value bindNArg
type Vars1
value bindN1
value glamN
value applyN
value applyN'
value abstractN
value abstractT
value lamTel
value appTel

PackageAgda-2.8.0.2
Exports32
LanguageHaskell2010
LicenceMIT
SourceNames.hs

newtypenewtype NamesT (m :: Type -> Type) a

Constructors

NamesT
- unName :: ReaderT Names m a

Instances18MonadTrans, MonadError, MonadState, Monad, Functor, Applicative, …

MonadTrans NamesTDefined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadError e m => MonadError e (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadState s m => MonadState s (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Monad m => Monad (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Functor m => Functor (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Applicative m => Applicative (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadIO m => MonadIO (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
HasOptions m => HasOptions (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadReduce m => MonadReduce (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadTCEnv m => MonadTCEnv (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadTCM m => MonadTCM (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadTCState m => MonadTCState (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
ReadTCState m => ReadTCState (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
HasBuiltins m => HasBuiltins (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadAddContext m => MonadAddContext (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
MonadDebug m => MonadDebug (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
HasConstInfo m => HasConstInfo (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names

typetype Names = [String]

Source#

A list of variable names from a context.

valuerunNamesT :: Names -> NamesT m a -> m a

valuerunNames :: Names -> NamesT Identity a -> a

valuecurrentCxt :: Monad m => NamesT m Names

valuecxtSubst :: Monad m => Names -> NamesT m (Substitution' a)

Source#

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

Precondition Γ is not a subcontext of the current one.

valueinCxt :: (Monad m, Subst a) => Names -> a -> NamesT m a

Source#

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

Fails whenever cxtSubst Γ would.

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

Source#

Closed terms

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

valueopen :: (Monad m, Subst a) => a -> NamesT m (NamesT m a)

Source#

Open terms in the current context.

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

Source#

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.

valuebind

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

Source#

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.

valuebind'

:: Monad m
=> ArgName
-> (forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a
-> NamesT m a

Source#

Like bind but returns a bare term.

Helpers to build lambda abstractions.

valueglam

:: Monad m
=> ArgInfo
-> ArgName
-> NamesT m Term -> NamesT m Term
-> NamesT m Term

valuelam

:: Monad m
=> ArgName
-> NamesT m Term -> NamesT m Term
-> NamesT m Term

valueilam

:: Monad m
=> ArgName
-> NamesT m Term -> NamesT m Term
-> NamesT m Term

Combinators for n-ary binders.

datadata AbsN a

Constructors

AbsN
- absNName :: [ArgName]
- unAbsN :: a

Instances5Functor, Foldable, Traversable, Subst, SubstArg

Functor AbsNDefined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Foldable AbsNDefined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Traversable AbsNDefined in Agda-2.8.0.2 · Agda.TypeChecking.Names
Subst a => Subst (AbsN a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
type SubstArg (AbsN a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Names

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

Source#

Will crash on NoAbs

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

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

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

valuebindN :: Monad m => [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a)

valuebindNArg

:: Monad m
=> [Arg ArgName]
-> ArgVars m -> NamesT m a
-> NamesT m (AbsN a)

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

valuebindN1

:: Monad m
=> List1 ArgName
-> Vars1 m -> NamesT m a
-> NamesT m (AbsN a)

valueglamN

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

valueapplyN

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

valueapplyN'

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

valueabstractN

:: (Monad m, Abstract a)
=> NamesT m Telescope
-> Vars m -> NamesT m a
-> NamesT m a

valueabstractT

:: (Monad m, Abstract a)
=> String
-> NamesT m Type
-> Var m -> NamesT m a
-> NamesT m a

valuelamTel :: Monad m => NamesT m (Abs [Term]) -> NamesT m [Term]

valueappTel :: Monad m => NamesT m [Term] -> NamesT m Term -> NamesT m [Term]