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

Copyright	(c) 2014 Aleksey Kliger
License	BSD3 (See LICENSE)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	None
Language	Haskell2010
Extensions	DeriveGeneric

Unbound.Generics.LocallyNameless.Bind

Contents

Name binding

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

data Bind p t = B p t

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

Instances details

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

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 #

substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b Source #

Generic (Bind p t) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Associated Types

type Rep (Bind p t)

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

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

Methods

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

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

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

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

show :: Bind p t -> String #

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

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

rnf :: Bind p t -> () #

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

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 #

Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

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