{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Ouroboros.Consensus.Util.SOP ( -- * Minor variations on standard SOP operators Lens (..) , allComposeShowK , fn_5 , lenses_NP , map_NP' , npToSListI , npWithIndices , nsFromIndex , nsToIndex , partition_NS , sequence_NS' -- * Type-level non-empty lists , IsNonEmpty (..) , ProofNonEmpty (..) , checkIsNonEmpty -- * Indexing SOP types , Index (..) , dictIndexAll , indices , injectNS , injectNS' , projectNP -- * Zipping with indices , hcimap , hcizipWith , hcizipWith3 , hcizipWith4 , himap , hizipWith , hizipWith3 , hizipWith4 ) where import Data.Coerce import Data.Kind (Type) import Data.SOP.Dict import Data.SOP.Strict import Data.Word {------------------------------------------------------------------------------- Minor variations on standard SOP operators -------------------------------------------------------------------------------} -- | Version of 'sequence_NS' that requires only 'Functor' -- -- The version in the library requires 'Applicative', which is unnecessary. sequence_NS' :: forall xs f g. Functor f => NS (f :.: g) xs -> f (NS g xs) sequence_NS' :: NS (f :.: g) xs -> f (NS g xs) sequence_NS' = NS (f :.: g) xs -> f (NS g xs) forall (xs' :: [k]). NS (f :.: g) xs' -> f (NS g xs') go where go :: NS (f :.: g) xs' -> f (NS g xs') go :: NS (f :.: g) xs' -> f (NS g xs') go (Z (Comp f (g x) fx)) = g x -> NS g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (g x -> NS g (x : xs)) -> f (g x) -> f (NS g (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f (g x) fx go (S NS (f :.: g) xs r) = NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS g xs -> NS g (x : xs)) -> f (NS g xs) -> f (NS g (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NS (f :.: g) xs -> f (NS g xs) forall (xs' :: [k]). NS (f :.: g) xs' -> f (NS g xs') go NS (f :.: g) xs r -- | Version of 'map_NP' that does not require a singleton map_NP' :: forall f g xs. (forall a. f a -> g a) -> NP f xs -> NP g xs map_NP' :: (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs map_NP' forall (a :: k). f a -> g a f = NP f xs -> NP g xs forall (xs' :: [k]). NP f xs' -> NP g xs' go where go :: NP f xs' -> NP g xs' go :: NP f xs' -> NP g xs' go NP f xs' Nil = NP g xs' forall k (f :: k -> *). NP f '[] Nil go (f x x :* NP f xs xs) = f x -> g x forall (a :: k). f a -> g a f f x x g x -> NP g xs -> NP g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP f xs -> NP g xs forall (xs' :: [k]). NP f xs' -> NP g xs' go NP f xs xs partition_NS :: forall xs f. SListI xs => [NS f xs] -> NP ([] :.: f) xs partition_NS :: [NS f xs] -> NP ([] :.: f) xs partition_NS = (NP ([] :.: f) xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs) -> NP ([] :.: f) xs -> [NP ([] :.: f) xs] -> NP ([] :.: f) xs forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr ((forall (a :: k). (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a) -> Prod NP ([] :.: f) xs -> NP ([] :.: f) xs -> NP ([] :.: f) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hzipWith forall (a :: k). (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a append) ((forall (a :: k). (:.:) [] f a) -> NP ([] :.: f) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HPure h, SListIN h xs) => (forall (a :: k). f a) -> h f xs hpure forall (a :: k). (:.:) [] f a nil) ([NP ([] :.: f) xs] -> NP ([] :.: f) xs) -> ([NS f xs] -> [NP ([] :.: f) xs]) -> [NS f xs] -> NP ([] :.: f) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . (NS f xs -> NP ([] :.: f) xs) -> [NS f xs] -> [NP ([] :.: f) xs] forall a b. (a -> b) -> [a] -> [b] map ((forall (a :: k). (:.:) [] f a) -> NS ([] :.: f) xs -> Prod NS ([] :.: f) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HExpand h, SListIN (Prod h) xs) => (forall (x :: k). f x) -> h f xs -> Prod h f xs hexpand forall (a :: k). (:.:) [] f a nil (NS ([] :.: f) xs -> NP ([] :.: f) xs) -> (NS f xs -> NS ([] :.: f) xs) -> NS f xs -> NP ([] :.: f) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: k). f a -> (:.:) [] f a) -> NS f xs -> NS ([] :.: f) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall (a :: k). f a -> (:.:) [] f a singleton) where nil :: ([] :.: f) a nil :: (:.:) [] f a nil = [f a] -> (:.:) [] f a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp [] singleton :: f a -> ([] :.: f) a singleton :: f a -> (:.:) [] f a singleton = [f a] -> (:.:) [] f a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp ([f a] -> (:.:) [] f a) -> (f a -> [f a]) -> f a -> (:.:) [] f a forall b c a. (b -> c) -> (a -> b) -> a -> c . (f a -> [f a] -> [f a] forall a. a -> [a] -> [a] :[]) append :: ([] :.: f) a -> ([] :.: f) a -> ([] :.: f) a append :: (:.:) [] f a -> (:.:) [] f a -> (:.:) [] f a append (Comp [f a] as) (Comp [f a] as') = [f a] -> (:.:) [] f a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp ([f a] as [f a] -> [f a] -> [f a] forall a. [a] -> [a] -> [a] ++ [f a] as') -- | We only allow up to 23 (so counting from 0, 24 elements in @xs@), because -- CBOR stores a 'Word8' in the range 0-23 as a single byte equal to the value -- of the 'Word8'. We rely on this in 'reconstructNestedCtxt' and other -- places. npWithIndices :: SListI xs => NP (K Word8) xs npWithIndices :: NP (K Word8) xs npWithIndices = Word8 -> SList xs -> NP (K Word8) xs forall k (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs' go Word8 0 SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: Word8 -> SList xs' -> NP (K Word8) xs' go :: Word8 -> SList xs' -> NP (K Word8) xs' go !Word8 _ SList xs' SNil = NP (K Word8) xs' forall k (f :: k -> *). NP f '[] Nil go Word8 24 SList xs' SCons = [Char] -> NP (K Word8) xs' forall a. HasCallStack => [Char] -> a error [Char] "npWithIndices out of range" go !Word8 i SList xs' SCons = Word8 -> K Word8 x forall k a (b :: k). a -> K a b K Word8 i K Word8 x -> NP (K Word8) xs -> NP (K Word8) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* Word8 -> SList xs -> NP (K Word8) xs forall k (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs' go (Word8 i Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Word8 1) SList xs forall k (xs :: [k]). SListI xs => SList xs sList nsToIndex :: SListI xs => NS f xs -> Word8 nsToIndex :: NS f xs -> Word8 nsToIndex = NS (K Word8) xs -> Word8 forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K Word8) xs -> Word8) -> (NS f xs -> NS (K Word8) xs) -> NS f xs -> Word8 forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: k). K Word8 a -> f a -> K Word8 a) -> Prod NS (K Word8) xs -> NS f xs -> NS (K Word8) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hzipWith forall (a :: k). K Word8 a -> f a -> K Word8 a forall a b. a -> b -> a const Prod NS (K Word8) xs forall k (xs :: [k]). SListI xs => NP (K Word8) xs npWithIndices -- | We only allow up to 23, see 'npWithIndices'. nsFromIndex :: SListI xs => Word8 -> Maybe (NS (K ()) xs) nsFromIndex :: Word8 -> Maybe (NS (K ()) xs) nsFromIndex Word8 n = Word8 -> SList xs -> Maybe (NS (K ()) xs) forall k (xs' :: [k]). Word8 -> SList xs' -> Maybe (NS (K ()) xs') go Word8 0 SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: Word8 -> SList xs' -> Maybe (NS (K ()) xs') go :: Word8 -> SList xs' -> Maybe (NS (K ()) xs') go !Word8 i SList xs' SCons | Word8 i Word8 -> Word8 -> Bool forall a. Eq a => a -> a -> Bool == Word8 24 = [Char] -> Maybe (NS (K ()) xs') forall a. HasCallStack => [Char] -> a error [Char] "nsFromIndex out of range" | Word8 i Word8 -> Word8 -> Bool forall a. Eq a => a -> a -> Bool == Word8 n = NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs)) forall a. a -> Maybe a Just (NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs))) -> NS (K ()) (x : xs) -> Maybe (NS (K ()) (x : xs)) forall a b. (a -> b) -> a -> b $ K () x -> NS (K ()) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (K () x -> NS (K ()) (x : xs)) -> K () x -> NS (K ()) (x : xs) forall a b. (a -> b) -> a -> b $ () -> K () x forall k a (b :: k). a -> K a b K () | Bool otherwise = NS (K ()) xs -> NS (K ()) (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS (K ()) xs -> NS (K ()) (x : xs)) -> Maybe (NS (K ()) xs) -> Maybe (NS (K ()) (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Word8 -> SList xs -> Maybe (NS (K ()) xs) forall k (xs' :: [k]). Word8 -> SList xs' -> Maybe (NS (K ()) xs') go (Word8 i Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Word8 1) SList xs forall k (xs :: [k]). SListI xs => SList xs sList go !Word8 _ SList xs' SNil = Maybe (NS (K ()) xs') forall a. Maybe a Nothing -- | Simple lens to access an element of an n-ary product. data Lens f xs a = Lens { Lens f xs a -> NP f xs -> f a getter :: NP f xs -> f a , Lens f xs a -> f a -> NP f xs -> NP f xs setter :: f a -> NP f xs -> NP f xs } -- | Generate all lenses to access the element of an n-ary product. lenses_NP :: forall f xs. SListI xs => NP (Lens f xs) xs lenses_NP :: NP (Lens f xs) xs lenses_NP = SList xs -> NP (Lens f xs) xs forall (xs' :: [k]). SList xs' -> NP (Lens f xs') xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: SList xs' -> NP (Lens f xs') xs' go :: SList xs' -> NP (Lens f xs') xs' go SList xs' SNil = NP (Lens f xs') xs' forall k (f :: k -> *). NP f '[] Nil go SList xs' SCons = Lens f (x : xs) x forall (x :: k) (xs' :: [k]). Lens f (x : xs') x lensFirst Lens f (x : xs) x -> NP (Lens f (x : xs)) xs -> NP (Lens f (x : xs)) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (forall (a :: k). Lens f xs a -> Lens f (x : xs) a) -> NP (Lens f xs) xs -> NP (Lens f (x : xs)) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall (a :: k). Lens f xs a -> Lens f (x : xs) a forall (xs' :: [k]) (a :: k) (x :: k). Lens f xs' a -> Lens f (x : xs') a shiftLens (SList xs -> NP (Lens f xs) xs forall (xs' :: [k]). SList xs' -> NP (Lens f xs') xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList) lensFirst :: Lens f (x ': xs') x lensFirst :: Lens f (x : xs') x lensFirst = Lens :: forall k (f :: k -> *) (xs :: [k]) (a :: k). (NP f xs -> f a) -> (f a -> NP f xs -> NP f xs) -> Lens f xs a Lens { getter :: NP f (x : xs') -> f x getter = NP f (x : xs') -> f x forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x hd , setter :: f x -> NP f (x : xs') -> NP f (x : xs') setter = \f x a' (f x _ :* NP f xs as) -> f x a' f x -> NP f xs -> NP f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP f xs as } shiftLens :: Lens f xs' a -> Lens f (x ': xs') a shiftLens :: Lens f xs' a -> Lens f (x : xs') a shiftLens Lens f xs' a l = Lens :: forall k (f :: k -> *) (xs :: [k]) (a :: k). (NP f xs -> f a) -> (f a -> NP f xs -> NP f xs) -> Lens f xs a Lens { getter :: NP f (x : xs') -> f a getter = Lens f xs' a -> NP f xs' -> f a forall k (f :: k -> *) (xs :: [k]) (a :: k). Lens f xs a -> NP f xs -> f a getter Lens f xs' a l (NP f xs' -> f a) -> (NP f (x : xs') -> NP f xs') -> NP f (x : xs') -> f a forall b c a. (b -> c) -> (a -> b) -> a -> c . NP f (x : xs') -> NP f xs' forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> NP f xs tl , setter :: f a -> NP f (x : xs') -> NP f (x : xs') setter = \f a a' (f x a :* NP f xs as) -> f x a f x -> NP f xs' -> NP f (x : xs') forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* Lens f xs' a -> f a -> NP f xs' -> NP f xs' forall k (f :: k -> *) (xs :: [k]) (a :: k). Lens f xs a -> f a -> NP f xs -> NP f xs setter Lens f xs' a l f a a' NP f xs' NP f xs as } -- | Conjure up an 'SListI' constraint from an 'NP' npToSListI :: NP a xs -> (SListI xs => r) -> r npToSListI :: NP a xs -> (SListI xs => r) -> r npToSListI NP a xs np = SList xs -> (SListI xs => r) -> r forall k (xs :: [k]) r. SList xs -> (SListI xs => r) -> r sListToSListI (SList xs -> (SListI xs => r) -> r) -> SList xs -> (SListI xs => r) -> r forall a b. (a -> b) -> a -> b $ NP a xs -> SList xs forall k (a :: k -> *) (xs :: [k]). NP a xs -> SList xs npToSList NP a xs np where sListToSListI :: SList xs -> (SListI xs => r) -> r sListToSListI :: SList xs -> (SListI xs => r) -> r sListToSListI SList xs SNil SListI xs => r k = r SListI xs => r k sListToSListI SList xs SCons SListI xs => r k = r SListI xs => r k npToSList :: NP a xs -> SList xs npToSList :: NP a xs -> SList xs npToSList NP a xs Nil = SList xs forall k. SList '[] SNil npToSList (a x _ :* NP a xs xs) = SList xs -> (SListI xs => SList xs) -> SList xs forall k (xs :: [k]) r. SList xs -> (SListI xs => r) -> r sListToSListI (NP a xs -> SList xs forall k (a :: k -> *) (xs :: [k]). NP a xs -> SList xs npToSList NP a xs xs) SListI xs => SList xs forall k (xs :: [k]) (x :: k). SListI xs => SList (x : xs) SCons allComposeShowK :: (SListI xs, Show a) => Proxy xs -> Proxy a -> Dict (All (Compose Show (K a))) xs allComposeShowK :: Proxy xs -> Proxy a -> Dict (All (Compose Show (K a))) xs allComposeShowK Proxy xs _ Proxy a _ = NP (Dict (Compose Show (K a))) xs -> Dict (All (Compose Show (K a))) xs forall k (c :: k -> Constraint) (xs :: [k]). NP (Dict c) xs -> Dict (All c) xs all_NP (NP (Dict (Compose Show (K a))) xs -> Dict (All (Compose Show (K a))) xs) -> NP (Dict (Compose Show (K a))) xs -> Dict (All (Compose Show (K a))) xs forall a b. (a -> b) -> a -> b $ (forall (a :: k). Dict (Compose Show (K a)) a) -> NP (Dict (Compose Show (K a))) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HPure h, SListIN h xs) => (forall (a :: k). f a) -> h f xs hpure forall (a :: k). Dict (Compose Show (K a)) a forall k (c :: k -> Constraint) (a :: k). c a => Dict c a Dict fn_5 :: (f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> (f0 -.-> f1 -.-> f2 -.-> f3 -.-> f4 -.-> f5) a fn_5 :: (f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a fn_5 f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a f = (f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a) -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a) -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a) -> (f0 a -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a) -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a forall a b. (a -> b) -> a -> b $ \f0 a x0 -> (f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a) -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a) -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a) -> (f1 a -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a) -> (-.->) f1 (f2 -.-> (f3 -.-> (f4 -.-> f5))) a forall a b. (a -> b) -> a -> b $ \f1 a x1 -> (f2 a -> (-.->) f3 (f4 -.-> f5) a) -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f2 a -> (-.->) f3 (f4 -.-> f5) a) -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a) -> (f2 a -> (-.->) f3 (f4 -.-> f5) a) -> (-.->) f2 (f3 -.-> (f4 -.-> f5)) a forall a b. (a -> b) -> a -> b $ \f2 a x2 -> (f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a) -> (f3 a -> (-.->) f4 f5 a) -> (-.->) f3 (f4 -.-> f5) a forall a b. (a -> b) -> a -> b $ \f3 a x3 -> (f4 a -> f5 a) -> (-.->) f4 f5 a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f4 a -> f5 a) -> (-.->) f4 f5 a) -> (f4 a -> f5 a) -> (-.->) f4 f5 a forall a b. (a -> b) -> a -> b $ \f4 a x4 -> f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a f f0 a x0 f1 a x1 f2 a x2 f3 a x3 f4 a x4 {------------------------------------------------------------------------------- Type-level non-empty lists -------------------------------------------------------------------------------} data ProofNonEmpty :: [a] -> Type where ProofNonEmpty :: Proxy x -> Proxy xs -> ProofNonEmpty (x ': xs) class IsNonEmpty xs where isNonEmpty :: proxy xs -> ProofNonEmpty xs instance IsNonEmpty (x ': xs) where isNonEmpty :: proxy (x : xs) -> ProofNonEmpty (x : xs) isNonEmpty proxy (x : xs) _ = Proxy x -> Proxy xs -> ProofNonEmpty (x : xs) forall a (x :: a) (xs :: [a]). Proxy x -> Proxy xs -> ProofNonEmpty (x : xs) ProofNonEmpty (Proxy x forall k (t :: k). Proxy t Proxy @x) (Proxy xs forall k (t :: k). Proxy t Proxy @xs) checkIsNonEmpty :: forall xs. SListI xs => Proxy xs -> Maybe (ProofNonEmpty xs) checkIsNonEmpty :: Proxy xs -> Maybe (ProofNonEmpty xs) checkIsNonEmpty Proxy xs _ = case SListI xs => SList xs forall k (xs :: [k]). SListI xs => SList xs sList @xs of SList xs SNil -> Maybe (ProofNonEmpty xs) forall a. Maybe a Nothing SList xs SCons -> ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs)) forall a. a -> Maybe a Just (ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs))) -> ProofNonEmpty (x : xs) -> Maybe (ProofNonEmpty (x : xs)) forall a b. (a -> b) -> a -> b $ Proxy x -> Proxy xs -> ProofNonEmpty (x : xs) forall a (x :: a) (xs :: [a]). Proxy x -> Proxy xs -> ProofNonEmpty (x : xs) ProofNonEmpty Proxy x forall k (t :: k). Proxy t Proxy Proxy xs forall k (t :: k). Proxy t Proxy {------------------------------------------------------------------------------- Indexing SOP types -------------------------------------------------------------------------------} data Index xs x where IZ :: Index (x ': xs) x IS :: Index xs x -> Index (y ': xs) x indices :: forall xs. SListI xs => NP (Index xs) xs indices :: NP (Index xs) xs indices = case SListI xs => SList xs forall k (xs :: [k]). SListI xs => SList xs sList @xs of SList xs SNil -> NP (Index xs) xs forall k (f :: k -> *). NP f '[] Nil SList xs SCons -> Index (x : xs) x forall a (x :: a) (xs :: [a]). Index (x : xs) x IZ Index (x : xs) x -> NP (Index (x : xs)) xs -> NP (Index (x : xs)) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (forall (a :: k). Index xs a -> Index (x : xs) a) -> NP (Index xs) xs -> NP (Index (x : xs)) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall (a :: k). Index xs a -> Index (x : xs) a forall a (xs :: [a]) (x :: a) (y :: a). Index xs x -> Index (y : xs) x IS NP (Index xs) xs forall k (xs :: [k]). SListI xs => NP (Index xs) xs indices dictIndexAll :: All c xs => Proxy c -> Index xs x -> Dict c x dictIndexAll :: Proxy c -> Index xs x -> Dict c x dictIndexAll Proxy c p = \case Index xs x IZ -> Dict c x forall k (c :: k -> Constraint) (a :: k). c a => Dict c a Dict IS Index xs x idx' -> Proxy c -> Index xs x -> Dict c x forall k (c :: k -> Constraint) (xs :: [k]) (x :: k). All c xs => Proxy c -> Index xs x -> Dict c x dictIndexAll Proxy c p Index xs x idx' injectNS :: forall f x xs. Index xs x -> f x -> NS f xs injectNS :: Index xs x -> f x -> NS f xs injectNS Index xs x idx f x x = case Index xs x idx of Index xs x IZ -> f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z f x x IS Index xs x idx' -> NS f xs -> NS f (y : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (Index xs x -> f x -> NS f xs forall k (f :: k -> *) (x :: k) (xs :: [k]). Index xs x -> f x -> NS f xs injectNS Index xs x idx' f x x) injectNS' :: forall f a b x xs. (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' :: Proxy f -> Index xs x -> a -> b injectNS' Proxy f _ Index xs x idx = NS f xs -> b coerce (NS f xs -> b) -> (a -> NS f xs) -> a -> b forall b c a. (b -> c) -> (a -> b) -> a -> c . Index xs x -> f x -> NS f xs forall k (f :: k -> *) (x :: k) (xs :: [k]). Index xs x -> f x -> NS f xs injectNS @f Index xs x idx (f x -> NS f xs) -> (a -> f x) -> a -> NS f xs forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> f x coerce projectNP :: Index xs x -> NP f xs -> f x projectNP :: Index xs x -> NP f xs -> f x projectNP Index xs x IZ (f x x :* NP f xs _) = f x f x x projectNP (IS Index xs x idx) (f x _ :* NP f xs xs) = Index xs x -> NP f xs -> f x forall k (xs :: [k]) (x :: k) (f :: k -> *). Index xs x -> NP f xs -> f x projectNP Index xs x idx NP f xs NP f xs xs {------------------------------------------------------------------------------- Zipping with indices -------------------------------------------------------------------------------} hcimap :: (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall a. c a => Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs hcimap :: proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs hcimap proxy c p forall (a :: k). c a => Index xs a -> f1 a -> f2 a f h f1 xs xs1 = proxy c -> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> f2) a) -> NP (Index xs -.-> (f1 -.-> f2)) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((Index xs a -> f1 a -> f2 a) -> (-.->) (Index xs) (f1 -.-> f2) a forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *). (f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a fn_2 Index xs a -> f1 a -> f2 a forall (a :: k). c a => Index xs a -> f1 a -> f2 a f) Prod NP (Index xs -.-> (f1 -.-> f2)) xs -> NP (Index xs) xs -> NP (f1 -.-> f2) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP (Index xs) xs forall k (xs :: [k]). SListI xs => NP (Index xs) xs indices Prod h (f1 -.-> f2) xs -> h f1 xs -> h f2 xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` h f1 xs xs1 himap :: (HAp h, SListI xs, Prod h ~ NP) => (forall a. Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs himap :: (forall (a :: k). Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs himap = Proxy Top -> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *) (f2 :: k -> *). (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs hcimap (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hcizipWith :: (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs hcizipWith :: proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs hcizipWith proxy c p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a f NP f1 xs xs1 h f2 xs xs2 = proxy c -> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a) -> NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((Index xs a -> f1 a -> f2 a -> f3 a) -> (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *). (f a -> f' a -> f'' a -> f''' a) -> (-.->) f (f' -.-> (f'' -.-> f''')) a fn_3 Index xs a -> f1 a -> f2 a -> f3 a forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a f) Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs -> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> f3)) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP (Index xs) xs forall k (xs :: [k]). SListI xs => NP (Index xs) xs indices Prod NP (f1 -.-> (f2 -.-> f3)) xs -> NP f1 xs -> NP (f2 -.-> f3) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f1 xs xs1 Prod h (f2 -.-> f3) xs -> h f2 xs -> h f3 xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` h f2 xs xs2 hizipWith :: (HAp h, SListI xs, Prod h ~ NP) => (forall a. Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs hizipWith :: (forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs hizipWith = Proxy Top -> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *) (f2 :: k -> *) (f3 :: k -> *). (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a) -> NP f1 xs -> h f2 xs -> h f3 xs hcizipWith (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hcizipWith3 :: (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs hcizipWith3 :: proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs hcizipWith3 proxy c p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a f NP f1 xs xs1 NP f2 xs xs2 h f3 xs xs3 = proxy c -> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a) -> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *) (f'''' :: k -> *). (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a fn_4 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a f) Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs -> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP (Index xs) xs forall k (xs :: [k]). SListI xs => NP (Index xs) xs indices Prod NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs -> NP f1 xs -> NP (f2 -.-> (f3 -.-> f4)) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f1 xs xs1 Prod NP (f2 -.-> (f3 -.-> f4)) xs -> NP f2 xs -> NP (f3 -.-> f4) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f2 xs xs2 Prod h (f3 -.-> f4) xs -> h f3 xs -> h f4 xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` h f3 xs xs3 hizipWith3 :: (HAp h, SListI xs, Prod h ~ NP) => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs hizipWith3 :: (forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs hizipWith3 = Proxy Top -> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *) (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *). (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a) -> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs hcizipWith3 (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hcizipWith4 :: (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs hcizipWith4 :: proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs hcizipWith4 proxy c p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a f NP f1 xs xs1 NP f2 xs xs2 NP f3 xs xs3 h f4 xs xs4 = proxy c -> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a) -> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a forall k (f0 :: k -> *) (a :: k) (f1 :: k -> *) (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *). (f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a fn_5 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a f) Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs -> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP (Index xs) xs forall k (xs :: [k]). SListI xs => NP (Index xs) xs indices Prod NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs -> NP f1 xs -> NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f1 xs xs1 Prod NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs -> NP f2 xs -> NP (f3 -.-> (f4 -.-> f5)) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f2 xs xs2 Prod NP (f3 -.-> (f4 -.-> f5)) xs -> NP f3 xs -> NP (f4 -.-> f5) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` NP f3 xs xs3 Prod h (f4 -.-> f5) xs -> h f4 xs -> h f5 xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs `hap` h f4 xs xs4 hizipWith4 :: (HAp h, SListI xs, Prod h ~ NP) => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs hizipWith4 :: (forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs hizipWith4 = Proxy Top -> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs forall k (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *) (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *). (HAp h, All c xs, Prod h ~ NP) => proxy c -> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a) -> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs hcizipWith4 (Proxy Top forall k (t :: k). Proxy t Proxy @Top)