{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE UndecidableInstances #-}

{- | An open sum implementation for value types.
-}

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 )

-- | Open sum of value types
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)

-- | Safely inject and project a value into an open sum
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