{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE BlockArguments #-}
{-# 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, extend1, cmap, produceB)
, produce
, empty
, ToList(toList)
, type ForAll
, buildProd
, ProdBuilder
, consB
, emptyB
, Index
, IndexIn
, HasIndexIn
, Consumer
, type (<>)
, Length
, Tail
, Init
, Replace
, Strengthen(strengthen)
, remap
, Selection(select)
, type FieldsFromSelector
, type Selector
) where
import Data.ForAll (type ForAll)
import Control.Monad (unless)
import Control.Exception (catch, SomeException)
import GHC.Exts (Any, Constraint)
import Unsafe.Coerce (unsafeCoerce)
import Data.Functor.Identity (Identity (..))
import Data.Vector (Vector)
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=), Nat)
import Data.Proxy (Proxy(Proxy))
import Control.Monad.ST
import Data.STRef (newSTRef, STRef, writeSTRef, readSTRef)
newtype Prod (xs :: [*]) = UnsafeProd { Prod xs -> Vector Any
unProd :: Vector Any }
newtype ProdBuilder (xs :: [*]) = UnsafeProdBuilder { ProdBuilder xs -> forall s. STRef s Int -> MVector s Any -> ST s ()
unProdBuilder :: forall s. STRef s Int -> V.MVector s Any -> ST s () }
consB :: x -> ProdBuilder xs -> ProdBuilder (x ': xs)
consB :: x -> ProdBuilder xs -> ProdBuilder (x : xs)
consB x
x (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
b) = (forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder (x : xs)
forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> STRef s Int -> (Int -> ST s ()) -> ST s ()
forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref \Int
i -> do
MVector (PrimState (ST s)) Any -> Int -> Any -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Any
MVector (PrimState (ST s)) Any
v Int
i (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
emptyB :: ProdBuilder '[]
emptyB :: ProdBuilder '[]
emptyB = (forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder '[]
forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
_ MVector s Any
_ -> () -> ST s ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
buildProd :: forall xs. (KnownNat (Length xs)) => ProdBuilder xs -> Prod xs
buildProd :: ProdBuilder xs -> Prod xs
buildProd (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
bs) = Vector Any -> Prod xs
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod xs) -> Vector Any -> Prod xs
forall a b. (a -> b) -> a -> b
$ (forall s. ST s (MVector s Any)) -> Vector Any
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create do
STRef s Int
ref <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef Int
0
MVector s Any
x <- Int -> ST s (MVector (PrimState (ST s)) Any)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Length xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Length xs)
forall k (t :: k). Proxy t
Proxy @(Length xs)))
STRef s Int -> MVector s Any -> ST s ()
forall s. STRef s Int -> MVector s Any -> ST s ()
bs STRef s Int
ref MVector s Any
x
MVector s Any -> ST s (MVector s Any)
forall (f :: * -> *) a. Applicative f => a -> f a
pure MVector s Any
x
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 Index (n :: Nat) (xs :: [k]) where
Index 0 (x ': xs) = x
Index n (_ ': xs) = Index (n - 1) 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 :: Word
index = Integer -> Word
forall a. Num a => Integer -> a
fromInteger (Integer -> Word) -> Integer -> Word
forall a b. (a -> b) -> a -> b
$ Proxy (IndexIn x xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (IndexIn x xs)
forall k (t :: k). Proxy t
Proxy @(IndexIn x xs))
{-# INLINE CONLIKE index #-}
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x
(UnsafeProd Vector Any
v) = Any -> x
forall a b. a -> b
unsafeCoerce (Any -> x) -> Any -> x
forall a b. (a -> b) -> a -> b
$ Vector Any
v Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (HasIndexIn x xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @x @xs)
{-# INLINE CONLIKE extract #-}
tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)
tailN :: Prod xs -> Prod (Tail n xs)
tailN (UnsafeProd Vector Any
v) = Vector Any -> Prod (Tail n xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (Tail n xs)) -> Vector Any -> Prod (Tail n xs)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
n (Vector Any -> Int
forall a. Vector a -> Int
V.length Vector Any
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) Vector Any
v
where
n :: Int
n = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
{-# INLINE CONLIKE tailN #-}
initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)
initN :: Prod xs -> Prod (Init n xs)
initN (UnsafeProd Vector Any
v) = Vector Any -> Prod (Init n xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (Init n xs)) -> Vector Any -> Prod (Init n xs)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
0 Int
n Vector Any
v
where
n :: Int
n = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
{-# INLINE CONLIKE initN #-}
dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs
dropFirst :: Prod (x : xs) -> Prod xs
dropFirst (UnsafeProd Vector Any
v) = Vector Any -> Prod xs
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod xs) -> Vector Any -> Prod xs
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
1 (Vector Any -> Int
forall a. Vector a -> Int
V.length Vector Any
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Vector Any
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 :: Prod xs -> Prod ys -> Prod (xs <> ys)
combine (UnsafeProd Vector Any
p) (UnsafeProd Vector Any
q) = Vector Any -> Prod (xs <> ys)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any
p Vector Any -> Vector Any -> Vector Any
forall a. Vector a -> Vector a -> Vector a
V.++ Vector Any
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 :: (x -> y) -> Prod xs -> Prod (Replace x y xs)
remap x -> y
f (UnsafeProd Vector Any
v) = Vector Any -> Prod (Replace x y xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Int -> Any -> Any
update (Int -> Any -> Any) -> Vector Any -> Vector Any
forall a b. (Int -> a -> b) -> Vector a -> Vector b
`V.imap` Vector Any
v) where
update :: Int -> Any -> Any
update :: Int -> Any -> Any
update (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral -> Word
n) Any
a
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasIndexIn x xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @x @xs = y -> Any
forall a b. a -> b
unsafeCoerce (y -> Any) -> y -> Any
forall a b. (a -> b) -> a -> b
$ x -> y
f (x -> y) -> x -> y
forall a b. (a -> b) -> a -> b
$ Any -> x
forall a b. a -> b
unsafeCoerce Any
a
| Bool
otherwise = Any
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
produceB :: (forall r. Consumer xs r -> r) -> ProdBuilder xs
extend1 :: x -> Consumer xs (ProdBuilder (x ': xs))
cmap :: (r -> r') -> Consumer xs r -> Consumer xs r'
produce :: (KnownNat (Length xs), Consume xs) => (forall r. Consumer xs r -> r) -> Prod xs
produce :: (forall r. Consumer xs r -> r) -> Prod xs
produce forall r. Consumer xs r -> r
f = ProdBuilder xs -> Prod xs
forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd (ProdBuilder xs -> Prod xs) -> ProdBuilder xs -> Prod xs
forall a b. (a -> b) -> a -> b
$ (forall r. Consumer xs r -> r) -> ProdBuilder xs
forall (xs :: [*]).
Consume xs =>
(forall r. Consumer xs r -> r) -> ProdBuilder xs
produceB forall r. Consumer xs r -> r
f
empty :: Prod '[]
empty :: Prod '[]
empty = ProdBuilder '[] -> Prod '[]
forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd (ProdBuilder '[] -> Prod '[]) -> ProdBuilder '[] -> Prod '[]
forall a b. (a -> b) -> a -> b
$ (forall r. Consumer '[] r -> r) -> ProdBuilder '[]
forall (xs :: [*]).
Consume xs =>
(forall r. Consumer xs r -> r) -> ProdBuilder xs
produceB forall a. a -> a
forall r. Consumer '[] r -> r
id
instance Consume '[] where
consume :: Prod '[] -> Consumer '[] r -> r
consume = (r -> Prod '[] -> r) -> Prod '[] -> r -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> Prod '[] -> r
forall a b. a -> b -> a
const
{-# INLINE CONLIKE consume #-}
produceB :: (forall r. Consumer '[] r -> r) -> ProdBuilder '[]
produceB forall r. Consumer '[] r -> r
x = (forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder '[]
forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> () -> ST s ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE CONLIKE produceB #-}
extend1 :: x -> Consumer '[] (ProdBuilder '[x])
extend1 x
x = (forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder '[x]
forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> STRef s Int -> (Int -> ST s ()) -> ST s ()
forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref \Int
i -> MVector (PrimState (ST s)) Any -> Int -> Any -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Any
MVector (PrimState (ST s)) Any
v Int
i (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE extend1 #-}
cmap :: (r -> r') -> Consumer '[] r -> Consumer '[] r'
cmap r -> r'
f Consumer '[] r
x = r -> r'
f r
Consumer '[] r
x
{-# INLINE CONLIKE cmap #-}
withIncrement :: STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement :: STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref Int -> ST s x
f = do
Int
i <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
ref
x
x <- Int -> ST s x
f Int
i
STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
ref (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
x -> ST s x
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
x
instance Consume xs => Consume (x ': xs) where
consume :: Prod (x : xs) -> Consumer (x : xs) r -> r
consume (UnsafeProd Vector Any
v) Consumer (x : xs) r
g = Prod xs -> Consumer xs r -> r
forall (xs :: [*]) r. Consume xs => Prod xs -> Consumer xs r -> r
consume @xs (Vector Any -> Prod xs
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Vector Any
forall a. Vector a -> Vector a
V.tail Vector Any
v)) (Consumer xs r -> r) -> Consumer xs r -> r
forall a b. (a -> b) -> a -> b
$ Consumer (x : xs) r
x -> Consumer xs r
g (Any -> x
forall a b. a -> b
unsafeCoerce (Any -> x) -> Any -> x
forall a b. (a -> b) -> a -> b
$ Vector Any
v Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0)
{-# INLINE CONLIKE consume #-}
produceB :: (forall r. Consumer (x : xs) r -> r) -> ProdBuilder (x : xs)
produceB forall r. Consumer (x : xs) r -> r
g = Consumer (x : xs) (ProdBuilder (x : xs)) -> ProdBuilder (x : xs)
forall r. Consumer (x : xs) r -> r
g (forall x. Consume xs => x -> Consumer xs (ProdBuilder (x : xs))
forall (xs :: [*]) x.
Consume xs =>
x -> Consumer xs (ProdBuilder (x : xs))
extend1 @xs)
{-# INLINE CONLIKE produceB #-}
cmap :: (r -> r') -> Consumer (x : xs) r -> Consumer (x : xs) r'
cmap r -> r'
f = (Consumer xs r -> Consumer xs r')
-> (x -> Consumer xs r) -> x -> Consumer xs r'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((r -> r') -> Consumer xs r -> Consumer xs r'
forall (xs :: [*]) r r'.
Consume xs =>
(r -> r') -> Consumer xs r -> Consumer xs r'
cmap @xs r -> r'
f)
{-# INLINE CONLIKE cmap #-}
extend1 :: x -> Consumer (x : xs) (ProdBuilder (x : x : xs))
extend1 (x
x1 :: x1) x
x = (ProdBuilder (x : xs) -> ProdBuilder (x : x : xs))
-> Consumer xs (ProdBuilder (x : xs))
-> Consumer xs (ProdBuilder (x : x : xs))
forall (xs :: [*]) r r'.
Consume xs =>
(r -> r') -> Consumer xs r -> Consumer xs r'
cmap @xs @(ProdBuilder (x ': xs)) @(ProdBuilder (x1 ': x ': xs)) ProdBuilder (x : xs) -> ProdBuilder (x : x : xs)
f (x -> Consumer xs (ProdBuilder (x : xs))
forall (xs :: [*]) x.
Consume xs =>
x -> Consumer xs (ProdBuilder (x : xs))
extend1 @xs x
x) where
f :: ProdBuilder (x : xs) -> ProdBuilder (x : x : xs)
f (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
b) = (forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder (x : x : xs)
forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> (STRef s Int -> (Int -> ST s ()) -> ST s ()
forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref \Int
i -> MVector (PrimState (ST s)) Any -> Int -> Any -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Any
MVector (PrimState (ST s)) Any
v Int
i (x -> Any
forall a b. a -> b
unsafeCoerce x
x1)) ST s () -> ST s () -> ST s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> STRef s Int -> MVector s Any -> ST s ()
forall s. STRef s Int -> MVector s Any -> ST s ()
b STRef s Int
ref MVector s Any
v
{-# INLINE CONLIKE extend1 #-}
instance Eq (Prod '[]) where
Prod '[]
_ == :: Prod '[] -> Prod '[] -> Bool
== Prod '[]
_ = Bool
True
{-# INLINE CONLIKE (==) #-}
instance (Eq x, Eq (Prod xs)) => Eq (Prod (x ': xs)) where
px :: Prod (x : xs)
px@(UnsafeProd Vector Any
x) == :: Prod (x : xs) -> Prod (x : xs) -> Bool
== py :: Prod (x : xs)
py@(UnsafeProd Vector Any
y) = Any -> x
forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
x Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0) x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Any -> x
forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
y Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0) Bool -> Bool -> Bool
&& Prod (x : xs) -> Prod xs
forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
px Prod xs -> Prod xs -> Bool
forall a. Eq a => a -> a -> Bool
== Prod (x : xs) -> Prod xs
forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
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 :: Prod xs -> Prod (y : ys)
strengthen Prod xs
p = Vector Any -> Prod (y : ys)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (y : ys)) -> Vector Any -> Prod (y : ys)
forall a b. (a -> b) -> a -> b
$ Any -> Vector Any
forall a. a -> Vector a
V.singleton (Any -> Any
forall a b. a -> b
unsafeCoerce (Any -> Any) -> Any -> Any
forall a b. (a -> b) -> a -> b
$ Prod xs -> Vector Any
forall (xs :: [*]). Prod xs -> Vector Any
unProd Prod xs
p Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (HasIndexIn y xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @y @xs)) Vector Any -> Vector Any -> Vector Any
forall a. Semigroup a => a -> a -> a
<> Prod ys -> Vector Any
forall (xs :: [*]). Prod xs -> Vector Any
unProd (Prod xs -> Prod ys
forall (xs :: [*]) (ys :: [*]).
Strengthen xs ys =>
Prod xs -> Prod ys
strengthen @xs @ys Prod xs
p)
{-# INLINE CONLIKE strengthen #-}
instance Strengthen xs '[] where
strengthen :: Prod xs -> Prod '[]
strengthen = Prod '[] -> Prod xs -> Prod '[]
forall a b. a -> b -> a
const (Vector Any -> Prod '[]
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd Vector Any
forall a. Vector a
V.empty)
{-# INLINE CONLIKE strengthen #-}
type family Selector def fields a where
Selector def (field ': fields) a = Index field def -> Selector def fields a
Selector def '[] a = a
type family FieldsFromSelector def selector where
FieldsFromSelector def (a -> b) = IndexIn a def ': FieldsFromSelector def b
FieldsFromSelector def (Identity a) = '[]
class Selection def selector a where
select :: Prod def -> selector -> a
instance Selection def a a where
select :: Prod def -> a -> a
select Prod def
_prod a
s = a
s
{-# INLINE CONLIKE select #-}
instance (HasIndexIn x def, Selection def xs a) => Selection def (x -> xs) a where
select :: Prod def -> (x -> xs) -> a
select Prod def
prod x -> xs
f = Prod def -> xs -> a
forall (def :: [*]) selector a.
Selection def selector a =>
Prod def -> selector -> a
select @_ @_ @a Prod def
prod (x -> xs
f (Prod def -> x
forall x (xs :: [*]). HasIndexIn x xs => Prod xs -> x
extract @x Prod def
prod))
{-# INLINE CONLIKE select #-}
class ForAll c xs => ToList c xs where
toList :: (forall a. c a => a -> b) -> Prod xs -> [b]
instance ToList c '[] where
toList :: (forall a. c a => a -> b) -> Prod '[] -> [b]
toList forall a. c a => a -> b
_f Prod '[]
_p = []
instance (c x, ToList c xs) => ToList c (x ': xs) where
toList :: (forall a. c a => a -> b) -> Prod (x : xs) -> [b]
toList forall a. c a => a -> b
f Prod (x : xs)
p = x -> b
forall a. c a => a -> b
f x
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: (forall a. c a => a -> b) -> Prod xs -> [b]
forall (c :: * -> Constraint) (xs :: [*]) b.
ToList c xs =>
(forall a. c a => a -> b) -> Prod xs -> [b]
toList @c forall a. c a => a -> b
f (Prod (x : xs) -> Prod xs
forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
p) where
x :: x
x = Prod (x : xs) -> x
forall x (xs :: [*]). HasIndexIn x xs => Prod xs -> x
extract @x Prod (x : xs)
p