{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms        #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}
module Options.Harg.Het.Variant where

import           Data.Kind            (Type)

import qualified Data.Barbie          as B

import           Options.Harg.Het.Nat


-- | A Variant is similar to nested 'Either's. For example, @Variant '[Int,
-- Bool, Char]@ is isomorphic to @Either Int (Either Bool Char)@. 'VariantF'
-- is a variant for higher-kinded types, which means that the type-level list
-- holds types of kind @(Type -> Type) -> Type@, and the second parameter is
-- the type constructor @f :: Type -> Type@. To pattern match on a variant,
-- @HereF@ and @ThereF@ can be used:
--
-- @
--   getFromVariant :: Variant '[Int, Bool, String] -> Bool
--   getFromVariant (ThereF (HereF b)) = b
-- @
--
data VariantF (xs :: [(Type -> Type) -> Type]) (f :: Type -> Type) where
  HereF  :: x f           -> VariantF (x ': xs) f
  ThereF :: VariantF xs f -> VariantF (y ': xs) f

instance
    ( B.FunctorB x
    , B.FunctorB (VariantF xs)
    ) => B.FunctorB (VariantF (x ': xs)) where
  bmap nat (HereF x)   = HereF $ B.bmap nat x
  bmap nat (ThereF xs) = ThereF $ B.bmap nat xs

instance B.FunctorB (VariantF '[]) where
  bmap _ _ = error "Impossible: empty variant"

instance
    ( B.TraversableB x
    , B.TraversableB (VariantF xs)
    ) => B.TraversableB (VariantF (x ': xs)) where
  btraverse nat (HereF x)   = HereF <$> B.btraverse nat x
  btraverse nat (ThereF xs) = ThereF <$> B.btraverse nat xs

instance B.TraversableB (VariantF '[]) where
  btraverse _ _ = error "Impossible: empty variant"

-- * Helpers for pattern-matching on variants
pattern In1 :: x1 f -> VariantF (x1 ': xs) f
pattern In1 x = HereF x

pattern In2 :: x2 f -> VariantF (x1 ': x2 ': xs) f
pattern In2 x = ThereF (In1 x)

pattern In3 :: x3 f -> VariantF (x1 ': x2 ': x3 ': xs) f
pattern In3 x = ThereF (In2 x)

pattern In4 :: x4 f -> VariantF (x1 ': x2 ': x3 ': x4 ': xs) f
pattern In4 x = ThereF (In3 x)

pattern In5 :: x5 f -> VariantF (x1 ': x2 ': x3 ': x4 ': x5 ': xs) f
pattern In5 x = ThereF (In4 x)

-- https://github.com/i-am-tom/learn-me-a-haskell/blob/master/src/OneOf/Fold.hs
-- | Create the signature needed for 'FromVariantF' to work. This constructs a
-- function that takes as arguments functions that can act upon each item in
-- the list that the 'VariantF' holds. For example, @VariantF [a, b, c]
-- f@ will result to the signature:
--
-- @
--   VariantF [a, b, c] f -> (a f -> r) -> (b f -> r) -> (c f -> r) -> r
-- @
--
type family FoldSignatureF (xs :: [(Type -> Type) -> Type]) r f where
  FoldSignatureF (x ': xs) r f = (x f -> r) -> FoldSignatureF xs r f
  FoldSignatureF '[] r f = r

class FromVariantF xs result f where
  fromVariantF :: VariantF xs f -> FoldSignatureF xs result f

instance FromVariantF '[x] result f where
  fromVariantF (HereF  x) f = f x
  fromVariantF (ThereF _) _ = error "Impossible: empty variant"

instance
    ( tail ~ (x' ': xs)
    , FromVariantF tail result f
    , IgnoreF tail result f
    ) => FromVariantF (x ': x' ': xs) result f where
  fromVariantF (ThereF x) _ = fromVariantF @_ @result x
  fromVariantF (HereF  x) f = ignoreF @tail (f x)

class IgnoreF (args :: [(Type -> Type) -> Type]) result f where
  ignoreF :: result -> FoldSignatureF args result f

instance IgnoreF '[] result f where
  ignoreF result = result

instance IgnoreF xs result f => IgnoreF (x ': xs) result f where
  ignoreF result _ = ignoreF @xs @_ @f result

-- | Given a type-level natural that designates a position of injection into
-- a 'VariantF', return a function that performs this injection. For example,
-- @S Z@ which corresponds to 1 or the second position in the type-level list
-- the variant holds, can give the injection @b f -> VariantF [a, b, c] f@.
-- The injection can as well be constructed without providing the position, but
-- it helps in case @x@ is not unique in @xs@.
class InjectPosF
    (n :: Nat)
    (x :: (Type -> Type) -> Type)
    (xs :: [(Type -> Type) -> Type])
    | n xs -> x where
  injectPosF :: SNat n -> (x f -> VariantF xs f)

instance InjectPosF Z x (x ': xs) where
  injectPosF SZ = HereF

instance InjectPosF n x xs => InjectPosF (S n) x (y ': xs) where
  injectPosF (SS n) = ThereF . injectPosF n