unbound-generics-0.4.3: Support for programming with names and binders using GHC Generics
Copyright(c) 2014 Aleksey Kliger
LicenseBSD3 (See LICENSE)
MaintainerAleksey Kliger
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Unbound.Generics.LocallyNameless.Name

Description

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

Synopsis

Names over terms

data Name a Source #

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

Instances details
Subst b (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

subst :: Name b -> b -> Name a -> Name a Source #

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

substBvs :: AlphaCtx -> [b] -> Name a -> Name a Source #

Generic (Name a) Source # 
Instance details

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 #

Show (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Methods

showsPrec :: Int -> Name a -> ShowS #

show :: Name a -> String #

showList :: [Name a] -> ShowS #

NFData (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Methods

rnf :: Name a -> () #

Eq (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Methods

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

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

Ord (Name a) Source # 
Instance details

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 #

Typeable a => Alpha (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

type Rep (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

isFreeName :: Name a -> Bool Source #

Returns True iff the given Name a is free.

Name construction

string2Name :: String -> Name a Source #

Make a free 'Name a' from a String

s2n :: String -> Name a Source #

Synonym for string2Name.

makeName :: String -> Integer -> Name a Source #

Make a name from a String and an Integer index

Name inspection

name2String :: Name a -> String Source #

Get the string part of a Name.

name2Integer :: Name a -> Integer Source #

Get the integer part of a Name.

Heterogeneous names

data AnyName where Source #

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

Constructors

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

Instances

Instances details
Show AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Eq AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Methods

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

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

Ord AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Alpha AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Alpha

Subst b AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst