Copyright	(c) 2014 Aleksey Kliger
License	BSD3 (See LICENSE)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	Safe
Language	Haskell2010

Unbound.Generics.LocallyNameless.Name

Contents

Names over terms
Name construction
Name inspection
Heterogeneous names

Description

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

Synopsis

data Name a
- = Fn String !Integer
- | Bn !Integer !Integer
isFreeName :: Name a -> Bool
string2Name :: String -> Name a
s2n :: String -> Name a
makeName :: String -> Integer -> Name a
name2String :: Name a -> String
name2Integer :: Name a -> Integer
data AnyName where
- AnyName :: Typeable a => Name a -> AnyName

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 consider 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) 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 #
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 #
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 #
Generic (Name a) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Name Associated Types type Rep (Name a) :: * -> * # Methods from :: Name a -> Rep (Name a) x # to :: Rep (Name a) x -> Name a #
NFData (Name a) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Name Methods rnf :: Name a -> () #
Typeable a => Alpha (Name a) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Alpha Methods aeq' :: AlphaCtx -> Name a -> Name a -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Name a -> f (Name a) Source # close :: AlphaCtx -> NamePatFind -> Name a -> Name a Source # open :: AlphaCtx -> NthPatFind -> Name a -> Name a Source # isPat :: Name a -> DisjointSet AnyName Source # isTerm :: Name a -> All Source # isEmbed :: Name a -> Bool Source # nthPatFind :: Name a -> NthPatFind Source # namePatFind :: Name a -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a Source # lfreshen' :: LFresh m => AlphaCtx -> Name a -> (Name a -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Name a -> m (Name a, Perm AnyName) Source # acompare' :: AlphaCtx -> Name a -> Name a -> Ordering Source #
type Rep (Name a) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Name type Rep (Name a) = D1 (MetaData "Name" "Unbound.Generics.LocallyNameless.Name" "unbound-generics-0.4.0-3CzcjD8SUhgLQazt2sGCP5" 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 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

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 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 Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Name Methods showsPrec :: Int -> AnyName -> ShowS # show :: AnyName -> String # showList :: [AnyName] -> ShowS #
Alpha AnyName Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Alpha Methods aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> AnyName -> f AnyName Source # close :: AlphaCtx -> NamePatFind -> AnyName -> AnyName Source # open :: AlphaCtx -> NthPatFind -> AnyName -> AnyName Source # isPat :: AnyName -> DisjointSet AnyName Source # isTerm :: AnyName -> All Source # isEmbed :: AnyName -> Bool Source # nthPatFind :: AnyName -> NthPatFind Source # namePatFind :: AnyName -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> AnyName -> AnyName Source # lfreshen' :: LFresh m => AlphaCtx -> AnyName -> (AnyName -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> AnyName -> m (AnyName, Perm AnyName) Source # acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering Source #
Subst b AnyName Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Subst Methods isvar :: AnyName -> Maybe (SubstName AnyName b) Source # isCoerceVar :: AnyName -> Maybe (SubstCoerce AnyName b) Source # subst :: Name b -> b -> AnyName -> AnyName Source # substs :: [(Name b, b)] -> AnyName -> AnyName Source #