Unbound.Generics.LocallyNameless.Operations

Operations on terms and patterns that contain names.

Equivalence, free variables, freshness

aeq :: Alpha a => a -> a -> Bool

aeq t1 t2 returns True iff t1 and t2 are alpha-equivalent terms.

acompare :: Alpha a => a -> a -> Ordering

An alpha-respecting total order on terms involving binders.

fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a

fvAny returns a fold over any names in a term a.

  fvAny :: Alpha a => Fold a AnyName

fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a

fv returns the free b variables of term a.

 fv :: (Alpha a, Typeable b) => Fold a (Name b)

freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)

Freshen a pattern by replacing all old binding Names with new fresh Names, returning a new pattern and a Perm Name specifying how Names were replaced.

lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b

"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.

swaps :: Alpha t => Perm AnyName -> t -> t

Apply the given permutation of variable names to the given term.

Binding, unbinding

data Bind p t

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

Instances

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

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

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

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

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

Generic (Bind p t)

Defined in Unbound.Generics.LocallyNameless.Bind

Associated Types

type Rep (Bind p t)

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)

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)

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

rnf :: Bind p t -> ()

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

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

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

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

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

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

isPat :: Bind p t -> DisjointSet AnyName

isTerm :: Bind p t -> All

isEmbed :: Bind p t -> Bool

nthPatFind :: Bind p t -> NthPatFind

namePatFind :: Bind p t -> NamePatFind

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

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

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

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

type Rep (Bind p t)

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)))

bind :: (Alpha p, Alpha t) => p -> t -> Bind p t

bind p t closes over the variables of pattern p in the term t

unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)

unbind b lets you descend beneath a binder b :: Bind p t by returning the pair of the pattern p and the term t where the variables in the pattern have been made globally fresh with respect to the freshness monad m.

lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c

lunbind opens a binding in an LFresh monad, ensuring that the names chosen for the binders are locally fresh. The components of the binding are passed to a continuation, and the resulting monadic action is run in a context extended to avoid choosing new names which are the same as the ones chosen for this binding.

For more information, see the documentation for the LFresh type class.

unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))

Simultaneously unbind two patterns in two terms, returning Nothing if the two patterns don't bind the same number of variables.

lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c

Simultaneously lunbind two patterns in two terms in the LFresh monad, passing Just (p1, t1, p2, t2) to the continuation such that the patterns are permuted such that they introduce the same free names, or Nothing if the number of variables differs.

unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2)

Simultaneously unbind two patterns in two terms, returning mzero if the patterns don't bind the same number of variables.

Rebinding, embedding

data Rebind p1 p2

Rebind p1 p2 is a pattern that binds the names of p1 and p2, and additionally brings the names of p1 into scope over p2.

This may be used, for example, to faithfully represent Scheme's let* binding form, defined by:

 (let* () body) ≙ body
 (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))

using the following AST:

type Var = Name Expr
data Lets = EmptyLs
          | ConsLs (Rebind (Var, Embed Expr) Lets)
data Expr = ...
          | LetStar (Bind Lets Expr)
          | ...

Instances

(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Rebind p1 p2 -> Maybe (SubstName (Rebind p1 p2) c)

isCoerceVar :: Rebind p1 p2 -> Maybe (SubstCoerce (Rebind p1 p2) c)

subst :: Name c -> c -> Rebind p1 p2 -> Rebind p1 p2

substs :: [(Name c, c)] -> Rebind p1 p2 -> Rebind p1 p2

substBvs :: AlphaCtx -> [c] -> Rebind p1 p2 -> Rebind p1 p2

Generic (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

Associated Types

type Rep (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

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

Methods

from :: Rebind p1 p2 -> Rep (Rebind p1 p2) x

to :: Rep (Rebind p1 p2) x -> Rebind p1 p2

(Show p1, Show p2) => Show (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

showsPrec :: Int -> Rebind p1 p2 -> ShowS

show :: Rebind p1 p2 -> String

showList :: [Rebind p1 p2] -> ShowS

(NFData p1, NFData p2) => NFData (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

rnf :: Rebind p1 p2 -> ()

(Eq p1, Eq p2) => Eq (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

(==) :: Rebind p1 p2 -> Rebind p1 p2 -> Bool

(/=) :: Rebind p1 p2 -> Rebind p1 p2 -> Bool

(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

aeq' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rebind p1 p2 -> f (Rebind p1 p2)

close :: AlphaCtx -> NamePatFind -> Rebind p1 p2 -> Rebind p1 p2

open :: AlphaCtx -> NthPatFind -> Rebind p1 p2 -> Rebind p1 p2

isPat :: Rebind p1 p2 -> DisjointSet AnyName

isTerm :: Rebind p1 p2 -> All

isEmbed :: Rebind p1 p2 -> Bool

nthPatFind :: Rebind p1 p2 -> NthPatFind

namePatFind :: Rebind p1 p2 -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p1 p2 -> Rebind p1 p2

lfreshen' :: LFresh m => AlphaCtx -> Rebind p1 p2 -> (Rebind p1 p2 -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Rebind p1 p2 -> m (Rebind p1 p2, Perm AnyName)

acompare' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Ordering

type Rep (Rebind p1 p2)

Defined in Unbound.Generics.LocallyNameless.Rebind

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

rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2

rebind p1 p2 is a smart constructor for Rebind. It captures the variables of pattern p1 that occur within p2 in addition to providing binding occurrences for all the variables of p1 and p2

unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)

unrebind p is the elimination form for Rebind. It is not monadic (unlike unbind) because a Rebind pattern can only occur somewhere in a pattern position of a Bind, and therefore unbind must have already been called and all names apropriately freshened.

newtype Embed t

Embed allows for terms to be embedded within patterns. Such embedded terms do not bind names along with the rest of the pattern. For examples, see the tutorial or examples directories.

If t is a term type, then Embed t is a pattern type.

Embed is not abstract since it involves no binding, and hence it is safe to manipulate directly. To create and destruct Embed terms, you may use the Embed constructor directly. (You may also use the functions embed and unembed, which additionally can construct or destruct any number of enclosing Shifts at the same time.)

Constructors

Embed t

Instances

Subst c a => Subst c (Embed a)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Embed a -> Maybe (SubstName (Embed a) c)

isCoerceVar :: Embed a -> Maybe (SubstCoerce (Embed a) c)

subst :: Name c -> c -> Embed a -> Embed a

substs :: [(Name c, c)] -> Embed a -> Embed a

substBvs :: AlphaCtx -> [c] -> Embed a -> Embed a

Generic (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Associated Types

type Rep (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

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

Methods

from :: Embed t -> Rep (Embed t) x

to :: Rep (Embed t) x -> Embed t

Show a => Show (Embed a)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

showsPrec :: Int -> Embed a -> ShowS

show :: Embed a -> String

showList :: [Embed a] -> ShowS

NFData t => NFData (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

rnf :: Embed t -> ()

Eq t => Eq (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

(==) :: Embed t -> Embed t -> Bool

(/=) :: Embed t -> Embed t -> Bool

Ord t => Ord (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

compare :: Embed t -> Embed t -> Ordering

(<) :: Embed t -> Embed t -> Bool

(<=) :: Embed t -> Embed t -> Bool

(>) :: Embed t -> Embed t -> Bool

(>=) :: Embed t -> Embed t -> Bool

max :: Embed t -> Embed t -> Embed t

min :: Embed t -> Embed t -> Embed t

Alpha t => Alpha (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Methods

aeq' :: AlphaCtx -> Embed t -> Embed t -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Embed t -> f (Embed t)

close :: AlphaCtx -> NamePatFind -> Embed t -> Embed t

open :: AlphaCtx -> NthPatFind -> Embed t -> Embed t

isPat :: Embed t -> DisjointSet AnyName

isTerm :: Embed t -> All

isEmbed :: Embed t -> Bool

nthPatFind :: Embed t -> NthPatFind

namePatFind :: Embed t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Embed t -> Embed t

lfreshen' :: LFresh m => AlphaCtx -> Embed t -> (Embed t -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Embed t -> m (Embed t, Perm AnyName)

acompare' :: AlphaCtx -> Embed t -> Embed t -> Ordering

IsEmbed (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Associated Types

type Embedded (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

type Embedded (Embed t) = t

Methods

embedded :: (Profunctor p, Functor f) => p (Embedded (Embed t)) (f (Embedded (Embed t))) -> p (Embed t) (f (Embed t))

type Rep (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

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

type Embedded (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

type Embedded (Embed t) = t

class IsEmbed e where

Associated Types

type Embedded e

The term type embedded in the embedding e

Methods

embedded :: (Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)

Insert or extract the embedded term. If you're not using the lens library, see embed and unembed otherwise embedded is an isomorphism that you can use with lens. embedded :: Iso' (Embedded e) e

Instances

IsEmbed (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

Associated Types

type Embedded (Embed t)

Defined in Unbound.Generics.LocallyNameless.Embed

type Embedded (Embed t) = t

Methods

embedded :: (Profunctor p, Functor f) => p (Embedded (Embed t)) (f (Embedded (Embed t))) -> p (Embed t) (f (Embed t))

IsEmbed e => IsEmbed (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Associated Types

type Embedded (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

type Embedded (Shift e) = Embedded e

Methods

embedded :: (Profunctor p, Functor f) => p (Embedded (Shift e)) (f (Embedded (Shift e))) -> p (Shift e) (f (Shift e))

embed :: IsEmbed e => Embedded e -> e

Embeds a term in an Embed, or an Embed under some number of Shift constructors.

unembed :: IsEmbed e => e -> Embedded e

unembed p extracts the term embedded in the pattern p.

Recursive bindings

data Rec p

If p is a pattern type, then Rec p is also a pattern type, which is recursive in the sense that p may bind names in terms embedded within itself. Useful for encoding e.g. lectrec and Agda's dot notation.

Instances

Subst c p => Subst c (Rec p)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Rec p -> Maybe (SubstName (Rec p) c)

isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) c)

subst :: Name c -> c -> Rec p -> Rec p

substs :: [(Name c, c)] -> Rec p -> Rec p

substBvs :: AlphaCtx -> [c] -> Rec p -> Rec p

Generic (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Associated Types

type Rep (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

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

Methods

from :: Rec p -> Rep (Rec p) x

to :: Rep (Rec p) x -> Rec p

Show a => Show (Rec a)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

showsPrec :: Int -> Rec a -> ShowS

show :: Rec a -> String

showList :: [Rec a] -> ShowS

NFData p => NFData (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

rnf :: Rec p -> ()

Eq p => Eq (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

(==) :: Rec p -> Rec p -> Bool

(/=) :: Rec p -> Rec p -> Bool

Alpha p => Alpha (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rec p -> f (Rec p)

close :: AlphaCtx -> NamePatFind -> Rec p -> Rec p

open :: AlphaCtx -> NthPatFind -> Rec p -> Rec p

isPat :: Rec p -> DisjointSet AnyName

isTerm :: Rec p -> All

isEmbed :: Rec p -> Bool

nthPatFind :: Rec p -> NthPatFind

namePatFind :: Rec p -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p

lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName)

acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering

type Rep (Rec p)

Defined in Unbound.Generics.LocallyNameless.Rec

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

rec :: Alpha p => p -> Rec p

Constructor for recursive patterns.

unrec :: Alpha p => Rec p -> p

Destructor for recursive patterns.

newtype TRec p

TRec is a standalone variant of Rec: the only difference is that whereas Rec p is a pattern type, TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Note that TRec corresponds to Pottier's abstraction construct from alpha-Caml. In this context, Embed t corresponds to alpha-Caml's inner t, and Shift (Embed t) corresponds to alpha-Caml's outer t.

Constructors

TRec (Bind (Rec p) ())

Instances

(Alpha p, Subst c p) => Subst c (TRec p)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: TRec p -> Maybe (SubstName (TRec p) c)

isCoerceVar :: TRec p -> Maybe (SubstCoerce (TRec p) c)

subst :: Name c -> c -> TRec p -> TRec p

substs :: [(Name c, c)] -> TRec p -> TRec p

substBvs :: AlphaCtx -> [c] -> TRec p -> TRec p

Generic (TRec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Associated Types

type Rep (TRec p)

Defined in Unbound.Generics.LocallyNameless.Rec

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

Methods

from :: TRec p -> Rep (TRec p) x

to :: Rep (TRec p) x -> TRec p

Show a => Show (TRec a)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

showsPrec :: Int -> TRec a -> ShowS

show :: TRec a -> String

showList :: [TRec a] -> ShowS

Alpha p => Alpha (TRec p)

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

aeq' :: AlphaCtx -> TRec p -> TRec p -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> TRec p -> f (TRec p)

close :: AlphaCtx -> NamePatFind -> TRec p -> TRec p

open :: AlphaCtx -> NthPatFind -> TRec p -> TRec p

isPat :: TRec p -> DisjointSet AnyName

isTerm :: TRec p -> All

isEmbed :: TRec p -> Bool

nthPatFind :: TRec p -> NthPatFind

namePatFind :: TRec p -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> TRec p -> TRec p

lfreshen' :: LFresh m => AlphaCtx -> TRec p -> (TRec p -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> TRec p -> m (TRec p, Perm AnyName)

acompare' :: AlphaCtx -> TRec p -> TRec p -> Ordering

type Rep (TRec p)

Defined in Unbound.Generics.LocallyNameless.Rec

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

trec :: Alpha p => p -> TRec p

Constructor for recursive abstractions.

untrec :: (Alpha p, Fresh m) => TRec p -> m p

Destructor for recursive abstractions which picks globally fresh names for the binders.

luntrec :: (Alpha p, LFresh m) => TRec p -> m p

Destructor for recursive abstractions which picks locally fresh names for binders (see LFresh).

Opaque terms

data Ignore t

Ignores a term t for the purpose of alpha-equality and substitution

Instances

Subst a (Ignore b)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Ignore b -> Maybe (SubstName (Ignore b) a)

isCoerceVar :: Ignore b -> Maybe (SubstCoerce (Ignore b) a)

subst :: Name a -> a -> Ignore b -> Ignore b

substs :: [(Name a, a)] -> Ignore b -> Ignore b

substBvs :: AlphaCtx -> [a] -> Ignore b -> Ignore b

Generic (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

Associated Types

type Rep (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

type Rep (Ignore t) = D1 ('MetaData "Ignore" "Unbound.Generics.LocallyNameless.Ignore" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))

Methods

from :: Ignore t -> Rep (Ignore t) x

to :: Rep (Ignore t) x -> Ignore t

Show t => Show (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

showsPrec :: Int -> Ignore t -> ShowS

show :: Ignore t -> String

showList :: [Ignore t] -> ShowS

NFData t => NFData (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

rnf :: Ignore t -> ()

Show t => Alpha (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

aeq' :: AlphaCtx -> Ignore t -> Ignore t -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ignore t -> f (Ignore t)

close :: AlphaCtx -> NamePatFind -> Ignore t -> Ignore t

open :: AlphaCtx -> NthPatFind -> Ignore t -> Ignore t

isPat :: Ignore t -> DisjointSet AnyName

isTerm :: Ignore t -> All

isEmbed :: Ignore t -> Bool

nthPatFind :: Ignore t -> NthPatFind

namePatFind :: Ignore t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Ignore t -> Ignore t

lfreshen' :: LFresh m => AlphaCtx -> Ignore t -> (Ignore t -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Ignore t -> m (Ignore t, Perm AnyName)

acompare' :: AlphaCtx -> Ignore t -> Ignore t -> Ordering

type Rep (Ignore t)

Defined in Unbound.Generics.LocallyNameless.Ignore

type Rep (Ignore t) = D1 ('MetaData "Ignore" "Unbound.Generics.LocallyNameless.Ignore" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))

ignore :: t -> Ignore t

Constructor for ignoring a term for the purposes of alpha-equality and substs

unignore :: Ignore t -> t

Destructor for ignored terms