{- |
Module: Agda.Unused.Utils

Utility functions for 'Maybe', 'Either', and 'Map' types.
-}
module Agda.Unused.Utils

  ( -- * Maybe

    liftMaybe

    -- * Either

  , mapLeft

    -- * List

  , stripSuffix

  ) where

import Control.Monad.Except
  (MonadError, throwError)
import Data.List
  (stripPrefix)

-- ## Maybe

-- | Lift a 'Maybe' type to an error monad by throwing a fixed error.
liftMaybe
  :: MonadError e m
  => e
  -> Maybe a
  -> m a
liftMaybe :: e -> Maybe a -> m a
liftMaybe e
e Maybe a
Nothing
  = e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e
liftMaybe e
_ (Just a
x)
  = a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

-- ## Either

-- | Map the left component of an 'Either' type.
mapLeft
  :: (e -> f)
  -> Either e a
  -> Either f a
mapLeft :: (e -> f) -> Either e a -> Either f a
mapLeft e -> f
f (Left e
e)
  = f -> Either f a
forall a b. a -> Either a b
Left (e -> f
f e
e)
mapLeft e -> f
_ (Right a
x)
  = a -> Either f a
forall a b. b -> Either a b
Right a
x

-- ## List

-- | Drop the given suffix from a list.
stripSuffix
  :: Eq a
  => [a]
  -> [a]
  -> Maybe [a]
stripSuffix :: [a] -> [a] -> Maybe [a]
stripSuffix [a]
xs [a]
ys
  = [a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> Maybe [a] -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [a] -> Maybe [a]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs) ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ys)