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 :: a -> f a -> f a -> f a
substitute a
a f a
p f a
w = f a
w f a -> (a -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then f a
p else a -> f a
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 :: a -> a -> f a -> f a
substituteVar a
a a
p = (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
b -> if a
a a -> a -> Bool
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 :: f a -> Maybe (f b)
closed = (a -> Maybe b) -> f a -> Maybe (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Maybe b -> a -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing)
{-# INLINE closed #-}
isClosed :: Foldable f => f a -> Bool
isClosed :: f a -> Bool
isClosed = (a -> Bool) -> f a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False)
{-# INLINE isClosed #-}