{-# 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)
, unwrapTuple
, tupleFromNP
, tupleToNP
, PairWise(..)
, mapTuple
, 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
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 #-}
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
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
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))
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
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