{-# 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
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"
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)
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
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