Unbound.Generics.LocallyNameless.Rec

The pattern Rec p binds the names in p like p itself would, but additionally, the names in p are scope over p.

The term TRec p is shorthand for Bind (Rec p) ()

Documentation

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)

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

Eq p => Eq (Rec p)

Methods

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

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

Show a => Show (Rec a)

Methods

showsPrec :: Int -> Rec a -> ShowS

show :: Rec a -> String

showList :: [Rec a] -> ShowS

Generic (Rec p)

Associated Types

type Rep (Rec p) :: * -> *

Methods

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

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

NFData p => NFData (Rec p)

Methods

rnf :: Rec p -> ()

Alpha p => Alpha (Rec p)

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)

type Rep (Rec p) = D1 * (MetaData "Rec" "Unbound.Generics.LocallyNameless.Rec" "unbound-generics-0.3.3-Bd10VW6EVFQ8rThToStmHN" True) (C1 * (MetaCons "Rec" PrefixI False) (S1 * (MetaSel (Nothing 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)

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

Show a => Show (TRec a)

Methods

showsPrec :: Int -> TRec a -> ShowS

show :: TRec a -> String

showList :: [TRec a] -> ShowS

Generic (TRec p)

Associated Types

type Rep (TRec p) :: * -> *

Methods

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

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

Alpha p => Alpha (TRec p)

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)

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