Copyright | (c) 2014 Aleksey Kliger |
---|---|
License | BSD3 (See LICENSE) |
Maintainer | Aleksey Kliger |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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
- module Unbound.Generics.LocallyNameless.Alpha
- data Name a
- 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
- module Unbound.Generics.LocallyNameless.Operations
- data Bind p t
- data Ignore t
- module Unbound.Generics.LocallyNameless.Embed
- module Unbound.Generics.LocallyNameless.Shift
- data Rebind p1 p2
- module Unbound.Generics.LocallyNameless.Rec
- module Unbound.Generics.LocallyNameless.Fresh
- module Unbound.Generics.LocallyNameless.LFresh
- module Unbound.Generics.LocallyNameless.Subst
Documentation
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
An AnyName
is a name that stands for a term of some (existentially hidden) type.
Instances
Show AnyName Source # | |
Eq AnyName Source # | |
Ord AnyName Source # | |
Defined in Unbound.Generics.LocallyNameless.Name | |
Alpha AnyName Source # | |
Defined in Unbound.Generics.LocallyNameless.Alpha 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 # | |
Defined in Unbound.Generics.LocallyNameless.Subst |
A term of type
is a term that binds the free
variable occurrences of the variables in pattern Bind
p tp
in the term
t
. In the overall term, those variables are now bound. See also
bind
and
unbind
and
lunbind
Instances
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Subst | |||||
Generic (Bind p t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Bind
| |||||
(Show p, Show t) => Show (Bind p t) Source # | |||||
(NFData p, NFData t) => NFData (Bind p t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Bind | |||||
(Alpha p, Alpha t) => Alpha (Bind p t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Bind 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 # | |||||
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))) |
Ignores a term t
for the purpose of alpha-equality and substitution
Instances
Subst a (Ignore b) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Subst | |||||
Generic (Ignore t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Ignore
| |||||
Show t => Show (Ignore t) Source # | |||||
NFData t => NFData (Ignore t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Ignore | |||||
Show t => Alpha (Ignore t) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Ignore 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 # | |||||
Defined in Unbound.Generics.LocallyNameless.Ignore |
is a pattern that binds the names of Rebind
p1 p2p1
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
(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Subst 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 # | |||||
Defined in Unbound.Generics.LocallyNameless.Rebind
| |||||
(Show p1, Show p2) => Show (Rebind p1 p2) Source # | |||||
(NFData p1, NFData p2) => NFData (Rebind p1 p2) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Rebind | |||||
(Eq p1, Eq p2) => Eq (Rebind p1 p2) Source # | |||||
(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Rebind 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 # | |||||
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))) |