{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Generics.MRSOP.Base.NS where
import Control.Monad
import Generics.MRSOP.Util
data NS :: (k -> *) -> [k] -> * where
There :: NS p xs -> NS p (x : xs)
Here :: p x -> NS p (x : xs)
mapNS :: f :-> g -> NS f ks -> NS g ks
mapNS f (Here p) = Here (f p)
mapNS f (There p) = There (mapNS f p)
mapNSM :: (Monad m) => (forall x . f x -> m (g x)) -> NS f ks -> m (NS g ks)
mapNSM f (Here p) = Here <$> f p
mapNSM f (There p) = There <$> mapNSM f p
elimNS :: (forall x . f x -> a) -> NS f ks -> a
elimNS f (Here p) = f p
elimNS f (There p) = elimNS f p
zipNS :: (MonadPlus m) => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)
zipNS (Here p) (Here q) = return (Here (p :*: q))
zipNS (There p) (There q) = There <$> zipNS p q
zipNS _ _ = mzero
cataNS :: (forall x xs . f x -> r (x ': xs))
-> (forall x xs . r xs -> r (x ': xs))
-> NS f xs -> r xs
cataNS fHere fThere (Here x) = fHere x
cataNS fHere fThere (There x) = fThere (cataNS fHere fThere x)
eqNS :: (forall x. p x -> p x -> Bool)
-> NS p xs -> NS p xs -> Bool
eqNS p x = maybe False (elimNS $ uncurry' p) . zipNS x