{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE UndecidableInstances #-}
module OpenSum (
OpenSum(..)
, Member(..)) where
import Data.Kind (Type, Constraint)
import Data.Typeable ( Typeable )
import FindElem ( Idx(..), FindElem(..) )
import GHC.TypeLits (Nat, KnownNat, natVal, TypeError, ErrorMessage (Text, (:$$:), (:<>:), ShowType))
import qualified GHC.TypeLits as TL
import Unsafe.Coerce ( unsafeCoerce )
data OpenSum (as :: [*]) where
UnsafeOpenSum :: Int -> a -> OpenSum as
instance Eq (OpenSum '[]) where
OpenSum '[]
x == :: OpenSum '[] -> OpenSum '[] -> Bool
== OpenSum '[]
_ = case OpenSum '[]
x of {}
instance forall a as. (Eq a, Eq (OpenSum as)) => Eq (OpenSum (a : as)) where
UnsafeOpenSum Int
i a
_ == :: OpenSum (a : as) -> OpenSum (a : as) -> Bool
== UnsafeOpenSum Int
j a
_ | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j = Bool
False
UnsafeOpenSum Int
0 a
x == UnsafeOpenSum Int
0 a
y =
a -> a
forall a b. a -> b
unsafeCoerce a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a
forall a b. a -> b
unsafeCoerce a
y :: a)
UnsafeOpenSum Int
i a
x == UnsafeOpenSum Int
j a
y =
Int -> a -> OpenSum as
forall a (as :: [*]). Int -> a -> OpenSum as
UnsafeOpenSum (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) a
x OpenSum as -> OpenSum as -> Bool
forall a. Eq a => a -> a -> Bool
== (Int -> a -> OpenSum as
forall a (as :: [*]). Int -> a -> OpenSum as
UnsafeOpenSum (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) a
y :: OpenSum as)
instance forall a as. (Show a, Show (OpenSum as)) => Show (OpenSum (a : as)) where
show :: OpenSum (a : as) -> String
show (UnsafeOpenSum Int
i a
a) =
if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then a -> String
forall a. Show a => a -> String
show (a -> a
forall a b. a -> b
unsafeCoerce a
a :: a)
else OpenSum as -> String
forall a. Show a => a -> String
show (Int -> a -> OpenSum as
forall a (as :: [*]). Int -> a -> OpenSum as
UnsafeOpenSum (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) a
a :: OpenSum as)
instance {-# OVERLAPPING #-} Show a => Show (OpenSum '[a]) where
show :: OpenSum '[a] -> String
show (UnsafeOpenSum Int
i a
a) = a -> String
forall a. Show a => a -> String
show (a -> a
forall a b. a -> b
unsafeCoerce a
a :: a)
class (FindElem a as) => Member (a :: *) (as :: [*]) where
inj :: a -> OpenSum as
prj :: OpenSum as -> Maybe a
instance (Typeable a, a ~ a') => Member a '[a'] where
inj :: a -> OpenSum '[a']
inj a
x = Int -> a -> OpenSum '[a']
forall a (as :: [*]). Int -> a -> OpenSum as
UnsafeOpenSum Int
0 a
x
prj :: OpenSum '[a'] -> Maybe a
prj (UnsafeOpenSum Int
_ a
x) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a b. a -> b
unsafeCoerce a
x)
instance (FindElem a as) => Member a as where
inj :: a -> OpenSum as
inj = Int -> a -> OpenSum as
forall a (as :: [*]). Int -> a -> OpenSum as
UnsafeOpenSum (Idx a as -> Int
forall {k1} {k2} (x :: k1) (xs :: k2). Idx x xs -> Int
unIdx (Idx a as
forall {k} {k} (x :: k) (xs :: k). FindElem x xs => Idx x xs
findElem :: Idx a as))
prj :: OpenSum as -> Maybe a
prj = Int -> OpenSum as -> Maybe a
forall {as :: [*]} {a}. Int -> OpenSum as -> Maybe a
prj' (Idx a as -> Int
forall {k1} {k2} (x :: k1) (xs :: k2). Idx x xs -> Int
unIdx (Idx a as
forall {k} {k} (x :: k) (xs :: k). FindElem x xs => Idx x xs
findElem :: Idx a as))
where prj' :: Int -> OpenSum as -> Maybe a
prj' Int
n (UnsafeOpenSum Int
n' a
x)
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a b. a -> b
unsafeCoerce a
x)
| Bool
otherwise = Maybe a
forall a. Maybe a
Nothing