| Copyright | (c) 2014 Aleksey Kliger |
|---|---|
| License | BSD3 (See LICENSE) |
| Maintainer | Aleksey Kliger |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
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
- module Unbound.Generics.LocallyNameless.Alpha
- data Name a
- data AnyName where
- 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
- 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
A term of type Bind p tp in the term
t. In the overall term, those variables are now bound. See also
bind and
unbind and
lunbind
Instances
Ignores a term t for the purpose of alpha-equality and substitution
Instances
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)
| ...