{-# 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)
    -- * Auxiliary
  , bimapTuple
    -- * Conversion between tuples and NP
  , tupleFromNP
  , tupleToNP
    -- * Re-exports
  , module Debug.RecoverRTTI.Tuple.Recursive
  , module Debug.RecoverRTTI.Tuple.Size
  ) where

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

import Debug.RecoverRTTI.Tuple.Recursive
import Debug.RecoverRTTI.Tuple.Size
import Debug.RecoverRTTI.Util.TypeLevel

{-------------------------------------------------------------------------------
  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.
-------------------------------------------------------------------------------}

newtype WrappedTuple xs = WrappedTuple (Tuple xs)

pattern TNil ::
     forall xs. (SListI xs, IsValidSize (Length xs))
  => xs ~ '[]
  => WrappedTuple xs
pattern $bTNil :: WrappedTuple xs
$mTNil :: forall r (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> ((xs ~ '[]) => r) -> (Void# -> r) -> r
TNil <- (viewWrapped -> TupleEmpty)
  where
    TNil = Tuple xs -> WrappedTuple xs
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 :: 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)
-> (Void# -> r)
-> r
TCons x xs <- (viewWrapped -> TupleNonEmpty x xs)
  where
    TCons x
x WrappedTuple xs
xs = (x, WrappedTuple xs) -> WrappedTuple (x : 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 #-}

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

bimapTuple ::
      ( SListI xs
      , SListI ys
      , IsValidSize (Length (x ': xs))
      , Length xs ~ Length ys
      )
   => (x -> y)
   -> (WrappedTuple xs -> WrappedTuple ys)
   -> WrappedTuple (x ': xs) -> WrappedTuple (y ': ys)
bimapTuple :: (x -> y)
-> (WrappedTuple xs -> WrappedTuple ys)
-> WrappedTuple (x : xs)
-> WrappedTuple (y : ys)
bimapTuple x -> y
f WrappedTuple xs -> WrappedTuple ys
g (TCons x
x WrappedTuple xs
xs) = y -> WrappedTuple ys -> WrappedTuple (y : ys)
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
x) (WrappedTuple xs -> WrappedTuple ys
g WrappedTuple xs
WrappedTuple xs
xs)

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

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

{-------------------------------------------------------------------------------
  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 :: WrappedTuple xs -> TupleView xs
viewWrapped (WrappedTuple Tuple xs
t) =
    SList xs -> Tuple xs -> TupleView xs
forall (xs :: [*]).
IsValidSize (Length xs) =>
SList xs -> Tuple xs -> TupleView xs
go SList xs
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 :: SList xs -> Tuple xs -> TupleView xs
go SList xs
SNil  () = TupleView xs
TupleView '[]
TupleEmpty
    go SList xs
SCons Tuple xs
xs = Tuple (x : xs) -> TupleView (x : xs)
forall x (xs :: [*]).
(SListI xs, IsValidSize (Length (x : xs))) =>
Tuple (x : xs) -> TupleView (x : xs)
goCons Tuple xs
Tuple (x : xs)
xs

    goCons :: forall x xs.
         (SListI xs, IsValidSize (Length (x ': xs)))
      => Tuple (x ': xs) -> TupleView (x ': xs)
    goCons :: Tuple (x : xs) -> TupleView (x : xs)
goCons Tuple (x : xs)
xs =
        Proxy ('S (Length xs))
-> (IsValidSize (Length xs) => TupleView (x : xs))
-> TupleView (x : xs)
forall (n :: Nat) r.
IsValidSize ('S n) =>
Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid (Proxy (Length (x : xs))
forall k (t :: k). Proxy t
Proxy @(Length (x ': xs))) ((IsValidSize (Length xs) => TupleView (x : xs))
 -> TupleView (x : xs))
-> (IsValidSize (Length xs) => TupleView (x : xs))
-> TupleView (x : xs)
forall a b. (a -> b) -> a -> b
$
          x -> WrappedTuple xs -> TupleView (x : xs)
forall (xs :: [*]) x.
(SListI xs, IsValidSize (Length xs)) =>
x -> WrappedTuple xs -> TupleView (x : xs)
TupleNonEmpty x
x (Tuple xs -> WrappedTuple xs
forall (xs :: [*]). Tuple xs -> WrappedTuple xs
WrappedTuple Tuple xs
xs')
      where
        (x
x, Tuple xs
xs') = Proxy xs
-> ValidSize (Length (x : xs)) -> Tuple (x : xs) -> (x, Tuple xs)
forall x (xs :: [*]).
SListI xs =>
Proxy xs
-> ValidSize (Length (x : xs)) -> Tuple (x : xs) -> (x, Tuple xs)
uncons (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) ValidSize (Length (x : 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 :: (x, WrappedTuple xs) -> WrappedTuple (x : xs)
consWrapped (x
x, WrappedTuple Tuple xs
xs) =
    Tuple (x : xs) -> WrappedTuple (x : xs)
forall (xs :: [*]). Tuple xs -> WrappedTuple xs
WrappedTuple (Proxy xs
-> ValidSize (Length (x : xs)) -> (x, Tuple xs) -> Tuple (x : xs)
forall x (xs :: [*]).
SListI xs =>
Proxy xs
-> ValidSize (Length (x : xs)) -> (x, Tuple xs) -> Tuple (x : xs)
cons (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) ValidSize (Length (x : 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
      ([ShowS] -> ShowS)
-> (WrappedTuple xs -> [ShowS]) -> WrappedTuple xs -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K ShowS) xs -> [ShowS]
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
      (NP (K ShowS) xs -> [ShowS])
-> (WrappedTuple xs -> NP (K ShowS) xs)
-> WrappedTuple xs
-> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy Show
-> (forall a. Show a => I a -> K ShowS a)
-> NP I xs
-> NP (K ShowS) xs
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 (Proxy Show
forall k (t :: k). Proxy t
Proxy @Show) ((a -> ShowS) -> I a -> K ShowS a
forall k a b (c :: k). (a -> b) -> I a -> K b c
mapIK a -> ShowS
forall a. Show a => a -> ShowS
shows)
      (NP I xs -> NP (K ShowS) xs)
-> (WrappedTuple xs -> NP I xs)
-> WrappedTuple xs
-> NP (K ShowS) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrappedTuple xs -> NP I xs
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
'('
                    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> ShowS -> ShowS) -> [ShowS] -> ShowS
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ShowS
s ShowS
r -> ShowS
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
',' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
r) [ShowS]
ss
                    ShowS -> ShowS -> ShowS
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
  (WrappedTuple xs -> NP I xs
forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP -> NP I xs
xs) == :: WrappedTuple xs -> WrappedTuple xs -> Bool
== (WrappedTuple xs -> NP I xs
forall (xs :: [*]).
(SListI xs, IsValidSize (Length xs)) =>
WrappedTuple xs -> NP I xs
tupleToNP -> NP I xs
ys) =
       [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (NP (K Bool) xs -> [Bool]) -> NP (K Bool) xs -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K Bool) xs -> [Bool]
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NP (K Bool) xs -> Bool) -> NP (K Bool) xs -> Bool
forall a b. (a -> b) -> a -> b
$ Proxy Eq
-> (forall a. Eq a => I a -> I a -> K Bool a)
-> Prod NP I xs
-> NP I xs
-> NP (K Bool) xs
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 (Proxy Eq
forall k (t :: k). Proxy t
Proxy @Eq) ((a -> a -> Bool) -> I a -> I a -> K Bool a
forall k a b c (d :: k). (a -> b -> c) -> I a -> I b -> K c d
mapIIK a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)) NP I xs
Prod NP I xs
xs NP I xs
ys