{-# 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
, FoldProd(foldProd)
, toList
, type ForAll
, atType
, buildProd
, ProdBuilder
, consB
, emptyB
, appendB
, Index
, IndexIn
, HasIndexIn
, Consumer
, type (<>)
, Length
, Tail
, Init
, Replace
, Strengthen(strengthenP)
, 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.Functor.Const (Const (..))
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)
import Data.Typeable (Typeable)
import Data.Monoid (Endo (Endo, appEndo))
import Data.List (intersperse)
import Data.Foldable (fold)
newtype Prod (xs :: [*]) = UnsafeProd { forall (xs :: [*]). Prod xs -> Vector Any
unProd :: Vector Any }
deriving (Typeable)
instance FoldProd Show xs => Show (Prod xs) where
showsPrec :: Int -> Prod xs -> ShowS
showsPrec Int
d Prod xs
xs = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Endo a -> a -> a
appEndo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$
[forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ \String
r -> String
"[" forall a. Semigroup a => a -> a -> a
<> String
r] forall a. Semigroup a => a -> a -> a
<> forall a. a -> [a] -> [a]
intersperse (forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ \String
r -> String
", " forall a. Semigroup a => a -> a -> a
<> String
r) (forall (c :: * -> Constraint) (xs :: [*]) a.
FoldProd c xs =>
(forall x. c x => x -> a) -> Prod xs -> [a]
toList @Show (forall a. (a -> a) -> Endo a
Endo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec (Int
d forall a. Num a => a -> a -> a
+ Int
1)) Prod xs
xs) forall a. Semigroup a => a -> a -> a
<> [forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ \String
r -> String
"]" forall a. Semigroup a => a -> a -> a
<> String
r]
atType :: forall a b xs f. (a `HasIndexIn` xs, Functor f) => (a -> f b) -> Prod xs -> f (Prod (Replace a b xs))
atType :: forall a b (xs :: [*]) (f :: * -> *).
(HasIndexIn a xs, Functor f) =>
(a -> f b) -> Prod xs -> f (Prod (Replace a b xs))
atType a -> f b
f (UnsafeProd Vector Any
v) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
b -> forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd forall a b. (a -> b) -> a -> b
$ Vector Any
v forall a. Vector a -> [(Int, a)] -> Vector a
V.// [(forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
i, forall a b. a -> b
unsafeCoerce b
b)]) (a -> f b
f (forall a b. a -> b
unsafeCoerce (Vector Any
v forall a. Vector a -> Int -> a
V.! forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
i))) where
i :: Word
i = forall {k} (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @a @xs
{-# INLINE CONLIKE atType #-}
newtype ProdBuilder (xs :: [*]) = UnsafeProdBuilder { forall (xs :: [*]).
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 :: forall x (xs :: [*]). x -> ProdBuilder xs -> ProdBuilder (x : xs)
consB x
x (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
b) = forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref \Int
i -> do
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Any
v Int
i (forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE consB #-}
emptyB :: ProdBuilder '[]
emptyB :: ProdBuilder '[]
emptyB = forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
_ MVector s Any
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE CONLIKE emptyB #-}
buildProd :: forall xs. (KnownNat (Length xs)) => ProdBuilder xs -> Prod xs
buildProd :: forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
bs) = forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd forall a b. (a -> b) -> a -> b
$ forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create do
STRef s Int
ref <- forall a s. a -> ST s (STRef s a)
newSTRef Int
0
MVector s Any
x <- forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @(Length xs)))
forall s. STRef s Int -> MVector s Any -> ST s ()
bs STRef s Int
ref MVector s Any
x
forall (f :: * -> *) a. Applicative f => a -> f a
pure MVector s Any
x
{-# INLINE CONLIKE buildProd #-}
appendB :: ProdBuilder xs -> ProdBuilder ys -> ProdBuilder (xs <> ys)
appendB :: forall (xs :: [*]) (ys :: [*]).
ProdBuilder xs -> ProdBuilder ys -> ProdBuilder (xs <> ys)
appendB (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
b) (UnsafeProdBuilder forall s. STRef s Int -> MVector s Any -> ST s ()
b') = forall (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> do
forall s. STRef s Int -> MVector s Any -> ST s ()
b STRef s Int
ref MVector s Any
v
forall s. STRef s Int -> MVector s Any -> ST s ()
b' STRef s Int
ref MVector s Any
v
{-# INLINE CONLIKE appendB #-}
singletonB :: x -> ProdBuilder '[x]
singletonB :: forall x. x -> ProdBuilder '[x]
singletonB x
x = forall x (xs :: [*]). x -> ProdBuilder xs -> ProdBuilder (x : xs)
consB x
x ProdBuilder '[]
emptyB
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 :: forall {k} (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @(IndexIn x xs))
{-# INLINE CONLIKE index #-}
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x
= forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b (xs :: [*]) (f :: * -> *).
(HasIndexIn a xs, Functor f) =>
(a -> f b) -> Prod xs -> f (Prod (Replace a b xs))
atType @x @() @xs forall {k} a (b :: k). a -> Const a b
Const
{-# INLINE CONLIKE extract #-}
tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)
tailN :: forall (n :: Nat) (xs :: [*]).
(KnownNat n, n <= Length xs) =>
Prod xs -> Prod (Tail n xs)
tailN (UnsafeProd Vector Any
v) = forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
n (forall a. Vector a -> Int
V.length Vector Any
v forall a. Num a => a -> a -> a
- Int
n) Vector Any
v
where
n :: Int
n = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (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 :: forall (n :: Nat) (xs :: [*]).
(KnownNat n, n <= Length xs) =>
Prod xs -> Prod (Init n xs)
initN (UnsafeProd Vector Any
v) = forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
0 Int
n Vector Any
v
where
n :: Int
n = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
{-# INLINE CONLIKE initN #-}
dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs
dropFirst :: forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst (UnsafeProd Vector Any
v) = forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
1 (forall a. Vector a -> Int
V.length Vector Any
v forall a. Num a => a -> a -> a
- Int
1) Vector Any
v
{-# INLINE CONLIKE dropFirst #-}
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 :: forall (xs :: [*]) (ys :: [*]).
Prod xs -> Prod ys -> Prod (xs <> ys)
combine (UnsafeProd Vector Any
p) (UnsafeProd Vector Any
q) = forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any
p 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
Replace x y '[] = '[]
remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)
remap :: forall x y (xs :: [*]).
HasIndexIn x xs =>
(x -> y) -> Prod xs -> Prod (Replace x y xs)
remap x -> y
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b (xs :: [*]) (f :: * -> *).
(HasIndexIn a xs, Functor f) =>
(a -> f b) -> Prod xs -> f (Prod (Replace a b xs))
atType @x @y @xs (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> y
f)
{-# 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 (xs :: [*]).
(KnownNat (Length xs), Consume xs) =>
(forall r. Consumer xs r -> r) -> Prod xs
produce forall r. Consumer xs r -> r
f = forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]).
Consume xs =>
(forall r. Consumer xs r -> r) -> ProdBuilder xs
produceB forall r. Consumer xs r -> r
f
{-# INLINE CONLIKE produce #-}
empty :: Prod '[]
empty :: Prod '[]
empty = forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd forall a b. (a -> b) -> a -> b
$ forall (xs :: [*]).
Consume xs =>
(forall r. Consumer xs r -> r) -> ProdBuilder xs
produceB forall a. a -> a
id
{-# INLINE CONLIKE empty #-}
instance Consume '[] where
consume :: forall r. Prod '[] -> Consumer '[] r -> r
consume = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. a -> b -> a
const
{-# INLINE CONLIKE consume #-}
produceB :: (forall r. Consumer '[] r -> r) -> ProdBuilder '[]
produceB forall r. Consumer '[] r -> r
x = ProdBuilder '[]
emptyB
{-# INLINE CONLIKE produceB #-}
extend1 :: forall x. x -> Consumer '[] (ProdBuilder '[x])
extend1 x
x = forall x (xs :: [*]). x -> ProdBuilder xs -> ProdBuilder (x : xs)
consB x
x ProdBuilder '[]
emptyB
{-# INLINE CONLIKE extend1 #-}
cmap :: forall r r'. (r -> r') -> Consumer '[] r -> Consumer '[] r'
cmap r -> r'
f Consumer '[] r
x = r -> r'
f Consumer '[] r
x
{-# INLINE CONLIKE cmap #-}
withIncrement :: STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement :: forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref Int -> ST s x
f = do
Int
i <- forall s a. STRef s a -> ST s a
readSTRef STRef s Int
ref
x
x <- Int -> ST s x
f Int
i
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
ref (Int
i forall a. Num a => a -> a -> a
+ Int
1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
x
{-# INLINE CONLIKE withIncrement #-}
instance Consume xs => Consume (x ': xs) where
consume :: forall r. Prod (x : xs) -> Consumer (x : xs) r -> r
consume (UnsafeProd Vector Any
v) Consumer (x : xs) r
g = forall (xs :: [*]) r. Consume xs => Prod xs -> Consumer xs r -> r
consume @xs (forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (forall a. Vector a -> Vector a
V.tail Vector Any
v)) forall a b. (a -> b) -> a -> b
$ Consumer (x : xs) r
g (forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ Vector Any
v 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 = forall r. Consumer (x : xs) r -> r
g (forall (xs :: [*]) x.
Consume xs =>
x -> Consumer xs (ProdBuilder (x : xs))
extend1 @xs)
{-# INLINE CONLIKE produceB #-}
cmap :: forall r r'.
(r -> r') -> Consumer (x : xs) r -> Consumer (x : xs) r'
cmap r -> r'
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (xs :: [*]) r r'.
Consume xs =>
(r -> r') -> Consumer xs r -> Consumer xs r'
cmap @xs r -> r'
f)
{-# INLINE CONLIKE cmap #-}
extend1 :: forall x. x -> Consumer (x : xs) (ProdBuilder (x : x : xs))
extend1 (x
x1 :: x1) x
x = 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 (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 (xs :: [*]).
(forall s. STRef s Int -> MVector s Any -> ST s ())
-> ProdBuilder xs
UnsafeProdBuilder \STRef s Int
ref MVector s Any
v -> (forall s x. STRef s Int -> (Int -> ST s x) -> ST s x
withIncrement STRef s Int
ref \Int
i -> forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Any
v Int
i (forall a b. a -> b
unsafeCoerce x
x1)) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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) = forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
x forall a. Vector a -> Int -> a
V.! Int
0) forall a. Eq a => a -> a -> Bool
== forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
y forall a. Vector a -> Int -> a
V.! Int
0) Bool -> Bool -> Bool
&& forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
px forall a. Eq a => a -> a -> Bool
== forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
py
{-# INLINE CONLIKE (==) #-}
class Strengthen xs ys where
strengthenP :: Prod xs -> ProdBuilder ys
strengthen :: (KnownNat (Length ys), Strengthen xs ys) => Prod xs -> Prod ys
strengthen :: forall (ys :: [*]) (xs :: [*]).
(KnownNat (Length ys), Strengthen xs ys) =>
Prod xs -> Prod ys
strengthen = forall (xs :: [*]).
KnownNat (Length xs) =>
ProdBuilder xs -> Prod xs
buildProd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [*]) (ys :: [*]).
Strengthen xs ys =>
Prod xs -> ProdBuilder ys
strengthenP
{-# INLINE CONLIKE strengthen #-}
instance (Strengthen xs ys, y `HasIndexIn` xs) => Strengthen xs (y ': ys) where
strengthenP :: Prod xs -> ProdBuilder (y : ys)
strengthenP Prod xs
p = forall x (xs :: [*]). x -> ProdBuilder xs -> ProdBuilder (x : xs)
consB (forall x (xs :: [*]). HasIndexIn x xs => Prod xs -> x
extract @y Prod xs
p) (forall (xs :: [*]) (ys :: [*]).
Strengthen xs ys =>
Prod xs -> ProdBuilder ys
strengthenP Prod xs
p)
{-# INLINE CONLIKE strengthenP #-}
instance Strengthen xs '[] where
strengthenP :: Prod xs -> ProdBuilder '[]
strengthenP Prod xs
p = ProdBuilder '[]
emptyB
{-# INLINE CONLIKE strengthenP #-}
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 = forall (def :: [*]) selector a.
Selection def selector a =>
Prod def -> selector -> a
select @_ @_ @a Prod def
prod (x -> xs
f (forall x (xs :: [*]). HasIndexIn x xs => Prod xs -> x
extract @x Prod def
prod))
{-# INLINE CONLIKE select #-}
class ForAll c xs => FoldProd c xs where
foldProd :: Monoid m => (forall a. c a => a -> m) -> Prod xs -> m
instance FoldProd c '[] where
foldProd :: forall m. Monoid m => (forall a. c a => a -> m) -> Prod '[] -> m
foldProd forall a. c a => a -> m
_f Prod '[]
_p = forall a. Monoid a => a
mempty
{-# INLINE CONLIKE foldProd #-}
instance (c x, FoldProd c xs) => FoldProd c (x ': xs) where
foldProd :: forall m.
Monoid m =>
(forall a. c a => a -> m) -> Prod (x : xs) -> m
foldProd forall a. c a => a -> m
f Prod (x : xs)
p = forall a. c a => a -> m
f x
x forall a. Semigroup a => a -> a -> a
<> forall (c :: * -> Constraint) (xs :: [*]) m.
(FoldProd c xs, Monoid m) =>
(forall a. c a => a -> m) -> Prod xs -> m
foldProd @c forall a. c a => a -> m
f (forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
p) where
x :: x
x = forall x (xs :: [*]). HasIndexIn x xs => Prod xs -> x
extract @x Prod (x : xs)
p
{-# INLINE CONLIKE foldProd #-}
toList :: forall c xs a. FoldProd c xs => (forall x. c x => x -> a) -> Prod xs -> [a]
toList :: forall (c :: * -> Constraint) (xs :: [*]) a.
FoldProd c xs =>
(forall x. c x => x -> a) -> Prod xs -> [a]
toList forall x. c x => x -> a
f = forall (c :: * -> Constraint) (xs :: [*]) m.
(FoldProd c xs, Monoid m) =>
(forall a. c a => a -> m) -> Prod xs -> m
foldProd @c (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. c x => x -> a
f)
{-# INLINE CONLIKE toList #-}