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

7 types
25 values

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]

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)

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

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

Closed terms

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

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

Open terms in the current context.

typetype 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.

valuebind

:: Monad 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.

valuebind'

:: Monad 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.

3 declarations

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.

16 declarations

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

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]