module Agda.Unused.Utils
(
liftMaybe
, mapLeft
, stripSuffix
, 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
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
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
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)
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
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)