module Bound.Term
( substitute
, substituteVar
, isClosed
, closed
) where
import Data.Foldable
import Data.Traversable
import Prelude hiding (all)
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
substitute :: forall (f :: * -> *) a. (Monad f, Eq a) => a -> f a -> f a -> f a
substitute a
a f a
p f a
w = f a
w forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
b -> if a
a forall a. Eq a => a -> a -> Bool
== a
b then f a
p else forall (m :: * -> *) a. Monad m => a -> m a
return a
b
{-# INLINE substitute #-}
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
substituteVar :: forall (f :: * -> *) a. (Functor f, Eq a) => a -> a -> f a -> f a
substituteVar a
a a
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
b -> if a
a forall a. Eq a => a -> a -> Bool
== a
b then a
p else a
b)
{-# INLINE substituteVar #-}
closed :: Traversable f => f a -> Maybe (f b)
closed :: forall (f :: * -> *) a b. Traversable f => f a -> Maybe (f b)
closed = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b. a -> b -> a
const forall a. Maybe a
Nothing)
{-# INLINE closed #-}
isClosed :: Foldable f => f a -> Bool
isClosed :: forall (f :: * -> *) a. Foldable f => f a -> Bool
isClosed = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b. a -> b -> a
const Bool
False)
{-# INLINE isClosed #-}