-- |
-- Module     : Unbound.Generics.LocallyNameless.Operations
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Operations on terms and patterns that contain names.
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Unbound.Generics.LocallyNameless.Operations
       (-- * Equivalence, free variables, freshness
         aeq
       , acompare
       , fvAny
       , fv
       , freshen
       , lfreshen
       , swaps
         -- * Binding, unbinding
       , Bind
       , bind
       , unbind
       , lunbind
       , unbind2
       , lunbind2
       , unbind2Plus
         -- * Rebinding, embedding
       , Rebind
       , rebind
       , unrebind
       , Embed(..)
       , IsEmbed(..)
       , embed
       , unembed
         -- * Recursive bindings
       , Rec
       , Unbound.Generics.LocallyNameless.Rec.rec
       , Unbound.Generics.LocallyNameless.Rec.unrec
       , TRec(..)
       , trec
       , untrec
       , luntrec
         -- * Opaque terms
       , Ignore
       , ignore
       , unignore
       ) 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(..), IsEmbed(..))
import Unbound.Generics.LocallyNameless.Rebind
import Unbound.Generics.LocallyNameless.Rec
import Unbound.Generics.LocallyNameless.Ignore
import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
import Unbound.Generics.LocallyNameless.Internal.Lens (view)
import Unbound.Generics.LocallyNameless.Internal.Iso (from)
import Unbound.Generics.PermM

-- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.
aeq :: Alpha a => a -> a -> Bool
aeq :: forall a. Alpha a => a -> a -> Bool
aeq = AlphaCtx -> a -> a -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' AlphaCtx
initialCtx

-- | An alpha-respecting total order on terms involving binders.
acompare :: Alpha a => a -> a -> Ordering
acompare :: forall a. Alpha a => a -> a -> Ordering
acompare = AlphaCtx -> a -> a -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
initialCtx

-- | @'fvAny'@ returns a fold over any names in a term @a@.
--
-- @
--   fvAny :: Alpha a => Fold a AnyName
-- @
fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
fvAny :: forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny = AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
fvAny' AlphaCtx
initialCtx

-- | @'fv'@ returns the free @b@ variables of term @a@.
--
-- @
--  fv :: (Alpha a, Typeable b) => Fold a (Name b)
-- @
fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)
      => (Name b -> f (Name b)) -> a -> f a
fv :: forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv = (AnyName -> f AnyName) -> a -> f a
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny ((AnyName -> f AnyName) -> a -> f a)
-> ((Name b -> f (Name b)) -> AnyName -> f AnyName)
-> (Name b -> f (Name b))
-> a
-> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AnyName -> Maybe (Name b)) -> Fold AnyName (Name b)
forall a b. (a -> Maybe b) -> Fold a b
justFiltered AnyName -> Maybe (Name b)
f
  where f :: AnyName -> Maybe (Name b)
        f :: AnyName -> Maybe (Name b)
