Unbound.LocallyNameless.Types

Special type combinators for specifying binding structure.

Documentation

data GenBind order card p t

Generic binding combinator for a pattern p within a term t. Flexible over the order and cardinality of the variables bound in the pattern

Constructors

B p t

Instances

(Rep order, Rep card, Rep p, Rep t, Sat (ctx p), Sat (ctx t)) => Rep1 ctx (GenBind order card p t)

Defined in Unbound.LocallyNameless.Types

Methods

rep1 :: R1 ctx (GenBind order card p t)

(Rep order, Rep card, Alpha p, Alpha t, Subst b p, Subst b t) => Subst b (GenBind order card p t)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: GenBind order card p t -> Maybe (SubstName (GenBind order card p t) b)

isCoerceVar :: GenBind order card p t -> Maybe (SubstCoerce (GenBind order card p t) b)

subst :: Name b -> b -> GenBind order card p t -> GenBind order card p t

substs :: [(Name b, b)] -> GenBind order card p t -> GenBind order card p t

substPat :: AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> GenBind order card p t -> GenBind order card p t

(Alpha a, Alpha b, Read a, Read b) => Read (Bind a b)

Defined in Unbound.LocallyNameless.Ops

Methods

readsPrec :: Int -> ReadS (Bind a b)

readList :: ReadS [Bind a b]

readPrec :: ReadPrec (Bind a b)

readListPrec :: ReadPrec [Bind a b]

(Show a, Show b) => Show (GenBind order card a b)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> GenBind order card a b -> ShowS

show :: GenBind order card a b -> String

showList :: [GenBind order card a b] -> ShowS

(Rep order, Rep card, Rep p, Rep t) => Rep (GenBind order card p t)

Defined in Unbound.LocallyNameless.Types

Methods

rep :: R (GenBind order card p t)

(Binary p, Binary t) => Binary (GenBind order card p t)

Defined in Unbound.LocallyNameless.Types

Methods

put :: GenBind order card p t -> Put

get :: Get (GenBind order card p t)

putList :: [GenBind order card p t] -> Put

(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t)

Defined in Unbound.LocallyNameless.Alpha

Methods

swaps' :: AlphaCtx -> Perm AnyName -> GenBind order card p t -> GenBind order card p t

fv' :: Collection f => AlphaCtx -> GenBind order card p t -> f AnyName

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

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

aeq' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Bool

acompare' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Ordering

close :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t

open :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t

isPat :: GenBind order card p t -> Maybe [AnyName]

isTerm :: GenBind order card p t -> Bool

isEmbed :: GenBind order card p t -> Bool

nthpatrec :: GenBind order card p t -> NthCont

findpatrec :: GenBind order card p t -> AnyName -> FindResult

type Bind p t = GenBind StrictOrder StrictCard p t

The most fundamental combinator for expressing binding structure is Bind. The term type Bind p t represents a pattern p paired with a term t, where names in p are bound within t.

Like Name, Bind is also abstract. You can create bindings using bind and take them apart with unbind and friends.

type SetBind p t = GenBind RelaxedOrder StrictCard p t

A variant of Bind where alpha-equivalence allows multiple variables bound in the same pattern to be reordered

type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t

A variant of Bind where alpha-equivalence allows multiple variables bound in the same pattern to be reordered, and allows the binding of unused variables For example, { a b c } . a b aeq { b a } . a b

data Rebind p1 p2

Rebind allows for nested bindings. If p1 and p2 are pattern types, then Rebind p1 p2 is also a pattern type, similar to the pattern type (p1,p2) except that p1 scopes over p2. That is, names within terms embedded in p2 may refer to binders in p1.

Constructors

R p1 p2

Instances

(Rep p1, Rep p2, Sat (ctx p1), Sat (ctx p2)) => Rep1 ctx (Rebind p1 p2)

Defined in Unbound.LocallyNameless.Types

Methods

rep1 :: R1 ctx (Rebind p1 p2)

(Alpha p, Alpha q, Subst b p, Subst b q) => Subst b (Rebind p q)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: Rebind p q -> Maybe (SubstName (Rebind p q) b)

isCoerceVar :: Rebind p q -> Maybe (SubstCoerce (Rebind p q) b)

subst :: Name b -> b -> Rebind p q -> Rebind p q

substs :: [(Name b, b)] -> Rebind p q -> Rebind p q

substPat :: AlphaCtx -> b -> Rebind p q -> Rebind p q

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Rebind p q -> Rebind p q

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

Compare for alpha-equality.

Defined in Unbound.LocallyNameless.Ops

Methods

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

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

(Show a, Show b) => Show (Rebind a b)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> Rebind a b -> ShowS

show :: Rebind a b -> String

showList :: [Rebind a b] -> ShowS

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

Defined in Unbound.LocallyNameless.Types

Methods

rep :: R (Rebind p1 p2)

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

Defined in Unbound.LocallyNameless.Types

Methods

put :: Rebind p1 p2 -> Put

get :: Get (Rebind p1 p2)

putList :: [Rebind p1 p2] -> Put

(Alpha p, Alpha q) => Alpha (Rebind p q)

Defined in Unbound.LocallyNameless.Alpha

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p q -> Rebind p q

fv' :: Collection f => AlphaCtx -> Rebind p q -> f AnyName

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

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

aeq' :: AlphaCtx -> Rebind p q -> Rebind p q -> Bool

acompare' :: AlphaCtx -> Rebind p q -> Rebind p q -> Ordering

close :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q

open :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q

isPat :: Rebind p q -> Maybe [AnyName]

isTerm :: Rebind p q -> Bool

isEmbed :: Rebind p q -> Bool

nthpatrec :: Rebind p q -> NthCont

findpatrec :: Rebind p q -> AnyName -> FindResult

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.

Constructors

Rec p

Instances

(Rep p, Sat (ctx p)) => Rep1 ctx (Rec p)

Defined in Unbound.LocallyNameless.Types

Methods

rep1 :: R1 ctx (Rec p)

(Alpha p, Subst b p) => Subst b (Rec p)

Defined in Unbound.LocallyNameless.Subst

Methods

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

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

subst :: Name b -> b -> Rec p -> Rec p

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

substPat :: AlphaCtx -> b -> Rec p -> Rec p

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Rec p -> Rec p

Show a => Show (Rec a)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> Rec a -> ShowS

show :: Rec a -> String

showList :: [Rec a] -> ShowS

Rep p => Rep (Rec p)

Defined in Unbound.LocallyNameless.Types

Methods

rep :: R (Rec p)

Alpha p => Alpha (Rec p)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

fv' :: Collection f => AlphaCtx -> Rec p -> f AnyName

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)

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

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

close :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p

open :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p

isPat :: Rec p -> Maybe [AnyName]

isTerm :: Rec p -> Bool

isEmbed :: Rec p -> Bool

nthpatrec :: Rec p -> NthCont

findpatrec :: Rec p -> AnyName -> FindResult

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

Show a => Show (TRec a)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> TRec a -> ShowS

show :: TRec a -> String

showList :: [TRec a] -> ShowS

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

(Rep t, Sat (ctx t)) => Rep1 ctx (Embed t)

Defined in Unbound.LocallyNameless.Types

Methods

rep1 :: R1 ctx (Embed t)

(Alpha t, Subst b t) => Subst b (Embed t)

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: Embed t -> Maybe (SubstName (Embed t) b)

isCoerceVar :: Embed t -> Maybe (SubstCoerce (Embed t) b)

subst :: Name b -> b -> Embed t -> Embed t

substs :: [(Name b, b)] -> Embed t -> Embed t

substPat :: AlphaCtx -> b -> Embed t -> Embed t

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Embed t -> Embed t

Eq t => Eq (Embed t)

Defined in Unbound.LocallyNameless.Types

Methods

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

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

Show a => Show (Embed a)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> Embed a -> ShowS

show :: Embed a -> String

showList :: [Embed a] -> ShowS

Rep t => Rep (Embed t)

Defined in Unbound.LocallyNameless.Types

Methods

rep :: R (Embed t)

