Unbound.Generics.LocallyNameless.Rebind

The pattern Rebind p1 p2 binds the names in p1 and p2 just as (p1, p2) would, however it additionally also brings the names of p1 into scope in p2.

Documentation

data Rebind p1 p2

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)
           | ...

Constructors

Rebnd p1 p2

Instances

(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)

(Eq p1, Eq p2) => Eq (Rebind p1 p2)

(Show p1, Show p2) => Show (Rebind p1 p2)

Generic (Rebind p1 p2)

(Alpha p1, Alpha p2) => Alpha (Rebind p1 p2)