f (AnyName Name a
n) = Name a -> Maybe (Name b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Name a
n

-- | Freshen a pattern by replacing all old binding 'Name's with new
--   fresh 'Name's, returning a new pattern and a @'Perm' 'Name'@
--   specifying how 'Name's were replaced.
freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
freshen :: forall p (m :: * -> *).
(Alpha p, Fresh m) =>
p -> m (p, Perm AnyName)
freshen = AlphaCtx -> p -> m (p, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> p -> m (p, Perm AnyName)
freshen' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx)

-- | \"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.
lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
lfreshen :: forall p (m :: * -> *) b.
(Alpha p, LFresh m) =>
p -> (p -> Perm AnyName -> m b) -> m b
lfreshen = AlphaCtx -> p -> (p -> Perm AnyName -> m b) -> m b
forall a (m :: * -> *) b.
(Alpha a, LFresh m) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> p -> (p -> Perm AnyName -> m b) -> m b
lfreshen' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx)

-- | Apply the given permutation of variable names to the given term.
swaps :: Alpha t => Perm AnyName -> t -> t
swaps :: forall t. Alpha t => Perm AnyName -> t -> t
swaps = AlphaCtx -> Perm AnyName -> t -> t
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' AlphaCtx
initialCtx

  
-- | @'bind' p t@ closes over the variables of pattern @p@ in the term @t@
bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
bind :: forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind p
p t
t = p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B p
p (AlphaCtx -> NamePatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close AlphaCtx
initialCtx (p -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind p
p) t
t)

-- | @'unbind' b@ lets you descend beneath a binder @b :: 'Bind' p t@
-- by returning the pair of the pattern @p@ and the term @t@ where the
-- variables in the pattern have been made globally fresh with respect
-- to the freshness monad @m@.
unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)
unbind :: forall p t (m :: * -> *).
(Alpha p, Alpha t, Fresh m) =>
Bind p t -> m (p, t)
unbind (B p
p t
t) = do
  (p
p', Perm AnyName
_) <- p -> m (p, Perm AnyName)
forall p (m :: * -> *).
(Alpha p, Fresh m) =>
p -> m (p, Perm AnyName)
freshen p
p
  (p, t) -> m (p, t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (p
p', AlphaCtx -> NthPatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx (p -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p
p') t
t)

-- | @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.
lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
lunbind :: forall (m :: * -> *) p t c.
(LFresh m, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> m c) -> m c
lunbind (B p
p t
t) (p, t) -> m c
cont =
  p -> (p -> Perm AnyName -> m c) -> m c
forall p (m :: * -> *) b.
(Alpha p, LFresh m) =>
p -> (p -> Perm AnyName -> m b) -> m b
lfreshen p
p (\p
x Perm AnyName
_ -> (p, t) -> m c
cont (p
x, AlphaCtx -> NthPatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx (p -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p
x) t
t))


-- | Simultaneously unbind two patterns in two terms, returning 'Nothing' if
-- the two patterns don't bind the same number of variables.
unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
           => Bind p1 t1
           -> Bind p2 t2
           -> m (Maybe (p1, t1, p2, t2))
unbind2 :: forall (m :: * -> *) p1 p2 t1 t2.
(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
p1 t1
t1) (B p2
p2 t2
t2) = do
      case [AnyName] -> [AnyName] -> Maybe (Perm AnyName)
forall a. Ord a => [a] -> [a] -> Maybe (Perm a)
mkPerm (Fold p2 AnyName -> p2 -> [AnyName]
forall s a. Fold s a -> s -> [a]
toListOf (AnyName -> f AnyName) -> p2 -> f p2
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
Fold p2 AnyName
fvAny p2
p2) (Fold p1 AnyName -> p1 -> [AnyName]
forall s a. Fold s a -> s -> [a]
toListOf (AnyName -> f AnyName) -> p1 -> f p1
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
Fold p1 AnyName
fvAny p1
p1) of
         Just Perm AnyName
pm -> do
           (p1
p1', Perm AnyName
pm') <- p1 -> m (p1, Perm AnyName)
forall p (m :: * -> *).
(Alpha p, Fresh m) =>
p -> m (p, Perm AnyName)
freshen p1
p1
           let npf :: NthPatFind
npf = p1 -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p1
p1'
           Maybe (p1, t1, p2, t2) -> m (Maybe (p1, t1, p2, t2))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (p1, t1, p2, t2) -> m (Maybe (p1, t1, p2, t2)))
-> Maybe (p1, t1, p2, t2) -> m (Maybe (p1, t1, p2, t2))
forall a b. (a -> b) -> a -> b
$ (p1, t1, p2, t2) -> Maybe (p1, t1, p2, t2)
forall a. a -> Maybe a
Just (p1
p1', AlphaCtx -> NthPatFind -> t1 -> t1
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx NthPatFind
npf t1
t1,
                          Perm AnyName -> p2 -> p2
forall t. Alpha t => Perm AnyName -> t -> t
swaps (Perm AnyName
pm' Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
pm) p2
p2, AlphaCtx -> NthPatFind -> t2 -> t2
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx NthPatFind
npf t2
t2)
         Maybe (Perm AnyName)
Nothing -> Maybe (p1, t1, p2, t2) -> m (Maybe (p1, t1, p2, t2))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (p1, t1, p2, t2)
forall a. Maybe a
Nothing

-- | Simultaneously 'lunbind' two patterns in two terms in the 'LFresh' monad,
-- passing @Just (p1, t1, p2, t2)@ to the continuation such that the patterns
-- are permuted such that they introduce the same free names, or 'Nothing' if
-- the number of variables differs.
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 :: forall (m :: * -> *) p1 p2 t1 t2 c.
(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
p1 t1
t1) (B p2
p2 t2
t2) Maybe (p1, t1, p2, t2) -> m c
cont =
  case [AnyName] -> [AnyName] -> Maybe (Perm AnyName)
forall a. Ord a => [a] -> [a] -> Maybe (Perm a)
mkPerm (Fold p2 AnyName -> p2 -> [AnyName]
forall s a. Fold s a -> s -> [a]
toListOf (AnyName -> f AnyName) -> p2 -> f p2
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
Fold p2 AnyName
fvAny p2
p2) (Fold p1 AnyName -> p1 -> [AnyName]
forall s a. Fold s a -> s -> [a]
toListOf (AnyName -> f AnyName) -> p1 -> f p1
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
Fold p1 AnyName
fvAny p1
p1) of
    Just Perm AnyName
pm ->
      p1 -> (p1 -> Perm AnyName -> m c) -> m c
forall p (m :: * -> *) b.
(Alpha p, LFresh m) =>
p -> (p -> Perm AnyName -> m b) -> m b
lfreshen p1
p1 ((p1 -> Perm AnyName -> m c) -> m c)
-> (p1 -> Perm AnyName -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \p1
p1' Perm AnyName
pm' ->
      Maybe (p1, t1, p2, t2) -> m c
cont (Maybe (p1, t1, p2, t2) -> m c) -> Maybe (p1, t1, p2, t2) -> m c
forall a b. (a -> b) -> a -> b
$ let npf :: NthPatFind
npf = p1 -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p1
p1'
             in (p1, t1, p2, t2) -> Maybe (p1, t1, p2, t2)
forall a. a -> Maybe a
Just (p1
p1', AlphaCtx -> NthPatFind -> t1 -> t1
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx NthPatFind
npf t1
t1,
                      Perm AnyName -> p2 -> p2
forall t. Alpha t => Perm AnyName -> t -> t
swaps (Perm AnyName
pm' Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
pm) p2
p2, AlphaCtx -> NthPatFind -> t2 -> t2
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
initialCtx NthPatFind
npf t2
t2)
    Maybe (Perm AnyName)
Nothing -> Maybe (p1, t1, p2, t2) -> m c
cont Maybe (p1, t1, p2, t2)
forall a. Maybe a
Nothing

-- | Simultaneously unbind two patterns in two terms, returning 'mzero' if
-- the patterns don't bind the same number of variables.
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 :: forall (m :: * -> *) p1 p2 t1 t2.
(MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>
Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2)
unbind2Plus Bind p1 t1
bnd Bind p2 t2
bnd' = m (p1, t1, p2, t2)
-> ((p1, t1, p2, t2) -> m (p1, t1, p2, t2))
-> Maybe (p1, t1, p2, t2)
-> m (p1, t1, p2, t2)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m (p1, t1, p2, t2)
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero (p1, t1, p2, t2) -> m (p1, t1, p2, t2)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (p1, t1, p2, t2) -> m (p1, t1, p2, t2))
-> m (Maybe (p1, t1, p2, t2)) -> m (p1, t1, p2, t2)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))
forall (m :: * -> *) p1 p2 t1 t2.
(Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>
Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))
unbind2 Bind p1 t1
bnd Bind p2 t2
bnd'


