Unbound.Generics.LocallyNameless.Embed

The pattern Embed t contains a term t.

Documentation

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)

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

Eq t => Eq (Embed t)

Methods

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

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

Ord t => Ord (Embed t)

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

Show a => Show (Embed a)

Methods

showsPrec :: Int -> Embed a -> ShowS

show :: Embed a -> String

showList :: [Embed a] -> ShowS

Generic (Embed t)

Associated Types

type Rep (Embed t) :: * -> *

Methods

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

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

NFData t => NFData (Embed t)

Methods

rnf :: Embed t -> ()

Alpha t => Alpha (Embed t)

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)

Associated Types

type Embedded (Embed 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)

type Rep (Embed t) = D1 (MetaData "Embed" "Unbound.Generics.LocallyNameless.Embed" "unbound-generics-0.3.1-8vyzNZGjRzxHnWFlDb51nu" True) (C1 (MetaCons "Embed" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t)))

type Embedded (Embed t)

type Embedded (Embed t) = t

class IsEmbed e where

Minimal complete definition

embedded

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)

Associated Types

type Embedded (Embed 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)

Associated Types

type Embedded (Shift e) :: *

Methods

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