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

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 WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type
type role WitnessMapFor representational representational
newtype WitnessMapFor f w = MkWitnessMapFor
    { forall k (f :: k -> Type) (w :: k -> Type).
WitnessMapFor f w -> [SomeFor f w]
witnessMapForToList :: [SomeFor f w]
    } deriving newtype (NonEmpty (WitnessMapFor f w) -> WitnessMapFor f w
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
(WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w)
-> (NonEmpty (WitnessMapFor f w) -> WitnessMapFor f w)
-> (forall b.
    Integral b =>
    b -> WitnessMapFor f w -> WitnessMapFor f w)
-> Semigroup (WitnessMapFor f w)
forall b. Integral b => b -> WitnessMapFor f w -> WitnessMapFor 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).
NonEmpty (WitnessMapFor f w) -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type) b.
Integral b =>
b -> WitnessMapFor f w -> WitnessMapFor f w
$c<> :: forall k (f :: k -> Type) (w :: k -> Type).
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
<> :: WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
$csconcat :: forall k (f :: k -> Type) (w :: k -> Type).
NonEmpty (WitnessMapFor f w) -> WitnessMapFor f w
sconcat :: NonEmpty (WitnessMapFor f w) -> WitnessMapFor f w
$cstimes :: forall k (f :: k -> Type) (w :: k -> Type) b.
Integral b =>
b -> WitnessMapFor f w -> WitnessMapFor f w
stimes :: forall b. Integral b => b -> WitnessMapFor f w -> WitnessMapFor f w
Semigroup, Semigroup (WitnessMapFor f w)
WitnessMapFor f w
Semigroup (WitnessMapFor f w) =>
WitnessMapFor f w
-> (WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w)
-> ([WitnessMapFor f w] -> WitnessMapFor f w)
-> Monoid (WitnessMapFor f w)
[WitnessMapFor f w] -> WitnessMapFor f w
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall k (f :: k -> Type) (w :: k -> Type).
Semigroup (WitnessMapFor f w)
forall k (f :: k -> Type) (w :: k -> Type). WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[WitnessMapFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
$cmempty :: forall k (f :: k -> Type) (w :: k -> Type). WitnessMapFor f w
mempty :: WitnessMapFor f w
$cmappend :: forall k (f :: k -> Type) (w :: k -> Type).
WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
mappend :: WitnessMapFor f w -> WitnessMapFor f w -> WitnessMapFor f w
$cmconcat :: forall k (f :: k -> Type) (w :: k -> Type).
[WitnessMapFor f w] -> WitnessMapFor f w
mconcat :: [WitnessMapFor f w] -> WitnessMapFor f w
Monoid)

-- | An empty dictionary.
emptyWitnessMapFor :: WitnessMapFor f w
emptyWitnessMapFor :: forall k (f :: k -> Type) (w :: k -> Type). WitnessMapFor f w
emptyWitnessMapFor = WitnessMapFor f w
forall a. Monoid a => a
mempty

