Unbound.Generics.LocallyNameless.Name

Names stand for values. They may be bound or free.

Names over terms

data Name a

An abstract datatype of names Name a that stand for terms of type a. The type a is used as a tag to distinguish these names from names that may stand for other sorts of terms.

Two names in a term are considered aeq equal when they are the same name (in the sense of '(==)'). In patterns, however, any two names are equal if they occur in the same place within the pattern. This induces alpha equivalence on terms in general.

Names may either be free or bound (see isFreeName). Free names may be extracted from patterns using isPat. Bound names cannot be.

Constructors

Fn String !Integer

Bn !Integer !Integer

Instances

Subst b (Name a)

Defined in Unbound.Generics.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

Eq (Name a)

Defined in Unbound.Generics.LocallyNameless.Name

Methods

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

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

Ord (Name a)

Defined in Unbound.Generics.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.Generics.LocallyNameless.Name

Methods

showsPrec :: Int -> Name a -> ShowS

show :: Name a -> String

showList :: [Name a] -> ShowS

Generic (Name a)

Defined in Unbound.Generics.LocallyNameless.Name

Associated Types

type Rep (Name a) :: Type -> Type

Methods

from :: Name a -> Rep (Name a) x

to :: Rep (Name a) x -> Name a

NFData (Name a)

Defined in Unbound.Generics.LocallyNameless.Name

Methods

rnf :: Name a -> ()

Typeable a => Alpha (Name a)

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Name a -> f (Name a)

close :: AlphaCtx -> NamePatFind -> Name a -> Name a

open :: AlphaCtx -> NthPatFind -> Name a -> Name a

isPat :: Name a -> DisjointSet AnyName

isTerm :: Name a -> All

isEmbed :: Name a -> Bool

nthPatFind :: Name a -> NthPatFind

namePatFind :: Name a -> NamePatFind

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

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)

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

type Rep (Name a)

Defined in Unbound.Generics.LocallyNameless.Name

type Rep (Name a) = D1 (MetaData "Name" "Unbound.Generics.LocallyNameless.Name" "unbound-generics-0.4.1-7nK9k72nPaDBZ99uX0BGq7" False) (C1 (MetaCons "Fn" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)) :+: C1 (MetaCons "Bn" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)))

isFreeName :: Name a -> Bool

Returns True iff the given Name a is free.

Name construction

string2Name :: String -> Name a

Make a free 'Name a' from a String

s2n :: String -> Name a

Synonym for string2Name.

makeName :: String -> Integer -> Name a

Make a name from a String and an Integer index

Name inspection

name2String :: Name a -> String

Get the string part of a Name.

name2Integer :: Name a -> Integer

Get the integer part of a Name.

Heterogeneous names

data AnyName where

An AnyName is a name that stands for a term of some (existentially hidden) type.

Constructors

AnyName :: Typeable a => Name a -> AnyName

Instances

Eq AnyName

Defined in Unbound.Generics.LocallyNameless.Name

Methods

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

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

Ord AnyName

Defined in Unbound.Generics.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.Generics.LocallyNameless.Name

Methods

showsPrec :: Int -> AnyName -> ShowS

show :: AnyName -> String

showList :: [AnyName] -> ShowS

Alpha AnyName

Defined in Unbound.Generics.LocallyNameless.Alpha

Methods

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

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> AnyName -> f AnyName

close :: AlphaCtx -> NamePatFind -> AnyName -> AnyName

open :: AlphaCtx -> NthPatFind -> AnyName -> AnyName

isPat :: AnyName -> DisjointSet AnyName

isTerm :: AnyName -> All

isEmbed :: AnyName -> Bool

nthPatFind :: AnyName -> NthPatFind

namePatFind :: AnyName -> NamePatFind

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

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

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

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

Subst b AnyName

Defined in Unbound.Generics.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