unbound-0.4.2: Generic support for programming with names and binders

PortabilityGHC only
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellNone

Unbound.LocallyNameless.Name

Contents

Description

An implementation of names in a locally nameless representation.

Synopsis

Name types

data Name a Source

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 a0, Sat (ctx0 (R a0)), Sat (ctx0 (String, Integer)), Sat (ctx0 Integer)) => Rep1 ctx0 (Name a0) 
Rep a => Subst b (Name a) 
Eq (Name a) 
Ord (Name a) 
Show (Name a) 
Rep a0 => Rep (Name a0) 
Rep a => Alpha (Name a) 

data AnyName Source

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

forall a . Rep a => AnyName (Name a) 

Constructing and destructing free names

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

Create a free Name from an Integer.

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

Create a free Name from a String.

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

Convenient synonym for string2Name.

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

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

name2Integer :: Name a -> IntegerSource

Get the integer index of a Name.

name2String :: Name a -> StringSource

Get the string part of a Name.

anyName2Integer :: AnyName -> IntegerSource

Get the integer index of an AnyName.

anyName2String :: AnyName -> StringSource

Get the string part of an AnyName.

Sorts

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

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

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

Change the sort of a name.

getR :: Name a -> R aSource

Determine the sort of a Name.

Utility

isBound :: Name a -> BoolSource

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 -> BoolSource

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

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

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

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

rAnyName1 :: forall ctx. R1 ctx AnyNameSource