{-# 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 :: f -> TIC xs -> TIC ys
hMapAux f
f (TIC Variant xs
a) = Variant ys -> TIC ys
forall (l :: [*]). Variant l -> TIC l
TIC (f -> Variant xs -> Variant ys
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 = (TIC l -> Variant l)
-> (Variant l -> TIC l)
-> p (Variant l) (f (Variant l))
-> p (TIC l) (f (TIC l))
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) Variant l -> TIC l
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 = (p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l)))
-> p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
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 p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
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 :: p (TIP (TagR a)) (f (TIP (TagR b))) -> p (Record s) (f (Record t))
typeIndexed = p (Record s) (f (Record t)) -> p (Record s) (f (Record t))
forall k m (x :: [k]) (y :: [m]) k k k (p :: k -> k -> *)
       (r :: [k] -> k) (f :: k -> k) (q :: [m] -> k).
SameLength x y =>
p (r x) (f (q y)) -> p (r x) (f (q y))
sameLength (p (Record s) (f (Record t)) -> p (Record s) (f (Record t)))
-> (p (TIP (TagR a)) (f (TIP (TagR b)))
    -> p (Record s) (f (Record t)))
-> p (TIP (TagR a)) (f (TIP (TagR b)))
-> p (Record s) (f (Record t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList a) (f (HList b)) -> p (Record s) (f (Record t))
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 (p (HList a) (f (HList b)) -> p (Record s) (f (Record t)))
-> (p (TIP (TagR a)) (f (TIP (TagR b)))
    -> p (HList a) (f (HList b)))
-> p (TIP (TagR a)) (f (TIP (TagR b)))
-> p (Record s) (f (Record t))
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 = (HList a -> TIP (TagR a))
-> (TIP (TagR b) -> HList b)
-> p (TIP (TagR a)) (f (TIP (TagR b)))
-> p (HList a) (f (HList b))
forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso (HList (TagR a) -> TIP (TagR a)
forall (l :: [*]). HList l -> TIP l
TIP (HList (TagR a) -> TIP (TagR a))
-> (HList a -> HList (TagR a)) -> HList a -> TIP (TagR a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HList a -> HList (TagR a)
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf) (\(TIP HList (TagR b)
a) -> HList (TagR b) -> HList b
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList (TagR b)
a)

instance TypeIndexed Variant TIC where
    typeIndexed :: p (TIC (TagR a)) (f (TIC (TagR b)))
-> p (Variant s) (f (Variant t))
typeIndexed = (Variant s -> Variant (TagR a))
-> (Variant (TagR b) -> Variant t)
-> p (Variant (TagR a)) (f (Variant (TagR b)))
-> p (Variant s) (f (Variant t))
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 Variant s -> Variant (TagR a)
forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant Variant (TagR b) -> Variant t
forall (v :: [*]) (v' :: [*]). Variant v -> Variant v'
unsafeCastVariant
                (p (Variant (TagR a)) (f (Variant (TagR b)))
 -> p (Variant s) (f (Variant t)))
-> (p (TIC (TagR a)) (f (TIC (TagR b)))
    -> p (Variant (TagR a)) (f (Variant (TagR b))))
-> p (TIC (TagR a)) (f (TIC (TagR b)))
-> p (Variant s) (f (Variant t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Variant (TagR a) -> TIC (TagR a))
-> (TIC (TagR b) -> Variant (TagR b))
-> p (TIC (TagR a)) (f (TIC (TagR b)))
-> p (Variant (TagR a)) (f (Variant (TagR b)))
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 Variant (TagR a) -> TIC (TagR a)
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 = (p (tr (TagR (RecordValuesR t))) (f (tr (TagR (RecordValuesR t))))
 -> p (r t) (f (r t)))
-> p (tr (TagR (RecordValuesR t)))
     (f (tr (TagR (RecordValuesR t))))
-> p (r t) (f (r t))
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 p (tr (TagR (RecordValuesR t))) (f (tr (TagR (RecordValuesR t))))
-> p (r t) (f (r t))
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' :: i -> proxy l -> TIC l
mkTIC' i
i proxy l
p = Variant l -> TIC l
forall (l :: [*]). Variant l -> TIC l
TIC (Label i -> i -> proxy l -> Variant l
forall k (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (Label i
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 :: i -> TIC '[Tagged i i]
mkTIC1 i
i = Variant '[Tagged i i] -> TIC '[Tagged i i]
forall (l :: [*]). Variant l -> TIC l
TIC (Label i -> i -> Variant '[Tagged i i]
forall k (l :: k) e. Label l -> e -> Variant '[Tagged l e]
mkVariant1 (Label i
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 = i -> Proxy l -> TIC l
forall i (l :: [*]) (proxy :: [*] -> *).
(HTypeIndexed l, MkVariant i i l) =>
i -> proxy l -> TIC l
mkTIC' i
i Proxy l
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) = Label o -> Variant l -> Maybe o
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 = Label o -> TIC l -> mo
forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel (Label o
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 :: p a (f b) -> p (TIC s) (f (TIC t))
ticPrism = p (Variant s) (f (Variant t)) -> p (TIC s) (f (TIC t))
forall (p :: * -> * -> *) (f :: * -> *) (l :: [*]) (l :: [*]).
(Profunctor p, Functor f) =>
p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant (p (Variant s) (f (Variant t)) -> p (TIC s) (f (TIC t)))
-> (p a (f b) -> p (Variant s) (f (Variant t)))
-> p a (f b)
-> p (TIC s) (f (TIC t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 b -> b -> Proxy t -> Variant t
forall k (x :: k) v (vs :: [*]) (proxy :: [*] -> *).
MkVariant x v vs =>
Label x -> v -> proxy vs -> Variant vs
mkVariant (Label b
forall k (l :: k). Label l
Label :: Label b) b
b Proxy t
forall k (t :: k). Proxy t
Proxy)
      (\Variant s
s -> case Label a -> Variant s -> Maybe a
forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel (Label a
forall k (l :: k). Label l
Label :: Label a) 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))

-- | @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 (f :: * -> *) (p :: * -> * -> *).
(Applicative f, Choice p) =>
p a (f b) -> p (TIC s) (f (TIC t))
ticPrism' = p (Variant s) (f (Variant t)) -> p (TIC s) (f (TIC t))
forall (p :: * -> * -> *) (f :: * -> *) (l :: [*]) (l :: [*]).
(Profunctor p, Functor f) =>
p (Variant l) (f (Variant l)) -> p (TIC l) (f (TIC l))
ticVariant (p (Variant s) (f (Variant t)) -> p (TIC s) (f (TIC t)))
-> (p a (f b) -> p (Variant s) (f (Variant t)))
-> p a (f b)
-> p (TIC s) (f (TIC t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label a -> p a (f b) -> p (Variant s) (f (Variant t))
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 (Label a
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{"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variant l -> ShowS
forall (vs :: [*]). ShowVariant vs => Variant vs -> ShowS
showVariant Variant l
v ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'}'Char -> ShowS
forall a. a -> [a] -> [a]
:)


instance (ReadVariant l, HAllTaggedEq l, HRLabelSet l) => Read (TIC l)
 where
   readsPrec :: Int -> ReadS (TIC l)
readsPrec Int
_ = ReadP (TIC l) -> ReadS (TIC l)
forall a. ReadP a -> ReadS a
readP_to_S (ReadP (TIC l) -> ReadS (TIC l)) -> ReadP (TIC l) -> ReadS (TIC l)
forall a b. (a -> b) -> a -> b
$ do
     String
_ <- String -> ReadP String
string String
"TIC{"
     Variant l
r <- ReadP (Variant l)
forall (vs :: [*]). ReadVariant vs => ReadP (Variant vs)
readVariant
     String
_ <- String -> ReadP String
string String
"}"
     TIC l -> ReadP (TIC l)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variant l -> TIC l
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 .*. :: me -> TIC l -> HExtendR me (TIC l)
.*. TIC l
_ = Variant (Tagged e e : l) -> TIC (Tagged e e : l)
forall (l :: [*]). Variant l -> TIC l
TIC (Int -> e -> Variant (Tagged e e : l)
forall v (vs :: [*]). Int -> v -> Variant vs
unsafeMkVariant Int
0 e
e)
    me
Nothing .*. TIC Variant l
x = Variant (Tagged e e : l) -> TIC (Tagged e e : l)
forall (l :: [*]). Variant l -> TIC l
TIC (Variant l -> Variant (Tagged e e : l)
forall (l :: [*]) e. Variant l -> Variant (e : l)
extendVariant Variant l
x)