Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
andu
will get weakened in the body. - - We apply f with the (@) combinator from Agda.TypeChecking.Primitive.
Synopsis
- newtype NamesT (m :: Type -> Type) a = NamesT {}
- type Names = [String]
- 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)
- inCxt :: forall (m :: Type -> Type) a. (MonadFail m, Subst a) => Names -> a -> NamesT m a
- cl' :: forall (m :: Type -> Type) a. Applicative m => a -> NamesT m a
- cl :: Monad m => m a -> NamesT m a
- open :: forall (m :: Type -> Type) a. (MonadFail m, Subst a) => a -> NamesT m (NamesT m a)
- type Var (m :: Type -> Type) = forall b. (Subst b, DeBruijn b) => NamesT m b
- 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' :: forall (m :: Type -> Type) a. MonadFail m => ArgName -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a) -> NamesT m a
- 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
- data AbsN a = AbsN {}
- toAbsN :: Abs (AbsN a) -> AbsN a
- 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]
Documentation
newtype NamesT (m :: Type -> Type) a Source #
Instances
currentCxt :: forall (m :: Type -> Type). Monad m => NamesT m Names Source #
cxtSubst :: forall (m :: Type -> Type) a. MonadFail m => Names -> NamesT m (Substitution' a) Source #
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 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.
open :: forall (m :: Type -> Type) a. (MonadFail m, Subst a) => a -> NamesT m (NamesT m a) Source #
Open terms in the current context.
type 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.
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) 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.
bind' :: forall (m :: Type -> Type) a. MonadFail 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.
glam :: forall (m :: Type -> Type). MonadFail m => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #
lam :: forall (m :: Type -> Type). MonadFail m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #
ilam :: forall (m :: Type -> Type). MonadFail m => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term Source #
Combinators for n-ary binders.
Instances
Functor AbsN Source # | |
Foldable AbsN Source # | |
Defined in Agda.TypeChecking.Names 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 elem :: Eq a => a -> AbsN a -> Bool maximum :: Ord a => AbsN a -> a | |
Traversable AbsN Source # | |
Subst a => Subst (AbsN a) Source # | |
Defined in Agda.TypeChecking.Names applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a Source # | |
type SubstArg (AbsN a) Source # | |
Defined in Agda.TypeChecking.Names |
bindN :: forall (m :: Type -> Type) a. MonadFail m => [ArgName] -> (Vars m -> NamesT m a) -> NamesT m (AbsN a) Source #
bindNArg :: forall (m :: Type -> Type) a. MonadFail m => [Arg ArgName] -> (ArgVars m -> NamesT m a) -> NamesT m (AbsN a) Source #
bindN1 :: forall (m :: Type -> Type) a. MonadFail m => List1 ArgName -> (Vars1 m -> NamesT m a) -> NamesT m (AbsN a) Source #
glamN :: forall (m :: Type -> Type). (Functor m, MonadFail m) => [Arg ArgName] -> (NamesT m Args -> NamesT m Term) -> NamesT m Term Source #
applyN :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a Source #
applyN' :: forall (m :: Type -> Type) a. (Monad m, Subst a) => NamesT m (AbsN a) -> NamesT m [SubstArg a] -> NamesT m a Source #
abstractN :: forall (m :: Type -> Type) a. (MonadFail m, Abstract a) => NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a Source #