| Copyright | (c) 2014, Aleksey Kliger |
|---|---|
| License | BSD3 (See LICENSE) |
| Maintainer | Aleksey Kliger |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Unbound.Generics.LocallyNameless.Operations
Contents
Description
Operations on terms and patterns that contain names.
- aeq :: Alpha a => a -> a -> Bool
- acompare :: Alpha a => a -> a -> Ordering
- fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
- fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a
- freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
- lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
- swaps :: Alpha t => Perm AnyName -> t -> t
- data Bind p t
- bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)
- lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
- unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))
- lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c
- unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2)
- data Rebind p1 p2
- rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
- unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
- newtype Embed t = Embed t
- class IsEmbed e where
- embed :: IsEmbed e => Embedded e -> e
- unembed :: IsEmbed e => e -> Embedded e
- data Rec p
- rec :: Alpha p => p -> Rec p
- unrec :: Alpha p => Rec p -> p
- newtype TRec p = TRec (Bind (Rec p) ())
- trec :: Alpha p => p -> TRec p
- untrec :: (Alpha p, Fresh m) => TRec p -> m p
- luntrec :: (Alpha p, LFresh m) => TRec p -> m p
Equivalence, free variables, freshness
aeq :: Alpha a => a -> a -> Bool Source #
aeq t1 t2True iff t1 and t2 are alpha-equivalent terms.
acompare :: Alpha a => a -> a -> Ordering Source #
An alpha-respecting total order on terms involving binders.
fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a Source #
fvAnya.
fvAny :: Alpha a => Fold a AnyName
fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a Source #
fvb variables of term a.
fv :: (Alpha a, Typeable b) => Fold a (Name b)
lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b Source #
"Locally" freshen a pattern, replacing all binding names with new names that are not already "in scope". The second argument is a continuation, which takes the renamed term and a permutation that specifies how the pattern has been renamed. The resulting computation will be run with the in-scope set extended by the names just generated.
swaps :: Alpha t => Perm AnyName -> t -> t Source #
Apply the given permutation of variable names to the given term.
Binding, unbinding
bind :: (Alpha p, Alpha t) => p -> t -> Bind p t Source #
bind p tp in the term t
lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c Source #
lunbind opens a binding in an LFresh monad, ensuring that the
names chosen for the binders are locally fresh. The components
of the binding are passed to a continuation, and the resulting
monadic action is run in a context extended to avoid choosing new
names which are the same as the ones chosen for this binding.
For more information, see the documentation for the LFresh type
class.
unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2)) Source #
Simultaneously unbind two patterns in two terms, returning Nothing if
the two patterns don't bind the same number of variables.
lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c Source #
unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2) Source #
Simultaneously unbind two patterns in two terms, returning mzero if
the patterns don't bind the same number of variables.
Rebinding, embedding
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 # | |
| (Eq p1, Eq p2) => Eq (Rebind p1 p2) Source # | |
| (Show p1, Show p2) => Show (Rebind p1 p2) Source # | |
| Generic (Rebind p1 p2) Source # | |
| (NFData p1, NFData p2) => NFData (Rebind p1 p2) Source # | |
| (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) Source # | |
| type Rep (Rebind p1 p2) Source # | |
Embed allows for terms to be embedded within patterns. Such
embedded terms do not bind names along with the rest of the
pattern. For examples, see the tutorial or examples directories.
If t is a term type, then Embed t is a pattern type.
Embed is not abstract since it involves no binding, and hence
it is safe to manipulate directly. To create and destruct
Embed terms, you may use the Embed constructor directly.
(You may also use the functions embed and unembed, which
additionally can construct or destruct any number of enclosing
Shifts at the same time.)
Constructors
| Embed t |
Instances
| Subst c a => Subst c (Embed a) Source # | |
| Eq t => Eq (Embed t) Source # | |
| Ord t => Ord (Embed t) Source # | |
| Show a => Show (Embed a) Source # | |
| Generic (Embed t) Source # | |
| NFData t => NFData (Embed t) Source # | |
| Alpha t => Alpha (Embed t) Source # | |
| IsEmbed (Embed t) Source # | |
| type Rep (Embed t) Source # | |
| type Embedded (Embed t) Source # | |
class IsEmbed e where Source #
Minimal complete definition
unembed :: IsEmbed e => e -> Embedded e Source #
unembed pp.
Recursive bindings
If p is a pattern type, then Rec p is also a pattern type,
which is recursive in the sense that p may bind names in terms
embedded within itself. Useful for encoding e.g. lectrec and
Agda's dot notation.
TRec is a standalone variant of Rec: the only difference is
that whereas Rec pTRec p
is a term type. It is isomorphic to Bind (Rec p) ()
Note that TRec corresponds to Pottier's abstraction construct
from alpha-Caml. In this context, Embed tinner t, and Shift (Embed t)outer t.