{-# 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) -- * 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.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 (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 #-} {------------------------------------------------------------------------------- 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