module Generics.SOP.NS
(
NS(..)
, SOP(..)
, unSOP
, Injection
, injections
, shift
, shiftInjection
, apInjs_NP
, apInjs_POP
, ap_NS
, ap_SOP
, liftA_NS
, liftA_SOP
, liftA2_NS
, liftA2_SOP
, cliftA_NS
, cliftA_SOP
, cliftA2_NS
, cliftA2_SOP
, map_NS
, map_SOP
, cmap_NS
, cmap_SOP
, cliftA2'_NS
, collapse_NS
, collapse_SOP
, sequence'_NS
, sequence'_SOP
, sequence_NS
, sequence_SOP
) where
#if !(MIN_VERSION_base(4,8,0))
import Control.Applicative
#endif
import Generics.SOP.BasicFunctors
import Generics.SOP.Classes
import Generics.SOP.Constraint
import Generics.SOP.NP
import Generics.SOP.Sing
data NS :: (k -> *) -> [k] -> * where
Z :: f x -> NS f (x ': xs)
S :: NS f xs -> NS f (x ': xs)
deriving instance All (Show `Compose` f) xs => Show (NS f xs)
deriving instance All (Eq `Compose` f) xs => Eq (NS f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)
newtype SOP (f :: (k -> *)) (xss :: [[k]]) = SOP (NS (NP f) xss)
deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss)
deriving instance (Eq (NS (NP f) xss)) => Eq (SOP f xss)
deriving instance (Ord (NS (NP f) xss)) => Ord (SOP f xss)
unSOP :: SOP f xss -> NS (NP f) xss
unSOP (SOP xss) = xss
type Injection (f :: k -> *) (xs :: [k]) = f -.-> K (NS f xs)
injections :: forall xs f. SListI xs => NP (Injection f xs) xs
injections = case sList :: SList xs of
SNil -> Nil
SCons -> fn (K . Z) :* liftA_NP shiftInjection injections
shiftInjection :: Injection f xs a -> Injection f (x ': xs) a
shiftInjection (Fn f) = Fn $ K . S . unK . f
shift :: Injection f xs a -> Injection f (x ': xs) a
shift = shiftInjection
apInjs_NP :: SListI xs => NP f xs -> [NS f xs]
apInjs_NP = hcollapse . hap injections
apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]
apInjs_POP = map SOP . apInjs_NP . unPOP
ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS (Fn f :* _) (Z x) = Z (f x)
ap_NS (_ :* fs) (S xs) = S (ap_NS fs xs)
ap_NS _ _ = error "inaccessible"
ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss
ap_SOP (POP fss') (SOP xss') = SOP (go fss' xss')
where
go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
go (fs :* _ ) (Z xs ) = Z (ap_NP fs xs )
go (_ :* fss) (S xss) = S (go fss xss)
go _ _ = error "inaccessible"
_ap_SOP_spec :: SListI xss => POP (t -.-> f) xss -> SOP t xss -> SOP f xss
_ap_SOP_spec (POP fs) (SOP xs) = SOP (liftA2_NS ap_NP fs xs)
type instance Prod NS = NP
type instance Prod SOP = POP
type instance SListIN NS = SListI
type instance SListIN SOP = SListI2
instance HAp NS where hap = ap_NS
instance HAp SOP where hap = ap_SOP
liftA_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs
liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss
liftA_NS = hliftA
liftA_SOP = hliftA
liftA2_NS :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs
liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss
liftA2_NS = hliftA2
liftA2_SOP = hliftA2
map_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs
map_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss
map_NS = hmap
map_SOP = hmap
cliftA_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs
cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss
cliftA_NS = hcliftA
cliftA_SOP = hcliftA
cliftA2_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs
cliftA2_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss
cliftA2_NS = hcliftA2
cliftA2_SOP = hcliftA2
cmap_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs
cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss
cmap_NS = hcmap
cmap_SOP = hcmap
cliftA2'_NS :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss
cliftA2'_NS = hcliftA2'
collapse_NS :: NS (K a) xs -> a
collapse_SOP :: SListI xss => SOP (K a) xss -> [a]
collapse_NS (Z (K x)) = x
collapse_NS (S xs) = collapse_NS xs
collapse_SOP = collapse_NS . hliftA (K . collapse_NP) . unSOP
type instance CollapseTo NS a = a
type instance CollapseTo SOP a = [a]
instance HCollapse NS where hcollapse = collapse_NS
instance HCollapse SOP where hcollapse = collapse_SOP
sequence'_NS :: Applicative f => NS (f :.: g) xs -> f (NS g xs)
sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)
sequence'_NS (Z mx) = Z <$> unComp mx
sequence'_NS (S mxs) = S <$> sequence'_NS mxs
sequence'_SOP = fmap SOP . sequence'_NS . hliftA (Comp . sequence'_NP) . unSOP
instance HSequence NS where hsequence' = sequence'_NS
instance HSequence SOP where hsequence' = sequence'_SOP
sequence_NS :: (SListI xs, Applicative f) => NS f xs -> f (NS I xs)
sequence_SOP :: (All SListI xss, Applicative f) => SOP f xss -> f (SOP I xss)
sequence_NS = hsequence
sequence_SOP = hsequence