module Morley.Util.Sing
( eqI
, eqParamSing
, eqParamSing2
, eqParamSing3
, eqParamMixed3
, castSing
, SingI1(..)
) where
import Data.Singletons (KindOf, Sing, SingI, sing)
import Data.Singletons.Decide (SDecide, decideEquality)
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Typeable (eqT)
eqI :: forall a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a))) => Maybe (a :~: b)
eqI :: 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 (SingI a => Sing a
forall k (a :: k). SingI a => Sing a
sing @a) (SingI b => Sing b
forall k (a :: k). SingI a => Sing a
sing @b)
eqParamSing ::
forall a1 a2 t.
( SingI a1
, SingI a2
, SDecide (KindOf a1)
, Eq (t a1)
)
=> t a1
-> t a2
-> Bool
eqParamSing :: t a1 -> t a2 -> Bool
eqParamSing t a1
t1 t a2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- SingI a1 => Sing a1
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` SingI a2 => Sing a2
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)
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 :: t a1 b1 -> t a2 b2 -> Bool
eqParamSing2 t a1 b1
t1 t a2 b2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- SingI a1 => Sing a1
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` SingI a2 => Sing a2
forall k (a :: k). SingI a => Sing a
sing @a2
b1 :~: b2
Refl <- SingI b1 => Sing b1
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` SingI b2 => Sing b2
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)
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 :: t a1 b1 c1 -> t a2 b2 c2 -> Bool
eqParamSing3 t a1 b1 c1
t1 t a2 b2 c2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- SingI a1 => Sing a1
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` SingI a2 => Sing a2
forall k (a :: k). SingI a => Sing a
sing @a2
b1 :~: b2
Refl <- SingI b1 => Sing b1
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` SingI b2 => Sing b2
forall k (a :: k). SingI a => Sing a
sing @b2
c1 :~: c2
Refl <- SingI c1 => Sing c1
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` SingI c2 => Sing c2
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)
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 :: t instr1 a1 b1 -> t instr2 a2 b2 -> Bool
eqParamMixed3 t instr1 a1 b1
t1 t instr2 a2 b2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
instr1 :~: instr2
Refl <- (Typeable instr1, Typeable instr2) => Maybe (instr1 :~: instr2)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @instr1 @instr2
a1 :~: a2
Refl <- SingI a1 => Sing a1
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` SingI a2 => Sing a2
forall k (a :: k). SingI a => Sing a
sing @a2
b1 :~: b2
Refl <- SingI b1 => Sing b1
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` SingI b2 => Sing b2
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 :: t a -> Maybe (t b)
castSing t a
ca = do
a :~: b
Refl <- 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` SingI b => Sing b
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
class SingI1 f where
withSingI1 :: forall x r. SingI x => (SingI (f x) => r) -> r