unbound-generics-0.3.3: Support for programming with names and binders using GHC Generics

Copyright(c) 2014 Aleksey Kliger
LicenseBSD3 (See LICENSE)
MaintainerAleksey Kliger
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010
ExtensionsDeriveGeneric

Unbound.Generics.LocallyNameless.Bind

Contents

Description

The fundamental binding form. The type Bind p t allows you to place a pattern p in a term t such that the names in the pattern scope over the term. Use bind and unbind and lunbind to work with Bind p t

Synopsis

Name binding

data Bind p t Source #

A term of type Bind p t is a term that binds the free variable occurrences of the variables in pattern p in the term t. In the overall term, those variables are now bound. See also bind and unbind and lunbind

Constructors

B p t 

Instances

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) Source # 

Methods

isvar :: Bind a b -> Maybe (SubstName (Bind a b) c) Source #

isCoerceVar :: Bind a b -> Maybe (SubstCoerce (Bind a b) c) Source #

subst :: Name c -> c -> Bind a b -> Bind a b Source #

substs :: [(Name c, c)] -> Bind a b -> Bind a b Source #

(Show p, Show t) => Show (Bind p t) Source # 

Methods

showsPrec :: Int -> Bind p t -> ShowS #

show :: Bind p t -> String #

showList :: [Bind p t] -> ShowS #

Generic (Bind p t) Source # 

Associated Types

type Rep (Bind p t) :: * -> * #

Methods

from :: Bind p t -> Rep (Bind p t) x #

to :: Rep (Bind p t) x -> Bind p t #

(NFData p, NFData t) => NFData (Bind p t) Source # 

Methods

rnf :: Bind p t -> () #

(Alpha p, Alpha t) => Alpha (Bind p t) Source # 

Methods

aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool Source #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t) Source #

close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t Source #

open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t Source #

isPat :: Bind p t -> DisjointSet AnyName Source #

isTerm :: Bind p t -> All Source #

isEmbed :: Bind p t -> Bool Source #

nthPatFind :: Bind p t -> NthPatFind Source #

namePatFind :: Bind p t -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t Source #

lfreshen' :: LFresh m => AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName) Source #

acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering Source #

type Rep (Bind p t) Source # 
type Rep (Bind p t) = D1 * (MetaData "Bind" "Unbound.Generics.LocallyNameless.Bind" "unbound-generics-0.3.3-Bd10VW6EVFQ8rThToStmHN" False) (C1 * (MetaCons "B" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * p)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))))