-- | Look up the first value in the dictionary that matches the given witness.
witnessMapForLookup :: TestEquality w => w a -> WitnessMapFor f w -> Maybe (f a)
witnessMapForLookup :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> WitnessMapFor f w -> Maybe (f a)
witnessMapForLookup w a
wit (MkWitnessMapFor [SomeFor f w]
cells) = [f a] -> Maybe (f a)
forall a. [a] -> Maybe a
listToMaybe ((SomeFor f w -> Maybe (f a)) -> [SomeFor f w] -> [f a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (w a -> SomeFor f w -> Maybe (f a)
forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> SomeFor f w -> Maybe (f a)
matchSomeFor w a
wit) [SomeFor f w]
cells)

-- | Modify the first value in the dictionary that matches a particular witness.
witnessMapForModify :: TestEquality w => w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForModify :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForModify w a
wit f a -> f a
amap (MkWitnessMapFor [SomeFor f w]
cells) =
    [SomeFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor ((SomeFor f w -> Maybe (SomeFor f w))
-> [SomeFor f w] -> [SomeFor f w]
forall a. (a -> Maybe a) -> [a] -> [a]
replaceFirst (((f a -> SomeFor f w) -> Maybe (f a) -> Maybe (SomeFor f w)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 -> SomeFor f w) -> (f a -> f a) -> f a -> SomeFor f w
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f a -> f a
amap)) (Maybe (f a) -> Maybe (SomeFor f w))
-> (SomeFor f w -> Maybe (f a))
-> SomeFor f w
-> Maybe (SomeFor f w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (w a -> SomeFor f w -> Maybe (f a)
forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> SomeFor f w -> Maybe (f a)
matchSomeFor w a
wit)) [SomeFor f w]
cells)
  where
    replaceFirst :: (a -> Maybe a) -> [a] -> [a]
    replaceFirst :: forall a. (a -> Maybe a) -> [a] -> [a]
replaceFirst a -> Maybe a
ama (a
a:[a]
aa) =
        case a -> Maybe a
ama a
a of
            Just a
newa -> (a
newa a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
aa)
            Maybe a
_ -> a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ((a -> Maybe a) -> [a] -> [a]
forall a. (a -> Maybe a) -> [a] -> [a]
replaceFirst a -> Maybe a
ama [a]
aa)
    replaceFirst a -> Maybe a
_ [a]
_ = []

-- | Replace the first value in the dictionary that matches the witness
witnessMapForReplace :: TestEquality w => w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForReplace :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForReplace w a
wit f a
newfa = w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForModify w a
wit (f a -> f a -> f a
forall a b. a -> b -> a
const f a
newfa)

-- | Add a witness and value as the first entry in the dictionary.
witnessMapForAdd :: w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForAdd :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForAdd w a
wit f a
fa (MkWitnessMapFor [SomeFor f w]
cells) = [SomeFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor ((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) SomeFor f w -> [SomeFor f w] -> [SomeFor f w]
forall a. a -> [a] -> [a]
: [SomeFor f w]
cells)

-- | A dictionary for a single witness and value
witnessMapForSingle :: w a -> f a -> WitnessMapFor f w
witnessMapForSingle :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
w a -> f a -> WitnessMapFor f w
witnessMapForSingle w a
wit f a
fa = [SomeFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor ([SomeFor f w] -> WitnessMapFor f w)
-> [SomeFor f w] -> WitnessMapFor f w
forall a b. (a -> b) -> a -> b
$ SomeFor f w -> [SomeFor f w]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SomeFor f w -> [SomeFor f w]) -> SomeFor f 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

witnessMapForFold :: Monoid m => WitnessMapFor f w -> (forall a. w a -> f a -> m) -> m
witnessMapForFold :: forall {k} m (f :: k -> Type) (w :: k -> Type).
Monoid m =>
WitnessMapFor f w -> (forall (a :: k). w a -> f a -> m) -> m
witnessMapForFold (MkWitnessMapFor [SomeFor f w]
cells) 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
wit f a
fa) -> w a -> f a -> m
forall (a :: k). w a -> f a -> m
f w a
wit f a
fa) [SomeFor f w]
cells

-- | Remove the first entry in the dictionary that matches the given witness.
witnessMapForRemove :: TestEquality w => w a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForRemove :: forall {k} (w :: k -> Type) (a :: k) (f :: k -> Type).
TestEquality w =>
w a -> WitnessMapFor f w -> WitnessMapFor f w
witnessMapForRemove w a
wit (MkWitnessMapFor [SomeFor f w]
cells) =
    [SomeFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor ((SomeFor f w -> Bool) -> [SomeFor f w] -> [SomeFor f w]
forall a. (a -> Bool) -> [a] -> [a]
removeFirst (\(MkSomeFor w a
cwit f a
_) -> Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (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
wit w a
cwit)) [SomeFor f w]
cells)
  where
    removeFirst :: (a -> Bool) -> [a] -> [a]
    removeFirst :: forall a. (a -> Bool) -> [a] -> [a]
removeFirst a -> Bool
p (a
a:[a]
as)
        | a -> Bool
p a
a = [a]
as
    removeFirst a -> Bool
p (a
a:[a]
as) = a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
removeFirst a -> Bool
p [a]
as)
    removeFirst a -> Bool
_ [a]
_ = []

-- | Create a dictionary from a list of witness\/value pairs
witnessMapForFromList :: [SomeFor f w] -> WitnessMapFor f w
witnessMapForFromList :: forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
witnessMapForFromList = [SomeFor f w] -> WitnessMapFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor

witnessMapForMapM :: Applicative m => (forall a. f a -> m (g a)) -> WitnessMapFor f w -> m (WitnessMapFor g w)
witnessMapForMapM :: forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (w :: k -> Type).
Applicative m =>
(forall (a :: k). f a -> m (g a))
-> WitnessMapFor f w -> m (WitnessMapFor g w)
witnessMapForMapM forall (a :: k). f a -> m (g a)
fmg (MkWitnessMapFor [SomeFor f w]
cells) =
    ([SomeFor g w] -> WitnessMapFor g w)
-> m [SomeFor g w] -> m (WitnessMapFor 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 [SomeFor g w] -> WitnessMapFor g w
forall k (f :: k -> Type) (w :: k -> Type).
[SomeFor f w] -> WitnessMapFor f w
MkWitnessMapFor (m [SomeFor g w] -> m (WitnessMapFor g w))
-> m [SomeFor g w] -> m (WitnessMapFor g w)
forall a b. (a -> b) -> a -> b
$ [SomeFor f w]
-> (SomeFor f w -> m (SomeFor g w)) -> m [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 [SomeFor f w]
cells ((SomeFor f w -> m (SomeFor g w)) -> m [SomeFor g w])
-> (SomeFor f w -> m (SomeFor g w)) -> m [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