-- | @'rebind' p1 p2@ is a smart constructor for 'Rebind'.  It
-- captures the variables of pattern @p1@ that occur within @p2@ in
-- addition to providing binding occurrences for all the variables of @p1@ and @p2@
rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
rebind :: forall p1 p2. (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
rebind p1
p1 p2
p2 = p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd p1
p1 (AlphaCtx -> NamePatFind -> p2 -> p2
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx) (p1 -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind p1
p1) p2
p2)

-- | @'unrebind' p@ is the elimination form for 'Rebind'. It is not
-- monadic (unlike 'unbind') because a @Rebind@ pattern can only occur
-- somewhere in a pattern position of a 'Bind', and therefore 'unbind'
-- must have already been called and all names apropriately
-- 'freshen'ed.
unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind :: forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind (Rebnd p1
p1 p2
p2) = (p1
p1, AlphaCtx -> NthPatFind -> p2 -> p2
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx) (p1 -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p1
p1) p2
p2)

-- | Embeds a term in an 'Embed', or an 'Embed' under some number of 'Unbound.Generics.LocallyNameless.Shift.Shift' constructors.
embed :: IsEmbed e => Embedded e -> e
embed :: forall e. IsEmbed e => Embedded e -> e
embed Embedded e
e = Getting e (Embedded e) e -> Embedded e -> e
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (AnIso e e (Embedded e) (Embedded e)
-> Iso (Embedded e) (Embedded e) e e
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso e e (Embedded e) (Embedded e)
forall e (p :: * -> * -> *) (f :: * -> *).
(IsEmbed e, Profunctor p, Functor f) =>
p (Embedded e) (f (Embedded e)) -> p e (f e)
forall (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Embedded e) (f (Embedded e)) -> p e (f e)
embedded) Embedded e
e

