{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Options.Harg.Het.Variant
  ( VariantF (..),
    fromVariantF,
    InjectPosF (..),
    pattern In1,
    pattern In2,
    pattern In3,
    pattern In4,
    pattern In5,
  )
where

import qualified Barbies as B
import Data.Kind (Type)
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 :: (forall a. f a -> g a)
-> VariantF (x : xs) f -> VariantF (x : xs) g
bmap nat :: forall a. f a -> g a
nat (HereF x :: x f
x) = x g -> VariantF (x : xs) g
forall (x :: (* -> *) -> *) (f :: * -> *) (xs :: [(* -> *) -> *]).
x f -> VariantF (x : xs) f
HereF (x g -> VariantF (x : xs) g) -> x g -> VariantF (x : xs) g
forall a b. (a -> b) -> a -> b
$ (forall a. f a -> g a) -> x f -> x g
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
B.bmap forall a. f a -> g a
nat x f
x
  bmap nat :: forall a. f a -> g a
nat (ThereF xs :: VariantF xs f
xs) = VariantF xs g -> VariantF (x : xs) g
forall (xs :: [(* -> *) -> *]) (f :: * -> *) (y :: (* -> *) -> *).
VariantF xs f -> VariantF (y : xs) f
ThereF (VariantF xs g -> VariantF (x : xs) g)
-> VariantF xs g -> VariantF (x : xs) g
forall a b. (a -> b) -> a -> b
$ (forall a. f a -> g a) -> VariantF xs f -> VariantF xs g
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
B.bmap forall a. f a -> g a
nat VariantF xs f
xs

instance B.FunctorB (VariantF '[]) where
  bmap :: (forall a. f a -> g a) -> VariantF '[] f -> VariantF '[] g
bmap _ _ = [Char] -> VariantF '[] g
forall a. HasCallStack => [Char] -> a
error "Impossible: empty variant"

instance
  ( B.TraversableB x,
    B.TraversableB (VariantF xs)
  ) =>
  B.TraversableB (VariantF (x ': xs))
  where
  btraverse :: (forall a. f a -> e (g a))
-> VariantF (x : xs) f -> e (VariantF (x : xs) g)
btraverse nat :: forall a. f a -> e (g a)
nat (HereF x :: x f
x) = x g -> VariantF (x : xs) g
forall (x :: (* -> *) -> *) (f :: * -> *) (xs :: [(* -> *) -> *]).
x f -> VariantF (x : xs) f
HereF (x g -> VariantF (x : xs) g) -> e (x g) -> e (VariantF (x : xs) g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. f a -> e (g a)) -> x f -> e (x g)
forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
B.btraverse forall a. f a -> e (g a)
nat x f
x
  btraverse nat :: forall a. f a -> e (g a)
nat (ThereF xs :: VariantF xs f
xs) = VariantF xs g -> VariantF (x : xs) g
forall (xs :: [(* -> *) -> *]) (f :: * -> *) (y :: (* -> *) -> *).
VariantF xs f -> VariantF (y : xs) f
ThereF (VariantF xs g -> VariantF (x : xs) g)
-> e (VariantF xs g) -> e (VariantF (x : xs) g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. f a -> e (g a)) -> VariantF xs f -> e (VariantF xs g)
forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
B.btraverse forall a. f a -> e (g a)
nat VariantF xs f
xs

instance B.TraversableB (VariantF '[]) where
  btraverse :: (forall a. f a -> e (g a)) -> VariantF '[] f -> e (VariantF '[] g)
btraverse _ _ = [Char] -> e (VariantF '[] g)
forall a. HasCallStack => [Char] -> a
error "Impossible: empty variant"

-- * Helpers for pattern-matching on variants

pattern In1 :: x1 f -> VariantF (x1 ': xs) f
pattern $bIn1 :: x1 f -> VariantF (x1 : xs) f
$mIn1 :: forall r (x1 :: (* -> *) -> *) (f :: * -> *)
       (xs :: [(* -> *) -> *]).
VariantF (x1 : xs) f -> (x1 f -> r) -> (Void# -> r) -> r
In1 x = HereF x

pattern In2 :: x2 f -> VariantF (x1 ': x2 ': xs) f
pattern $bIn2 :: x2 f -> VariantF (x1 : x2 : xs) f
$mIn2 :: forall r (x2 :: (* -> *) -> *) (f :: * -> *) (x1 :: (* -> *) -> *)
       (xs :: [(* -> *) -> *]).
VariantF (x1 : x2 : xs) f -> (x2 f -> r) -> (Void# -> r) -> r
In2 x = ThereF (In1 x)

pattern In3 :: x3 f -> VariantF (x1 ': x2 ': x3 ': xs) f
pattern $bIn3 :: x3 f -> VariantF (x1 : x2 : x3 : xs) f
$mIn3 :: forall r (x3 :: (* -> *) -> *) (f :: * -> *) (x1 :: (* -> *) -> *)
       (x2 :: (* -> *) -> *) (xs :: [(* -> *) -> *]).
VariantF (x1 : x2 : x3 : xs) f -> (x3 f -> r) -> (Void# -> r) -> r
In3 x = ThereF (In2 x)

pattern In4 :: x4 f -> VariantF (x1 ': x2 ': x3 ': x4 ': xs) f
pattern $bIn4 :: x4 f -> VariantF (x1 : x2 : x3 : x4 : xs) f
$mIn4 :: forall r (x4 :: (* -> *) -> *) (f :: * -> *) (x1 :: (* -> *) -> *)
       (x2 :: (* -> *) -> *) (x3 :: (* -> *) -> *)
       (xs :: [(* -> *) -> *]).
VariantF (x1 : x2 : x3 : x4 : xs) f
-> (x4 f -> r) -> (Void# -> r) -> r
In4 x = ThereF (In3 x)

pattern In5 :: x5 f -> VariantF (x1 ': x2 ': x3 ': x4 ': x5 ': xs) f
pattern $bIn5 :: x5 f -> VariantF (x1 : x2 : x3 : x4 : x5 : xs) f
$mIn5 :: forall r (x5 :: (* -> *) -> *) (f :: * -> *) (x1 :: (* -> *) -> *)
       (x2 :: (* -> *) -> *) (x3 :: (* -> *) -> *) (x4 :: (* -> *) -> *)
       (xs :: [(* -> *) -> *]).
VariantF (x1 : x2 : x3 : x4 : x5 : xs) f
-> (x5 f -> r) -> (Void# -> r) -> r
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 :: VariantF '[x] f -> FoldSignatureF '[x] result f
fromVariantF (HereF x :: x f
x) f :: x f -> result
f = x f -> result
x f -> result
f x f
x
  fromVariantF (ThereF _) _ = [Char] -> result
forall a. HasCallStack => [Char] -> a
error "Impossible: empty variant"

instance
  ( tail ~ (x' ': xs),
    FromVariantF tail result f,
    IgnoreF tail result f
  ) =>
  FromVariantF (x ': x' ': xs) result f
  where
  fromVariantF :: VariantF (x : x' : xs) f -> FoldSignatureF (x : x' : xs) result f
fromVariantF (ThereF x :: VariantF xs f
x) _ = VariantF xs f -> FoldSignatureF xs result f
forall (xs :: [(* -> *) -> *]) result (f :: * -> *).
FromVariantF xs result f =>
VariantF xs f -> FoldSignatureF xs result f
fromVariantF @_ @result VariantF xs f
x
  fromVariantF (HereF x :: x f
x) f :: x f -> result
f = result -> FoldSignatureF tail result f
forall (args :: [(* -> *) -> *]) result (f :: * -> *).
IgnoreF args result f =>
result -> FoldSignatureF args result f
ignoreF @tail (x f -> result
x f -> result
f x f
x)

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

instance IgnoreF '[] result f where
  ignoreF :: result -> FoldSignatureF '[] result f
ignoreF result :: result
result = result
FoldSignatureF '[] result f
result

instance IgnoreF xs result f => IgnoreF (x ': xs) result f where
  ignoreF :: result -> FoldSignatureF (x : xs) result f
ignoreF result :: result
result _ = result -> FoldSignatureF xs result f
forall (args :: [(* -> *) -> *]) result (f :: * -> *).
IgnoreF args result f =>
result -> FoldSignatureF args result f
ignoreF @xs @_ @f result
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 :: SNat 'Z -> x f -> VariantF (x : xs) f
injectPosF SZ = x f -> VariantF (x : xs) f
forall (x :: (* -> *) -> *) (f :: * -> *) (xs :: [(* -> *) -> *]).
x f -> VariantF (x : xs) f
HereF

instance InjectPosF n x xs => InjectPosF (S n) x (y ': xs) where
  injectPosF :: SNat ('S n) -> x f -> VariantF (y : xs) f
injectPosF (SS n :: SNat n
n) = VariantF xs f -> VariantF (y : xs) f
forall (xs :: [(* -> *) -> *]) (f :: * -> *) (y :: (* -> *) -> *).
VariantF xs f -> VariantF (y : xs) f
ThereF (VariantF xs f -> VariantF (y : xs) f)
-> (x f -> VariantF xs f) -> x f -> VariantF (y : xs) f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> x f -> VariantF xs f
forall (n :: Nat) (x :: (* -> *) -> *) (xs :: [(* -> *) -> *])
       (f :: * -> *).
InjectPosF n x xs =>
SNat n -> x f -> VariantF xs f
injectPosF SNat n
n