| Portability | GHC only |
|---|---|
| Maintainer | Brent Yorgey <byorgey@cis.upenn.edu> |
| Safe Haskell | None |
Unbound.LocallyNameless.Name
Description
An implementation of names in a locally nameless representation.
- data Name a
- data AnyName = forall a . Rep a => AnyName (Name a)
- integer2Name :: Rep a => Integer -> Name a
- string2Name :: Rep a => String -> Name a
- s2n :: Rep a => String -> Name a
- makeName :: Rep a => String -> Integer -> Name a
- name2Integer :: Name a -> Integer
- name2String :: Name a -> String
- anyName2Integer :: AnyName -> Integer
- anyName2String :: AnyName -> String
- toSortedName :: Rep a => AnyName -> Maybe (Name a)
- translate :: Rep b => Name a -> Name b
- getR :: Name a -> R a
- isBound :: Name a -> Bool
- isFree :: Name a -> Bool
- 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
Name types
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.
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.
Constructing and destructing free names
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.
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.