{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Debug.RecoverRTTI.Tuple (
WrappedTuple(WrappedTuple, TNil, TCons)
, bimapTuple
, tupleFromNP
, tupleToNP
, 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
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 #-}
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)
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
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))
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
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