-- | @'unembed' p@ extracts the term embedded in the pattern @p@.
unembed :: IsEmbed e => e -> Embedded e
unembed :: forall e. IsEmbed e => e -> Embedded e
unembed e
e = Getting (Embedded e) e (Embedded e) -> e -> Embedded e
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Embedded e) e (Embedded e)
forall e (p :: * -> * -> *) (f :: * -> *).
(IsEmbed e, Profunctor p, Functor f) =>
p (Embedded e) (f (Embedded e)) -> p e (f e)
forall (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Embedded e) (f (Embedded e)) -> p e (f e)
embedded e
e

-- | Constructor for recursive abstractions.
trec :: Alpha p => p -> TRec p
trec :: forall p. Alpha p => p -> TRec p
trec p
p = Bind (Rec p) () -> TRec p
forall p. Bind (Rec p) () -> TRec p
TRec (Rec p -> () -> Bind (Rec p) ()
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (p -> Rec p
forall p. Alpha p => p -> Rec p
rec p
p) ())

-- | Destructor for recursive abstractions which picks globally fresh
--   names for the binders.
untrec :: (Alpha p, Fresh m) => TRec p -> m p
untrec :: forall p (m :: * -> *). (Alpha p, Fresh m) => TRec p -> m p
untrec (TRec Bind (Rec p) ()
b) = do
  (Rec p
p, ()) <- Bind (Rec p) () -> m (Rec p, ())
forall p t (m :: * -> *).
(Alpha p, Alpha t, Fresh m) =>
Bind p t -> m (p, t)
unbind Bind (Rec p) ()
b
  p -> m p
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rec p -> p
forall p. Alpha p => Rec p -> p
unrec Rec p
p)

-- | Destructor for recursive abstractions which picks /locally/ fresh
--   names for binders (see 'LFresh').
luntrec :: (Alpha p, LFresh m) => TRec p -> m p
luntrec :: forall p (m :: * -> *). (Alpha p, LFresh m) => TRec p -> m p
luntrec (TRec Bind (Rec p) ()
b) =
  Bind (Rec p) () -> ((Rec p, ()) -> m p) -> m p
forall (m :: * -> *) p t c.
(LFresh m, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> m c) -> m c
lunbind Bind (Rec p) ()
b (((Rec p, ()) -> m p) -> m p) -> ((Rec p, ()) -> m p) -> m p
forall a b. (a -> b) -> a -> b
$ \(Rec p
p, ()) -> p -> m p
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rec p -> p
forall p. Alpha p => Rec p -> p
unrec Rec p
p)

-- | Constructor for ignoring a term for the purposes of alpha-equality and substs
ignore :: t -> Ignore t
ignore :: forall t. t -> Ignore t
ignore t
t = t -> Ignore t
forall t. t -> Ignore t
I t
t

-- | Destructor for ignored terms
unignore :: Ignore t -> t
unignore :: forall t. Ignore t -> t
unignore (I t
t) = t
t