Unbound.LocallyNameless.Name

An implementation of names in a locally nameless representation.

Name types

data Name a

Names are things that get bound. This type is intentionally abstract; to create a Name you can use string2Name or integer2Name. The type parameter is a tag, or sort, which tells us what sorts of things this name may stand for. The sort must be a representable type, i.e. an instance of the Rep type class from the RepLib generic programming framework.

To hide the sort of a name, use AnyName.

Constructors

Nm (R a) (String, Integer)

Bn (R a) Integer Integer

Instances

(Rep a, Sat (ctx (R a)), Sat (ctx (String, Integer)), Sat (ctx Integer)) => Rep1 ctx (Name a)

Defined in Unbound.LocallyNameless.Name

Methods

rep1 :: R1 ctx (Name a)

Rep a => Subst b (Name a)

Defined in Unbound.LocallyNameless.Subst

Methods

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

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

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

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

substPat :: AlphaCtx -> b -> Name a -> Name a

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

Eq (Name a)

Defined in Unbound.LocallyNameless.Name

Methods

(==) :: Name a -> Name a -> Bool

(/=) :: Name a -> Name a -> Bool

Ord (Name a)

Defined in Unbound.LocallyNameless.Name

Methods

compare :: Name a -> Name a -> Ordering

(<) :: Name a -> Name a -> Bool

(<=) :: Name a -> Name a -> Bool

(>) :: Name a -> Name a -> Bool

(>=) :: Name a -> Name a -> Bool

max :: Name a -> Name a -> Name a

min :: Name a -> Name a -> Name a

Show (Name a)

Defined in Unbound.LocallyNameless.Name

Methods

showsPrec :: Int -> Name a -> ShowS

show :: Name a -> String

showList :: [Name a] -> ShowS

Rep a => Rep (Name a)

Defined in Unbound.LocallyNameless.Name

Methods

rep :: R (Name a)

Rep a => Binary (Name a)

Defined in Unbound.LocallyNameless.Types

Methods

put :: Name a -> Put

get :: Get (Name a)

putList :: [Name a] -> Put

Rep a => Alpha (Name a)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: Name a -> Maybe [AnyName]

isTerm :: Name a -> Bool

isEmbed :: Name a -> Bool

nthpatrec :: Name a -> NthCont

findpatrec :: Name a -> AnyName -> FindResult

data AnyName

A name with a hidden (existentially quantified) sort. To hide the sort of a name, use the AnyName constructor directly; to extract a name with a hidden sort, use toSortedName.

Constructors

Rep a => AnyName (Name a)

Instances

Eq AnyName

Defined in Unbound.LocallyNameless.Name

Methods

(==) :: AnyName -> AnyName -> Bool

(/=) :: AnyName -> AnyName -> Bool

Ord AnyName

Defined in Unbound.LocallyNameless.Name

Methods

compare :: AnyName -> AnyName -> Ordering

(<) :: AnyName -> AnyName -> Bool

(<=) :: AnyName -> AnyName -> Bool

(>) :: AnyName -> AnyName -> Bool

(>=) :: AnyName -> AnyName -> Bool

max :: AnyName -> AnyName -> AnyName

min :: AnyName -> AnyName -> AnyName

Show AnyName

Defined in Unbound.LocallyNameless.Name

Methods

showsPrec :: Int -> AnyName -> ShowS

show :: AnyName -> String

showList :: [AnyName] -> ShowS

Rep AnyName

Defined in Unbound.LocallyNameless.Name

Methods

rep :: R AnyName

Alpha AnyName

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool

acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering

close :: Alpha b => AlphaCtx -> b -> AnyName -> AnyName

open :: Alpha b => AlphaCtx -> b -> AnyName -> AnyName

isPat :: AnyName -> Maybe [AnyName]

isTerm :: AnyName -> Bool

isEmbed :: AnyName -> Bool

nthpatrec :: AnyName -> NthCont

findpatrec :: AnyName -> AnyName -> FindResult

Rep1 ctx AnyName

Defined in Unbound.LocallyNameless.Name

Methods

rep1 :: R1 ctx AnyName

Subst b AnyName

Defined in Unbound.LocallyNameless.Subst

Methods

isvar :: AnyName -> Maybe (SubstName AnyName b)

isCoerceVar :: AnyName -> Maybe (SubstCoerce AnyName b)

subst :: Name b -> b -> AnyName -> AnyName

substs :: [(Name b, b)] -> AnyName -> AnyName

substPat :: AlphaCtx -> b -> AnyName -> AnyName

substPats :: Proxy b -> AlphaCtx -> [Dyn] -> AnyName -> AnyName

Constructing and destructing free names

integer2Name :: Rep a => Integer -> Name a

Create a free Name from an Integer.

string2Name :: Rep a => String -> Name a

Create a free Name from a String.

s2n :: Rep a => String -> Name a

Convenient synonym for string2Name.

makeName :: Rep a => String -> Integer -> Name a

Create a free Name from a String and an Integer index.

name2Integer :: Name a -> Integer

Get the integer index of a Name.

name2String :: Name a -> String

Get the string part of a Name.

anyName2Integer :: AnyName -> Integer

Get the integer index of an AnyName.

anyName2String :: AnyName -> String

Get the string part of an AnyName.

Sorts

toSortedName :: Rep a => AnyName -> Maybe (Name a)

Cast a name with an existentially hidden sort to an explicitly sorted name.

translate :: Rep b => Name a -> Name b

Change the sort of a name.

getR :: Name a -> R a

Determine the sort of a Name.

Utility

isBound :: Name a -> Bool

Test whether a name is a bound variable (i.e. a reference to some binding site, represented as a de Bruijn index). Normal users of the library should not need this function, as it is impossible to encounter a bound name when using the abstract interface provided by Unbound.LocallyNameless.

isFree :: Name a -> Bool

Test whether a name is a free variable. Normal users of the library should not need this function, as all the names encountered will be free variables when using the abstract interface provided by Unbound.LocallyNameless.

Representations

Automatically generated representation objects.

rR :: forall a. Rep a => R (R a)

rR1 :: forall ctx a. Rep a => R1 ctx (R a)

rName :: forall a. Rep a => R (Name a)

rName1 :: forall ctx a. Rep a => (ctx (R a), ctx (String, Integer)) -> (ctx (R a), ctx Integer, ctx Integer) -> R1 ctx (Name a)

rAnyName :: R AnyName

rAnyName1 :: forall ctx. R1 ctx AnyName

Orphan instances

Rep a => Rep1 ctx (R a)

Methods

rep1 :: R1 ctx (R a)

Rep a => Rep (R a)

Methods

rep :: R (R a)