module Data.Diverse.Many.Internal (
Many(..)
, IsMany(..)
, fromMany'
, toMany'
, nil
, single
, prefix
, (./)
, postfix
, (\.)
, append
, (/./)
, front
, back
, aft
, fore
, fetch
, fetchL
, fetchN
, replace
, replace'
, replaceL
, replaceL'
, replaceN
, replaceN'
, Select
, select
, selectL
, SelectN
, selectN
, Amend
, amend
, Amend'
, amend'
, amendL
, amendL'
, AmendN
, amendN
, AmendN'
, amendN'
, forMany
, collect
, forManyN
, collectN
) where
import Control.Applicative
import Data.Bool
import Data.Diverse.AFoldable
import Data.Diverse.Case
import Data.Diverse.Reiterate
import Data.Diverse.TypeLevel
import Data.Kind
import qualified Data.Map.Strict as M
import Data.Proxy
import Data.Tagged
import qualified GHC.Generics as G
import GHC.Prim (Any, coerce)
import GHC.TypeLits
import Text.ParserCombinators.ReadPrec
import Text.Read
import qualified Text.Read.Lex as L
import Unsafe.Coerce
import Prelude as Partial
data Many (xs :: [Type]) = Many !Int (M.Map Int Any)
type role Many representational
data Many_ (xs :: [Type]) = Many_ [Any]
type role Many_ representational
toMany_ :: Many xs -> Many_ xs
toMany_ (Many _ m) = Many_ (snd <$> M.toAscList m)
fromMany_ :: Many_ xs -> Many xs
fromMany_ (Many_ xs) = Many 0 (M.fromList (zip [(0 :: Int)..] xs))
instance G.Generic (Many '[]) where
type Rep (Many '[]) = G.U1
from _ = G.U1
to G.U1 = nil
instance G.Generic (Many (x ': xs)) where
type Rep (Many (x ': xs)) = (G.Rec0 x) G.:*: (G.Rec0 (Many xs))
from r = ( G.K1 (front r)) G.:*: ( G.K1 (aft r))
to (( G.K1 a) G.:*: ( G.K1 b)) = a ./ b
class IsMany t xs a where
toMany :: t xs a -> Many xs
fromMany :: Many xs -> t xs a
toMany' :: IsMany Tagged xs a => a -> Many xs
toMany' a = toMany (Tagged a)
fromMany' :: IsMany Tagged xs a => Many xs -> a
fromMany' = unTagged . fromMany
instance IsMany Tagged '[] () where
toMany _ = nil
fromMany _ = Tagged ()
instance IsMany Tagged '[a] a where
toMany (Tagged a) = single a
fromMany r = Tagged (fetch @a r)
instance IsMany Tagged '[a,b] (a,b) where
toMany (Tagged (a,b)) = a./b./nil
fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r)
instance IsMany Tagged '[a,b,c] (a,b,c) where
toMany (Tagged (a,b,c)) = a./b./c./nil
fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r)
instance IsMany Tagged '[a,b,c,d] (a,b,c,d) where
toMany (Tagged (a,b,c,d)) = a./b./c./d./nil
fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r)
instance IsMany Tagged '[a,b,c,d,e] (a,b,c,d,e) where
toMany (Tagged (a,b,c,d,e)) = a./b./c./d./e./nil
fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r)
instance IsMany Tagged '[a,b,c,d,e,f] (a,b,c,d,e,f) where
toMany (Tagged (a,b,c,d,e,f)) = a./b./c./d./e./f./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r)
instance IsMany Tagged '[a,b,c,d,e,f,g] (a,b,c,d,e,f,g) where
toMany (Tagged (a,b,c,d,e,f,g)) = a./b./c./d./e./f./g./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h] (a,b,c,d,e,f,g,h) where
toMany (Tagged (a,b,c,d,e,f,g,h)) = a./b./c./d./e./f./g./h./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i] (a,b,c,d,e,f,g,h,i) where
toMany (Tagged (a,b,c,d,e,f,g,h,i)) = a./b./c./d./e./f./g./h./i./ nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j] (a,b,c,d,e,f,g,h,i,j) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j)) = a./b./c./d./e./f./g./h./i./j./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k] (a,b,c,d,e,f,g,h,i,j,k) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k)) = a./b./c./d./e./f./g./h./i./j./k./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r
, fetchN (Proxy @10) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l] (a,b,c,d,e,f,g,h,i,j,k,l) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l)) = a./b./c./d./e./f./g./h./i./j./k./l./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r
, fetchN (Proxy @10) r, fetchN (Proxy @11) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m] (a,b,c,d,e,f,g,h,i,j,k,l,m) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m)) = a./b./c./d./e./f./g./h./i./j./k./l./m./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r
, fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m,n] (a,b,c,d,e,f,g,h,i,j,k,l,m,n) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m,n)) = a./b./c./d./e./f./g./h./i./j./k./l./m./n./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r
, fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r, fetchN (Proxy @13) r)
instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o] (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) where
toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)) = a./b./c./d./e./f./g./h./i./j./k./l./m./n./o./nil
fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r
, fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r
, fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r, fetchN (Proxy @13) r, fetchN (Proxy @14) r)
rightKeyForSnoc :: Int -> Int -> Int -> Int -> Int
rightKeyForSnoc lo ld ro rk = rk ro + lo + ld
rightOffsetForCons :: Int -> Int -> Int
rightOffsetForCons ld ro = ro ld
leftKeyForCons :: Int -> Int -> Int -> Int
leftKeyForCons lo ro lk = lk lo + ro
nil :: Many '[]
nil = Many 0 M.empty
single :: x -> Many '[x]
single v = Many 0 (M.singleton 0 (unsafeCoerce v))
prefix :: x -> Many xs -> Many (x ': xs)
prefix x (Many ro rm) = Many nro
(M.insert
(leftKeyForCons 0 nro 0)
(unsafeCoerce x)
rm)
where
nro = rightOffsetForCons 1 ro
infixr 5 `prefix`
prefix' :: x -> Many_ xs -> Many_ (x ': xs)
prefix' x (Many_ xs) = Many_ (unsafeCoerce x : xs)
(./) :: x -> Many xs -> Many (x ': xs)
(./) = prefix
infixr 5 ./
postfix :: Many xs -> y -> Many (Append xs '[y])
postfix (Many lo lm) y = Many lo
(M.insert (rightKeyForSnoc lo (M.size lm) 0 0)
(unsafeCoerce y)
lm)
infixl 5 `postfix`
(\.) :: Many xs -> y -> Many (Append xs '[y])
(\.) = postfix
infixl 5 \.
(/./) :: Many xs -> Many ys -> Many (Append xs ys)
(/./) = append
infixr 5 /./
append :: Many xs -> Many ys -> Many (Append xs ys)
append (Many lo lm) (Many ro rm) = if ld >= rd
then Many
lo
(lm `M.union` (M.mapKeys (rightKeyForSnoc lo ld ro) rm))
else Many
nro
((M.mapKeys (leftKeyForCons lo nro) lm) `M.union` rm)
where
ld = M.size lm
rd = M.size rm
nro = rightOffsetForCons ld ro
infixr 5 `append`
front :: Many (x ': xs) -> x
front (Many _ m) = unsafeCoerce (snd . Partial.head $ M.toAscList m)
front' :: Many_ (x ': xs) -> x
front' (Many_ xs) = unsafeCoerce (Partial.head xs)
back :: Many (x ': xs) -> Last (x ': xs)
back (Many _ m) = unsafeCoerce (snd . Partial.head $ M.toDescList m)
aft :: Many (x ': xs) -> Many xs
aft (Many o m) = Many (o + 1) (M.delete o m)
aft' :: Many_ (x ': xs) -> Many_ xs
aft' (Many_ xs) = Many_ (Partial.tail xs)
fore :: Many (x ': xs) -> Many (Init (x ': xs))
fore (Many o m) = Many o (M.delete (o + M.size m 1) m)
fetch :: forall x xs. UniqueMember x xs => Many xs -> x
fetch = fetch_
fetch_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => Many xs -> x
fetch_ (Many o m) = unsafeCoerce (m M.! (o + i))
where i = fromInteger (natVal @n Proxy)
fetchL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x
fetchL _ = fetch_ @x
fetchN :: forall n x xs proxy. MemberAt n x xs => proxy n -> Many xs -> x
fetchN p (Many o m) = unsafeCoerce (m M.! (o + i))
where i = fromInteger (natVal p)
replace :: forall x xs. UniqueMember x xs => Many xs -> x -> Many xs
replace = replace_
replace_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => Many xs -> x -> Many xs
replace_ (Many o m) v = Many o (M.insert (o + i) (unsafeCoerce v) m)
where i = fromInteger (natVal @n Proxy)
replace' :: forall x y xs proxy. UniqueMember x xs => proxy x -> Many xs -> y -> Many (Replace x y xs)
replace' = replace'_
replace'_ :: forall x y xs n proxy. (KnownNat n, n ~ IndexOf x xs) => proxy x -> Many xs -> y -> Many (Replace x y xs)
replace'_ _ (Many o m) v = Many o (M.insert (o + i) (unsafeCoerce v) m)
where i = fromInteger (natVal @n Proxy)
replaceL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs
replaceL _ = replace_ @x
replaceL' :: forall l y xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs)
replaceL' _ = replace'_ @x Proxy
replaceN :: forall n x y xs proxy. MemberAt n x xs => proxy n -> Many xs -> y -> Many xs
replaceN p (Many o m) v = Many o (M.insert (o + i) (unsafeCoerce v) m)
where i = fromInteger (natVal p)
replaceN' :: forall n x y xs proxy. MemberAt n x xs => proxy n -> Many xs -> y -> Many (ReplaceIndex n y xs)
replaceN' p (Many o m) v = Many o (M.insert (o + i) (unsafeCoerce v) m)
where i = fromInteger (natVal p)
fromList' :: Ord k => [(k, WrappedAny)] -> M.Map k Any
fromList' xs = M.fromList (coerce xs)
class CaseAny c (xs :: [Type]) r where
caseAny :: c xs r -> Any -> r
data CollectorAny c (xs :: [Type]) r = CollectorAny (c xs r) [Any]
instance AFoldable (CollectorAny c '[]) r where
afoldr _ z _ = z
instance ( CaseAny c (x ': xs) r
, Reiterate c (x ': xs)
, AFoldable (CollectorAny c xs) r
) =>
AFoldable (CollectorAny c (x ': xs)) r where
afoldr f z (CollectorAny c xs) = f (caseAny c x) (afoldr f z (CollectorAny (reiterate c) xs'))
where
x = Partial.head xs
xs' = Partial.tail xs
forMany' :: c xs r -> Many xs -> CollectorAny c xs r
forMany' c (Many _ xs) = CollectorAny c (snd <$> M.toAscList xs)
data CollectorAnyN c n (xs :: [Type]) r = CollectorAnyN (c n xs r) [Any]
instance AFoldable (CollectorAnyN c n '[]) r where
afoldr _ z _ = z
instance ( CaseAny (c n) (x ': xs) r
, ReiterateN c n (x ': xs)
, AFoldable (CollectorAnyN c (n + 1) xs) r
) =>
AFoldable (CollectorAnyN c n (x ': xs)) r where
afoldr f z (CollectorAnyN c xs) = f (caseAny c x) (afoldr f z (CollectorAnyN (reiterateN c) xs'))
where
x = Partial.head xs
xs' = Partial.tail xs
forManyN' :: c n xs r -> Many xs -> CollectorAnyN c n xs r
forManyN' c (Many _ xs) = CollectorAnyN c (snd <$> M.toAscList xs)
data Collector c (xs :: [Type]) r = Collector (c xs r) [Any]
instance AFoldable (Collector c '[]) r where
afoldr _ z _ = z
instance ( Case c (x ': xs) r
, Reiterate c (x ': xs)
, AFoldable (Collector c xs) r
) =>
AFoldable (Collector c (x ': xs)) r where
afoldr f z (Collector c xs) = f (case' c v) (afoldr f z (Collector (reiterate c) xs'))
where
v = unsafeCoerce $ Partial.head xs
xs' = Partial.tail xs
forMany :: c xs r -> Many xs -> Collector c xs r
forMany c (Many _ xs) = Collector c (snd <$> M.toAscList xs)
collect :: Many xs -> c xs r -> Collector c xs r
collect = flip forMany
data CollectorN c (n :: Nat) (xs :: [Type]) r = CollectorN (c n xs r) [Any]
instance AFoldable (CollectorN c n '[]) r where
afoldr _ z _ = z
instance ( Case (c n) (x ': xs) r
, ReiterateN c n (x ': xs)
, AFoldable (CollectorN c (n + 1) xs) r
) =>
AFoldable (CollectorN c n (x ': xs)) r where
afoldr f z (CollectorN c xs) = f (case' c v) (afoldr f z (CollectorN (reiterateN c) xs'))
where
v = unsafeCoerce $ Partial.head xs
xs' = Partial.tail xs
forManyN :: c n xs r -> Many xs -> CollectorN c n xs r
forManyN c (Many _ xs) = CollectorN c (snd <$> M.toAscList xs)
collectN :: Many xs -> c n xs r -> CollectorN c n xs r
collectN = flip forManyN
type Select (smaller :: [Type]) (larger :: [Type]) =
(AFoldable
( CollectorAny (CaseSelect smaller larger) larger) (Maybe (Int, WrappedAny)))
select :: forall smaller larger. Select smaller larger => Many larger -> Many smaller
select t = Many 0 (fromList' xs')
where
xs' = afoldr (\a z -> maybe z (: z) a) [] (forMany' (CaseSelect @smaller @larger @larger) t)
data CaseSelect (smaller :: [Type]) (larger :: [Type]) (xs :: [Type]) r = CaseSelect
instance Reiterate (CaseSelect smaller larger) (x ': xs) where
reiterate = coerce
instance forall smaller larger x xs n. (UniqueIfExists smaller x larger, MaybeUniqueMemberAt n x smaller) =>
CaseAny (CaseSelect smaller larger) (x ': xs) (Maybe (Int, WrappedAny)) where
caseAny _ v =
case i of
0 -> Nothing
i' -> Just (i' 1, WrappedAny v)
where
i = fromInteger (natVal @n Proxy)
selectL
:: forall ls smaller larger proxy.
( Select smaller larger
, smaller ~ KindsAtLabels ls larger
, IsDistinct ls
, UniqueLabels ls larger)
=> proxy ls -> Many larger -> Many smaller
selectL _ = select @smaller
type SelectN (ns :: [Nat]) (smaller ::[Type]) (larger :: [Type]) =
( AFoldable (CollectorAnyN (CaseSelectN ns smaller) 0 larger) (Maybe (Int, WrappedAny))
, smaller ~ KindsAtIndices ns larger
, IsDistinct ns)
selectN
:: forall ns smaller larger proxy.
SelectN ns smaller larger
=> proxy ns -> Many larger -> Many smaller
selectN _ xs = Many 0 (fromList' xs')
where
xs' = afoldr (\a z -> maybe z (: z) a) [] (forManyN' (CaseSelectN @ns @smaller @0 @larger) xs)
data CaseSelectN (indices :: [Nat]) (smaller :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseSelectN
instance ReiterateN (CaseSelectN indices smaller) n (x ': xs) where
reiterateN CaseSelectN = CaseSelectN
instance forall indices smaller n x xs n'. (MaybeMemberAt n' x smaller, n' ~ PositionOf n indices) =>
CaseAny (CaseSelectN indices smaller n) (x ': xs) (Maybe (Int, WrappedAny)) where
caseAny _ v =
case i of
0 -> Nothing
i' -> Just (i' 1, WrappedAny v)
where
i = fromInteger (natVal @n' Proxy)
type Amend smaller larger = (AFoldable (CollectorAny (CaseAmend larger) smaller) (Int, WrappedAny)
, IsDistinct smaller)
amend :: forall smaller larger. Amend smaller larger => Many larger -> Many smaller -> Many larger
amend (Many lo lm) t = Many lo (fromList' xs' `M.union` lm)
where
xs' = afoldr (:) [] (forMany' (CaseAmend @larger @smaller lo) t)
newtype CaseAmend (larger :: [Type]) (xs :: [Type]) r = CaseAmend Int
instance Reiterate (CaseAmend larger) (x ': xs) where
reiterate = coerce
instance UniqueMemberAt n x larger => CaseAny (CaseAmend larger) (x ': xs) (Int, WrappedAny) where
caseAny (CaseAmend lo) v = (lo + i, WrappedAny v)
where
i = fromInteger (natVal @n Proxy)
amendL
:: forall ls smaller larger proxy.
( Amend smaller larger
, smaller ~ KindsAtLabels ls larger
, IsDistinct ls
, UniqueLabels ls larger)
=> proxy ls -> Many larger -> Many smaller -> Many larger
amendL _ = amend @(KindsAtLabels ls larger)
type Amend' smaller smaller' larger zipped =
( AFoldable (CollectorAny (CaseAmend' larger) zipped) (Int, WrappedAny)
, IsDistinct smaller
, zipped ~ Zip smaller smaller')
amend' :: forall smaller smaller' larger proxy zipped. Amend' smaller smaller' larger zipped
=> proxy smaller -> Many larger -> Many smaller' -> Many (Replaces smaller smaller' larger)
amend' _ (Many lo lm) t = Many lo (fromList' xs' `M.union` lm)
where
xs' = afoldr (:) [] (forMany'' @smaller Proxy (CaseAmend' @larger @zipped lo) t)
forMany'' :: Proxy xs -> c (Zip xs ys) r -> Many ys -> CollectorAny c (Zip xs ys) r
forMany'' _ c (Many _ ys) = CollectorAny c (snd <$> M.toAscList ys)
newtype CaseAmend' (larger :: [Type]) (zs :: [Type]) r = CaseAmend' Int
instance Reiterate (CaseAmend' larger) (z ': zs) where
reiterate = coerce
instance (UniqueMemberAt n x larger) => CaseAny (CaseAmend' larger) ((x, y) ': zs) (Int, WrappedAny) where
caseAny (CaseAmend' lo) v = (lo + i, WrappedAny v)
where
i = fromInteger (natVal @n Proxy)
amendL'
:: forall ls smaller smaller' larger proxy zipped.
( Amend' smaller smaller' larger zipped
, smaller ~ KindsAtLabels ls larger
, IsDistinct ls
, UniqueLabels ls larger
)
=> proxy ls
-> Many larger
-> Many smaller'
-> Many (Replaces smaller smaller' larger)
amendL' _ = amend' @(KindsAtLabels ls larger) Proxy
type AmendN ns smaller larger =
( AFoldable (CollectorAnyN (CaseAmendN ns larger) 0 smaller) (Int, WrappedAny)
, smaller ~ KindsAtIndices ns larger
, IsDistinct ns)
amendN :: forall ns smaller larger proxy.
(AmendN ns smaller larger)
=> proxy ns -> Many larger -> Many smaller -> Many larger
amendN _ (Many lo lm) t = Many lo (fromList' xs' `M.union` lm)
where
xs' = afoldr (:) [] (forManyN' (CaseAmendN @ns @larger @0 @smaller lo) t)
newtype CaseAmendN (indices :: [Nat]) (larger :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseAmendN Int
instance ReiterateN (CaseAmendN indices larger) n (x ': xs) where
reiterateN = coerce
instance (MemberAt n' x larger, n' ~ KindAtIndex n indices) =>
CaseAny (CaseAmendN indices larger n) (x ': xs) (Int, WrappedAny) where
caseAny (CaseAmendN lo) v = (lo + i, WrappedAny v)
where
i = fromInteger (natVal @n' Proxy)
type AmendN' ns smaller smaller' larger zipped =
( AFoldable (CollectorAnyN (CaseAmendN' ns larger) 0 zipped) (Int, WrappedAny)
, smaller ~ KindsAtIndices ns larger
, IsDistinct ns
, zipped ~ Zip smaller smaller')
amendN' :: forall ns smaller smaller' larger proxy zipped.
(AmendN' ns smaller smaller' larger zipped)
=> proxy ns -> Many larger -> Many smaller' -> Many (ReplacesIndex ns smaller' larger)
amendN' _ (Many lo lm) t = Many lo (fromList' xs' `M.union` lm)
where
xs' = afoldr (:) [] (forManyN'' @smaller Proxy (CaseAmendN' @ns @larger @0 @zipped lo) t)
forManyN'' :: Proxy xs -> c n (Zip xs ys) r -> Many ys -> CollectorAnyN c n (Zip xs ys) r
forManyN'' _ c (Many _ ys) = CollectorAnyN c (snd <$> M.toAscList ys)
newtype CaseAmendN' (indices :: [Nat]) (larger :: [Type]) (n :: Nat) (zs :: [Type]) r = CaseAmendN' Int
instance ReiterateN (CaseAmendN' indices larger) n (z ': zs) where
reiterateN = coerce
instance (MemberAt n' x larger, n' ~ KindAtIndex n indices) =>
CaseAny (CaseAmendN' indices larger n) ((x, y) ': zs) (Int, WrappedAny) where
caseAny (CaseAmendN' lo) v = (lo + i, WrappedAny v)
where
i = fromInteger (natVal @n' Proxy)
instance Eq (Many_ '[]) where
_ == _ = True
instance (Eq x, Eq (Many_ xs)) => Eq (Many_ (x ': xs)) where
ls == rs = case front' ls == front' rs of
False -> False
_ -> (aft' ls) == (aft' rs)
instance Eq (Many_ xs) => Eq (Many xs) where
lt == rt = toMany_ lt == toMany_ rt
instance Ord (Many_ '[]) where
compare _ _ = EQ
instance (Ord x, Ord (Many_ xs)) => Ord (Many_ (x ': xs)) where
compare ls rs = case compare (front' ls) (front' rs) of
LT -> LT
GT -> GT
EQ -> compare (aft' ls) (aft' rs)
instance Ord (Many_ xs) => Ord (Many xs) where
compare xs ys = compare (toMany_ xs) (toMany_ ys)
instance Show (Many_ '[]) where
showsPrec d _ = showParen (d > app_prec) $ showString "nil"
where
app_prec = 10
instance (Show x, Show (Many_ xs)) => Show (Many_ (x ': xs)) where
showsPrec d ls@(Many_ xs) =
showParen (d > cons_prec) $
showsPrec (cons_prec + 1) v .
showString " ./ " .
showsPrec cons_prec (aft' ls)
where
cons_prec = 5
v = unsafeCoerce (Partial.head xs) :: x
instance Show (Many_ xs) => Show (Many xs) where
showsPrec d xs = showsPrec d (toMany_ xs)
instance Read (Many_ '[]) where
readPrec = parens $ prec app_prec $ do
lift $ L.expect (Ident "nil")
pure $ Many_ []
where
app_prec = 10
instance (Read x, Read (Many_ xs)) => Read (Many_ (x ': xs)) where
readPrec = parens $ prec cons_prec $ do
a <- step (readPrec @x)
lift $ L.expect (Symbol "./")
as <- readPrec @(Many_ xs)
pure $ prefix' a as
where
cons_prec = 5
instance Read (Many_ xs) => Read (Many xs) where
readPrec = do
xs <- readPrec @(Many_ xs)
pure $ fromMany_ xs
newtype WrappedAny = WrappedAny Any