-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

module Morley.Util.Sing
  ( eqI
  , geqI
  , eqParamSing
  , eqParamSing2
  , eqParamSing3
  , eqParamMixed3
  , castSing
  , SingIOne
  , withSingIOne
  , genSingletonsType
  ) where

import Data.Singletons (KindOf, Sing, SingI, sing)
import Data.Singletons.Decide (SDecide, decideEquality)
import Data.Singletons.TH (genSingletons, singDecideInstance)
import Data.Singletons.TH.Options (Options(..), OptionsMonad, defaultOptions, withOptions)
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Typeable (eqT)
import Language.Haskell.TH (Dec, Name, mkName, nameBase)

-- | Version of 'testEquality' that uses 'SingI'
eqI :: forall a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a))) => Maybe (a :~: b)
eqI :: forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI = Sing a -> Sing b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a) (forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b)

-- | Suppose you have a data type @X@ with parameter @a@ and you have
-- two values: @x1 :: X a1@ and @x2 :: X a2@. You can't compare them
-- using '==', because they have different types. However, you can
-- compare them using 'eqParamSing' as long as both parameters have
-- SingI instances and their kind is `SDecide`.
eqParamSing ::
  forall a1 a2 t.
  ( SingI a1
  , SingI a2
  , SDecide (KindOf a1)
  , Eq (t a1)
  )
  => t a1
  -> t a2
  -> Bool
eqParamSing :: forall {k} (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
eqParamSing t a1
t1 t a2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a1 Sing a1 -> Sing a2 -> Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a2
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1
t1 t a1 -> t a1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1
t a2
t2)

-- | Version of 'eqParamSing' for types with 2 parameters.
eqParamSing2 ::
  forall a1 a2 b1 b2 t.
  ( SingI a1
  , SingI a2
  , SingI b1
  , SingI b2
  , SDecide (KindOf a1)
  , SDecide (KindOf b1)
  , Eq (t a1 b2)
  )
  => t a1 b1
  -> t a2 b2
  -> Bool
eqParamSing2 :: forall {k} {k} (a1 :: k) (a2 :: k) (b1 :: k) (b2 :: k)
       (t :: k -> k -> *).
(SingI a1, SingI a2, SingI b1, SingI b2, SDecide k, SDecide k,
 Eq (t a1 b2)) =>
t a1 b1 -> t a2 b2 -> Bool
eqParamSing2 t a1 b1
t1 t a2 b2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a1 Sing a1 -> Sing a2 -> Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a2
  b1 :~: b2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b1 Sing b1 -> Sing b2 -> Maybe (b1 :~: b2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b2
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1 b1
t1 t a1 b1 -> t a1 b1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1 b1
t a2 b2
t2)

-- | Version of 'eqParamSing' for types with 3 parameters.
eqParamSing3 ::
  forall a1 a2 b1 b2 c1 c2 t.
  ( SingI a1
  , SingI a2
  , SingI b1
  , SingI b2
  , SingI c1
  , SingI c2
  , SDecide (KindOf a1)
  , SDecide (KindOf b1)
  , SDecide (KindOf c1)
  , Eq (t a1 b1 c1)
  )
  => t a1 b1 c1
  -> t a2 b2 c2
  -> Bool
eqParamSing3 :: forall {k} {k} {k} (a1 :: k) (a2 :: k) (b1 :: k) (b2 :: k)
       (c1 :: k) (c2 :: k) (t :: k -> k -> k -> *).
(SingI a1, SingI a2, SingI b1, SingI b2, SingI c1, SingI c2,
 SDecide k, SDecide k, SDecide k, Eq (t a1 b1 c1)) =>
