-----------------------------------------------------------------------------

-- |

-- 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 :: 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' 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 :: 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 #-}

-- | 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 :: 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 #-}

-- | A closed term has no free variables.

--

-- >>> isClosed []

-- True

--

-- >>> isClosed [1,2,3]

-- False

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 #-}