{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Prodder
(
Prod
, extract
, index
, tailN
, initN
, dropFirst
, Consume(consume, produce, extend1, cmap)
, IndexIn
, HasIndexIn
, Consumer
, (<>)
, Length
, Tail
, Init
, Replace
, Strengthen(strengthen)
, remap
) where
import Control.Monad (unless)
import Control.Exception (catch, SomeException)
import GHC.Exts (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.Vector (Vector)
import qualified Data.Vector as V
import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=))
import Data.Proxy (Proxy(Proxy))
data Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any }
type role Prod representational
type family IndexIn (x :: k) (xs :: [k]) where
IndexIn x (x ': xs) = 0
IndexIn x (y ': xs) = 1 + IndexIn x xs
type family Length (xs :: [k]) where
Length '[] = 0
Length (x ': xs) = 1 + Length xs
type family Tail n xs where
Tail 0 xs = xs
Tail n (x ': xs) = Tail (n - 1) xs
type family Init n xs where
Init 0 xs = '[]
Init n (x ': xs) = x ': Init (n - 1) xs
class KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs
instance KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs
index :: forall x xs. x `HasIndexIn` xs => Word
index = fromInteger $ natVal (Proxy @(IndexIn x xs))
{-# INLINE CONLIKE index #-}
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x
extract (UnsafeProd v) = unsafeCoerce $ v V.! fromIntegral (index @x @xs)
{-# INLINE CONLIKE extract #-}
tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)
tailN (UnsafeProd v) = UnsafeProd $ V.slice n (V.length v - n) v
where
n = fromInteger $ natVal (Proxy @n)
{-# INLINE CONLIKE tailN #-}
initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)
initN (UnsafeProd v) = UnsafeProd $ V.slice 0 n v
where
n = fromInteger $ natVal (Proxy @n)
{-# INLINE CONLIKE initN #-}
dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs
dropFirst (UnsafeProd v) = UnsafeProd $ V.slice 1 (V.length v - 1) v
type family (<>) (xs :: [k]) (ys :: [k]) :: [k] where
'[] <> ys = ys
(x ': xs) <> ys = x ': (xs <> ys)
combine :: forall xs ys. Prod xs -> Prod ys -> Prod (xs <> ys)
combine (UnsafeProd p) (UnsafeProd q) = UnsafeProd (p V.++ q)
{-# INLINE CONLIKE combine #-}
type family Replace x y xs where
Replace x y (x ': xs) = y ': xs
Replace x y (z ': xs) = z ': Replace x y xs
remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)
remap f (UnsafeProd v) = UnsafeProd (update `V.imap` v) where
update :: Int -> Any -> Any
update (fromIntegral -> n) a
| n == index @x @xs = unsafeCoerce $ f $ unsafeCoerce a
| otherwise = a
{-# INLINE CONLIKE update #-}
{-# INLINE CONLIKE remap #-}
type family Consumer xs r where
Consumer '[] r = r
Consumer (x ': xs) r = x -> Consumer xs r
class Consume xs where
consume :: forall r. Prod xs -> Consumer xs r -> r
produce :: (forall r. Consumer xs r -> r) -> Prod xs
extend1 :: x -> Consumer xs (Prod (x ': xs))
cmap :: (r -> r') -> Consumer xs r -> Consumer xs r'
instance Consume '[] where
consume = flip const
{-# INLINE CONLIKE consume #-}
produce x = UnsafeProd V.empty
{-# INLINE CONLIKE produce #-}
extend1 x = UnsafeProd (V.singleton (unsafeCoerce x))
{-# INLINE CONLIKE extend1 #-}
cmap f x = f x
{-# INLINE CONLIKE cmap #-}
instance Consume xs => Consume (x ': xs) where
consume (UnsafeProd v) g = consume @xs (UnsafeProd (V.tail v)) $ g (unsafeCoerce $ v V.! 0)
{-# INLINE CONLIKE consume #-}
produce g = g (extend1 @xs)
{-# INLINE CONLIKE produce #-}
cmap f = fmap (cmap @xs f)
{-# INLINE CONLIKE cmap #-}
extend1 (x1 :: x1) x = cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)
{-# INLINE CONLIKE extend1 #-}
instance Eq (Prod '[]) where
_ == _ = True
{-# INLINE CONLIKE (==) #-}
instance (Eq x, Eq (Prod xs)) => Eq (Prod (x ': xs)) where
px@(UnsafeProd x) == py@(UnsafeProd y) = unsafeCoerce @_ @x (x V.! 0) == unsafeCoerce @_ @x (y V.! 0) && dropFirst px == dropFirst py
{-# INLINE CONLIKE (==) #-}
class Strengthen xs ys where
strengthen :: Prod xs -> Prod ys
instance (Strengthen xs ys, y `HasIndexIn` xs) => Strengthen xs (y ': ys) where
strengthen p = UnsafeProd $ V.singleton (unsafeCoerce $ unProd p V.! fromIntegral (index @y @xs)) <> unProd (strengthen @xs @ys p)
{-# INLINE CONLIKE strengthen #-}
instance Strengthen xs '[] where
strengthen = const (UnsafeProd V.empty)
{-# INLINE CONLIKE strengthen #-}