t a1 b1 c1 -> t a2 b2 c2 -> Bool
eqParamSing3 t a1 b1 c1
t1 t a2 b2 c2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a1 Sing a1 -> Sing a2 -> Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a2
  b1 :~: b2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b1 Sing b1 -> Sing b2 -> Maybe (b1 :~: b2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b2
  c1 :~: c2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @c1 Sing c1 -> Sing c2 -> Maybe (c1 :~: c2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @c2
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1 b1 c1
t1 t a1 b1 c1 -> t a1 b1 c1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1 b1 c1
t a2 b2 c2
t2)

-- | Version of 'eqParamSing' for types with 3 parameters.
eqParamMixed3 ::
  forall instr1 instr2 a1 a2 b1 b2 t.
  ( Typeable instr1
  , Typeable instr2
  , SingI a1
  , SingI a2
  , SingI b1
  , SingI b2
  , SDecide (KindOf a1)
  , SDecide (KindOf b1)
  , Eq (t instr1 a1 b1)
  )
  => t instr1 a1 b1
  -> t instr2 a2 b2
  -> Bool
eqParamMixed3 :: forall {k} {k} {k} (instr1 :: k) (instr2 :: k) (a1 :: k) (a2 :: k)
       (b1 :: k) (b2 :: k) (t :: k -> k -> k -> *).
(Typeable instr1, Typeable instr2, SingI a1, SingI a2, SingI b1,
 SingI b2, SDecide k, SDecide k, Eq (t instr1 a1 b1)) =>
t instr1 a1 b1 -> t instr2 a2 b2 -> Bool
eqParamMixed3 t instr1 a1 b1
t1 t instr2 a2 b2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  instr1 :~: instr2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @instr1 @instr2
  a1 :~: a2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a1 Sing a1 -> Sing a2 -> Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a2
  b1 :~: b2
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b1 Sing b1 -> Sing b2 -> Maybe (b1 :~: b2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b2
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t instr1 a1 b1
t1 t instr1 a1 b1 -> t instr1 a1 b1 -> Bool
forall a. Eq a => a -> a -> Bool
== t instr1 a1 b1
t instr2 a2 b2
t2)

castSing :: forall a b t.
  (SingI a, SingI b, SDecide (KindOf a))
  => t a
  -> Maybe (t b)
castSing :: forall {k} (a :: k) (b :: k) (t :: k -> *).
(SingI a, SingI b, SDecide k) =>
t a -> Maybe (t b)
castSing t a
ca = do
  a :~: b
Refl <- forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @a Sing a -> Sing b -> Maybe (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @b
  t a -> Maybe (t a)
forall (m :: * -> *) a. Monad m => a -> m a
return t a
ca

-- | A second-order analogue of 'SingI'. This serves the same purpose as the
-- @"Data.Singletons".'Data.Singletons.SingIOne'@ class. However, the @singletons@
-- version requires a separate instance for each type in order to support GHC
-- versions that don't offer @QuantifiedConstraints@. We only need one instance
-- for all types.
class (forall x. SingI x => SingI (f x)) => SingIOne f
instance (forall x. SingI x => SingI (f x)) => SingIOne f

withSingIOne :: forall f x r. (SingIOne f, SingI x) => (SingI (f x) => r) -> r
withSingIOne :: forall {k} {k} (f :: k -> k) (x :: k) r.
(SingIOne f, SingI x) =>
(SingI (f x) => r) -> r
withSingIOne SingI (f x) => r
f = r
SingI (f x) => r
f

-- | Helper function to generate 'SingI' and 'Data.Singletons.TH.SDecide' instances
-- using @Sing@ as prefix for the type names and @S@ for constructors'.
genSingletonsType :: OptionsMonad q => Name -> q [Dec]
genSingletonsType :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
genSingletonsType Name
name =
  let
    singPrefix, sPrefix :: Name -> Name
    singPrefix :: Name -> Name
singPrefix Name
nm = [Char] -> Name
mkName ([Char]
"Sing" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
nameBase Name
nm)
    sPrefix :: Name -> Name
sPrefix Name
nm = [Char] -> Name
mkName ([Char]
"S" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
nameBase Name
nm)
  in
    Options -> OptionsM q [Dec] -> q [Dec]
forall (m :: * -> *) a. Options -> OptionsM m a -> m a
withOptions Options
defaultOptions{singledDataConName :: Name -> Name
singledDataConName = Name -> Name
sPrefix, singledDataTypeName :: Name -> Name
singledDataTypeName = Name -> Name
singPrefix} (OptionsM q [Dec] -> q [Dec]) -> OptionsM q [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$
    [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> OptionsM q [[Dec]] -> OptionsM q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [OptionsM q [Dec]] -> OptionsM q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
      [ [Name] -> OptionsM q [Dec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
genSingletons [Name
name], Name -> OptionsM q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
singDecideInstance Name
name]

-- | Singleton-based implementation of @geq@
geqI
  :: forall f a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a)), Eq (f b))
  => f a -> f b -> Maybe (a :~: b)
geqI :: forall {k} (f :: k -> *) (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing, Eq (f b)) =>
f a -> f b -> Maybe (a :~: b)
geqI f a
l f b
r = case forall (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @a @b of
  Just a :~: b
Refl | f a
l f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f b
r -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall {k} (a :: k). a :~: a
Refl
  Maybe (a :~: b)
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing