Copyright	(c) 2015 Aleksey Kliger
License	BSD3 (See LICENSE)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	None
Language	Haskell2010
Extensions	MonoLocalBinds TypeFamilies KindSignatures ExplicitNamespaces

Unbound.Generics.LocallyNameless.Shift

Description

The pattern Shift e shifts the scope of the embedded term in e one level outwards.

Synopsis

newtype Shift e = Shift e

Documentation

newtype Shift e Source #

The type Shift e is an embedding pattern that shifts the scope of the free variables of the embedded term Embedded e up by one level.

Constructors

Shift e

Instances

Instances details

Functor Shift Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

fmap :: (a -> b) -> Shift a -> Shift b #

(<$) :: a -> Shift b -> Shift a #

Subst c e => Subst c (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Shift e -> Maybe (SubstName (Shift e) c) Source #

isCoerceVar :: Shift e -> Maybe (SubstCoerce (Shift e) c) Source #

subst :: Name c -> c -> Shift e -> Shift e Source #

substs :: [(Name c, c)] -> Shift e -> Shift e Source #

substBvs :: AlphaCtx -> [c] -> Shift e -> Shift e Source #

Show e => Show (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

showsPrec :: Int -> Shift e -> ShowS #

show :: Shift e -> String #

showList :: [Shift e] -> ShowS #

NFData e => NFData (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

rnf :: Shift e -> () #

Alpha e => Alpha (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

aeq' :: AlphaCtx -> Shift e -> Shift e -> Bool Source #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Shift e -> f (Shift e) Source #

close :: AlphaCtx -> NamePatFind -> Shift e -> Shift e Source #

open :: AlphaCtx -> NthPatFind -> Shift e -> Shift e Source #

isPat :: Shift e -> DisjointSet AnyName Source #

isTerm :: Shift e -> All Source #

isEmbed :: Shift e -> Bool Source #

nthPatFind :: Shift e -> NthPatFind Source #

namePatFind :: Shift e -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> Shift e -> Shift e Source #

lfreshen' :: LFresh m => AlphaCtx -> Shift e -> (Shift e -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Shift e -> m (Shift e, Perm AnyName) Source #

acompare' :: AlphaCtx -> Shift e -> Shift e -> Ordering Source #

IsEmbed e => IsEmbed (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

Associated Types

type Embedded (Shift e)
Instance details 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)) Source #

type Embedded (Shift e) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Shift

type Embedded (Shift e) = Embedded e