-- Copyright 2018-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

-- | A 'Functor10' made by applying the argument to an existential type.

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}

module Data.Ten.Exists (Exists(..)) where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), TestEquality(..))

import Data.GADT.Compare (GEq(..), GCompare(..), GOrdering(..))
import Data.Hashable (Hashable(..))
import Data.Portray (Portray(..), Portrayal(..))
import Data.Portray.Diff (Diff(..), diffVs)

import Data.Ten.Functor (Functor10(..))
import Data.Ten.Foldable (Foldable10(..))
import Data.Ten.Traversable (Traversable10(..))

-- | A 'Functor10' made by applying the argument to an existential type.
data Exists (m :: k -> Type) where
  Exists :: forall a m. m a -> Exists m

deriving stock instance (forall a. Show (m a)) => Show (Exists m)

instance GEq m => Eq (Exists m) where
  Exists m a
x == :: Exists m -> Exists m -> Bool
== Exists m a
y = case m a -> m a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq m a
x m a
y of
    Maybe (a :~: a)
Nothing -> Bool
False
    Just a :~: a
_ -> Bool
True

instance GCompare m => Ord (Exists m) where
  compare :: Exists m -> Exists m -> Ordering
compare (Exists m a
x) (Exists m a
y) = case m a -> m a -> GOrdering a a
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare m a
x m a
y of
    GOrdering a a
GLT -> Ordering
LT
    GOrdering a a
GEQ -> Ordering
EQ
    GOrdering a a
GGT -> Ordering
GT

instance (forall a. Hashable (m a)) => Hashable (Exists m) where
  hashWithSalt :: Int -> Exists m -> Int
hashWithSalt Int
s (Exists m a
ka) = Int -> m a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s m a
ka

instance (forall a. Portray (m a)) => Portray (Exists m) where
  portray :: Exists m -> Portrayal
portray (Exists m a
x) = Portrayal -> [Portrayal] -> Portrayal
Apply (Ident -> Portrayal
Name Ident
"Exists") [m a -> Portrayal
forall a. Portray a => a -> Portrayal
portray m a
x]

-- N.B. we do actually want TestEquality rather than GEq here, because we want
-- to diff same-typed-but-not-equal values according to their Diff instances.
instance (TestEquality m, forall a. Portray (m a), forall a. Diff (m a))
      => Diff (Exists m) where
  diff :: Exists m -> Exists m -> Maybe Portrayal
diff (Exists m a
x) (Exists m a
y) = case m a -> m a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality m a
x m a
y of
    Just a :~: a
Refl -> m a -> m a -> Maybe Portrayal
forall a. Diff a => a -> a -> Maybe Portrayal
diff m a
x m a
m a
y
    Maybe (a :~: a)
Nothing   -> Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just (Portrayal -> Maybe Portrayal) -> Portrayal -> Maybe Portrayal
forall a b. (a -> b) -> a -> b
$ m a -> Portrayal
forall a. Portray a => a -> Portrayal
portray m a
x Portrayal -> Portrayal -> Portrayal
`diffVs` m a -> Portrayal
forall a. Portray a => a -> Portrayal
portray m a
y

instance Functor10 Exists where
  fmap10 :: (forall (a :: k). m a -> n a) -> Exists m -> Exists n
fmap10 forall (a :: k). m a -> n a
f (Exists m a
x) = n a -> Exists n
forall k (a :: k) (m :: k -> *). m a -> Exists m
Exists (m a -> n a
forall (a :: k). m a -> n a
f m a
x)

instance Foldable10 Exists where
  foldMap10 :: (forall (a :: k). m a -> w) -> Exists m -> w
foldMap10 forall (a :: k). m a -> w
f (Exists m a
x) = m a -> w
forall (a :: k). m a -> w
f m a
x

instance Traversable10 Exists where
  mapTraverse10 :: (Exists n -> r)
-> (forall (a :: k). m a -> f (n a)) -> Exists m -> f r
mapTraverse10 Exists n -> r
r forall (a :: k). m a -> f (n a)
f (Exists m a
x) = Exists n -> r
r (Exists n -> r) -> (n a -> Exists n) -> n a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n a -> Exists n
forall k (a :: k) (m :: k -> *). m a -> Exists m
Exists (n a -> r) -> f (n a) -> f r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> f (n a)
forall (a :: k). m a -> f (n a)
f m a
x