{-# 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)
#if __GLASGOW_HASKELL__ <= 906
import Data.Semigroup (Semigroup( .. ))
#endif
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 = Int -> Any -> Variant vs
forall (vs :: [*]). Int -> Any -> Variant vs
Variant Int
n (v -> Any
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) = Int -> Any -> Variant v'
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 = Variant v -> Variant v'
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 = (Variant s -> Variant a)
-> (Variant b -> Variant t)
-> p (Variant a) (f (Variant b))
-> p (Variant s) (f (Variant t))
forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso Variant s -> Variant a
forall (v :: [*]) (v' :: [*]).
(RecordValuesR v ~ RecordValuesR v', SameLength v v') =>
Variant v -> Variant v'
castVariant Variant b -> Variant t
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) = 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 = Int -> () -> Variant '[]
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 Label l -> Maybe e -> Tagged l (Maybe e)
forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. e -> Maybe e
forall a. a -> Maybe a
Just e
v Tagged l (Maybe e)
-> Variant '[] -> HExtendR (Tagged l (Maybe e)) (Variant '[])
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 = Int -> v -> Variant vs
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant (Proxy n -> Int
forall i. Integral i => Proxy n -> i
forall (n :: HNat) i. (HNat2Integral n, Integral i) => Proxy n -> i
hNat2Integral (Proxy n
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)
          | Proxy n -> Int
forall i. Integral i => Proxy n -> i
forall (n :: HNat) i. (HNat2Integral n, Integral i) => Proxy n -> i
hNat2Integral (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = a -> Maybe a
forall a. a -> Maybe a
Just (Any -> a
forall a b. a -> b
unsafeCoerce Any
d)
          | Bool
otherwise = Maybe a
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) = x -> Either x (Variant xs)
forall a b. a -> Either a b
Left (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)
splitVariant1 (Variant Int
n Any
x) = Variant xs -> Either x (Variant xs)
forall a b. b -> Either a b
Right (Int -> Any -> Variant xs
forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nInt -> Int -> Int
forall 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) = x -> Either x (Variant xs)
forall a b. a -> Either a b
Left (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)
splitVariant1' (Variant Int
n Any
x) = Variant xs -> Either x (Variant xs)
forall a b. b -> Either a b
Right (Int -> Any -> Variant xs
forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nInt -> Int -> Int
forall 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) = Int -> Any -> Variant (e : l)
forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
mInt -> Int -> Int
forall 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 = (b -> Variant t)
-> (Variant s -> Either (Variant t) a)
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p a (f b) -> p (Variant s) (f (Variant t))
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 -> Label x -> b -> Proxy t -> Variant t
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label x -> b -> proxy t -> Variant t
mkVariant Label x
x b
b Proxy t
forall {k} (t :: k). Proxy t
Proxy)
                  (\Variant s
s -> case Label x -> Variant s -> Maybe a
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 -> a -> Either (Variant t) a
forall a b. b -> Either a b
Right a
a
                    Maybe a
Nothing -> Variant t -> Either (Variant t) a
forall a b. a -> Either a b
Left (Variant s -> Variant t
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{"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variant vs -> ShowS
forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant vs
v ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'}'Char -> ShowS
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 Variant (Tagged l v : w : ws) -> Either v (Variant (w : ws))
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 -> Label l -> String
forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel Label l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rest
        Right Variant (w : ws)
wws -> Variant (w : ws) -> ShowS
forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant (w : ws)
wws
      where l :: Label l
l = Label 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 Variant '[Tagged l v] -> Either v (Variant '[])
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant '[lv]
Variant '[Tagged l v]
vs of
        Left v
v -> \String
rest -> Label l -> String
forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel Label l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rest
        Right Variant '[]
_ -> String -> ShowS
forall a. HasCallStack => String -> a
error String
"invalid variant"
      where l :: Label l
l = Label 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
_ = ReadP (Variant v) -> ReadS (Variant v)
forall a. ReadP a -> ReadS a
readP_to_S (ReadP (Variant v) -> ReadS (Variant v))
-> ReadP (Variant v) -> ReadS (Variant v)
forall a b. (a -> b) -> a -> b
$ do
      String
_ <- String -> ReadP String
string String
"V{"
      Variant v
r <- ReadP (Variant v)
forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
      String
_ <- String -> ReadP String
string String
"}"
      Variant v -> ReadP (Variant v)
forall a. a -> ReadP a
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 = Variant '[] -> ReadP (Variant '[])
forall a. a -> ReadP a
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 <- ReadP v -> ReadP (Maybe v)
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 <- ReadP (Variant vs)
forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
          Variant (Tagged l v : vs) -> ReadP (Variant (Tagged l v : vs))
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (Label l
l Label l -> Maybe v -> Tagged l (Maybe v)
forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. Maybe v
mlv Tagged l (Maybe v)
-> Variant vs -> HExtendR (Tagged l (Maybe v)) (Variant vs)
forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Variant vs
rest)
        Just v
e -> do
          Variant (Tagged l v : vs) -> ReadP (Variant (Tagged l v : vs))
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (Label l
-> v -> Proxy (Tagged l v : vs) -> Variant (Tagged l v : vs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label l
-> v -> proxy (Tagged l v : vs) -> Variant (Tagged l v : vs)
mkVariant Label l
l v
e Proxy (Tagged l v : vs)
p)

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

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

        p :: Proxy (Tagged l v : vs)
p = Proxy (Tagged l v : vs)
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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant v -> c (Variant v)
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')
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant v -> c (Variant v)
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 b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy v -> Int -> c (Variant v)
forall (es :: [*]) (v :: [*]) (c :: * -> *).
GunfoldVariant es v =>
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy es -> Int -> c (Variant v)
forall (c :: * -> *).
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy v -> Int -> c (Variant v)
gunfoldVariant (\b -> Variant v
con -> c (b -> Variant v) -> c (Variant v)
forall b r. Data b => c (b -> r) -> c r
k ((b -> Variant v) -> c (b -> Variant v)
forall r. r -> c r
z b -> Variant v
con)) (Proxy v
forall {k} (t :: k). Proxy t
Proxy :: Proxy v) (Constr -> Int
constrIndex Constr
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    toConstr :: Variant v -> Constr
toConstr v :: Variant v
v@(Variant Int
n Any
_) = case Int -> [Constr] -> [Constr]
forall a. Int -> [a] -> [a]
drop Int
n (DataType -> Variant v -> [Constr]
forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
forall (proxy :: [*] -> *). DataType -> proxy v -> [Constr]
variantConstrs (Variant v -> DataType
forall a. Data a => a -> DataType
dataTypeOf Variant v
v) Variant v
v) of
        Constr
c : [Constr]
_ -> Constr
c
        [Constr]
_ -> String -> 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 (TypeRep -> String
forall a. Show a => a -> String
show (Variant v -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Variant v
x)) (DataType -> Variant v -> [Constr]
forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
forall (proxy :: [*] -> *). DataType -> proxy v -> [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 (Label l -> String
forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel (Label l
forall {k} (l :: k). Label l
Label :: Label l)) [] Fixity
Prefix Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
:
        DataType -> Proxy xs -> [Constr]
forall (xs :: [*]) (proxy :: [*] -> *).
VariantConstrs xs =>
DataType -> proxy xs -> [Constr]
forall (proxy :: [*] -> *). DataType -> proxy xs -> [Constr]
variantConstrs DataType
dt (Proxy xs
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
_ = (e -> Variant v) -> c (Variant v)
forall b. Data b => (b -> Variant v) -> c (Variant v)
f (\e
e -> Label l -> e -> Proxy v -> Variant v
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> e -> proxy v -> Variant v
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) Proxy v
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 = (e -> Variant v) -> c (Variant v)
forall b. Data b => (b -> Variant v) -> c (Variant v)
f (\e
e -> Label l -> e -> Proxy v -> Variant v
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> e -> proxy v -> Variant v
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) Proxy v
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 b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy (b : bs) -> Int -> c (Variant v)
forall (es :: [*]) (v :: [*]) (c :: * -> *).
GunfoldVariant es v =>
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy es -> Int -> c (Variant v)
forall (c :: * -> *).
(forall b. Data b => (b -> Variant v) -> c (Variant v))
-> Proxy (b : bs) -> Int -> c (Variant v)
gunfoldVariant (b -> Variant v) -> c (Variant v)
forall b. Data b => (b -> Variant v) -> c (Variant v)
f (Proxy (b : bs)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (b ': bs)) (Int
nInt -> Int -> Int
forall 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 Variant (Tagged l v : b : c) -> Either v (Variant (b : c))
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (a : b : c)
Variant (Tagged l v : b : c)
xxs of
      Right Variant (b : c)
xs -> (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant (b : c) -> c (Variant r)
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')
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Variant (b : c) -> c (Variant r)
gfoldlVariant c (d -> b) -> d -> c b
forall d b. Data d => c (d -> b) -> d -> c b
k g -> c g
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 = Label l -> v -> Proxy r -> Variant r
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> v -> proxy r -> Variant r
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) v
e Proxy r
forall {k} (t :: k). Proxy t
Proxy
            in (v -> Variant r) -> c (v -> Variant r)
forall g. g -> c g
z v -> Variant r
mkV c (v -> Variant r) -> v -> c (Variant r)
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 = (v -> Variant b) -> c (v -> Variant b)
forall g. g -> c g
z v -> Variant b
mkV c (v -> Variant b) -> v -> c (Variant b)
forall d b. Data d => c (d -> b) -> d -> c b
`k` Variant '[a] -> v
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[a]
xxs
        where mkV :: v -> Variant b
mkV v
e = Label l -> v -> Proxy b -> Variant b
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> v -> proxy b -> Variant b
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) v
e Proxy b
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 = HMapV f -> Variant x -> Variant y
forall f a b. ApplyAB f a b => f -> a -> b
applyAB (f -> HMapV f
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 = Variant y -> z
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant (f -> Variant x -> Variant y
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 = HFmap f -> Variant x -> Variant y
forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux (f -> HFmap f
forall f. f -> HFmap f
HFmap f
f) vx
Variant x
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 Variant '[te] -> Either te (Variant '[])
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant '[te]
v of
        Left te
te -> Int -> te' -> Variant '[te']
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 (f -> te -> te'
forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f te
te :: te')
        Right Variant '[]
_ -> String -> Variant '[te']
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 Variant (te : l : ls) -> Either te (Variant (l : ls))
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (te : l : ls)
v of
          Left te
te -> Int -> te' -> Variant (te' : l' : ls')
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 (f -> te -> te'
forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f te
te :: te')
          Right Variant (l : ls)
es -> Variant (l' : ls') -> Variant (te' : l' : ls')
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (f -> Variant (l : ls) -> Variant (l' : ls')
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 Label l -> Variant v -> Maybe _e
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 -> Label l -> e -> Proxy v' -> Variant v'
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> e -> proxy v' -> Variant v'
mkVariant Label l
l e
e (Proxy v'
forall {k} (t :: k). Proxy t
Proxy :: Proxy v')
          Maybe _e
Nothing -> Variant v -> Variant v'
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
_ = Int -> e -> Variant (Tagged l e : v)
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 e
e
    Tagged Maybe e
Nothing .*. (Variant Int
n Any
e) = Int -> Any -> Variant (Tagged l e : v)
forall (vs :: [*]). Int -> Any -> Variant vs
Variant (Int
nInt -> Int -> Int
forall 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' = Variant v -> e
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 = Proxy b -> Variant v -> e
forall {k} (b :: k) (v :: [*]) e.
Unvariant1 b v e =>
Proxy b -> Variant v -> e
unvariant1 (Proxy b
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
_ = Variant (v : vs) -> e
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
_ = String -> Variant (v : vs) -> UnvariantTypeMismatch (v : vs)
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
_ = String -> Variant '[] -> Proxy "Unvariant applied to empty variant"
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
_) = (b -> Variant t) -> f b -> f (Variant t)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
e' -> Int -> b -> Variant t
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
n b
e')
                                      (a -> f b
f (Variant s -> a
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 = (Variant t -> f (Variant t)) -> Variant t -> f (Variant t)
forall a (p :: * -> * -> *) (f :: * -> *). p a (f a) -> p a (f a)
simple ((a -> f a) -> Variant t -> f (Variant t)
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 '[]
_ = Maybe (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 (Variant (Tagged t x : xs) -> Either x (Variant xs)
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (tx : xs)
Variant (Tagged t x : xs)
x, Variant (Tagged t y : ys) -> Either y (Variant ys)
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (ty : ys)
Variant (Tagged t y : ys)
y) of
        (Left x
x', Left y
y') -> Variant (txy : zs) -> Maybe (Variant (txy : zs))
forall a. a -> Maybe a
Just (Label t -> (x, y) -> Proxy (txy : zs) -> Variant (txy : zs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> (x, y) -> proxy (txy : zs) -> Variant (txy : zs)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (x
x',y
y') Proxy (txy : zs)
forall {k} (t :: k). Proxy t
Proxy)
        (Right Variant xs
x', Right Variant ys
y') -> Variant zs -> Variant (txy : zs)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant zs -> Variant (txy : zs))
-> Maybe (Variant zs) -> Maybe (Variant (txy : zs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variant xs -> Variant ys -> Maybe (Variant zs)
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))
_ -> Maybe (Variant (txy : zs))
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 Variant (Tagged t (x, y) : xy2 : xys)
-> Either (x, y) (Variant (xy2 : xys))
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (txy : xy2 : xys)
Variant (Tagged t (x, y) : xy2 : xys)
xy of
      Left (x
x,y
y) -> (Label t -> x -> Proxy (tx : x2 : xs) -> Variant (tx : x2 : xs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> x -> proxy (tx : x2 : xs) -> Variant (tx : x2 : xs)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
x Proxy (tx : x2 : xs)
forall {k} (t :: k). Proxy t
Proxy,
                     Label t -> y -> Proxy (ty : y2 : ys) -> Variant (ty : y2 : ys)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> y -> proxy (ty : y2 : ys) -> Variant (ty : y2 : ys)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) y
y Proxy (ty : y2 : ys)
forall {k} (t :: k). Proxy t
Proxy)
      Right Variant (xy2 : xys)
xy' | (Variant (x2 : xs)
x,Variant (y2 : ys)
y) <- Variant (xy2 : xys) -> (Variant (x2 : xs), Variant (y2 : ys))
forall (r :: [*] -> *) (x :: [*]) (y :: [*]) (xy :: [*]).
HUnzip r x y xy =>
r xy -> (r x, r y)
hUnzip Variant (xy2 : xys)
xy' ->
                    (Variant (x2 : xs) -> Variant (tx : x2 : xs)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant (x2 : xs)
x,
                     Variant (y2 : ys) -> Variant (ty : y2 : ys)
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) <- Variant '[txy] -> Tagged t (x, y)
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[txy]
xy =
        (Label t -> x -> Variant '[Tagged t x]
forall {k} {l :: k} {e}. Label l -> e -> Variant '[Tagged l e]
mkVariant1 Label t
forall {k} (l :: k). Label l
Label x
x, Label t -> y -> Variant '[Tagged t y]
forall {k} {l :: k} {e}. Label l -> e -> Variant '[Tagged l e]
mkVariant1 Label t
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 Variant (Tagged l v : vs) -> Either v (Variant vs)
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (lv : vs)
Variant (Tagged l v : vs)
lvs of
                  Left v
v | v'
v' <- Label l -> Record fs -> (v -> v) -> DemoteMaybe (v -> v) f
forall t. Label l -> Record fs -> t -> DemoteMaybe t f
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 (v -> v
forall a. a -> a
id :: v -> v) v
v -> Label l -> v' -> Proxy (lv' : rs) -> Variant (lv' : rs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label l -> v' -> proxy (lv' : rs) -> Variant (lv' : rs)
mkVariant Label l
l v'
v' Proxy (lv' : rs)
forall {k} (t :: k). Proxy t
Proxy
                  Right Variant vs
vs -> Variant rs -> Variant (lv' : rs)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant rs -> Variant (lv' : rs))
-> Variant rs -> Variant (lv' : rs)
forall a b. (a -> b) -> a -> b
$ Record fs -> Variant vs -> Variant rs
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 = Label 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 = Record fs -> Variant v -> Variant v'
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 (Variant (x : xs) -> Either x (Variant xs)
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
v, Variant (x : xs) -> Either x (Variant xs)
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
v') of
    (Left x
l, Left x
r) -> x
l x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
r
    (Right Variant xs
l, Right Variant xs
r) -> Variant xs
l Variant xs -> Variant xs -> Bool
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' = Bool -> (Variant x -> Bool) -> Maybe (Variant x) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (UncurryEq -> Variant x -> Bool
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) (Maybe (Variant x) -> Bool) -> Maybe (Variant x) -> Bool
forall a b. (a -> b) -> a -> b
$ Variant x -> Variant y -> Maybe (Variant x)
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 e -> e -> Bool
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 = Either x (Variant xs) -> Either x (Variant xs) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Variant (x : xs) -> Either x (Variant xs)
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (x : xs)
a) (Variant (x : xs) -> Either x (Variant xs)
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 = Label s
-> x -> Proxy (Tagged s x : xs) -> Variant (Tagged s x : xs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label s
-> x -> proxy (Tagged s x : xs) -> Variant (Tagged s x : xs)
mkVariant (Label s
forall {k} (l :: k). Label l
Label :: Label s) (x
forall a. Bounded a => a
minBound :: x) Proxy (Tagged s x : xs)
forall {k} (t :: k). Proxy t
Proxy
  maxBound :: Variant (Tagged s x : xs)
maxBound = Label t
-> z -> Proxy (Tagged s x : xs) -> Variant (Tagged s x : xs)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> z -> proxy (Tagged s x : xs) -> Variant (Tagged s x : xs)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (z
forall a. Bounded a => a
maxBound :: z) Proxy (Tagged s x : xs)
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 Variant (Tagged s x : y : z) -> Either x (Variant (y : z))
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 -> x -> Int
forall a. Enum a => a -> Int
fromEnum x
x
    Right Variant (y : z)
yz -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tagged s x -> Int
forall a. Enum a => a -> Int
fromEnum (Tagged s x
forall a. Bounded a => a
maxBound :: Tagged s x) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Variant (y : z) -> Int
forall a. Enum a => a -> Int
fromEnum Variant (y : z)
yz

  toEnum :: Int -> Variant (Tagged s x : y : z)
toEnum Int
n
      | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = Label s
-> x -> Proxy (Tagged s x : y : z) -> Variant (Tagged s x : y : z)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label s
-> x -> proxy (Tagged s x : y : z) -> Variant (Tagged s x : y : z)
mkVariant (Label s
forall {k} (l :: k). Label l
Label :: Label s) (Int -> x
forall a. Enum a => Int -> a
toEnum Int
n) Proxy (Tagged s x : y : z)
forall {k} (t :: k). Proxy t
Proxy
      | Bool
otherwise = Variant (y : z) -> Variant (Tagged s x : y : z)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant (y : z) -> Variant (Tagged s x : y : z))
-> Variant (y : z) -> Variant (Tagged s x : y : z)
forall a b. (a -> b) -> a -> b
$ Int -> Variant (y : z)
forall a. Enum a => Int -> a
toEnum (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    where m :: Int
m = Tagged s x -> Int
forall a. Enum a => a -> Int
fromEnum (Tagged s x
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 Variant '[Tagged s x] -> Either x (Variant '[])
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 -> x -> Int
forall a. Enum a => a -> Int
fromEnum x
x
    Either x (Variant '[])
_ -> String -> Int
forall a. HasCallStack => String -> a
error String
"Data.HList.Variant fromEnum impossible"
  toEnum :: Int -> Variant '[Tagged s x]
toEnum Int
n = Label s -> x -> Proxy '[Tagged s x] -> Variant '[Tagged s x]
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label s -> x -> proxy '[Tagged s x] -> Variant '[Tagged s x]
mkVariant (Label s
forall {k} (l :: k). Label l
Label :: Label s) (Int -> x
forall a. Enum a => Int -> a
toEnum Int
n) Proxy '[Tagged s x]
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 (Variant '[Tagged t x] -> x
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
a, Variant '[Tagged t x] -> x
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
b) of
                    (x
l, x
r) -> Label t -> x -> Proxy '[Tagged t x] -> Variant '[Tagged t x]
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> x -> proxy '[Tagged t x] -> Variant '[Tagged t x]
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (x
l x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
r) Proxy '[Tagged t x]
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 (Variant (Tagged t x : a : b) -> Either x (Variant (a : b))
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
a, Variant (Tagged t x : a : b) -> Either x (Variant (a : b))
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) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (x
l x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
r) Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Left x
l, Either x (Variant (a : b))
_) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
l Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Either x (Variant (a : b))
_, Left x
r) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
r Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Right Variant (a : b)
l, Right Variant (a : b)
r) -> Variant (a : b) -> Variant (Tagged t x : a : b)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant (a : b) -> Variant (Tagged t x : a : b))
-> Variant (a : b) -> Variant (Tagged t x : a : b)
forall a b. (a -> b) -> a -> b
$ Variant (a : b)
l Variant (a : b) -> Variant (a : b) -> Variant (a : b)
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 = Label t -> x -> Proxy '[Tagged t x] -> Variant '[Tagged t x]
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> x -> proxy '[Tagged t x] -> Variant '[Tagged t x]
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
forall a. Monoid a => a
mempty Proxy '[Tagged t x]
forall {k} (t :: k). Proxy t
Proxy
#if __GLASGOW_HASKELL__ <= 906
    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 (Variant '[Tagged t x] -> x
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
a, Variant '[Tagged t x] -> x
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[Tagged t x]
b) of
                    (x
l, x
r) -> Label t -> x -> Proxy '[Tagged t x] -> Variant '[Tagged t x]
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> x -> proxy '[Tagged t x] -> Variant '[Tagged t x]
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (x -> x -> x
forall a. Monoid a => a -> a -> a
mappend x
l x
r) Proxy '[Tagged t x]
forall {k} (t :: k). Proxy t
Proxy
#endif


instance (Monoid x, Monoid (Variant (a ': b))) => Monoid (Variant (Tagged t x ': a ': b)) where
    mempty :: Variant (Tagged t x : a : b)
mempty = Variant (a : b) -> Variant (Tagged t x : a : b)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant (a : b)
forall a. Monoid a => a
mempty
#if __GLASGOW_HASKELL__ <= 906
    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 (Variant (Tagged t x : a : b) -> Either x (Variant (a : b))
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (Tagged t x : a : b)
a, Variant (Tagged t x : a : b) -> Either x (Variant (a : b))
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) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) (x -> x -> x
forall a. Monoid a => a -> a -> a
mappend x
l x
r) Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Left x
l, Either x (Variant (a : b))
_) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
l Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Either x (Variant (a : b))
_, Left x
r) -> Label t
-> x -> Proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t
-> x -> proxy (Tagged t x : a : b) -> Variant (Tagged t x : a : b)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) x
r Proxy (Tagged t x : a : b)
forall {k} (t :: k). Proxy t
Proxy
                    (Right Variant (a : b)
l, Right Variant (a : b)
r) -> Variant (a : b) -> Variant (Tagged t x : a : b)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant (Variant (a : b) -> Variant (Tagged t x : a : b))
-> Variant (a : b) -> Variant (Tagged t x : a : b)
forall a b. (a -> b) -> a -> b
$ Variant (a : b) -> Variant (a : b) -> Variant (a : b)
forall a. Monoid a => a -> a -> a
mappend Variant (a : b)
l Variant (a : b)
r
#endif

-- * 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 Maybe (Variant (ty : ys))
-> Maybe (Variant (ty : ys)) -> Maybe (Variant (ty : ys))
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (Variant (ty : ys))
ys
      where t :: Label t
t = Label t
forall {k} (l :: k). Label l
Label :: Label t
            y :: Maybe (Variant (ty : ys))
y = (\y
v -> Label t -> y -> Proxy (ty : ys) -> Variant (ty : ys)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> y -> proxy (ty : ys) -> Variant (ty : ys)
mkVariant Label t
t y
v Proxy (ty : ys)
forall {k} (t :: k). Proxy t
Proxy) (y -> Variant (ty : ys)) -> Maybe y -> Maybe (Variant (ty : ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variant x
x Variant x -> Label t -> Maybe y
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  Tagged t (Maybe y)
-> Variant ys -> HExtendR (Tagged t (Maybe y)) (Variant ys)
forall e l. HExtend e l => e -> l -> HExtendR e l
.*.) (Variant ys -> Variant (ty : ys))
-> Maybe (Variant ys) -> Maybe (Variant (ty : ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Variant x -> Maybe (Variant ys)
forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x :: Maybe (Variant ys))
            mty :: Tagged t (Maybe y)
mty = Maybe y -> Tagged t (Maybe y)
forall {k} (s :: k) b. b -> Tagged s b
Tagged Maybe y
forall a. Maybe a
Nothing :: Tagged t (Maybe y)

instance ProjectVariant x '[] where
    projectVariant :: Variant x -> Maybe (Variant '[])
projectVariant Variant x
_ = Maybe (Variant '[])
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 '[]
_ = Maybe (Variant y)
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 Variant (lv : xs) -> Either lv (Variant xs)
forall x (xs :: [*]). Variant (x : xs) -> Either x (Variant xs)
splitVariant1' Variant (lv : xs)
v of
      Left lv
lv -> Proxy inY -> lv -> Maybe (Variant y)
forall (inY :: Maybe [*]) lv (y :: [*]).
ProjectExtendVariant' inY lv y =>
Proxy inY -> lv -> Maybe (Variant y)
projectExtendVariant' (Proxy inY
forall {k} (t :: k). Proxy t
Proxy :: Proxy inY) lv
lv
      Right Variant xs
v' -> Variant xs -> Maybe (Variant y)
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
_ = Maybe (Variant y)
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) = Variant y -> Maybe (Variant y)
forall a. a -> Maybe a
Just (Label l -> v -> Proxy y -> Variant y
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> v -> proxy y -> Variant y
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) v
v Proxy y
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 (Variant x -> Maybe (Variant yin)
forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x, Variant x -> Maybe (Variant yout)
forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant x
x) of
   (Maybe (Variant yin)
Nothing, Just Variant yout
yout) -> Variant yout -> Either (Variant yin) (Variant yout)
forall a b. b -> Either a b
Right Variant yout
yout
   (Just Variant yin
yin, Maybe (Variant yout)
Nothing) -> Variant yin -> Either (Variant yin) (Variant yout)
forall a b. a -> Either a b
Left Variant yin
yin
   (Maybe (Variant yin), Maybe (Variant yout))
_ -> String -> Either (Variant yin) (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 Variant (Tagged l e : b : bs) -> Either e (Variant (b : bs))
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (le : b : bs)
Variant (Tagged l e : b : bs)
v of
        Left e
e -> Label l -> e -> Proxy y -> Variant y
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> e -> proxy y -> Variant y
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) (e
e :: e) Proxy y
forall {k} (t :: k). Proxy t
Proxy
        Right Variant (b : bs)
vs -> Variant (b : bs) -> Variant y
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 = Label l -> e -> Proxy x -> Variant x
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *). Label l -> e -> proxy x -> Variant x
mkVariant (Label l
forall {k} (l :: k). Label l
Label :: Label l) (Variant '[le] -> e
forall (v :: [*]) e. Unvariant v e => Variant v -> e
unvariant Variant '[le]
v) Proxy x
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 = Variant v -> Variant 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 = (Variant s -> Variant a)
-> (Variant b -> Variant t)
-> p (Variant a) (f (Variant b))
-> p (Variant s) (f (Variant t))
forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso Variant s -> Variant a
forall (v :: [*]) (v' :: [*]).
(SameLength v v', ExtendsVariant v v') =>
Variant v -> Variant v'
rearrangeVariant Variant b -> Variant t
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 = (Variant v -> Record r)
-> (Record x -> Either (Record r) (Variant v))
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p (Variant v) (f (Variant v)) -> p (Record x) (f (Record r))
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 Variant v -> Record r
forall (v :: [*]) (r :: [*]).
VariantToHMaybied v r =>
Variant v -> Record r
variantToHMaybied
    (\Record x
s -> case Record x -> [Variant v]
forall (r :: [*]) (v :: [*]).
(HFoldr HMaybiedToVariantFs [Variant '[]] r [Variant v],
 VariantToHMaybied v r) =>
Record r -> [Variant v]
hMaybiedToVariants Record x
s of
          [Variant v
a] -> Variant v -> Either (Record r) (Variant v)
forall a b. b -> Either a b
Right Variant v
a
          [Variant v]
_ -> Record r -> Either (Record r) (Variant v)
forall a b. a -> Either a b
Left (HCastF -> Record x -> Record r
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 = x -> Maybe y
forall x y. HCast x y => x -> Maybe y
hCast (x -> Maybe y) -> Maybe x -> Maybe y
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< mx
Maybe x
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 = p (Record x) (f (Record x)) -> p (Record x) (f (Record x))
forall a (p :: * -> * -> *) (f :: * -> *). p a (f a) -> p a (f a)
simple (p (Variant v) (f (Variant v)) -> p (Record x) (f (Record x))
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 (p (Variant v) (f (Variant v)) -> p (Variant v) (f (Variant v))
forall a (p :: * -> * -> *) (f :: * -> *). p a (f a) -> p a (f 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 Variant (Tagged t x : v) -> Either x (Variant v)
forall {k} (s :: k) x (xs :: [*]).
Variant (Tagged s x : xs) -> Either x (Variant xs)
splitVariant1 Variant (tx : v)
Variant (Tagged t x : v)
v of
            Left x
x -> HList (tmx : r) -> Record (tmx : r)
forall (r :: [*]). HList r -> Record r
Record
                (HList (tmx : r) -> Record (tmx : r))
-> HList (tmx : r) -> Record (tmx : r)
forall a b. (a -> b) -> a -> b
$ tmx -> HList r -> HList (tmx : r)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (Maybe x -> Tagged t (Maybe x)
forall {k} (s :: k) b. b -> Tagged s b
Tagged (x -> Maybe x
forall a. a -> Maybe a
Just x
x))
                (HList r -> HList (tmx : r)) -> HList r -> HList (tmx : r)
forall a b. (a -> b) -> a -> b
$ Proxy nr -> ConstTaggedNothing -> () -> HList r
forall (n :: HNat) f z (r :: [*]).
(HReplicateF n f z r, HLengthEq r n) =>
Proxy n -> f -> z -> HList r
hReplicateF Proxy nr
forall {k} (t :: k). Proxy t
Proxy ConstTaggedNothing
ConstTaggedNothing ()
            Right Variant v
rest ->
                case Variant v -> Record r
forall (v :: [*]) (r :: [*]).
VariantToHMaybied v r =>
Variant v -> Record r
variantToHMaybied Variant v
rest of
                  Record HList r
a -> HList (tmx : r) -> Record (tmx : r)
forall (r :: [*]). HList r -> Record r
Record (HList (tmx : r) -> Record (tmx : r))
-> HList (tmx : r) -> Record (tmx : r)
forall a b. (a -> b) -> a -> b
$ (Maybe x -> Tagged t (Maybe x)
forall {k} (s :: k) b. b -> Tagged s b
Tagged Maybe x
forall a. Maybe a
Nothing :: Tagged t (Maybe x)) tmx -> HList r -> HList (tmx : r)
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
_ = Maybe e -> Tagged t (Maybe e)
forall {k} (s :: k) b. b -> Tagged s b
Tagged Maybe e
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) = HMaybiedToVariantFs -> [Variant '[]] -> HList r -> [Variant v]
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 -> Label t -> e -> Proxy (Tagged t e : v) -> Variant (Tagged t e : v)
forall {k} (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
forall (proxy :: [*] -> *).
Label t -> e -> proxy (Tagged t e : v) -> Variant (Tagged t e : v)
mkVariant (Label t
forall {k} (l :: k). Label l
Label :: Label t) e
e Proxy (Tagged t e : v)
forall {k} (t :: k). Proxy t
Proxy Variant (Tagged t e : v)
-> [Variant (Tagged t e : v)] -> [Variant (Tagged t e : v)]
forall a. a -> [a] -> [a]
: (Variant v -> Variant (Tagged t e : v))
-> [Variant v] -> [Variant (Tagged t e : v)]
forall a b. (a -> b) -> [a] -> [b]
map Variant v -> Variant (Tagged t e : v)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant [Variant v]
v
    Maybe e
_ -> (Variant v -> Variant (Tagged t e : v))
-> [Variant v] -> [Variant (Tagged t e : v)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Variant v -> Variant (Tagged t e : v)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant [Variant v]
v