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

Unbound.Generics.LocallyNameless

Description

The purpose of unbound-genrics is to simplify the construction of data structures with rich variable binding structure by providing generic implementations of alpha-equivalence (aeq), free variable permutation (swaps), local and global variable freshness (lfresh, fresh),

See Alpha, Bind, Unbound.Generics.LocallyNameless.Operations for more information.

Synopsis

Documentation

module Unbound.Generics.LocallyNameless.Alpha

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.

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) 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

type Rep (Name a) = D1 ('MetaData "Name" "Unbound.Generics.LocallyNameless.Name" "unbound-generics-0.4.4-inplace" '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)))

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

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.4-inplace" '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.

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

name2String :: Name a -> String Source #

Get the string part of a Name.

name2Integer :: Name a -> Integer Source #

Get the integer part of a Name.

data AnyName where Source #

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

Constructors

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

Instances

Instances details
Show AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Name

Methods

showsPrec :: Int -> AnyName -> ShowS #

show :: AnyName -> String #

showList :: [AnyName] -> ShowS #

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 #

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 #

substBvs :: AlphaCtx -> [b] -> AnyName -> AnyName Source #

module Unbound.Generics.LocallyNameless.Operations

data Bind p t Source #

A term of type Bind p t is a term that binds the free variable occurrences of the variables in pattern p in the term t. In the overall term, those variables are now bound. See also bind and unbind and lunbind

Instances

Instances details
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

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

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

substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b Source #

