-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2012 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  portable
--
----------------------------------------------------------------------------
module Bound.Term
  ( substitute
  , substituteVar
  , isClosed
  , closed
  ) where

import Data.Foldable
import Data.Traversable
import Prelude hiding (all)

-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.
--
-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
-- ["goodnight","Gracie","!!!"]
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' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.
--
-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
-- ["Bob","Bob","Charlie"]
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 #-}

-- | If a term has no free variables, you can freely change the type of
-- free variables it is parameterized on.
--
-- >>> closed [12]
-- Nothing
--
-- >>> closed ""
-- Just []
--
-- >>> :t closed ""
-- closed "" :: Maybe [b]
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 #-}

-- | A closed term has no free variables.
--
-- >>> isClosed []
-- True
--
-- >>> isClosed [1,2,3]
-- False
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 #-}