{-# LANGUAGE CPP #-}

{- |
   Description: Variants, i.e., labelled sums, generalizations of Either

   The HList library

   See <Data-HList-CommonMain.html#t:Variant CommonMain#Variant>
   for the public (safe) interface.

   The implementation here follows "Data.Dynamic", though Typeable is not
   needed.

   See @broken/VariantP.hs@ and @broken/VariantOld.hs@ for different approaches
   to open sums.
-}

module Data.HList.Variant where

import Data.HList.FakePrelude
import Data.HList.Record
import Data.HList.HList
import Data.HList.HListPrelude
import Data.HList.HOccurs()
import Data.HList.HArray

import Text.ParserCombinators.ReadP hiding (optional)

import Unsafe.Coerce
import GHC.Exts (Constraint)

import Data.Semigroup (Semigroup( .. ))
import Data.Data
import Control.Applicative
import LensDefs
import Control.Monad

-- * Labels for doctests

{- $setup

>>> import Data.HList.RecordPuns
>>> let x = Label :: Label "x"
>>> let y = Label :: Label "y"
>>> let z = Label :: Label "z"
>>> let _left = Label :: Label "left"
>>> let _right = Label :: Label "right"

>>> :set -XQuasiQuotes -XViewPatterns -XDataKinds


-- * Creating Variants

It is necessary to specify the order in which the fields occur, using
a data type like

>>> let p = Proxy :: Proxy '[Tagged "left" Char, Tagged "right" Int]

Then this argument can be passed into 'mkVariant'

>>> let v = mkVariant _left 'x' p
>>> let w = mkVariant _right 5  p

>>> :t v
v :: Variant '[Tagged "left" Char, Tagged "right" Int]

>>> :t w
w :: Variant '[Tagged "left" Char, Tagged "right" Int]


>>> [v,w]
[V{left='x'},V{right=5}]

-}


-- ** Alternative: a 'Record' as the Proxy
{- $mkVariant2

The type of mkVariant also allows using a 'Record' as the proxy. For example:

>>> :{
let p2 = [pun| left right |] where
            left = 'a'
            right = (4::Int)
:}

>>> let v2 = mkVariant _left 'x' p2
>>> let w2 = mkVariant _right 5  p2

>>> :t v2
v2 :: Variant '[Tagged "left" Char, Tagged "right" Int]

>>> :t w2
w2 :: Variant '[Tagged "left" Char, Tagged "right" Int]

>>> (v2,w2)
(V{left='x'},V{right=5})

-}

-- ** A polymorphic Proxy
{- $mkVariant3

It is also possible to leave the @Char@ and @Int@ as type variables,
and have them inferred.

>>> let p3 = Proxy :: Proxy '[Tagged "left" a, Tagged "right" b]

Using @p3@ takes some care. The following attempt shows the problem:

>>> :{
let v3' = mkVariant _left 'x' p3
    w3' = mkVariant _right (5::Int) p3
:}

>>> :t v3'
v3' :: Variant '[Tagged "left" Char, Tagged "right" b]

>>> :t w3'
w3' :: Variant '[Tagged "left" a, Tagged "right" Int]

Here each use of @p3@ does not constrain the type of the other use.
In some cases those type variables will be inferred from other constraints,
such as when putting the variants into a list

>>> [v3', w3']
[V{left='x'},V{right=5}]

In other cases the other tags will be defaulted to (), at least if `ExtendedDefaultRules` is enabled:

>>> v3'
V{left='x'}

>>> :set -XNoExtendedDefaultRules
>>> v3'
...
...No instance for (Show ...) arising from a use of ‘print’
...


Another way around this issue is to make sure that the proxy
is bound in a monomorphic pattern. These are patterns that allow
name shadowing.

* @\p -> ...@
* @case e of p -> ...@
* @do p <- e; ...@
* implicit parameters @let ?p = e in ...@
* <http://stackoverflow.com/questions/23899279#23899611 other patterns involved in mutually recursive bindings>

An example of the case:

>>> :{
let (v3,w3) = case p3 of
              p -> (mkVariant _left 'x' p,
                    mkVariant _right (5 :: Int) p)
:}


>>> :t v3
v3 :: Variant '[Tagged "left" Char, Tagged "right" Int]

>>> :t w3
w3 :: Variant '[Tagged "left" Char, Tagged "right" Int]

-}

-- --------------------------------------------------------------------------
{- |
@Variant vs@ has an implementation similar to 'Dynamic', except the
contained value is one of the elements of the @vs@ list, rather than
being one particular instance of 'Typeable'.

>>> v .!. _right
Nothing

>>> v .!. _left
Just 'x'

In some cases the 'pun' quasiquote works with variants,

>>> let f [pun| left right |] = (left,right)
>>> f v
(Just 'x',Nothing)

>>> f w
(Nothing,Just 5)


>>> let add1 v = hMapV (Fun succ :: Fun '[Enum] '()) v

>>> f (add1 v)
(Just 'y',Nothing)

>>> f (add1 w)
(Nothing,Just 6)


-}
data Variant (vs :: [*]) = Variant !Int Any

#if __GLASGOW_HASKELL__ > 707
-- the inferred role is phantom, which is not safe
type role Variant representational
#endif



-- ** Unsafe operations

-- | This is only safe if the n'th element of vs has type @Tagged t v@
unsafeMkVariant :: Int -- ^ n
                -> v
                -> Variant vs
unsafeMkVariant :: forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
n v
a = forall (vs :: [*]). Int -> Any -> Variant vs
Variant Int
n (forall a b. a -> b
unsafeCoerce v
a)

{- | Safe when (e ~ e') given that

> Tagged t e ~ HLookupByHNatR n v
> Tagged t' e' ~ HLookupByHNatR n v'

'hUpdateAtLabel' is the safe version

-}
unsafeCastVariant :: Variant v -> Variant v'
unsafeCastVariant :: forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant (Variant Int
n Any
e) = forall (vs :: [*]). Int -> Any -> Variant vs
Variant Int
n Any
e

-- | in ghc>=7.8, 'Data.Coerce.coerce' is probably a better choice
castVariant :: (RecordValuesR v ~ RecordValuesR v',
              SameLength v v') => Variant v -> Variant v'
castVariant :: forall (v :: [*]) (v' :: [*]).
(RecordValuesR v ~ RecordValuesR v', SameLength v v') =>
Variant v -> Variant v'
castVariant = forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant

instance Relabeled Variant where
    relabeled :: forall (p :: * -> * -> *) (f :: * -> *) (s :: [*]) (t :: [*])
       (a :: [*]) (b :: [*]).
(HMapTaggedFn (RecordValuesR s) a,
 HMapTaggedFn (RecordValuesR b) t, SameLengths '[s, a, t, b],
 RecordValuesR t ~ RecordValuesR b,
 RecordValuesR s ~ RecordValuesR a, RecordValues b, RecordValues s,
 Profunctor p, Functor f) =>
p (Variant a) (f (Variant b)) -> p (Variant s) (f (Variant t))
relabeled = forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso forall (v :: [*]) (v' :: [*]).
(RecordValuesR v ~ RecordValuesR v', SameLength v v') =>
Variant v -> Variant v'
castVariant forall (v :: [*]) (v' :: [*]).
(RecordValuesR v ~ RecordValuesR v', SameLength v v') =>
Variant v -> Variant v'
castVariant

-- | private destructor. This is safe only if the value
-- contained actually has type `e`
unsafeUnVariant :: Variant v -> e
unsafeUnVariant :: forall (v :: [*]) e. Variant v -> e
unsafeUnVariant (Variant Int
_ Any
e) = forall a b. a -> b
unsafeCoerce Any
e


{- | This function is unsafe because it can lead to a runtime error
when used together with the 'HExtend' instance (.*.)

>>> print $ (Label :: Label "x") .=. (Nothing :: Maybe ()) .*. unsafeEmptyVariant
V{*** Exception: invalid variant

use 'mkVariant1' instead

-}
unsafeEmptyVariant :: Variant '[]
unsafeEmptyVariant :: Variant '[]
unsafeEmptyVariant = forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 ()

-- --------------------------------------------------------------------------
-- * Public constructor

class HasField x (Variant vs) (Maybe v) =>
      MkVariant x v vs | x vs -> v where
    mkVariant :: Label x -- ^ the tag
        -> v -- ^ value to be stored
        -> proxy vs -- ^ a helper to fix the ordering and types of the
                    -- potential values that this variant contains.
                    -- Typically this will be a 'Proxy', 'Record' or
                    -- another 'Variant'
        -> Variant vs

mkVariant1 :: Label l -> e -> HExtendR (Tagged l (Maybe e)) (Variant '[])
mkVariant1 Label l
l e
v = Label l
l forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. forall a. a -> Maybe a
Just e
v forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Variant '[]
unsafeEmptyVariant

instance (HFindLabel x vs n,
          HNat2Integral n,
          HasField x (Variant vs) (Maybe v)) =>
    MkVariant x v vs where
  mkVariant :: forall (proxy :: [*] -> *). Label x -> v -> proxy vs -> Variant vs
mkVariant Label x
_x v
y proxy vs
_p = forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant (forall (n :: HNat) i. (HNat2Integral n, Integral i) => Proxy n -> i
hNat2Integral (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) v
y
  -- done as a one-instance class instead of a function to be able to hide
  -- the 'n' type variable

-- --------------------------------------------------------------------------
-- * Public destructor

{- $note 'hLookupByLabel' (synonym '.!.')

> (.!.)             :: Variant v -> Label x -> Maybe e
> hLookupByLabel    :: Label x -> Variant v -> Maybe e

'hPrism' and 'hLens'' combine this with 'mkVariant'
-}
instance (HasField x (Record vs) a,
          HFindLabel x vs n,
          HNat2Integral n)
  => HasField x (Variant vs) (Maybe a) where
  hLookupByLabel :: Label x -> Variant vs -> Maybe a
hLookupByLabel Label x
_x (Variant Int
n Any
d)
          | forall (n :: HNat) i. (HNat2Integral n, Integral i) => Proxy n -> i
hNat2Integral (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) forall a. Eq a => a -> a -> Bool
== Int
n = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce Any
d)
          | Bool
otherwise = forall a. Maybe a
Nothing

splitVariant1 :: Variant (Tagged s x ': xs) -> Either x (Variant xs)
splitVariant1 :: forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 (Variant Int
0 Any
x) = forall a b. a -> Either a b
Left (forall a b. a -> b
unsafeCoerce Any
x)
splitVariant1 (Variant Int
n Any
x) = forall a b. b -> Either a b
Right (forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nforall a. Num a => a -> a -> a
-Int
1) Any
x)

-- | x ~ Tagged s t
splitVariant1' :: Variant (x ': xs) -> Either x (Variant xs)
splitVariant1' :: forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' (Variant Int
0 Any
x) = forall a b. a -> Either a b
Left (forall a b. a -> b
unsafeCoerce Any
x)
splitVariant1' (Variant Int
n Any
x) = forall a b. b -> Either a b
Right (forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nforall a. Num a => a -> a -> a
-Int
1) Any
x)

extendVariant :: Variant l -> Variant (e ': l)
extendVariant :: forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant Int
m Any
e) = forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
mforall a. Num a => a -> a -> a
+Int
1) Any
e

-- --------------------------------------------------------------------------
-- * Prism

{- | Make a @Prism (Variant s) (Variant t) a b@ out of a Label.

See "Data.HList.Labelable".'hLens'' is a more overloaded version.

Few type annotations are necessary because of the restriction
that `s` and `t` have the same labels in the same order, and to
get \"t\" the \"a\" in \"s\" is replaced with \"b\".

-}
class (SameLength s t, SameLabels s t)
        => HPrism x s t a b
          | x s -> a, x t -> b,    -- lookup
            x s b -> t, x t a -> s -- update
  where
    hPrism :: (Choice p, Applicative f)
        => Label x -> p a (f b) -> p (Variant s) (f (Variant t))


instance (
    MkVariant x b t,

    HasField x (Variant s) (Maybe a),

    -- labels in the HList are not changed at all:
    -- number, ordering, actual values are all constant
    SameLength s t,
    SameLabels s t,

    -- only the target of the prism can have it's type changed
    H2ProjectByLabels '[Label x] s si so,
    H2ProjectByLabels '[Label x] t ti to,
    so ~ to,

    -- to convince GHC the fundeps are satisfied
    HUpdateAtLabel Variant x b s t,
    HUpdateAtLabel Variant x a t s
   ) => HPrism x s t a b where
    hPrism :: forall (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
Label x -> p a (f b) -> p (Variant s) (f (Variant t))
hPrism Label x
x = forall b t s a.
(b -> t)
-> (s -> Either t a)
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p a (f b) -> p s (f t)
prism (\b
b -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant Label x
x b
b forall {k} (t :: k). Proxy t
Proxy)
                  (\Variant s
s -> case forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label x
x Variant s
s of
                    Just a
a -> forall a b. b -> Either a b
Right a
a
                    Maybe a
Nothing -> forall a b. a -> Either a b
Left (forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant Variant s
s :: Variant t))



-- --------------------------------------------------------------------------
-- * Read
-- | Variants are not opaque
instance (ShowVariant vs) => Show (Variant vs) where
    showsPrec :: Int -> Variant vs -> ShowS
showsPrec Int
_ Variant vs
v = (String
"V{"forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant vs
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'}'forall a. a -> [a] -> [a]
:)


-- | helper class for defining the Show instance
class ShowVariant vs where
    showVariant :: Variant vs -> ShowS

instance (ShowLabel l, Show v, ShowVariant (w ': ws))
      => ShowVariant (Tagged l v ': w ': ws) where
    showVariant :: Variant (Tagged l v : w : ws) -> ShowS
showVariant Variant (Tagged l v : w : ws)
vs = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged l v : w : ws)
vs of
        Left v
v -> \String
rest -> forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel Label l
l forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show v
v forall a. [a] -> [a] -> [a]
++ String
rest
        Right Variant (w : ws)
wws -> forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant (w : ws)
wws
      where l :: Label l
l = forall {k} (l :: k). Label l
Label :: Label l

instance (ShowLabel l, Show v, lv ~ Tagged l v) => ShowVariant '[lv] where
    showVariant :: Variant '[lv] -> ShowS
showVariant Variant '[lv]
vs = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant '[lv]
vs of
        Left v
v -> \String
rest -> forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel Label l
l forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show v
v forall a. [a] -> [a] -> [a]
++ String
rest
        Right Variant '[]
_ -> forall a. HasCallStack => String -> a
error String
"invalid variant"
      where l :: Label l
l = forall {k} (l :: k). Label l
Label :: Label l

-- --------------------------------------------------------------------------
-- * Show
-- | A corresponding read instance

instance ReadVariant v => Read (Variant v) where
    readsPrec :: Int -> ReadS (Variant v)
readsPrec Int
_ = forall a. ReadP a -> ReadS a
readP_to_S forall a b. (a -> b) -> a -> b
$ do
      String
_ <- String -> ReadP String
string String
"V{"
      Variant v
r <- forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
      String
_ <- String -> ReadP String
string String
"}"
      forall (m :: * -> *) a. Monad m => a -> m a
return Variant v
r

class ReadVariant vs where
    readVariant :: ReadP (Variant vs)

instance ReadVariant '[] where
    readVariant :: ReadP (Variant '[])
readVariant = forall (m :: * -> *) a. Monad m => a -> m a
return Variant '[]
unsafeEmptyVariant

instance (ShowLabel l, Read v, ReadVariant vs,
          HOccursNot (Label l) (LabelsOf vs))
    => ReadVariant (Tagged l v ': vs) where
    readVariant :: ReadP (Variant (Tagged l v : vs))
readVariant = do
      Maybe v
mlv <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ReadP v
lv
      case Maybe v
mlv of
        Maybe v
Nothing -> do
          Variant vs
rest <- forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
          forall (m :: * -> *) a. Monad m => a -> m a
return (Label l
l forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. Maybe v
mlv forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Variant vs
rest)
        Just v
e -> do
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant Label l
l v
e Proxy (Tagged l v : vs)
p)

      where
        lv :: ReadP v
lv = do
            String
_ <- String -> ReadP String
string (forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel Label l
l)
            String
_ <- String -> ReadP String
string String
"="
            forall a. ReadS a -> ReadP a
readS_to_P forall a. Read a => ReadS a
reads

        l :: Label l
l = forall {k} (l :: k). Label l
Label :: Label l

        p :: Proxy (Tagged l v : vs)
p = forall {k} (t :: k). Proxy t
Proxy :: Proxy (Tagged l v ': vs)


-- * Data
instance (Typeable (Variant v), GfoldlVariant v v,
          GunfoldVariant v v,
          VariantConstrs v)
        => Data (Variant v) where
    gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant v -> c (Variant v)
gfoldl = forall (xs :: [*]) (xs' :: [*]) (c :: * -> *).
GfoldlVariant xs xs' =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant xs -> c (Variant xs')
gfoldlVariant
    gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Variant v)
gunfold forall b r. Data b => c (b -> r) -> c r
k forall r. r -> c r
z Constr
c = forall (es :: [*]) (v :: [*]) (c :: * -> *).
GunfoldVariant es v =>
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy es -> Int -> c (Variant v)
gunfoldVariant (\b -> Variant v
con -> forall b r. Data b => c (b -> r) -> c r
k (forall r. r -> c r
z b -> Variant v
con)) (forall {k} (t :: k). Proxy t
Proxy :: Proxy v) (Constr -> Int
constrIndex Constr
c forall a. Num a => a -> a -> a
- Int
1)
    toConstr :: Variant v -> Constr
toConstr v :: Variant v
v@(Variant Int
n Any
_) = case forall a. Int -> [a] -> [a]
drop Int
n (forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
variantConstrs (forall a. Data a => a -> DataType
dataTypeOf Variant v
v) Variant v
v) of
        Constr
c : [Constr]
_ -> Constr
c
        [Constr]
_ -> forall a. HasCallStack => String -> a
error String
"Data.HList.Variant.toConstr impossible"
    dataTypeOf :: Variant v -> DataType
dataTypeOf Variant v
x = let self :: DataType
self = String -> [Constr] -> DataType
mkDataType (forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf Variant v
x)) (forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
variantConstrs DataType
self Variant v
x)
          in DataType
self

class VariantConstrs (xs :: [*]) where
  variantConstrs :: DataType -> proxy xs -> [Constr]

instance VariantConstrs '[] where
  variantConstrs :: forall (proxy :: [*] -> *). DataType -> proxy '[] -> [Constr]
variantConstrs DataType
_ proxy '[]
_ = []

instance (ShowLabel l, VariantConstrs xs) => VariantConstrs (Tagged l e ': xs) where
  variantConstrs :: forall (proxy :: [*] -> *).
DataType -> proxy (Tagged l e : xs) -> [Constr]
variantConstrs DataType
dt proxy (Tagged l e : xs)
_ = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
dt (forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel (forall {k} (l :: k). Label l
Label :: Label l)) [] Fixity
Prefix forall a. a -> [a] -> [a]
:
        forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
variantConstrs DataType
dt (forall {k} (t :: k). Proxy t
Proxy :: Proxy xs)




{- | [@implementation of gunfold for Variant@]

In ghci

> :set -ddump-deriv -XDeriveDataTypeable
> data X a b c = A a | B b | C c deriving (Data,Typeable)

shows that gunfold is defined something like

> gunfold k z c = case constrIndex c of
>       1 -> k (z Ghci1.A)
>       2 -> k (z Ghci1.B)
>       _ -> k (z Ghci1.C)

If we instead had

> type X a b c = Variant [Tagged "A" a, Tagged "B" b, Tagged "C" c]

Then we could write:

> gunfold1 :: (forall b r. Data b => (b -> r) -> c r)
>          -> Variant [Tagged "A" a, Tagged "B" b, Tagged "C" c]
> gunfold1 f c = case constrIndex c of
>       1 -> f mkA
>       2 -> f mkB
>       _ -> f mkC
>   where mkA a = mkVariant (Label :: Label "A") (a :: a) v
>         mkB b = mkVariant (Label :: Label "B") (b :: b) v
>         mkC c = mkVariant (Label :: Label "C") (c :: c) v
>         v = Proxy :: Proxy [Tagged "A" a, Tagged "B" b, Tagged "C" c]

where @f = k.z@


-}
class GunfoldVariant (es :: [*]) v where
    gunfoldVariant ::
        (forall b. Data b => (b -> Variant v) -> c (Variant v))
          -- ^ @f = k . z@
        -> Proxy es
        -> Int
        -> c (Variant v)

instance (MkVariant l e v, Data e) => GunfoldVariant '[Tagged l e] v where
    gunfoldVariant :: forall (c :: * -> *).
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy '[Tagged l e] -> Int -> c (Variant v)
gunfoldVariant forall b. Data b => (b -> Variant v) -> c (Variant v)
f Proxy '[Tagged l e]
_ Int
_ = forall b. Data b => (b -> Variant v) -> c (Variant v)
f (\e
e -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) forall {k} (t :: k). Proxy t
Proxy)

instance (MkVariant l e v, Data e,
        GunfoldVariant (b ': bs) v) => GunfoldVariant (Tagged l e ': b ': bs)  v where
    gunfoldVariant :: forall (c :: * -> *).
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy (Tagged l e : b : bs) -> Int -> c (Variant v)
gunfoldVariant forall b. Data b => (b -> Variant v) -> c (Variant v)
f Proxy (Tagged l e : b : bs)
_ Int
0 = forall b. Data b => (b -> Variant v) -> c (Variant v)
f (\e
e -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) forall {k} (t :: k). Proxy t
Proxy)
    gunfoldVariant forall b. Data b => (b -> Variant v) -> c (Variant v)
f Proxy (Tagged l e : b : bs)
_ Int
n = forall (es :: [*]) (v :: [*]) (c :: * -> *).
GunfoldVariant es v =>
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy es -> Int -> c (Variant v)
gunfoldVariant forall b. Data b => (b -> Variant v) -> c (Variant v)
f (forall {k} (t :: k). Proxy t
Proxy :: Proxy (b ': bs)) (Int
nforall a. Num a => a -> a -> a
-Int
1)



class GfoldlVariant xs xs' where
  -- | the same as 'gfoldl', except the variant that is returned can have more
  -- possible values (needed to actually implement gfoldl).
  gfoldlVariant ::
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Variant xs -> c (Variant xs')

instance (a ~ Tagged l v, MkVariant l v r, Data v,
          GfoldlVariant (b ': c) r)
      => GfoldlVariant (a ': b ': c) r where
  gfoldlVariant :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant (a : b : c) -> c (Variant r)
gfoldlVariant forall d b. Data d => c (d -> b) -> d -> c b
k forall g. g -> c g
z Variant (a : b : c)
xxs = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (a : b : c)
xxs of
      Right Variant (b : c)
xs -> forall (xs :: [*]) (xs' :: [*]) (c :: * -> *).
GfoldlVariant xs xs' =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant xs -> c (Variant xs')
gfoldlVariant forall d b. Data d => c (d -> b) -> d -> c b
k forall g. g -> c g
z Variant (b : c)
xs
      -- If the c@type variable in 'gfoldl' had a Functor constraint,
      -- this case could be extendVariant `fmap` gfoldl k z xs,
      -- and then 'GfoldlVariant' would be unnecessary
      Left v
x ->
            let mkV :: v -> Variant r
mkV v
e = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) v
e forall {k} (t :: k). Proxy t
Proxy
            in forall g. g -> c g
z v -> Variant r
mkV forall d b. Data d => c (d -> b) -> d -> c b
`k` v
x

instance (Unvariant '[a] v, a ~ Tagged l v, Data v,
          MkVariant l v b) => GfoldlVariant '[a] b where
    gfoldlVariant :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant '[a] -> c (Variant b)
gfoldlVariant forall d b. Data d => c (d -> b) -> d -> c b
k forall g. g -> c g
z Variant '[a]
xxs = forall g. g -> c g
z v -> Variant b
mkV forall d b. Data d => c (d -> b) -> d -> c b
`k` forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[a]
xxs
        where mkV :: v -> Variant b
mkV v
e = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) v
e forall {k} (t :: k). Proxy t
Proxy



-- --------------------------------------------------------------------------
-- * Map
-- | Apply a function to all possible elements of the variant
newtype HMapV f = HMapV f

-- | shortcut for @applyAB . HMapV@. 'hMap' is more general
hMapV :: f -> Variant x -> Variant y
hMapV f
f Variant x
v = forall f a b. ApplyAB f a b => f -> a -> b
applyAB (forall f. f -> HMapV f
HMapV f
f) Variant x
v

-- | @hMapOutV f = unvariant . hMapV f@, except an ambiguous type
-- variable is resolved by 'HMapOutV_gety'
hMapOutV :: forall x y z f. (SameLength x y,
      HMapAux Variant (HFmap f) x y,
      Unvariant y z,
      HMapOutV_gety x z ~ y
  ) => f -> Variant x -> z
hMapOutV :: forall (x :: [*]) (y :: [*]) z f.
(SameLength x y, HMapAux Variant (HFmap f) x y, Unvariant y z,
 HMapOutV_gety x z ~ y) =>
f -> Variant x -> z
hMapOutV f
f Variant x
v = forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant (forall {f} {x :: [*]} {y :: [*]}.
(HMapAux Variant (HFmap f) x y, SameLength' x y,
 SameLength' y x) =>
f -> Variant x -> Variant y
hMapV f
f Variant x
v :: Variant y)


-- | resolves an ambiguous type in 'hMapOutV'
type family HMapOutV_gety (x :: [*]) (z :: *) :: [*]
type instance HMapOutV_gety (Tagged s x ': xs) z = Tagged s z ': HMapOutV_gety xs z
type instance HMapOutV_gety '[] z = '[]


-- | apply a function to all values that could be in the variant.
instance (vx ~ Variant x,
          vy ~ Variant y,
          HMapAux Variant (HFmap f) x y,
          SameLength x y)
     => ApplyAB (HMapV f) vx vy where
    applyAB :: HMapV f -> vx -> vy
applyAB (HMapV f
f) vx
x = forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux (forall f. f -> HFmap f
HFmap f
f) vx
x

instance (ApplyAB f te te') => HMapAux Variant f '[te] '[te'] where
    hMapAux :: SameLength '[te] '[te'] => f -> Variant '[te] -> Variant '[te']
hMapAux f
f Variant '[te]
v = case forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant '[te]
v of
        Left te
te -> forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f te
te :: te')
        Right Variant '[]
_ -> forall a. HasCallStack => String -> a
error String
"HMapVAux: variant invariant broken"

instance (ApplyAB f te te',
          HMapCxt Variant f (l ': ls) (l' ': ls'))
    => HMapAux Variant f (te ': l ': ls) (te' ': l' ': ls') where
      hMapAux :: SameLength (te : l : ls) (te' : l' : ls') =>
f -> Variant (te : l : ls) -> Variant (te' : l' : ls')
hMapAux f
f Variant (te : l : ls)
v = case forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (te : l : ls)
v of
          Left te
te -> forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f te
te :: te')
          Right Variant (l : ls)
es -> forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f Variant (l : ls)
es)

-- --------------------------------------------------------------------------
-- * HUpdateAtLabel instance

{- |

> hUpdateAtLabel x e' (mkVariant x e proxy) == mkVariant x e' proxy
> hUpdateAtLabel y e' (mkVariant x e proxy) == mkVariant x e  proxy

-}
instance
   (HUpdateVariantAtLabelCxt l e v v' n _e) =>
    HUpdateAtLabel Variant l e v v' where
    hUpdateAtLabel :: SameLength v v' => Label l -> e -> Variant v -> Variant v'
hUpdateAtLabel Label l
l e
e Variant v
v = case forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label l
l Variant v
v of
          Just _e
_e -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant Label l
l e
e (forall {k} (t :: k). Proxy t
Proxy :: Proxy v')
          Maybe _e
Nothing -> forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant Variant v
v

type HUpdateVariantAtLabelCxt l e v v' n _e =
   (HFindLabel l v n,
    HFindLabel l v' n,
    HUpdateAtHNatR n (Tagged l e) v ~ v',
    HasField l (Variant v) (Maybe _e),
    HasField l (Record v') e,
    MkVariant l e v')


-- --------------------------------------------------------------------------
-- * HExtend instance
{- | Extension for Variants prefers the first value

> (l .=. Nothing) .*. v = v
> (l .=. Just e)  .*. _ = mkVariant l e Proxy

-}
instance (le ~ Tagged l (Maybe e), HOccursNot (Label l) (LabelsOf v)) =>
    HExtend le (Variant v) where
    type HExtendR le (Variant v) = Variant (UnMaybe le ': v)
    Tagged (Just e
e) .*. :: le -> Variant v -> HExtendR le (Variant v)
.*. Variant v
_ = forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 e
e
    Tagged Maybe e
Nothing .*. (Variant Int
n Any
e) = forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nforall a. Num a => a -> a -> a
+Int
1) Any
e

type family UnMaybe le
type instance UnMaybe (Tagged l (Maybe e)) = Tagged l e

-- | used for 'HExtend' 'TIP'
type instance UnMaybe (Maybe e) = e


-- --------------------------------------------------------------------------
-- * Conversion to an untagged value
class HAllEqVal (x :: [*]) (b :: Bool) | x -> b
instance HAllEqVal '[] True
instance HAllEqVal '[x] True
instance (HEq a a' b,
          HAllEqVal (Tagged t a' ': xs) b2,
          HAnd b b2 ~ b3) =>
  HAllEqVal (Tagged s a ': Tagged t a' ': xs) b3


class HAllEqVal' (x :: [*])
instance HAllEqVal' '[]
instance HAllEqVal' '[x]
instance (HAllEqVal' (ta ': xs),
          a' ~ a,
          ta ~ Tagged t a,
          ta' ~ Tagged t' a')
  => HAllEqVal' (ta' ': ta ': xs)


{- | Similar to 'unvariant', except type variables in @v@
will be made equal to @e@ if possible. That allows the type
of @Nothing@ to be inferred as @Maybe Char@.

>>> unvariant' $ x .=. Nothing .*. mkVariant1 y 'y'
'y'

However, this difference leads to more local error messages
(@Couldn't match type ‘()’ with ‘Char’@), rather than the following
with @unvariant@:

> Fail
>    '("Variant",
>      '[Tagged "left" Char, Tagged "right" ()],
>      "must have all values equal to ",
>      e))

-}
class Unvariant' v e | v -> e where
    unvariant' :: Variant v -> e

instance (HAllEqVal' (Tagged () e ': v), Unvariant v e) =>
    Unvariant' v e where
  unvariant' :: Variant v -> e
unvariant' = forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant

{- | Convert a Variant which has all possibilities having the same type
into a value of that type. Analogous to @either id id@.

See also 'unvariant'' -}
class Unvariant v e | v -> e where
    unvariant :: Variant v -> e

instance (Unvariant1 b v e,
          HAllEqVal v b,
          HAllEqVal (Tagged () e ': v) b)
    => Unvariant v e where
      unvariant :: Variant v -> e
unvariant = forall {k} (b :: k) (v :: [*]) e.
Unvariant1 b v e =>
Proxy b -> Variant v -> e
unvariant1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b)


class Unvariant1 b v e | b v -> e where
    unvariant1 :: Proxy b -> Variant v -> e

instance (v ~ Tagged t1 e)
    => Unvariant1 True (v ': vs) e where
    unvariant1 :: Proxy 'True -> Variant (v : vs) -> e
unvariant1 Proxy 'True
_ = forall (v :: [*]) e. Variant v -> e
unsafeUnVariant

data UnvariantTypeMismatch (vs :: [*])

instance Fail (UnvariantTypeMismatch (v ': vs))
      => Unvariant1 False (v ': vs) (UnvariantTypeMismatch (v ': vs)) where
    unvariant1 :: Proxy 'False -> Variant (v : vs) -> UnvariantTypeMismatch (v : vs)
unvariant1 Proxy 'False
_ = forall a. HasCallStack => String -> a
error String
"Data.HList.Variant.Unvariant1 Fail must have no instances"

instance Fail "Unvariant applied to empty variant"
      => Unvariant1 b '[] (Proxy "Unvariant applied to empty variant") where
    unvariant1 :: Proxy b
-> Variant '[] -> Proxy "Unvariant applied to empty variant"
unvariant1 Proxy b
_ = forall a. HasCallStack => String -> a
error String
"Data.HList.Variant.Unvariant1 Fail must have no instances"

{- | @Lens (Variant s) (Variant t) a b@

Analogue of @Control.Lens.chosen :: Lens (Either a a) (Either b b) a b@
-}
unvarianted :: (Unvariant' s a,
                Unvariant' t b,
                SameLabels s t, -- extra constraints to reduce ambiguity
                SameLength s t,
                Functor f) =>
    (a -> f b) -> Variant s -> f (Variant t)
unvarianted :: forall (s :: [*]) a (t :: [*]) b (f :: * -> *).
(Unvariant' s a, Unvariant' t b, SameLabels s t, SameLength s t,
 Functor f) =>
(a -> f b) -> Variant s -> f (Variant t)
unvarianted a -> f b
f v :: Variant s
v@(Variant Int
n Any
_) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
e' -> forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
n b
e')
                                      (a -> f b
f (forall (v :: [*]) e. Unvariant' v e => Variant v -> e
unvariant' Variant s
v))

-- | @Lens' (Variant s) a@
--
-- where we might have @s ~ '[Tagged t1 a, Tagged t2 a]@
unvarianted' :: (a -> f a) -> Variant t -> f (Variant t)
unvarianted' a -> f a
x = forall a. Equality' a a
simple (forall (s :: [*]) a (t :: [*]) b (f :: * -> *).
(Unvariant' s a, Unvariant' t b, SameLabels s t, SameLength s t,
 Functor f) =>
(a -> f b) -> Variant s -> f (Variant t)
unvarianted a -> f a
x)

-- * Zip

{- | Applies to variants that have the same labels
in the same order. A generalization of

> zipEither :: Either a b -> Either a b -> Maybe (Either (a,a) (b,b))
> zipEither (Left a) (Left a') = Just (Left (a,a'))
> zipEither (Right a) (Right a') = Just (Right (a,a'))
> zipEither _ _ = Nothing

see 'HZip' for zipping other collections

-}
class ZipVariant x y xy | x y -> xy, xy -> x y where
    zipVariant :: Variant x -> Variant y -> Maybe (Variant xy)

instance ZipVariant '[] '[] '[] where
    zipVariant :: Variant '[] -> Variant '[] -> Maybe (Variant '[])
zipVariant Variant '[]
_ Variant '[]
_ = forall a. Maybe a
Nothing

instance (tx ~ Tagged t x,
          ty ~ Tagged t y,
          txy ~ Tagged t (x,y),
          ZipVariant xs ys zs,
          MkVariant t (x,y) (txy ': zs))
  => ZipVariant (tx ': xs) (ty ': ys) (txy ': zs) where
    zipVariant :: Variant (tx : xs)
-> Variant (ty : ys) -> Maybe (Variant (txy : zs))
zipVariant Variant (tx : xs)
x Variant (ty : ys)
y = case (forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (tx : xs)
x, forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (ty : ys)
y) of
        (Left x
x', Left y
y') -> forall a. a -> Maybe a
Just (forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (x
x',y
y') forall {k} (t :: k). Proxy t
Proxy)
        (Right Variant xs
x', Right Variant ys
y') -> forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: [*]) (y :: [*]) (xy :: [*]).
ZipVariant x y xy =>
Variant x -> Variant y -> Maybe (Variant xy)
zipVariant Variant xs
x' Variant ys
y'
        (Either x (Variant xs), Either y (Variant ys))
_ -> forall a. Maybe a
Nothing


instance (HUnzip Variant (x2 ': xs) (y2 ': ys) (xy2 ': xys),
          SameLength xs ys,
          SameLength ys xys,
          tx ~ Tagged t x,
          ty ~ Tagged t y,
          txy ~ Tagged t (x,y))
      => HUnzip Variant (tx ': x2 ': xs) (ty ': y2 ': ys) (txy ': xy2 ': xys) where
    hUnzip :: Variant (txy : xy2 : xys)
-> (Variant (tx : x2 : xs), Variant (ty : y2 : ys))
hUnzip Variant (txy : xy2 : xys)
xy = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (txy : xy2 : xys)
xy of
      Left (x
x,y
y) -> (forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) x
x forall {k} (t :: k). Proxy t
Proxy,
                     forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) y
y forall {k} (t :: k). Proxy t
Proxy)
      Right Variant (xy2 : xys)
xy' | (Variant (x2 : xs)
x,Variant (y2 : ys)
y) <- forall (r :: [*] -> *) (x :: [*]) (y :: [*]) (xy :: [*]).
HUnzip r x y xy =>
r xy -> (r x, r y)
hUnzip Variant (xy2 : xys)
xy' ->
                    (forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant (x2 : xs)
x,
                     forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant (y2 : ys)
y)

instance (Unvariant '[txy] txy,
          tx ~ Tagged t x,
          ty ~ Tagged t y,
          txy ~ Tagged t (x,y))
      => HUnzip Variant '[tx] '[ty] '[txy] where
    hUnzip :: Variant '[txy] -> (Variant '[tx], Variant '[ty])
hUnzip Variant '[txy]
xy | Tagged (x
x,y
y) <- forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[txy]
xy =
        (forall {k} {l :: k} {e}. Label l -> e -> Variant '[Tagged l e]
mkVariant1 forall {k} (l :: k). Label l
Label x
x, forall {k} {l :: k} {e}. Label l -> e -> Variant '[Tagged l e]
mkVariant1 forall {k} (l :: k). Label l
Label y
y)


-- ** with a record

{- | Apply a record of functions to a variant of values.
The functions are selected based on those having the same
label as the value.

-}
class (SameLength v v',
       SameLabels v v')  => ZipVR fs v v' | fs v -> v' where
    -- | 'zipVR' is probably a better choice in most
    -- situations, since it requires that @fs@ has one function for every
    -- element of @v@
    zipVR_ :: Record fs -> Variant v -> Variant v'

instance (lv ~ Tagged l v,
          lv' ~ Tagged l v',
          HMemberM (Label l) (LabelsOf fs) b,
          HasFieldM l (Record fs) f,
          DemoteMaybe (v -> v) f ~ (v -> v'),
          MkVariant l v' (lv' ': rs),
          ZipVR fs vs rs) =>
          ZipVR fs (lv ': vs) (lv' ': rs) where
    zipVR_ :: Record fs -> Variant (lv : vs) -> Variant (lv' : rs)
zipVR_ Record fs
r Variant (lv : vs)
lvs = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (lv : vs)
lvs of
                  Left v
v | v'
v' <- forall k (l :: k) r (v :: Maybe (*)) t.
HasFieldM l r v =>
Label l -> r -> t -> DemoteMaybe t v
hLookupByLabelM Label l
l Record fs
r (forall a. a -> a
id :: v -> v) v
v -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant Label l
l v'
v' forall {k} (t :: k). Proxy t
Proxy
                  Right Variant vs
vs -> forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall a b. (a -> b) -> a -> b
$ forall (fs :: [*]) (v :: [*]) (v' :: [*]).
ZipVR fs v v' =>
Record fs -> Variant v -> Variant v'
zipVR_ Record fs
r Variant vs
vs
      where l :: Label l
l = forall {k} (l :: k). Label l
Label :: Label l


instance ZipVR fs '[] '[] where
    zipVR_ :: Record fs -> Variant '[] -> Variant '[]
zipVR_ Record fs
_ Variant '[]
x = Variant '[]
x

{- |

>>> let xy = x .*. y .*. emptyProxy
>>> let p = Proxy `asLabelsOf` xy
>>> let vs = [ mkVariant x 1.0 p, mkVariant y () p ]


>>> zipVR (hBuild (+1) id) `map` vs
[V{x=2.0},V{y=()}]


-}
zipVR :: (SameLabels fs v, SameLength fs v, ZipVR fs v v',
          ZipVRCxt fs v v')
    => Record fs -> Variant v -> Variant v'
zipVR :: forall (fs :: [*]) (v :: [*]) (v' :: [*]).
(SameLabels fs v, SameLength fs v, ZipVR fs v v',
 ZipVRCxt fs v v') =>
Record fs -> Variant v -> Variant v'
zipVR = forall (fs :: [*]) (v :: [*]) (v' :: [*]).
ZipVR fs v v' =>
Record fs -> Variant v -> Variant v'
zipVR_


{- | Lets 'zipVR' act as if @'ZipVR' fs v v'@ had an FD @v v' -> fs@

> ZipVRCxt [Tagged s f,  Tagged t g]
>          [Tagged s fx, Tagged t gx]
>          [Tagged s fy, Tagged t gy]
>   = (f ~ (fx -> fy), g ~ (gx -> gy))

-}
type family ZipVRCxt (fs :: [*]) (xs :: [*]) (ys :: [*]) :: Constraint

type instance ZipVRCxt (Tagged s f ': fs) (Tagged s x ': xs) (Tagged s y ': ys) =
        (f ~ (x -> y), ZipVRCxt fs xs ys)
type instance ZipVRCxt '[] '[] '[] = ()

-- * Eq
instance Eq (Variant '[]) where
  Variant '[]
_ == :: Variant '[] -> Variant '[] -> Bool
== Variant '[]
_ = Bool
True

instance (Eq (Variant xs), Eq x) => Eq (Variant (x ': xs)) where
  Variant (x : xs)
v == :: Variant (x : xs) -> Variant (x : xs) -> Bool
== Variant (x : xs)
v' = case (forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
v, forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
v') of
    (Left x
l, Left x
r) -> x
l forall a. Eq a => a -> a -> Bool
== x
r
    (Right Variant xs
l, Right Variant xs
r) -> Variant xs
l forall a. Eq a => a -> a -> Bool
== Variant xs
r
    (Either x (Variant xs), Either x (Variant xs))
_ -> Bool
False

-- ** Alternative Eq
-- | implemented like @and (zipWith (==) xs ys)@. Behaves the same as the Eq instances for 'Variant'
eqVariant :: Variant x -> Variant y -> Bool
eqVariant Variant x
v Variant y
v' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (x :: [*]) (y :: [*]) z f.
(SameLength x y, HMapAux Variant (HFmap f) x y, Unvariant y z,
 HMapOutV_gety x z ~ y) =>
f -> Variant x -> z
hMapOutV UncurryEq
UncurryEq) forall a b. (a -> b) -> a -> b
$ forall (x :: [*]) (y :: [*]) (xy :: [*]).
ZipVariant x y xy =>
Variant x -> Variant y -> Maybe (Variant xy)
zipVariant Variant x
v Variant y
v'

data UncurryEq = UncurryEq

instance (ee ~ (e,e), Eq e, bool ~ Bool) =>
    ApplyAB UncurryEq ee bool where
      applyAB :: UncurryEq -> ee -> bool
applyAB UncurryEq
_ (e
e,e
e') = e
e forall a. Eq a => a -> a -> Bool
== e
e'

-- * Ord
instance Ord (Variant '[]) where
  compare :: Variant '[] -> Variant '[] -> Ordering
compare Variant '[]
_ Variant '[]
_ = Ordering
EQ

instance (Ord x, Ord (Variant xs)) => Ord (Variant (x ': xs)) where
  compare :: Variant (x : xs) -> Variant (x : xs) -> Ordering
compare Variant (x : xs)
a Variant (x : xs)
b = forall a. Ord a => a -> a -> Ordering
compare (forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
a) (forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
b)

-- * Bounded
instance (Bounded x, Bounded z,
          HRevAppR (Tagged s x ': xs) '[] ~ (Tagged t z ': sx),
          MkVariant t z (Tagged s x ': xs))
        => Bounded (Variant (Tagged s x ': xs)) where
  minBound :: Variant (Tagged s x : xs)
minBound = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label s) (forall a. Bounded a => a
minBound :: x) forall {k} (t :: k). Proxy t
Proxy
  maxBound :: Variant (Tagged s x : xs)
maxBound = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (forall a. Bounded a => a
maxBound :: z) forall {k} (t :: k). Proxy t
Proxy

-- * Enum
{- |

>>> let t = minBound :: Variant '[Tagged "x" Bool, Tagged "y" Bool]
>>> [t .. maxBound]
[V{x=False},V{x=True},V{y=False},V{y=True}]


[@Odd behavior@]
There are some arguments that this instance should not exist.

The last type in the Variant does not need to be Bounded. This
means that 'enumFrom' behaves a bit unexpectedly:

>>> [False .. ]
[False,True]

>>> [t .. ]
[V{x=False},V{x=True},V{y=False},V{y=True},V{y=*** Exception: Prelude.Enum.Bool.toEnum: bad argument

This is a \"feature\" because it allows an @Enum (Variant '[Tagged \"a\" Bool, Tagged \"n\" 'Integer'])@

Another difficult choice is that the lower bound is @fromEnum 0@ rather than @minBound@:

>>> take 5 [ minBound :: Variant '[Tagged "b" Bool, Tagged "i" Int] .. ]
[V{b=False},V{b=True},V{i=0},V{i=1},V{i=2}]

-}
instance (Enum x, Bounded x, Enum (Variant (y ': z))) => Enum (Variant (Tagged s x ': y ': z)) where
  fromEnum :: Variant (Tagged s x : y : z) -> Int
fromEnum Variant (Tagged s x : y : z)
v = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged s x : y : z)
v of
    Left x
x -> forall a. Enum a => a -> Int
fromEnum x
x
    Right Variant (y : z)
yz -> Int
1 forall a. Num a => a -> a -> a
+ forall a. Enum a => a -> Int
fromEnum (forall a. Bounded a => a
maxBound :: Tagged s x) forall a. Num a => a -> a -> a
+ forall a. Enum a => a -> Int
fromEnum Variant (y : z)
yz

  toEnum :: Int -> Variant (Tagged s x : y : z)
toEnum Int
n
      | Int
m forall a. Ord a => a -> a -> Bool
>= Int
n = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label s) (forall a. Enum a => Int -> a
toEnum Int
n) forall {k} (t :: k). Proxy t
Proxy
      | Bool
otherwise = forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum (Int
n forall a. Num a => a -> a -> a
- Int
m forall a. Num a => a -> a -> a
- Int
1)
    where m :: Int
m = forall a. Enum a => a -> Int
fromEnum (forall a. Bounded a => a
maxBound :: Tagged s x)

{- |

While the instances could be written Enum (Variant '[])
Eq/Ord which cannot produce values, so they have instances for
empty variants ('unsafeEmptyVariant'). Enum can produce values,
so it is better that @fromEnum 0 :: Variant '[]@ fails with No instance for
@Enum (Variant '[])@ than producing an invalid variant.

-}
instance Enum x => Enum (Variant '[Tagged s x]) where
  fromEnum :: Variant '[Tagged s x] -> Int
fromEnum Variant '[Tagged s x]
v = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant '[Tagged s x]
v of
    Left x
x -> forall a. Enum a => a -> Int
fromEnum x
x
    Either x (Variant '[])
_ -> forall a. HasCallStack => String -> a
error String
"Data.HList.Variant fromEnum impossible"
  toEnum :: Int -> Variant '[Tagged s x]
toEnum Int
n = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label s) (forall a. Enum a => Int -> a
toEnum Int
n) forall {k} (t :: k). Proxy t
Proxy

-- * Ix (TODO)

-- * Semigroup
instance (Unvariant '[Tagged t x] x, Semigroup x) => Semigroup (Variant '[Tagged t x]) where
    Variant '[Tagged t x]
a <> :: Variant '[Tagged t x]
-> Variant '[Tagged t x] -> Variant '[Tagged t x]
<> Variant '[Tagged t x]
b = case (forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
a, forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
b) of
                    (x
l, x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (x
l forall a. Semigroup a => a -> a -> a
<> x
r) forall {k} (t :: k). Proxy t
Proxy

instance (Semigroup x, Semigroup (Variant (a ': b))) => Semigroup (Variant (Tagged t x ': a ': b)) where
    Variant (Tagged t x : a : b)
a <> :: Variant (Tagged t x : a : b)
-> Variant (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
<> Variant (Tagged t x : a : b)
b = case (forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
a, forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
b) of
                    (Left x
l, Left x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (x
l forall a. Semigroup a => a -> a -> a
<> x
r) forall {k} (t :: k). Proxy t
Proxy
                    (Left x
l, Either x (Variant (a : b))
_) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) x
l forall {k} (t :: k). Proxy t
Proxy
                    (Either x (Variant (a : b))
_, Left x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) x
r forall {k} (t :: k). Proxy t
Proxy
                    (Right Variant (a : b)
l, Right Variant (a : b)
r) -> forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall a b. (a -> b) -> a -> b
$ Variant (a : b)
l forall a. Semigroup a => a -> a -> a
<> Variant (a : b)
r

-- * Monoid
instance (Unvariant '[Tagged t x] x, Monoid x) => Monoid (Variant '[Tagged t x]) where
    mempty :: Variant '[Tagged t x]
mempty = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) forall a. Monoid a => a
mempty forall {k} (t :: k). Proxy t
Proxy
    mappend :: Variant '[Tagged t x]
-> Variant '[Tagged t x] -> Variant '[Tagged t x]
mappend Variant '[Tagged t x]
a Variant '[Tagged t x]
b = case (forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
a, forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
b) of
                    (x
l, x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (forall a. Monoid a => a -> a -> a
mappend x
l x
r) forall {k} (t :: k). Proxy t
Proxy


instance (Monoid x, Monoid (Variant (a ': b))) => Monoid (Variant (Tagged t x ': a ': b)) where
    mempty :: Variant (Tagged t x : a : b)
mempty = forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall a. Monoid a => a
mempty
    mappend :: Variant (Tagged t x : a : b)
-> Variant (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mappend Variant (Tagged t x : a : b)
a Variant (Tagged t x : a : b)
b = case (forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
a, forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
b) of
                    (Left x
l, Left x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) (forall a. Monoid a => a -> a -> a
mappend x
l x
r) forall {k} (t :: k). Proxy t
Proxy
                    (Left x
l, Either x (Variant (a : b))
_) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) x
l forall {k} (t :: k). Proxy t
Proxy
                    (Either x (Variant (a : b))
_, Left x
r) -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) x
r forall {k} (t :: k). Proxy t
Proxy
                    (Right Variant (a : b)
l, Right Variant (a : b)
r) -> forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a -> a -> a
mappend Variant (a : b)
l Variant (a : b)
r

-- * Projection

{- | convert a variant with more fields into one with fewer (or the same)
fields.


>>> let ty = Proxy :: Proxy [Tagged "left" Int, Tagged "right" Int]
>>> let l = mkVariant _left 1 ty
>>> let r = mkVariant _right 2 ty


>>> map projectVariant [l, r] :: [Maybe (Variant '[Tagged "left" Int])]
[Just V{left=1},Nothing]


@'rearrangeVariant' = 'fromJust' . 'projectVariant'@ is one implementation
of 'rearrangeVariant', since the result can have the same fields with
a different order:

>>> let yt = Proxy :: Proxy [Tagged "right" Int, Tagged "left" Int]

>>> map projectVariant [l, r] `asTypeOf` [Just (mkVariant _left 0 yt)]
[Just V{left=1},Just V{right=2}]


-}
class ProjectVariant x y where
    projectVariant :: Variant x -> Maybe (Variant y)

instance (ProjectVariant x ys,
          HasField t (Variant x) (Maybe y),
          HOccursNot (Label t) (LabelsOf ys),
          ty ~ Tagged t y)
  => ProjectVariant x (ty ': ys) where
    projectVariant :: Variant x -> Maybe (Variant (ty : ys))
projectVariant Variant x
x = Maybe (Variant (ty : ys))
y forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (Variant (ty : ys))
ys
      where t :: Label t
t = forall {k} (l :: k). Label l
Label :: Label t
            y :: Maybe (Variant (ty : ys))
y = (\y
v -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant Label t
t y
v forall {k} (t :: k). Proxy t
Proxy) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variant x
x forall {k} (l :: k) r v. HasField l r v => r -> Label l -> v
.!. Label t
t
            ys :: Maybe (Variant (ty : ys))
ys = (Tagged t (Maybe y)
mty  forall e l. HExtend e l => e -> l -> HExtendR e l
.*.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x :: Maybe (Variant ys))
            mty :: Tagged t (Maybe y)
mty = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. Maybe a
Nothing :: Tagged t (Maybe y)

instance ProjectVariant x '[] where
    projectVariant :: Variant x -> Maybe (Variant '[])
projectVariant Variant x
_ = forall a. Maybe a
Nothing



{- | @projectExtendVariant = fmap 'extendVariant' . 'projectVariant'@

where intermediate variant is as large as possible. Used to implement
"Data.HList.Labelable".'projected'

Note that:

>>> let r = projectExtendVariant (mkVariant1 Label 1 :: Variant '[Tagged "x" Int])
>>> r :: Maybe (Variant '[Tagged "x" Integer])
Nothing

-}
class HAllTaggedLV y => ProjectExtendVariant x y where
    projectExtendVariant :: Variant x -> Maybe (Variant y)

instance HAllTaggedLV y => ProjectExtendVariant '[] y where
    projectExtendVariant :: Variant '[] -> Maybe (Variant y)
projectExtendVariant Variant '[]
_ = forall a. Maybe a
Nothing

instance (lv ~ Tagged l v,
          HMemberM lv y inY,
          ProjectExtendVariant' inY lv y,
          ProjectExtendVariant xs y
      ) => ProjectExtendVariant (lv ': xs) y where
  projectExtendVariant :: Variant (lv : xs) -> Maybe (Variant y)
projectExtendVariant Variant (lv : xs)
v = case forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (lv : xs)
v of
      Left lv
lv -> forall (inY :: Maybe [*]) lv (y :: [*]).
ProjectExtendVariant' inY lv y =>
Proxy inY -> lv -> Maybe (Variant y)
projectExtendVariant' (forall {k} (t :: k). Proxy t
Proxy :: Proxy inY) lv
lv
      Right Variant xs
v' -> forall (x :: [*]) (y :: [*]).
ProjectExtendVariant x y =>
Variant x -> Maybe (Variant y)
projectExtendVariant Variant xs
v'


class ProjectExtendVariant' (inY :: Maybe [*]) lv (y :: [*]) where
    projectExtendVariant' :: Proxy inY -> lv -> Maybe (Variant y)

instance ProjectExtendVariant' Nothing lv y where
    projectExtendVariant' :: Proxy 'Nothing -> lv -> Maybe (Variant y)
projectExtendVariant' Proxy 'Nothing
_ lv
_ = forall a. Maybe a
Nothing

instance (MkVariant l v y, lv ~ Tagged l v) => ProjectExtendVariant' (Just t) lv y where
    projectExtendVariant' :: Proxy ('Just t) -> lv -> Maybe (Variant y)
projectExtendVariant' Proxy ('Just t)
_ (Tagged v
v) = forall a. a -> Maybe a
Just (forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) v
v forall {k} (t :: k). Proxy t
Proxy)



class (ProjectVariant x yin,
       ProjectVariant x yout) => SplitVariant x yin yout where
    splitVariant :: Variant x -> Either (Variant yin) (Variant yout)

instance
   (-- implementation
    ProjectVariant x yin,
    ProjectVariant x yout,

    -- constraints to ensure exactly one of
    -- the uses of projectVariant gives a Just
    H2ProjectByLabels (LabelsOf yin) x xi xo,
    HRearrange (LabelsOf yin) xi yin,
    HRearrange (LabelsOf yout) xo yout,

    HLeftUnion xi xo xixo,
    HRearrange (LabelsOf x) xixo x,

    -- probably redundant
    HAllTaggedLV x, HAllTaggedLV yin, HAllTaggedLV yout) =>
  SplitVariant x yin yout where
  splitVariant :: Variant x -> Either (Variant yin) (Variant yout)
splitVariant Variant x
x = case (forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x, forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x) of
   (Maybe (Variant yin)
Nothing, Just Variant yout
yout) -> forall a b. b -> Either a b
Right Variant yout
yout
   (Just Variant yin
yin, Maybe (Variant yout)
Nothing) -> forall a b. a -> Either a b
Left Variant yin
yin
   (Maybe (Variant yin), Maybe (Variant yout))
_ -> forall a. HasCallStack => String -> a
error String
"Data.HList.Variant:splitVariant impossible"

-- | @projectVariant . extendsVariant = Just@ (when the types match up)
--
-- 'extendVariant' is a special case
class (HAllTaggedLV y, HAllTaggedLV x) => ExtendsVariant x y where
    extendsVariant :: Variant x -> Variant y

instance (MkVariant l e y, le ~ Tagged l e,
          ExtendsVariant (b ': bs) y) => ExtendsVariant (le ': b ': bs) y where
    extendsVariant :: Variant (le : b : bs) -> Variant y
extendsVariant Variant (le : b : bs)
v = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (le : b : bs)
v of
        Left e
e -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) forall {k} (t :: k). Proxy t
Proxy
        Right Variant (b : bs)
vs -> forall (x :: [*]) (y :: [*]).
ExtendsVariant x y =>
Variant x -> Variant y
extendsVariant Variant (b : bs)
vs

instance (HAllTaggedLV x, Unvariant '[le] e, MkVariant l e x,
          le ~ Tagged l e) => ExtendsVariant '[le] x where
    extendsVariant :: Variant '[le] -> Variant x
extendsVariant Variant '[le]
v = forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label l) (forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[le]
v) forall {k} (t :: k). Proxy t
Proxy


-- | @rearrangeVariant@ is a specialization of 'extendsVariant' whose
-- result is always . see also 'rearranged'
rearrangeVariant :: (SameLength v v', ExtendsVariant v v')
      => Variant v -> Variant v'
rearrangeVariant :: forall (v :: [*]) (v' :: [*]).
(SameLength v v', ExtendsVariant v v') =>
Variant v -> Variant v'
rearrangeVariant Variant v
v = forall (x :: [*]) (y :: [*]).
ExtendsVariant x y =>
Variant x -> Variant y
extendsVariant Variant v
v

instance (SameLength s a, ExtendsVariant s a,
          SameLength b t, ExtendsVariant b t) => Rearranged Variant s t a b
  where
    rearranged :: forall (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Variant a) (f (Variant b)) -> p (Variant s) (f (Variant t))
rearranged = forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso forall (v :: [*]) (v' :: [*]).
(SameLength v v', ExtendsVariant v v') =>
Variant v -> Variant v'
rearrangeVariant forall (v :: [*]) (v' :: [*]).
(SameLength v v', ExtendsVariant v v') =>
Variant v -> Variant v'
rearrangeVariant

-- | @Prism (Record tma) (Record tmb) (Variant ta) (Variant tb)@
--
-- see 'hMaybied''
hMaybied :: p (Variant v) (f (Variant v)) -> p (Record x) (f (Record r))
hMaybied p (Variant v) (f (Variant v))
x = forall b t s a.
(b -> t)
-> (s -> Either t a)
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p a (f b) -> p s (f t)
prism forall (v :: [*]) (r :: [*]).
VariantToHMaybied v r =>
Variant v -> Record r
variantToHMaybied
    (\Record x
s -> case forall (r :: [*]) (v :: [*]).
(HFoldr HMaybiedToVariantFs [Variant '[]] r [Variant v],
 VariantToHMaybied v r) =>
Record r -> [Variant v]
hMaybiedToVariants Record x
s of
          [Variant v
a] -> forall a b. b -> Either a b
Right Variant v
a
          [Variant v]
_ -> forall a b. a -> Either a b
Left (forall {x :: [*]} {y :: [*]} {f}.
(SameLength' x y, SameLength' y x, HMapAux HList (HFmap f) x y) =>
f -> Record x -> Record y
hMapR HCastF
HCastF Record x
s))
    p (Variant v) (f (Variant v))
x


data HCastF = HCastF

instance (mx ~ Maybe x,
          my ~ Maybe y,
          HCast y x) =>
  ApplyAB HCastF mx my where
    applyAB :: HCastF -> mx -> my
applyAB HCastF
_ mx
x = forall x y. HCast x y => x -> Maybe y
hCast forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< mx
x



{- | @Prism' (Record tma) (Variant ta)@

where @tma@ and @tmb@ are lists like

> tma ~ '[Tagged x (Maybe a), Tagged y (Maybe b)]
> ta  ~ '[Tagged x        a , Tagged y        b ]

If one element of the record is Just, the Variant will
contain that element. Otherwise, the prism fails.

[@Note@]

The types work out to define a prism:

@l = 'prism'' 'variantToHMaybied' ('listToMaybe' . 'hMaybiedToVariants')@

but the law: @s^?l ≡ Just a ==> l # a ≡ s@ is not followed,
because we could have:

@
  s, s2 :: Record '[Tagged "x" (Maybe Int), Tagged "y" (Maybe Char)]
  s = hBuild (Just 1) (Just '2')
  s2 = hBuild (Just 1) Nothing

  v :: Variant '[Tagged "x" Int, Tagged "y" Char]
  v = mkVariant (Label :: Label "x") 1 Proxy
@

So that @s^?l == Just v@. But @l#v == s2 /= s@, while the law
requires @l#v == s@. hMaybied avoids this problem by only
producing a value when there is only one present.

-}
hMaybied' :: p (Variant v) (f (Variant v)) -> p (Record x) (f (Record x))
hMaybied' p (Variant v) (f (Variant v))
x = forall a. Equality' a a
simple (forall {p :: * -> * -> *} {f :: * -> *} {x :: [*]} {v :: [*]}
       {v :: [*]} {r :: [*]}.
(Choice p, Applicative f,
 HFoldr HMaybiedToVariantFs [Variant '[]] x [Variant v],
 VariantToHMaybied v r, VariantToHMaybied v x, SameLength' x r,
 SameLength' r x, HMapAux HList (HFmap HCastF) x r) =>
p (Variant v) (f (Variant v)) -> p (Record x) (f (Record r))
hMaybied (forall a. Equality' a a
simple p (Variant v) (f (Variant v))
x))

class VariantToHMaybied v r | v -> r, r -> v where
    variantToHMaybied :: Variant v -> Record r

instance VariantToHMaybied '[] '[] where
    variantToHMaybied :: Variant '[] -> Record '[]
variantToHMaybied Variant '[]
_ = Record '[]
emptyRecord

instance (VariantToHMaybied v r,
          HReplicateF nr ConstTaggedNothing () r,

          tx ~ Tagged t x,
          tmx ~ Tagged t (Maybe x))
    => VariantToHMaybied (tx ': v) (tmx ': r) where
      variantToHMaybied :: Variant (tx : v) -> Record (tmx : r)
variantToHMaybied Variant (tx : v)
v = case forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (tx : v)
v of
            Left x
x -> forall (r :: [*]). HList r -> Record r
Record
                forall a b. (a -> b) -> a -> b
$ forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a. a -> Maybe a
Just x
x))
                forall a b. (a -> b) -> a -> b
$ forall (n :: HNat) f z (r :: [*]).
(HReplicateF n f z r, HLengthEq r n) =>
Proxy n -> f -> z -> HList r
hReplicateF forall {k} (t :: k). Proxy t
Proxy ConstTaggedNothing
ConstTaggedNothing ()
            Right Variant v
rest ->
                case forall (v :: [*]) (r :: [*]).
VariantToHMaybied v r =>
Variant v -> Record r
variantToHMaybied Variant v
rest of
                  Record HList r
a -> forall (r :: [*]). HList r -> Record r
Record forall a b. (a -> b) -> a -> b
$ (forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. Maybe a
Nothing :: Tagged t (Maybe x)) forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList r
a
          -- don't use (.*.) because we have (LabelsOf v ~ LabelsOf r), so
          -- the duplicate check (HRLabelSet) implied by (.*.) is redundant

data ConstTaggedNothing = ConstTaggedNothing
instance (y ~ Tagged t (Maybe e)) => ApplyAB ConstTaggedNothing x y where
    applyAB :: ConstTaggedNothing -> x -> y
applyAB ConstTaggedNothing
_ x
_ = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. Maybe a
Nothing

-- | Every element of the record that is Just becomes one element
-- in the resulting list. See 'hMaybied'' example types that @r@
-- and @v@ can take.
hMaybiedToVariants ::
  (HFoldr HMaybiedToVariantFs [Variant '[]] r [Variant v], -- impl
   VariantToHMaybied v r -- evidence for typechecking
  ) => Record r -> [Variant v]
hMaybiedToVariants :: forall (r :: [*]) (v :: [*]).
(HFoldr HMaybiedToVariantFs [Variant '[]] r [Variant v],
 VariantToHMaybied v r) =>
Record r -> [Variant v]
hMaybiedToVariants (Record HList r
r) = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr HMaybiedToVariantFs
HMaybiedToVariantFs ([] :: [Variant '[]]) HList r
r

data HMaybiedToVariantFs = HMaybiedToVariantFs

instance (x ~ (Tagged t (Maybe e), [Variant v]),
          y ~ [Variant (Tagged t e ': v)],
          MkVariant t e (Tagged t e ': v))
        => ApplyAB HMaybiedToVariantFs x y where

  applyAB :: HMaybiedToVariantFs -> x -> y
applyAB HMaybiedToVariantFs
_ (Tagged Maybe e
me, [Variant v]
v) = case Maybe e
me of
    Just e
e -> forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (forall {k} (l :: k). Label l
Label :: Label t) e
e forall {k} (t :: k). Proxy t
Proxy forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant [Variant v]
v
    Maybe e
_ -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant [Variant v]
v