{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE PatternSynonyms      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns         #-}

module Debug.RecoverRTTI.Tuple (
    -- * Wrapped tuple
    WrappedTuple(WrappedTuple, TNil, TCons)
  , unwrapTuple
    -- * Conversion between tuples and NP
  , tupleFromNP
  , tupleToNP
    -- * Mapping
  , PairWise(..)
  , mapTuple
    -- * Re-exports
  , module Debug.RecoverRTTI.Tuple.Recursive
  , module Debug.RecoverRTTI.Tuple.Size
  ) where

import Data.SOP hiding (NS(..))

import Debug.RecoverRTTI.Nat
import Debug.RecoverRTTI.Tuple.Recursive
import Debug.RecoverRTTI.Tuple.Size

{-------------------------------------------------------------------------------
  Wrapped tuple

  NOTE: We cannot add any dictionaries in @WrappedTuple@ itself, it /MUST/ be
  a type synonym: it is critical that we can 'unsafeCoerce' a regular tuple to a
  wrapped tuple.
-------------------------------------------------------------------------------}

-- | Inductive tuple
--
-- Inductive view on tuples that can be constructed with or pattern matched on
-- using 'TNil' and 'TCons'. The underlying representation is a /true/ tuple
-- however; for example, @Tuple '[Int, Bool, Char] ~ (Int, Bool, Char)@.
newtype WrappedTuple xs = WrappedTuple { forall (xs :: [*]). WrappedTuple xs -> Tuple xs
unwrapTuple :: Tuple xs }

pattern TNil ::
     forall xs. (SListI xs, IsValidSize (Length xs))
  => xs ~ '[]
  => WrappedTuple xs
pattern $bTNil :: forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs), xs ~ '[]) =>
WrappedTuple xs
$mTNil :: forall {r} {xs :: [*]}.
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> ((xs ~ '[]) => r) -> ((# #) -> r) -> r
TNil <- (viewWrapped -> TupleEmpty)
  where
    TNil = forall (xs :: [*]). Tuple xs -> WrappedTuple xs
WrappedTuple ()

pattern TCons ::
     forall   xs'. (SListI xs', IsValidSize (Length xs'))
  => forall x xs . (xs' ~ (x ': xs), SListI xs, IsValidSize (Length xs))
  => x -> WrappedTuple xs -> WrappedTuple xs'
pattern $bTCons :: forall (xs' :: [*]) x (xs :: [*]).
(SListI xs', IsValidSize (Length xs'), xs' ~ (x : xs), SListI xs,
 IsValidSize (Length xs)) =>
x -> WrappedTuple xs -> WrappedTuple xs'
$mTCons :: forall {r} {xs' :: [*]}.
(SListI xs', IsValidSize (Length xs')) =>
WrappedTuple xs'
-> (forall {x} {xs :: [*]}.
    (xs' ~ (x : xs), SListI xs, IsValidSize (Length xs)) =>
    x -> WrappedTuple xs -> r)
-> ((# #) -> r)
-> r
TCons x xs <- (viewWrapped -> TupleNonEmpty x xs)
  where
    TCons x
x WrappedTuple xs
xs = forall x (xs :: [*]).
(SListI xs, IsValidSize (Length (x : xs))) =>
(x, WrappedTuple xs) -> WrappedTuple (x : xs)
consWrapped (x
x, WrappedTuple xs
xs)

{-# COMPLETE TNil, TCons #-}

{-------------------------------------------------------------------------------
  Conversion to/from NP
-------------------------------------------------------------------------------}

tupleFromNP :: forall xs.
     (SListI xs, IsValidSize (Length xs))
  => NP I xs -> WrappedTuple xs
tupleFromNP :: forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
NP I xs -> WrappedTuple xs
tupleFromNP NP I xs
Nil         = forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs), xs ~ '[]) =>
WrappedTuple xs
TNil
tupleFromNP (I x
x :* NP I xs
xs) = forall (n :: Nat) r.
IsValidSize ('S n) =>
Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid (forall {k} (t :: k). Proxy t
Proxy @(Length xs))
                        forall a b. (a -> b) -> a -> b
$ forall (xs' :: [*]) x (xs :: [*]).
(SListI xs', IsValidSize (Length xs'), xs' ~ (x : xs), SListI xs,
 IsValidSize (Length xs)) =>
x -> WrappedTuple xs -> WrappedTuple xs'
TCons x
x (forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
NP I xs -> WrappedTuple xs
tupleFromNP NP I xs
xs)

tupleToNP ::
     (SListI xs, IsValidSize (Length xs))
  => WrappedTuple xs -> NP I xs
tupleToNP :: forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP WrappedTuple xs
TNil         = forall {k} (a :: k -> *). NP a '[]
Nil
tupleToNP (TCons x
x WrappedTuple xs
xs) = forall a. a -> I a
I x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP WrappedTuple xs
xs

{-------------------------------------------------------------------------------
  Mapping
-------------------------------------------------------------------------------}

data PairWise f xs ys where
  PNil  :: PairWise f '[] '[]
  PCons :: f x y -> PairWise f xs ys -> PairWise f (x:xs) (y:ys)

data SameListShape xs ys where
  SameListShape :: (SListI ys, Length xs ~ Length ys) => SameListShape xs ys

mapTuple' ::
     (SListI xs, IsValidSize (Length xs))
  => PairWise (->) xs ys
  -> WrappedTuple xs -> (SameListShape xs ys, WrappedTuple ys)
mapTuple' :: forall (xs :: [*]) (ys :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
PairWise (->) xs ys
-> WrappedTuple xs -> (SameListShape xs ys, WrappedTuple ys)
mapTuple' PairWise (->) xs ys
PNil          WrappedTuple xs
TNil        = (forall (ys :: [*]) (xs :: [*]).
(SListI ys, Length xs ~ Length ys) =>
SameListShape xs ys
SameListShape, forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs), xs ~ '[]) =>
WrappedTuple xs
TNil)
mapTuple' (PCons x -> y
f PairWise (->) xs ys
fs) (TCons x
x WrappedTuple xs
xs) =
    case forall (xs :: [*]) (ys :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
PairWise (->) xs ys
-> WrappedTuple xs -> (SameListShape xs ys, WrappedTuple ys)
mapTuple' PairWise (->) xs ys
fs WrappedTuple xs
xs of
      (SameListShape xs ys
SameListShape, WrappedTuple ys
ys) -> (forall (ys :: [*]) (xs :: [*]).
(SListI ys, Length xs ~ Length ys) =>
SameListShape xs ys
SameListShape, forall (xs' :: [*]) x (xs :: [*]).
(SListI xs', IsValidSize (Length xs'), xs' ~ (x : xs), SListI xs,
 IsValidSize (Length xs)) =>
x -> WrappedTuple xs -> WrappedTuple xs'
TCons (x -> y
f x
x) WrappedTuple ys
ys)

mapTuple ::
     (SListI xs, IsValidSize (Length xs))
  => PairWise (->) xs ys -> WrappedTuple xs -> WrappedTuple ys
mapTuple :: forall (xs :: [*]) (ys :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
PairWise (->) xs ys -> WrappedTuple xs -> WrappedTuple ys
mapTuple PairWise (->) xs ys
fs = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [*]) (ys :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
PairWise (->) xs ys
-> WrappedTuple xs -> (SameListShape xs ys, WrappedTuple ys)
mapTuple' PairWise (->) xs ys
fs

{-------------------------------------------------------------------------------
  Internal auxiliary functions for defining the pattern synonym
-------------------------------------------------------------------------------}

data TupleView xs where
  TupleEmpty    :: TupleView '[]
  TupleNonEmpty :: (SListI xs, IsValidSize (Length xs))
                => x -> WrappedTuple xs -> TupleView (x ': xs)

viewWrapped ::
     (SListI xs, IsValidSize (Length xs))
  => WrappedTuple xs
  -> TupleView xs
viewWrapped :: forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> TupleView xs
viewWrapped (WrappedTuple Tuple xs
t) =
    forall (xs :: [*]).
IsValidSize (Length xs) =>
SList xs -> Tuple xs -> TupleView xs
go forall {k} (xs :: [k]). SListI xs => SList xs
sList Tuple xs
t
  where
    go :: forall xs.
         IsValidSize (Length xs)
      => SList xs -> Tuple xs -> TupleView xs
    go :: forall (xs :: [*]).
IsValidSize (Length xs) =>
SList xs -> Tuple xs -> TupleView xs
go SList xs
SNil  () = TupleView '[]
TupleEmpty
    go SList xs
SCons Tuple xs
xs = forall x (xs :: [*]).
(SListI xs, IsValidSize (Length (x : xs))) =>
Tuple (x : xs) -> TupleView (x : xs)
goCons Tuple xs
xs

    goCons :: forall x xs.
         (SListI xs, IsValidSize (Length (x ': xs)))
      => Tuple (x ': xs) -> TupleView (x ': xs)
    goCons :: forall x (xs :: [*]).
(SListI xs, IsValidSize (Length (x : xs))) =>
Tuple (x : xs) -> TupleView (x : xs)
goCons Tuple (x : xs)
xs =
        forall (n :: Nat) r.
IsValidSize ('S n) =>
Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid (forall {k} (t :: k). Proxy t
Proxy @(Length (x ': xs))) forall a b. (a -> b) -> a -> b
$
          forall (xs :: [*]) x.
(SListI xs, IsValidSize (Length xs)) =>
x -> WrappedTuple xs -> TupleView (x : xs)
TupleNonEmpty x
x (forall (xs :: [*]). Tuple xs -> WrappedTuple xs
WrappedTuple Tuple xs
xs')
      where
        (x
x, Tuple xs
xs') = forall x (xs :: [*]).
SListI xs =>
Proxy xs
-> ValidSize (Length (x : xs)) -> Tuple (x : xs) -> (x, Tuple xs)
uncons (forall {k} (t :: k). Proxy t
Proxy @xs) forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize Tuple (x : xs)
xs

consWrapped :: forall x xs.
     (SListI xs, IsValidSize (Length (x ': xs)))
  => (x, WrappedTuple xs) -> WrappedTuple (x ': xs)
consWrapped :: forall x (xs :: [*]).
(SListI xs, IsValidSize (Length (x : xs))) =>
(x, WrappedTuple xs) -> WrappedTuple (x : xs)
consWrapped (x
x, WrappedTuple Tuple xs
xs) =
    forall (xs :: [*]). Tuple xs -> WrappedTuple xs
WrappedTuple (forall x (xs :: [*]).
SListI xs =>
Proxy xs
-> ValidSize (Length (x : xs)) -> (x, Tuple xs) -> Tuple (x : xs)
cons (forall {k} (t :: k). Proxy t
Proxy @xs) forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize (x
x, Tuple xs
xs))

{-------------------------------------------------------------------------------
  Instances
-------------------------------------------------------------------------------}

instance ( SListI xs
         , IsValidSize (Length xs)
         , All Show xs
         ) => Show (WrappedTuple xs) where
  showsPrec :: Int -> WrappedTuple xs -> ShowS
showsPrec Int
_ =
        [ShowS] -> ShowS
show_tuple
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (forall {k} (t :: k). Proxy t
Proxy @Show) (forall {k} a b (c :: k). (a -> b) -> I a -> K b c
mapIK forall a. Show a => a -> ShowS
shows)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP
    where
      -- Copied from @GHC.Show@ (not exported)
      show_tuple :: [ShowS] -> ShowS
      show_tuple :: [ShowS] -> ShowS
show_tuple [ShowS]
ss = Char -> ShowS
showChar Char
'('
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ShowS
s ShowS
r -> ShowS
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
',' forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
r) [ShowS]
ss
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
')'

instance ( SListI xs
         , IsValidSize (Length xs)
         , All Eq xs
         ) => Eq (WrappedTuple xs) where
  (forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP -> NP I xs
xs) == :: WrappedTuple xs -> WrappedTuple xs -> Bool
== (forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP -> NP I xs
ys) =
       forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse forall a b. (a -> b) -> a -> b
$ forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hczipWith (forall {k} (t :: k). Proxy t
Proxy @Eq) (forall {k} a b c (d :: k). (a -> b -> c) -> I a -> I b -> K c d
mapIIK forall a. Eq a => a -> a -> Bool
(==)) NP I xs
xs NP I xs
ys