module Unbound.Generics.LocallyNameless.Operations
(
aeq
, fvAny
, fv
, freshen
, lfreshen
, swaps
, Bind
, bind
, unbind
, lunbind
, unbind2
, lunbind2
, unbind2Plus
, Rebind
, rebind
, unrebind
, Embed(..)
, embed
, unembed
, Rec
, Unbound.Generics.LocallyNameless.Rec.rec
, Unbound.Generics.LocallyNameless.Rec.unrec
, TRec(..)
, trec
, untrec
, luntrec
) where
import Control.Applicative (Applicative)
import Control.Monad (MonadPlus(mzero))
import Data.Functor.Contravariant (Contravariant)
import Data.Monoid ((<>))
import Data.Typeable (Typeable, cast)
import Unbound.Generics.LocallyNameless.Alpha
import Unbound.Generics.LocallyNameless.Fresh
import Unbound.Generics.LocallyNameless.LFresh
import Unbound.Generics.LocallyNameless.Name
import Unbound.Generics.LocallyNameless.Bind
import Unbound.Generics.LocallyNameless.Embed (Embed(..))
import Unbound.Generics.LocallyNameless.Rebind
import Unbound.Generics.LocallyNameless.Rec
import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
import Unbound.Generics.PermM
aeq :: Alpha a => a -> a -> Bool
aeq = aeq' initialCtx
fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
fvAny = fvAny' initialCtx
fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)
=> (Name b -> f (Name b)) -> a -> f a
fv = fvAny . justFiltered f
where f :: AnyName -> Maybe (Name b)
f (AnyName n) = cast n
freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
freshen = freshen' (patternCtx initialCtx)
lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
lfreshen = lfreshen' (patternCtx initialCtx)
swaps :: Alpha t => Perm AnyName -> t -> t
swaps = swaps' initialCtx
bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
bind p t = B p (close initialCtx p t)
unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)
unbind (B p t) = do
(p', _) <- freshen p
return (p', open initialCtx p' t)
lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
lunbind (B p t) cont =
lfreshen p (\x _ -> cont (x, open initialCtx x t))
unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
=> Bind p1 t1
-> Bind p2 t2
-> m (Maybe (p1, t1, p2, t2))
unbind2 (B p1 t1) (B p2 t2) = do
case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of
Just pm -> do
(p1', pm') <- freshen p1
return $ Just (p1', open initialCtx p1' t1,
swaps (pm' <> pm) p2, open initialCtx p1' t2)
Nothing -> return Nothing
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
lunbind2 (B p1 t1) (B p2 t2) cont =
case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of
Just pm ->
lfreshen p1 $ \p1' pm' ->
cont $ Just (p1', open initialCtx p1' t1,
swaps (pm' <> pm) p2, open initialCtx p1' t2)
Nothing -> cont Nothing
unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
=> Bind p1 t1
-> Bind p2 t2
-> m (p1, t1, p2, t2)
unbind2Plus bnd bnd' = maybe mzero return =<< unbind2 bnd bnd'
rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
rebind p1 p2 = Rebnd p1 (close (patternCtx initialCtx) p1 p2)
unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) p1 p2)
embed :: t -> Embed t
embed = Embed
unembed :: Embed t -> t
unembed (Embed t) = t
trec :: Alpha p => p -> TRec p
trec p = TRec (bind (rec p) ())
untrec :: (Alpha p, Fresh m) => TRec p -> m p
untrec (TRec b) = do
(p, ()) <- unbind b
return (unrec p)
luntrec :: (Alpha p, LFresh m) => TRec p -> m p
luntrec (TRec b) =
lunbind b $ \(p, ()) -> return (unrec p)