Binary p => Binary (Embed p)

Defined in Unbound.LocallyNameless.Types

Methods

put :: Embed p -> Put

get :: Get (Embed p)

putList :: [Embed p] -> Put

IsEmbed (Embed t)

Defined in Unbound.LocallyNameless.Alpha

Associated Types

type Embedded (Embed t) :: *

Methods

embed :: Embedded (Embed t) -> Embed t

unembed :: Embed t -> Embedded (Embed t)

Alpha t => Alpha (Embed t)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

fv' :: Collection f => AlphaCtx -> Embed t -> f AnyName

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)

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

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

close :: Alpha b => AlphaCtx -> b -> Embed t -> Embed t

open :: Alpha b => AlphaCtx -> b -> Embed t -> Embed t

isPat :: Embed t -> Maybe [AnyName]

isTerm :: Embed t -> Bool

isEmbed :: Embed t -> Bool

nthpatrec :: Embed t -> NthCont

findpatrec :: Embed t -> AnyName -> FindResult

type Embedded (Embed t)

Defined in Unbound.LocallyNameless.Alpha

type Embedded (Embed t) = t

newtype Shift p

Shift the scope of an embedded term one level outwards.

Constructors

Shift p

Instances

(Rep p, Sat (ctx p)) => Rep1 ctx (Shift p)

Defined in Unbound.LocallyNameless.Types

Methods

rep1 :: R1 ctx (Shift p)

(Alpha a, Subst b a) => Subst b (Shift a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

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

subst :: Name b -> b -> Shift a -> Shift a

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

substPat :: AlphaCtx -> b -> Shift a -> Shift a

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> Shift a -> Shift a

Eq p => Eq (Shift p)

Defined in Unbound.LocallyNameless.Types

Methods

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

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

Show a => Show (Shift a)

Defined in Unbound.LocallyNameless.Types

Methods

showsPrec :: Int -> Shift a -> ShowS

show :: Shift a -> String

showList :: [Shift a] -> ShowS

Rep p => Rep (Shift p)

Defined in Unbound.LocallyNameless.Types

Methods

rep :: R (Shift p)

IsEmbed e => IsEmbed (Shift e)

Defined in Unbound.LocallyNameless.Alpha

Associated Types

type Embedded (Shift e) :: *

Methods

embed :: Embedded (Shift e) -> Shift e

unembed :: Shift e -> Embedded (Shift e)

Alpha a => Alpha (Shift a)

Defined in Unbound.LocallyNameless.Alpha

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Shift a -> Shift a

fv' :: Collection f => AlphaCtx -> Shift a -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Shift a -> (Shift a -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Shift a -> m (Shift a, Perm AnyName)

aeq' :: AlphaCtx -> Shift a -> Shift a -> Bool

acompare' :: AlphaCtx -> Shift a -> Shift a -> Ordering

close :: Alpha b => AlphaCtx -> b -> Shift a -> Shift a

open :: Alpha b => AlphaCtx -> b -> Shift a -> Shift a

isPat :: Shift a -> Maybe [AnyName]

isTerm :: Shift a -> Bool

isEmbed :: Shift a -> Bool

nthpatrec :: Shift a -> NthCont

findpatrec :: Shift a -> AnyName -> FindResult

type Embedded (Shift e)

Defined in Unbound.LocallyNameless.Alpha

type Embedded (Shift e) = Embedded e

module Unbound.LocallyNameless.Name

Pay no attention to the man behind the curtain

These type representation objects are exported so they can be referenced by auto-generated code. Please pretend they do not exist.

rGenBind :: forall order card p t. (Rep order, Rep card, Rep p, Rep t) => R (GenBind order card p t)

rRebind :: forall p1 p2. (Rep p1, Rep p2) => R (Rebind p1 p2)

rEmbed :: forall t. Rep t => R (Embed t)

rRec :: forall p. Rep p => R (Rec p)

rShift :: forall p. Rep p => R (Shift p)

Orphan instances

Rep a => Binary (Name a)

Methods

put :: Name a -> Put

get :: Get (Name a)

putList :: [Name a] -> Put