{-# 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
Copyright: (c) Samuel Schlesinger 2020
License: MIT
Maintainer: sgschlesinger@gmail.com
Stability: experimental
Portability: non-portable
Description: Extensible products
-}
module Data.Prodder
  ( -- * The extensible product type
    Prod
    -- * Construction and deconstruction
  , extract
  , index
  , tailN
  , initN
  , dropFirst
  , Consume(consume, extend1, cmap, produceB)
  , produce
  , empty
  , ToList(toList)
  , type ForAll
    -- ** Efficient Iterative Construction
  , buildProd
  , ProdBuilder
  , consB
  , emptyB
    -- * Type families
  , Index
  , IndexIn
  , HasIndexIn
  , Consumer
  , type (<>)
  , Length
  , Tail
  , Init
  , Replace
    -- * Rearranging and removing elements
  , Strengthen(strengthen)
    -- * Transforming extensible products
  , remap
    -- * Picking out individual components of a product
  , Selection(select)
  , type FieldsFromSelector
  , type Selector
    -- * Efficiently building 'Prod's
  ) 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)

-- | An extensible product type
newtype Prod (xs :: [*]) = UnsafeProd { Prod xs -> Vector Any
unProd :: Vector Any }

-- | A type for constructing products with linear memory use.
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 () }

-- | Cons an element onto the head of a 'ProdBuilder'.
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)

-- | Empty 'ProdBuilder'.
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 ()

-- | Execute a 'ProdBuilder', pulling out a 'Prod'.
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

-- | A type family for computing the index of a type in a list of types.
type family IndexIn (x :: k) (xs :: [k]) where
  IndexIn x (x ': xs) = 0
  IndexIn x (y ': xs) = 1 + IndexIn x xs

-- | A type family for indexing into lists of types.
type family Index (n :: Nat) (xs :: [k]) where
  Index 0 (x ': xs) = x
  Index n (_ ': xs) = Index (n - 1) xs

-- | A type family for computing the length of a type level list
type family Length (xs :: [k]) where
  Length '[] = 0
  Length (x ': xs) = 1 + Length xs

-- | A type family for computing the tail of a type level list
type family Tail n xs where
  Tail 0 xs = xs
  Tail n (x ': xs) = Tail (n - 1) xs

-- | A type family for computing the initial segment of a type level list
type family Init n xs where
  Init 0 xs = '[]
  Init n (x ': xs) = x ': Init (n - 1) xs

-- | A class that is used for convenience in order to make certain type
-- signatures read more clearly.
class KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs
instance KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs

-- | Computes the index of the given type in the given type level list.
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 a value at a particular index
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x
extract :: Prod xs -> x
extract (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 #-}

-- | Takes the tail of a product after the nth element.
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 #-}

-- | Takes the initial length n segment of a product.
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 #-}

-- | Drop the first element of a product. Sometimes needed for better type
-- inference and less piping around of constraints.
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 for replacing one type in a type level list with another
type family Replace x y xs where
  Replace x y (x ': xs) = y ': xs
  Replace x y (z ': xs) = z ': Replace x y xs

-- | Replaces one type with another via a function
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 #-}

-- | This is a reified pattern match on an extensible product
type family Consumer xs r where
  Consumer '[] r = r
  Consumer (x ': xs) r = x -> Consumer xs r

-- | A typeclass that is useful to define the scott encoding/decoding for
-- extensible products.
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
    
      
     
  -- 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
  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 (==) #-}

-- | A typeclass to rearrange and possibly remove things from a product.
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 #-}

-- | A typeclass for creating a selection function which is valid on the given definition.
type family Selector def fields a where
  Selector def (field ': fields) a = Index field def -> Selector def fields a
  Selector def '[] a = a

-- | Extracts the fields intended from the given selector type.
type family FieldsFromSelector def selector where
  FieldsFromSelector def (a -> b) = IndexIn a def ': FieldsFromSelector def b
  FieldsFromSelector def (Identity a) = '[]

-- | A class for constructing the select function inductively.
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 #-}

-- | A class for turning a 'Prod' into a regular list using a
-- function which takes an argument only constrained by a 'Constraint'
-- each element of the product has.
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