-- | Non-empty maps.
--
--   Provides type @Map1@ of non-empty maps.
--
--   Import:
--   @
--
--     import           Agda.Utils.Map1 (Map1)
--     import qualified Agda.Utils.Map1 as Map1
--
--   @

module Agda.Utils.Map1
  ( module Agda.Utils.Map1
  , module Map1
  ) where

import Data.Map (Map)
import Data.Map.NonEmpty as Map1

type Map1 = Map1.NEMap

ifNull :: Map k a -> b -> (Map1 k a -> b) -> b
ifNull :: forall k a b. Map k a -> b -> (Map1 k a -> b) -> b
ifNull Map k a
s b
b Map1 k a -> b
f = b -> (Map1 k a -> b) -> Map k a -> b
forall r k a. r -> (NEMap k a -> r) -> Map k a -> r
Map1.withNonEmpty b
b Map1 k a -> b
f Map k a
s

-- | A more general type would be @Null m => Map k a -> (Map1 k a -> m) -> m@
--   but this type is problematic as we do not have a general
--   @instance Applicative m => Null (m ())@.
--
unlessNull :: Applicative m => Map k a -> (Map1 k a -> m ()) -> m ()
unlessNull :: forall (m :: * -> *) k a.
Applicative m =>
Map k a -> (Map1 k a -> m ()) -> m ()
unlessNull = ((Map1 k a -> m ()) -> Map k a -> m ())
-> Map k a -> (Map1 k a -> m ()) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Map1 k a -> m ()) -> Map k a -> m ())
 -> Map k a -> (Map1 k a -> m ()) -> m ())
-> ((Map1 k a -> m ()) -> Map k a -> m ())
-> Map k a
-> (Map1 k a -> m ())
-> m ()
forall a b. (a -> b) -> a -> b
$ m () -> (Map1 k a -> m ()) -> Map k a -> m ()
forall r k a. r -> (NEMap k a -> r) -> Map k a -> r
Map1.withNonEmpty (m () -> (Map1 k a -> m ()) -> Map k a -> m ())
-> m () -> (Map1 k a -> m ()) -> Map k a -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE unlessNull #-}

unlessNullM :: Monad m => m (Map k a) -> (Map1 k a -> m ()) -> m ()
unlessNullM :: forall (m :: * -> *) k a.
Monad m =>
m (Map k a) -> (Map1 k a -> m ()) -> m ()
unlessNullM m (Map k a)
m Map1 k a -> m ()
k = m (Map k a)
m m (Map k a) -> (Map k a -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Map k a -> (Map1 k a -> m ()) -> m ()
forall (m :: * -> *) k a.
Applicative m =>
Map k a -> (Map1 k a -> m ()) -> m ()
`unlessNull` Map1 k a -> m ()
k)
{-# INLINE unlessNullM #-}