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

Unbound.Generics.LocallyNameless.Rec

Description

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

Synopsis

newtype Rec p = Rec p
rec :: Alpha p => p -> Rec p
unrec :: Alpha p => Rec p -> p
newtype TRec p = TRec (Bind (Rec p) ())

Documentation

newtype Rec p Source #

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.

Constructors

Rec p

Instances

Instances details

Subst c p => Subst c (Rec p) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

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

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

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

Generic (Rec p) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Associated Types

type Rep (Rec p)
Instance details 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) Source #

Instance details

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

rnf :: Rec p -> () #

Eq p => Eq (Rec p) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

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

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

Alpha p => Alpha (Rec p) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Methods

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

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

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

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

isPat :: Rec p -> DisjointSet AnyName Source #

isTerm :: Rec p -> All Source #

isEmbed :: Rec p -> Bool Source #

nthPatFind :: Rec p -> NthPatFind Source #

namePatFind :: Rec p -> NamePatFind Source #

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

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

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

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

type Rep (Rec p) Source #

Instance details

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 Source #

Constructor for recursive patterns.

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

Destructor for recursive patterns.

newtype TRec p Source #

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

Instances details

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

Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

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

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

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

Generic (TRec p) Source #

Instance details

Defined in Unbound.Generics.LocallyNameless.Rec

Associated Types

type Rep (TRec p)
Instance details 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) ()))))