module Data.Type.Witness.Specific.OrderedWitnessMap.For where

import qualified Data.Map as Map
import Data.Type.Witness.General.Order
import Data.Type.Witness.Specific.Some
import Import

-- | A dictionary that is heterogenous up to its simple witness type @w@.
-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.
type OrderedWitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
newtype OrderedWitnessMapFor f w =
    MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))
    deriving (NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
forall b.
Integral b =>
b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type) b.
(TestOrder w, Integral b) =>
b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
stimes :: forall b.
Integral b =>
b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
$cstimes :: forall k (f :: k -> Type) (w :: k -> Type) b.
(TestOrder w, Integral b) =>
b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
sconcat :: NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
$csconcat :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
<> :: OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
$c<> :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
Semigroup, OrderedWitnessMapFor f w
[OrderedWitnessMapFor f w] -> OrderedWitnessMapFor f w
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
Semigroup (OrderedWitnessMapFor f w)
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
[OrderedWitnessMapFor f w] -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
mconcat :: [OrderedWitnessMapFor f w] -> OrderedWitnessMapFor f w
$cmconcat :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
[OrderedWitnessMapFor f w] -> OrderedWitnessMapFor f w
mappend :: OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
$cmappend :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
mempty :: OrderedWitnessMapFor f w
$cmempty :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
Monoid)

-- | An empty dictionary.
emptyOrderedWitnessMapFor :: TestOrder w => OrderedWitnessMapFor f w
emptyOrderedWitnessMapFor :: forall {k} (w :: k -> Type) (f :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
emptyOrderedWitnessMapFor = forall a. Monoid a => a
mempty

-- | Look up the value in the dictionary that matches the given witness.
orderedWitnessMapForLookup :: TestOrder w => w a -> OrderedWitnessMapFor f w -> Maybe (f a)
orderedWitnessMapForLookup :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestOrder w =>
w a -> OrderedWitnessMapFor f w -> Maybe (f a)
orderedWitnessMapForLookup w a
wit (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
wmap) = do
    MkSomeFor w a
wa f a
fa <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) Map (Some w) (SomeFor f w)
wmap
    a :~: a
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wa w a
wit -- should always succeed
    forall (m :: Type -> Type) a. Monad m => a -> m a
return f a
fa

-- | Modify the value in the dictionary that matches a particular witness.
orderedWitnessMapForModify ::
       forall f w a. TestOrder w
    => w a
    -> (f a -> f a)
    -> OrderedWitnessMapFor f w
    -> OrderedWitnessMapFor f w
orderedWitnessMapForModify :: forall {k} (f :: k -> Type) (w :: k -> Type) (a :: k).
TestOrder w =>
w a
-> (f a -> f a)
-> OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w
orderedWitnessMapForModify w a
wit f a -> f a
amap (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
wmap) = let
    updater :: SomeFor f w -> Maybe (SomeFor f w)
    updater :: SomeFor f w -> Maybe (SomeFor f w)
updater (MkSomeFor w a
wa f a
fa) = do
        a :~: a
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wa w a
wit -- should always succeed
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
wa forall a b. (a -> b) -> a -> b
$ f a -> f a
amap f a
fa
    in forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update SomeFor f w -> Maybe (SomeFor f w)
updater (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) Map (Some w) (SomeFor f w)
wmap

-- | Replace the value in the dictionary that matches the witness
orderedWitnessMapForReplace :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForReplace :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestOrder w =>
w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForReplace w a
wit f a
newfa = forall {k} (f :: k -> Type) (w :: k -> Type) (a :: k).
TestOrder w =>
w a
-> (f a -> f a)
-> OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w
orderedWitnessMapForModify w a
wit (forall a b. a -> b -> a
const f a
newfa)

-- | Add a witness and value to the dictionary.
orderedWitnessMapForAdd :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForAdd :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestOrder w =>
w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForAdd w a
wit f a
fa (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
wmap) =
    forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) (forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
wit f a
fa) Map (Some w) (SomeFor f w)
wmap

-- | A dictionary for a single witness and value
orderedWitnessMapForSingle :: w a -> f a -> OrderedWitnessMapFor f w
orderedWitnessMapForSingle :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
w a -> f a -> OrderedWitnessMapFor f w
orderedWitnessMapForSingle w a
wit f a
fa = forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
wit f a
fa

orderedWitnessMapForFold :: Monoid m => OrderedWitnessMapFor f w -> (forall a. w a -> f a -> m) -> m
orderedWitnessMapForFold :: forall {k} m (f :: k -> Type) (w :: k -> Type).
Monoid m =>
OrderedWitnessMapFor f w -> (forall (a :: k). w a -> f a -> m) -> m
orderedWitnessMapForFold OrderedWitnessMapFor f w
wmf forall (a :: k). w a -> f a -> m
f = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkSomeFor w a
wa f a
fa) -> forall (a :: k). w a -> f a -> m
f w a
wa f a
fa) forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type) (w :: k -> Type).
OrderedWitnessMapFor f w -> [SomeFor f w]
orderedWitnessMapForToList OrderedWitnessMapFor f w
wmf

-- | Remove the entry in the dictionary that matches the given witness.
orderedWitnessMapForRemove :: TestOrder w => w a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForRemove :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestOrder w =>
w a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
orderedWitnessMapForRemove w a
wit (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
wmap) = forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) Map (Some w) (SomeFor f w)
wmap

orderedWitnessMapForToList :: OrderedWitnessMapFor f w -> [SomeFor f w]
orderedWitnessMapForToList :: forall {k} (f :: k -> Type) (w :: k -> Type).
OrderedWitnessMapFor f w -> [SomeFor f w]
orderedWitnessMapForToList (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
wmap) = forall k a. Map k a -> [a]
Map.elems Map (Some w) (SomeFor f w)
wmap

-- | Create a dictionary from a list of witness\/value pairs
orderedWitnessMapForFromList :: TestOrder w => [SomeFor f w] -> OrderedWitnessMapFor f w
orderedWitnessMapForFromList :: forall {k} (w :: k -> Type) (f :: k -> Type).
TestOrder w =>
[SomeFor f w] -> OrderedWitnessMapFor f w
orderedWitnessMapForFromList [SomeFor f w]
ee =
    forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\swf :: SomeFor f w
swf@(MkSomeFor w a
wa f a
_) -> (forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wa, SomeFor f w
swf)) [SomeFor f w]
ee

orderedWitnessMapForMapM ::
       Applicative m => (forall a. f a -> m (g a)) -> OrderedWitnessMapFor f w -> m (OrderedWitnessMapFor g w)
orderedWitnessMapForMapM :: forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (w :: k -> Type).
Applicative m =>
(forall (a :: k). f a -> m (g a))
-> OrderedWitnessMapFor f w -> m (OrderedWitnessMapFor g w)
orderedWitnessMapForMapM forall (a :: k). f a -> m (g a)
fmg (MkOrderedWitnessMapFor Map (Some w) (SomeFor f w)
cells) =
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Map (Some w) (SomeFor f w)
cells forall a b. (a -> b) -> a -> b
$ \(MkSomeFor w a
wit f a
fa) -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
wit) forall a b. (a -> b) -> a -> b
$ forall (a :: k). f a -> m (g a)
fmg f a
fa