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

import Data.Map qualified 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
type role OrderedWitnessMapFor representational nominal
newtype OrderedWitnessMapFor f w =
    MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))
    deriving newtype (NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
(OrderedWitnessMapFor f w
 -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w)
-> (NonEmpty (OrderedWitnessMapFor f w)
    -> OrderedWitnessMapFor f w)
-> (forall b.
    Integral b =>
    b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w)
-> Semigroup (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
$c<> :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
<> :: OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
$csconcat :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
NonEmpty (OrderedWitnessMapFor f w) -> OrderedWitnessMapFor f w
sconcat :: NonEmpty (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
stimes :: forall b.
Integral b =>
b -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
Semigroup, Semigroup (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] -> OrderedWitnessMapFor f w)
-> Monoid (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
$cmempty :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
mempty :: OrderedWitnessMapFor f w
$cmappend :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
mappend :: OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w
$cmconcat :: forall k (f :: k -> Type) (w :: k -> Type).
TestOrder w =>
[OrderedWitnessMapFor f w] -> OrderedWitnessMapFor f w
mconcat :: [OrderedWitnessMapFor f 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 = OrderedWitnessMapFor f w
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 <- Some w -> Map (Some w) (SomeFor f w) -> Maybe (SomeFor f w)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (w a -> Some w
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 <- w a -> w a -> Maybe (a :~: a)
forall (a :: k) (b :: k). w a -> w b -> Maybe (a :~: b)
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
    f a -> Maybe (f a)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return f a
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 <- w a -> w a -> Maybe (a :~: a)
forall (a :: k) (b :: k). w a -> w b -> Maybe (a :~: b)
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
        SomeFor f w -> Maybe (SomeFor f w)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SomeFor f w -> Maybe (SomeFor f w))
-> SomeFor f w -> Maybe (SomeFor f w)
forall a b. (a -> b) -> a -> b
$ w a -> f a -> SomeFor f w
forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
w a
wa (f a -> SomeFor f w) -> f a -> SomeFor f w
forall a b. (a -> b) -> a -> b
$ f a -> f a
amap f a
f a
fa
    in Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w)
-> Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ (SomeFor f w -> Maybe (SomeFor f w))
-> Some w
-> Map (Some w) (SomeFor f w)
-> Map (Some w) (SomeFor f w)
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 (w a -> Some w
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 = w a
-> (f a -> f a)
-> OrderedWitnessMapFor f w
-> OrderedWitnessMapFor f w
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 -> f a
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) =
    Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w)
-> Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ Some w
-> SomeFor f w
-> Map (Some w) (SomeFor f w)
-> Map (Some w) (SomeFor f w)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (w a -> Some w
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) (w a -> f a -> SomeFor f w
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 = Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w)
-> Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ Some w -> SomeFor f w -> Map (Some w) (SomeFor f w)
forall k a. k -> a -> Map k a
Map.singleton (w a -> Some w
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w a
wit) (SomeFor f w -> Map (Some w) (SomeFor f w))
-> SomeFor f w -> Map (Some w) (SomeFor f w)
forall a b. (a -> b) -> a -> b
$ w a -> f a -> SomeFor f w
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 = [m] -> m
forall a. Monoid a => [a] -> a
mconcat ([m] -> m) -> [m] -> m
forall a b. (a -> b) -> a -> b
$ (SomeFor f w -> m) -> [SomeFor f w] -> [m]
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) -> w a -> f a -> m
forall (a :: k). w a -> f a -> m
f w a
wa f a
fa) ([SomeFor f w] -> [m]) -> [SomeFor f w] -> [m]
forall a b. (a -> b) -> a -> b
$ OrderedWitnessMapFor f w -> [SomeFor f w]
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) = Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w)
-> Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ Some w -> Map (Some w) (SomeFor f w) -> Map (Some w) (SomeFor f w)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (w a -> Some w
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) = Map (Some w) (SomeFor f w) -> [SomeFor f w]
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 =
    Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w)
-> Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ [(Some w, SomeFor f w)] -> Map (Some w) (SomeFor f w)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Some w, SomeFor f w)] -> Map (Some w) (SomeFor f w))
-> [(Some w, SomeFor f w)] -> Map (Some w) (SomeFor f w)
forall a b. (a -> b) -> a -> b
$ (SomeFor f w -> (Some w, SomeFor f w))
-> [SomeFor f w] -> [(Some w, SomeFor f w)]
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
_) -> (w a -> Some w
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) =
    (Map (Some w) (SomeFor g w) -> OrderedWitnessMapFor g w)
-> m (Map (Some w) (SomeFor g w)) -> m (OrderedWitnessMapFor g w)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Map (Some w) (SomeFor g w) -> OrderedWitnessMapFor g w
forall k (f :: k -> Type) (w :: k -> Type).
Map (Some w) (SomeFor f w) -> OrderedWitnessMapFor f w
MkOrderedWitnessMapFor (m (Map (Some w) (SomeFor g w)) -> m (OrderedWitnessMapFor g w))
-> m (Map (Some w) (SomeFor g w)) -> m (OrderedWitnessMapFor g w)
forall a b. (a -> b) -> a -> b
$ Map (Some w) (SomeFor f w)
-> (SomeFor f w -> m (SomeFor g w))
-> m (Map (Some w) (SomeFor g w))
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 ((SomeFor f w -> m (SomeFor g w))
 -> m (Map (Some w) (SomeFor g w)))
-> (SomeFor f w -> m (SomeFor g w))
-> m (Map (Some w) (SomeFor g w))
forall a b. (a -> b) -> a -> b
$ \(MkSomeFor w a
wit f a
fa) -> (g a -> SomeFor g w) -> m (g a) -> m (SomeFor g w)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (w a -> g a -> SomeFor g w
forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor w a
wit) (m (g a) -> m (SomeFor g w)) -> m (g a) -> m (SomeFor g w)
forall a b. (a -> b) -> a -> b
$ f a -> m (g a)
forall (a :: k). f a -> m (g a)
fmg f a
fa