{-# OPTIONS_HADDOCK not-home #-}

module Hasura.Incremental.Select
  ( Select (..),
    ConstS (..),
    selectKey,
    FieldS (..),
    UniqueS,
    newUniqueS,
    DMapS (..),

    -- * Re-exports
    GEq (..),
    GCompare (..),
    GOrdering (..),
    (:~:) (..),
  )
where

import Control.Monad.Unique
import Data.Dependent.Map qualified as DM
import "some" Data.GADT.Compare
import Data.HashMap.Strict qualified as M
import Data.Kind
import Data.Proxy (Proxy (..))
import Data.Type.Equality
import GHC.OverloadedLabels (IsLabel (..))
import GHC.Records (HasField (..))
import GHC.TypeLits (KnownSymbol, sameSymbol, symbolVal)
import Hasura.Prelude
import Unsafe.Coerce (unsafeCoerce)

-- | The 'Select' class provides a way to access subparts of a product type using a reified
-- 'Selector'. A @'Selector' a b@ is essentially a function from @a@ to @b@, and indeed 'select'
-- converts a 'Selector' to such a function. However, unlike functions, 'Selector's can be compared
-- for equality using 'GEq' and ordered using 'GCompare'.
--
-- This is useful to implement dependency tracking, since it’s possible to track in a reified form
-- exactly which parts of a data structure are used.
--
-- Instances of 'Select' can be automatically derived for record types (just define an empty
-- instance). The instance uses the magical 'HasField' constraints, and 'Selector's for the type can
-- be written using @OverloadedLabels@.
class (GCompare (Selector a)) => Select a where
  type Selector a :: Type -> Type
  select :: Selector a b -> a -> b

  type Selector r = FieldS r
  default select :: Selector a ~ FieldS a => Selector a b -> a -> b
  select (FieldS (_ :: Proxy s)) = forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField s r a => r -> a
getField @s

instance (Eq k, Ord k, Hashable k) => Select (HashMap k v) where
  type Selector (HashMap k v) = ConstS k (Maybe v)
  select :: Selector (HashMap k v) b -> HashMap k v -> b
select (ConstS k) = k -> HashMap k v -> Maybe v
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
k

instance (GCompare k) => Select (DM.DMap k f) where
  type Selector (DM.DMap k f) = DMapS k f
  select :: Selector (DMap k f) b -> DMap k f -> b
select (DMapS k) = k a -> DMap k f -> Maybe (f a)
forall k1 (k2 :: k1 -> *) (f :: k1 -> *) (v :: k1).
GCompare k2 =>
k2 v -> DMap k2 f -> Maybe (f v)
DM.lookup k a
k

-- | The constant selector, which is useful for representing selectors into data structures where
-- all fields have the same type. Matching on a value of type @'ConstS' k a b@ causes @a@ and @b@ to
-- unify, effectively “pinning” @b@ to @a@.
data ConstS k a b where
  ConstS :: !k -> ConstS k a a

selectKey :: (Select a, Selector a ~ ConstS k v) => k -> a -> v
selectKey :: k -> a -> v
selectKey = ConstS k v v -> a -> v
forall a b. Select a => Selector a b -> a -> b
select (ConstS k v v -> a -> v) -> (k -> ConstS k v v) -> k -> a -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> ConstS k v v
forall k a. k -> ConstS k a a
ConstS

instance (Eq k) => GEq (ConstS k a) where
  ConstS k
a geq :: ConstS k a a -> ConstS k a b -> Maybe (a :~: b)
`geq` ConstS k
b
    | k
a k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
b = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance (Ord k) => GCompare (ConstS k a) where
  ConstS k
a gcompare :: ConstS k a a -> ConstS k a b -> GOrdering a b
`gcompare` ConstS k
b = case k -> k -> Ordering
forall a. Ord a => a -> a -> Ordering
compare k
a k
b of
    Ordering
LT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> GOrdering a b
forall k (a :: k). GOrdering a a
GEQ
    Ordering
GT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT

data FieldS r a where
  FieldS :: (KnownSymbol s, HasField s r a) => !(Proxy s) -> FieldS r a

instance (KnownSymbol s, HasField s r a) => IsLabel s (FieldS r a) where
  fromLabel :: FieldS r a
fromLabel = Proxy s -> FieldS r a
forall (s :: Symbol) r a.
(KnownSymbol s, HasField s r a) =>
Proxy s -> FieldS r a
FieldS (Proxy s
forall k (t :: k). Proxy t
Proxy @s)

instance GEq (FieldS r) where
  FieldS Proxy s
a geq :: FieldS r a -> FieldS r b -> Maybe (a :~: b)
`geq` FieldS Proxy s
b = case Proxy s -> Proxy s -> Maybe (s :~: s)
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol Proxy s
a Proxy s
b of
    -- If two fields of the same record have the same name, then their fields fundamentally must
    -- have the same type! However, unfortunately, `HasField` constraints use a functional
    -- dependency to enforce this rather than a type family, and functional dependencies don’t
    -- provide evidence, so we have to use `unsafeCoerce` here. Yuck!
    Just s :~: s
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
    Maybe (s :~: s)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare (FieldS r) where
  FieldS Proxy s
a gcompare :: FieldS r a -> FieldS r b -> GOrdering a b
`gcompare` FieldS Proxy s
b = case Proxy s -> Proxy s -> Maybe (s :~: s)
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol Proxy s
a Proxy s
b of
    -- See note about `HasField` and `unsafeCoerce` above.
    Just s :~: s
Refl -> GOrdering Any Any -> GOrdering a b
forall a b. a -> b
unsafeCoerce GOrdering Any Any
forall k (a :: k). GOrdering a a
GEQ
    Maybe (s :~: s)
Nothing
      | Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy s
a String -> String -> Bool
forall a. Ord a => a -> a -> Bool
< Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy s
b -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
      | Bool
otherwise -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT

-- | A 'UniqueS' is, as the name implies, a globally-unique 'Selector', which can be created using
-- 'newUniqueS'. If a value of type @'UniqueS' a@ is found to be equal (via 'geq') with another
-- value of type @'UniqueS' b@, then @a@ and @b@ must be the same type. This effectively allows the
-- creation of a dynamically-extensible sum type, where new constructors can be created at runtime
-- using 'newUniqueS'.
type role UniqueS nominal

newtype UniqueS a = UniqueS Unique
  deriving (UniqueS a -> UniqueS a -> Bool
(UniqueS a -> UniqueS a -> Bool)
-> (UniqueS a -> UniqueS a -> Bool) -> Eq (UniqueS a)
forall a. UniqueS a -> UniqueS a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UniqueS a -> UniqueS a -> Bool
$c/= :: forall a. UniqueS a -> UniqueS a -> Bool
== :: UniqueS a -> UniqueS a -> Bool
$c== :: forall a. UniqueS a -> UniqueS a -> Bool
Eq)

newUniqueS :: (MonadUnique m) => m (UniqueS a)
newUniqueS :: m (UniqueS a)
newUniqueS = Unique -> UniqueS a
forall a. Unique -> UniqueS a
UniqueS (Unique -> UniqueS a) -> m Unique -> m (UniqueS a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Unique
forall (m :: * -> *). MonadUnique m => m Unique
newUnique
{-# INLINE newUniqueS #-}

instance GEq UniqueS where
  UniqueS Unique
a geq :: UniqueS a -> UniqueS b -> Maybe (a :~: b)
`geq` UniqueS Unique
b
    -- This use of `unsafeCoerce` is safe as long as we don’t export the constructor of `UniqueS`.
    -- Because a `UniqueS` is, in fact, unique, then we can be certain that equality of 'UniqueS's
    -- implies equality of their argument types.
    | Unique
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
b = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
    | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare UniqueS where
  UniqueS Unique
a gcompare :: UniqueS a -> UniqueS b -> GOrdering a b
`gcompare` UniqueS Unique
b = case Unique -> Unique -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Unique
a Unique
b of
    Ordering
LT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
    -- See note about `unsafeCoerce` above.
    Ordering
EQ -> GOrdering Any Any -> GOrdering a b
forall a b. a -> b
unsafeCoerce GOrdering Any Any
forall k (a :: k). GOrdering a a
GEQ
    Ordering
GT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT

data DMapS k f a where
  DMapS :: !(k a) -> DMapS k f (Maybe (f a))

instance (GEq k) => GEq (DMapS k f) where
  DMapS k a
a geq :: DMapS k f a -> DMapS k f b -> Maybe (a :~: b)
`geq` DMapS k a
b = case k a
a k a -> k a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` k a
b of
    Just a :~: a
Refl -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    Maybe (a :~: a)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance (GCompare k) => GCompare (DMapS k f) where
  DMapS k a
a gcompare :: DMapS k f a -> DMapS k f b -> GOrdering a b
`gcompare` DMapS k a
b = case k a
a k a -> k a -> GOrdering a a
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
`gcompare` k a
b of
    GOrdering a a
GLT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
    GOrdering a a
GEQ -> GOrdering a b
forall k (a :: k). GOrdering a a
GEQ
    GOrdering a a
GGT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT