{-# LANGUAGE CPP #-}

{- |
   The HList library

   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

   Type-indexed co-products. The public interface is exposed
   in <Data-HList-CommonMain.html#t:TIC CommonMain#TIC>

   (There are other ways: see ConsUnion.hs, for example)
-}

module Data.HList.TIC where

import Data.HList.TIP
import Data.HList.FakePrelude
import Data.HList.HListPrelude

import Data.HList.Record
import Data.HList.Variant
import Data.HList.HList

import Data.HList.HArray

import Data.Array (Ix)
import Data.Semigroup (Semigroup)

import Text.ParserCombinators.ReadP
import LensDefs

-- --------------------------------------------------------------------------
-- | A datatype for type-indexed co-products. A 'TIC' is just a 'Variant',
-- where the elements of the type-level list @\"l\"@ are in the form
-- @Tagged x x@.

newtype TIC (l :: [*]) = TIC (Variant l)

deriving instance Eq (Variant l) => Eq (TIC l)
deriving instance Ord (Variant l) => Ord (TIC l)
deriving instance Ix (Variant l) => Ix (TIC l)
deriving instance Bounded (Variant l) => Bounded (TIC l)
deriving instance Enum (Variant l) => Enum (TIC l)
deriving instance Monoid (Variant l) => Monoid (TIC l)
deriving instance Semigroup (Variant l) => Semigroup (TIC l)


instance HMapAux Variant f xs ys => HMapAux TIC f xs ys where
    hMapAux :: SameLength xs ys => f -> TIC xs -> TIC ys
hMapAux f
f (TIC Variant xs
a) = forall (l :: [*]). Variant l -> TIC l
TIC (forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f Variant xs
a)

-- | @Iso (TIC s) (TIC t) (Variant s) (Variant t)@
--
-- 'typeIndexed' may be more appropriate
ticVariant :: p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant p (Variant l) (f (Variant l))
x = forall (p :: * -> * -> *) (f :: * -> *) b t a s.
(Profunctor p, Functor f, Coercible b t, Coercible a s) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
isoNewtype (\(TIC Variant l
a) -> Variant l
a) forall (l :: [*]). Variant l -> TIC l
TIC p (Variant l) (f (Variant l))
x

-- | @Iso' (TIC s) (Variant s)@
ticVariant' :: p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant' p (Variant l) (f (Variant l))
x = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple forall {p :: * -> * -> *} {f :: * -> *} {l :: [*]} {l :: [*]}.
(Profunctor p, Functor f) =>
p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant p (Variant l) (f (Variant l))
x


-- --------------------------------------------------------------------------

{- | Conversion between type indexed collections ('TIC' and 'TIP')
and the corresponding collection that has other label types ('Variant'
and 'Record' respectively)

See 'typeIndexed''

-}
class TypeIndexed r tr | r -> tr, tr -> r where
    -- | @Iso (r s) (r t) (tr a) (tr b)@
    typeIndexed :: forall p f s t a b.
       (TypeIndexedCxt s t a b, Profunctor p, Functor f) =>
      p (tr (TagR a)) (f (tr (TagR b))) -> p (r s) (f (r t))

type TypeIndexedCxt s t a b =
 (HMapCxt HList TaggedFn b t,
  RecordValues s, RecordValues t,
  a ~ RecordValuesR s,
  b ~ RecordValuesR t,
  SameLabels s t,
  SameLength s t,
  SameLength b a,
  {- to use castVariant instead of unsafeCastVariant
  RecordValuesR (TagR a) ~ a,
  RecordValuesR (TagR b) ~ b,
  SameLength (TagR a) s,
  SameLength (TagR b) t,
  -}
  Coercible (TagR b) t,
  Coercible (TagR a) s,
  HAllTaggedLV s,
  HRLabelSet t,
  TagUntag a,
  TagUntag b)

instance TypeIndexed Record TIP where
    typeIndexed :: forall (p :: * -> * -> *) (f :: * -> *) (s :: [*]) (t :: [*])
       (a :: [*]) (b :: [*]).
(TypeIndexedCxt s t a b, Profunctor p, Functor f) =>
p (TIP (TagR a)) (f (TIP (TagR b))) -> p (Record s) (f (Record t))
typeIndexed = forall k m (x :: [k]) (y :: [m]) {k1} {k2} {k3}
       (p :: k1 -> k2 -> *) (r :: [k] -> k1) (f :: k3 -> k2)
       (q :: [m] -> k3).
SameLength x y =>
p (r x) (f (q y)) -> p (r x) (f (q y))
sameLength forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: [*]) (y :: [*]) (p :: * -> * -> *) (f :: * -> *).
(Unlabeled x y, Profunctor p, Functor f) =>
p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
-> p (Record x) (f (Record y))
unlabeled forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (TIP (TagR a)) (f (TIP (TagR b))) -> p (HList a) (f (HList b))
fromTipHList
      where fromTipHList :: p (TIP (TagR a)) (f (TIP (TagR b))) -> p (HList a) (f (HList b))
fromTipHList = 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 (l :: [*]). HList l -> TIP l
TIP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf) (\(TIP HList (TagR b)
a) -> forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList (TagR b)
a)

instance TypeIndexed Variant TIC where
    typeIndexed :: forall (p :: * -> * -> *) (f :: * -> *) (s :: [*]) (t :: [*])
       (a :: [*]) (b :: [*]).
(TypeIndexedCxt s t a b, Profunctor p, Functor f) =>
p (TIC (TagR a)) (f (TIC (TagR b)))
-> p (Variant s) (f (Variant t))
typeIndexed = forall (p :: * -> * -> *) (f :: * -> *) b t a s.
(Profunctor p, Functor f, Coercible b t, Coercible a s) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
isoNewtype forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) (f :: * -> *) b t a s.
(Profunctor p, Functor f, Coercible b t, Coercible a s) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
isoNewtype forall (l :: [*]). Variant l -> TIC l
TIC (\(TIC Variant (TagR b)
a) -> Variant (TagR b)
a)

{- |

@'Iso'' ('Variant' s) ('TIC' a)@

@'Iso'' ('Record' s) ('TIP' a)@

where @s@ has a type like @'[Tagged \"x\" Int]@, and
@a@ has a type like @'[Tagged Int Int]@.
-}
typeIndexed' :: p (tr (TagR (RecordValuesR t))) (f (tr (TagR (RecordValuesR t))))
-> p (r t) (f (r t))
typeIndexed' p (tr (TagR (RecordValuesR t))) (f (tr (TagR (RecordValuesR t))))
x = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple forall (r :: [*] -> *) (tr :: [*] -> *) (p :: * -> * -> *)
       (f :: * -> *) (s :: [*]) (t :: [*]) (a :: [*]) (b :: [*]).
(TypeIndexed r tr, TypeIndexedCxt s t a b, Profunctor p,
 Functor f) =>
p (tr (TagR a)) (f (tr (TagR b))) -> p (r s) (f (r t))
typeIndexed p (tr (TagR (RecordValuesR t))) (f (tr (TagR (RecordValuesR t))))
x

-- --------------------------------------------------------------------------
-- | Public constructor (or, open union's injection function)

mkTIC' :: forall i l proxy.
         ( HTypeIndexed l
         , MkVariant i i l
         )
      => i
      -> proxy l -- ^ the ordering of types in the @l :: [*]@ matters.
                 -- This argument is intended to fix the ordering
                 -- it can be a Record, Variant, TIP, Proxy
      -> TIC l

mkTIC' :: forall i (l :: [*]) (proxy :: [*] -> *).
(HTypeIndexed l, MkVariant i i l) =>
i -> proxy l -> TIC l
mkTIC' i
i proxy l
p = forall (l :: [*]). Variant l -> TIC l
TIC (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 i) i
i proxy l
p)

-- | make a TIC that contains one element
mkTIC1 :: forall i. MkVariant i i '[Tagged i i] => i -> TIC '[Tagged i i]
mkTIC1 :: forall i. MkVariant i i '[Tagged i i] => i -> TIC '[Tagged i i]
mkTIC1 i
i = forall (l :: [*]). Variant l -> TIC l
TIC (forall {k} {l :: k} {e}. Label l -> e -> Variant '[Tagged l e]
mkVariant1 (forall {k} (l :: k). Label l
Label :: Label i) i
i)

-- | make a TIC for use in contexts where the result type is fixed
mkTIC :: i -> TIC l
mkTIC i
i = forall i (l :: [*]) (proxy :: [*] -> *).
(HTypeIndexed l, MkVariant i i l) =>
i -> proxy l -> TIC l
mkTIC' i
i forall {k} (t :: k). Proxy t
Proxy


-- --------------------------------------------------------------------------
-- | Public destructor (or, open union's projection function)
instance HasField o (Variant l) (Maybe o) =>
      HasField o (TIC l) (Maybe o) where
    hLookupByLabel :: Label o -> TIC l -> Maybe o
hLookupByLabel Label o
l (TIC Variant l
i) = forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label o
l Variant l
i


instance (HasField o (TIC l) mo, mo ~ Maybe o) => HOccurs mo (TIC l) where
    hOccurs :: TIC l -> mo
hOccurs = forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel (forall {k} (l :: k). Label l
Label :: Label o)


-- | similar to 'HPrism'
class TICPrism s t a b | s a b -> t, t a b -> s where
  ticPrism :: (SameLength s t, Choice p, Applicative f)
      => (a `p` f b) -> (TIC s `p` f (TIC t))

instance (
    MkVariant b b t,
    HasField a (Variant s) (Maybe a),
    SameLength s t,

    HFindLabel b t n,
    HFindLabel a s n,

    HUpdateAtHNatR n (Tagged b b) s ~ t,
    HUpdateAtHNatR n (Tagged a a) t ~ s

    ) => TICPrism s t a b where
  ticPrism :: forall (p :: * -> * -> *) (f :: * -> *).
(SameLength s t, Choice p, Applicative f) =>
p a (f b) -> p (TIC s) (f (TIC t))
ticPrism = forall {p :: * -> * -> *} {f :: * -> *} {l :: [*]} {l :: [*]}.
(Profunctor p, Functor f) =>
p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall {k} (l :: k). Label l
Label :: Label b) 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 (forall {k} (l :: k). Label l
Label :: Label a) 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))

-- | @Prism' (TIC s) a@
ticPrism' :: forall s t a b. (HPrism a s t a b, a~b, s~t)
  => (forall f p. (Applicative f, Choice p) => (a `p` f b) -> (TIC s `p` f (TIC t)))
ticPrism' :: forall (s :: [*]) (t :: [*]) a b (f :: * -> *) (p :: * -> * -> *).
(HPrism a s t a b, a ~ b, s ~ t, Applicative f, Choice p) =>
p a (f b) -> p (TIC s) (f (TIC t))
ticPrism' = forall {p :: * -> * -> *} {f :: * -> *} {l :: [*]} {l :: [*]}.
(Profunctor p, Functor f) =>
p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (x :: k) (s :: [*]) (t :: [*]) a b (p :: * -> * -> *)
       (f :: * -> *).
(HPrism x s t a b, Choice p, Applicative f) =>
Label x -> p a (f b) -> p (Variant s) (f (Variant t))
hPrism (forall {k} (l :: k). Label l
Label :: Label a)


-- --------------------------------------------------------------------------
-- | TICs are not opaque

instance ShowVariant l => Show (TIC l)
 where
  showsPrec :: Int -> TIC l -> ShowS
showsPrec Int
_ (TIC Variant l
v) = (String
"TIC{"forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant l
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'}'forall a. a -> [a] -> [a]
:)


instance (ReadVariant l, HAllTaggedEq l, HRLabelSet l) => Read (TIC l)
 where
   readsPrec :: Int -> ReadS (TIC l)
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
"TIC{"
     Variant l
r <- forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
     String
_ <- String -> ReadP String
string String
"}"
     forall (m :: * -> *) a. Monad m => a -> m a
return (forall (l :: [*]). Variant l -> TIC l
TIC Variant l
r)


{- |
> Nothing .*. x = x
> Just a .*. y = mkTIC a
-}
instance (me ~ Maybe e, HOccursNot (Tagged e e) l)
       => HExtend me (TIC l) where
    type HExtendR me (TIC l) = TIC (Tagged (UnMaybe me) (UnMaybe me) ': l)
    Just e
e .*. :: me -> TIC l -> HExtendR me (TIC l)
.*. TIC l
_ = forall (l :: [*]). Variant l -> TIC l
TIC (forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 e
e)
    me
Maybe e
Nothing .*. TIC Variant l
x = forall (l :: [*]). Variant l -> TIC l
TIC (forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant l
x)