{- |
Module: Agda.Unused.Utils

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

  ( -- * Maybe

    liftMaybe

    -- * Either

  , mapLeft

    -- * List

  , stripSuffix

    -- * Map

  , mapDeletes
  , mapUpdateKey

  ) where

import Control.Monad.Except
  (MonadError, throwError)
import Data.List
  (stripPrefix)
import Data.Map.Strict
  (Map)
import qualified Data.Map.Strict
  as Map

-- ## 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
e Nothing
  = e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e
liftMaybe _ (Just x :: 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 f :: e -> f
f (Left e :: e
e)
  = f -> Either f a
forall a b. a -> Either a b
Left (e -> f
f e
e)
mapLeft _ (Right x :: 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 xs :: [a]
xs ys :: [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)

-- ## Map

-- | Delete a list of keys from a map.
mapDeletes
  :: Ord k
  => [k]
  -> Map k a
  -> Map k a
mapDeletes :: [k] -> Map k a -> Map k a
mapDeletes ks :: [k]
ks xs :: Map k a
xs
  = (k -> Map k a -> Map k a) -> Map k a -> [k] -> Map k a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map k a
xs [k]
ks

-- | Modify a key of a map.
--
-- - If the source key is not present, do nothing.
-- - If the target key is already present, overwrite it.
mapUpdateKey
  :: Ord k
  => k
  -> k
  -> Map k a
  -> Map k a
mapUpdateKey :: k -> k -> Map k a -> Map k a
mapUpdateKey k :: k
k k' :: k
k' m :: Map k a
m
  = Map k a -> (a -> Map k a) -> Maybe a -> Map k a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map k a
m (\x :: a
x -> k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k' a
x (k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete k
k Map k a
m)) (k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k a
m)