Generic (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Associated Types

type Rep (Bind p t) 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

type Rep (Bind p t) = D1 ('MetaData "Bind" "Unbound.Generics.LocallyNameless.Bind" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

Methods

from :: Bind p t -> Rep (Bind p t) x #

to :: Rep (Bind p t) x -> Bind p t #

(Show p, Show t) => Show (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

showsPrec :: Int -> Bind p t -> ShowS #

show :: Bind p t -> String #

showList :: [Bind p t] -> ShowS #

(NFData p, NFData t) => NFData (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

rnf :: Bind p t -> () #

(Alpha p, Alpha t) => Alpha (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool Source #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t) Source #

close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t Source #

open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t Source #

isPat :: Bind p t -> DisjointSet AnyName Source #

isTerm :: Bind p t -> All Source #

isEmbed :: Bind p t -> Bool Source #

nthPatFind :: Bind p t -> NthPatFind Source #

namePatFind :: Bind p t -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t Source #

lfreshen' :: LFresh m => AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName) Source #

acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering Source #

type Rep (Bind p t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Bind

type Rep (Bind p t) = D1 ('MetaData "Bind" "Unbound.Generics.LocallyNameless.Bind" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

data Ignore t Source #

Ignores a term t for the purpose of alpha-equality and substitution

Instances

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

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

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

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

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

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

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

Generic (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

Associated Types

type Rep (Ignore t) 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

type Rep (Ignore t) = D1 ('MetaData "Ignore" "Unbound.Generics.LocallyNameless.Ignore" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))

Methods

from :: Ignore t -> Rep (Ignore t) x #

to :: Rep (Ignore t) x -> Ignore t #

Show t => Show (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

showsPrec :: Int -> Ignore t -> ShowS #

show :: Ignore t -> String #

showList :: [Ignore t] -> ShowS #

NFData t => NFData (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

rnf :: Ignore t -> () #

Show t => Alpha (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

Methods

aeq' :: AlphaCtx -> Ignore t -> Ignore t -> Bool Source #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ignore t -> f (Ignore t) Source #

close :: AlphaCtx -> NamePatFind -> Ignore t -> Ignore t Source #

open :: AlphaCtx -> NthPatFind -> Ignore t -> Ignore t Source #

isPat :: Ignore t -> DisjointSet AnyName Source #

isTerm :: Ignore t -> All Source #

isEmbed :: Ignore t -> Bool Source #

nthPatFind :: Ignore t -> NthPatFind Source #

namePatFind :: Ignore t -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> Ignore t -> Ignore t Source #

lfreshen' :: LFresh m => AlphaCtx -> Ignore t -> (Ignore t -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Ignore t -> m (Ignore t, Perm AnyName) Source #

acompare' :: AlphaCtx -> Ignore t -> Ignore t -> Ordering Source #

type Rep (Ignore t) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Ignore

type Rep (Ignore t) = D1 ('MetaData "Ignore" "Unbound.Generics.LocallyNameless.Ignore" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))

module Unbound.Generics.LocallyNameless.Embed

module Unbound.Generics.LocallyNameless.Shift

data Rebind p1 p2 Source #

Rebind p1 p2 is a pattern that binds the names of p1 and p2, and additionally brings the names of p1 into scope over p2.

This may be used, for example, to faithfully represent Scheme's let* binding form, defined by:

 (let* () body) ≙ body
 (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))

using the following AST:

type Var = Name Expr
data Lets = EmptyLs
          | ConsLs (Rebind (Var, Embed Expr) Lets)
data Expr = ...
          | LetStar (Bind Lets Expr)
          | ...

Instances

Instances details
(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Rebind p1 p2 -> Maybe (SubstName (Rebind p1 p2) c) Source #

isCoerceVar :: Rebind p1 p2 -> Maybe (SubstCoerce (Rebind p1 p2) c) Source #

subst :: Name c -> c -> Rebind p1 p2 -> Rebind p1 p2 Source #

substs :: [(Name c, c)] -> Rebind p1 p2 -> Rebind p1 p2 Source #

substBvs :: AlphaCtx -> [c] -> Rebind p1 p2 -> Rebind p1 p2 Source #

Generic (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Associated Types

type Rep (Rebind p1 p2) 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

type Rep (Rebind p1 p2) = D1 ('MetaData "Rebind" "Unbound.Generics.LocallyNameless.Rebind" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "Rebnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p2)))

Methods

from :: Rebind p1 p2 -> Rep (Rebind p1 p2) x #

to :: Rep (Rebind p1 p2) x -> Rebind p1 p2 #

(Show p1, Show p2) => Show (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

showsPrec :: Int -> Rebind p1 p2 -> ShowS #

show :: Rebind p1 p2 -> String #

showList :: [Rebind p1 p2] -> ShowS #

(NFData p1, NFData p2) => NFData (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

rnf :: Rebind p1 p2 -> () #

(Eq p1, Eq p2) => Eq (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

(==) :: Rebind p1 p2 -> Rebind p1 p2 -> Bool #

(/=) :: Rebind p1 p2 -> Rebind p1 p2 -> Bool #

(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

Methods

aeq' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Bool Source #

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Rebind p1 p2 -> f (Rebind p1 p2) Source #

close :: AlphaCtx -> NamePatFind -> Rebind p1 p2 -> Rebind p1 p2 Source #

open :: AlphaCtx -> NthPatFind -> Rebind p1 p2 -> Rebind p1 p2 Source #

isPat :: Rebind p1 p2 -> DisjointSet AnyName Source #

isTerm :: Rebind p1 p2 -> All Source #

isEmbed :: Rebind p1 p2 -> Bool Source #

nthPatFind :: Rebind p1 p2 -> NthPatFind Source #

namePatFind :: Rebind p1 p2 -> NamePatFind Source #

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p1 p2 -> Rebind p1 p2 Source #

lfreshen' :: LFresh m => AlphaCtx -> Rebind p1 p2 -> (Rebind p1 p2 -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rebind p1 p2 -> m (Rebind p1 p2, Perm AnyName) Source #

acompare' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Ordering Source #

type Rep (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Rebind

type Rep (Rebind p1 p2) = D1 ('MetaData "Rebind" "Unbound.Generics.LocallyNameless.Rebind" "unbound-generics-0.4.4-inplace" 'False) (C1 ('MetaCons "Rebnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p2)))

module Unbound.Generics.LocallyNameless.Rec

module Unbound.Generics.LocallyNameless.Fresh

module Unbound.Generics.LocallyNameless.LFresh

module Unbound.Generics.LocallyNameless.Subst