{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Topaz.Types
  ( Elem(..)
  , Rec(..)
  -- , BiRec(..)
  , NestRec(..)
  , Fix(..)
  , HFix(..)
  , Nest(..)
  , EqHetero(..)
  , TestEqualityHetero(..)
  , Nat(..)
  , SingNat(..)
  , Vector(..)
  , type (++)
  ) where

import Control.Applicative (liftA2)
import Data.Exists
import Data.Foldable (foldrM)
import Data.Hashable (Hashable(..))
import Data.Kind (Type)
import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)
import Data.Proxy (Proxy(..))
import Data.Type.Coercion
import Data.Type.Equality
import Foreign.Ptr (castPtr,plusPtr)
import Foreign.Storable (Storable(..))

import qualified Data.Aeson as AE
import qualified Data.Aeson.Types as AET
import qualified Data.Semigroup as SG
import qualified Data.Vector as V

data Nat = Succ Nat | Zero

data SingNat :: Nat -> Type where
  SingZero :: SingNat 'Zero
  SingSucc :: SingNat n -> SingNat ('Succ n)

type instance Sing = SingNat

data Vector :: Nat -> Type -> Type where
  VectorNil :: Vector 'Zero a
  VectorCons :: a -> Vector n a -> Vector ('Succ n) a

instance Eq a => Eq (Vector n a) where
  Vector n a
VectorNil == :: Vector n a -> Vector n a -> Bool
== Vector n a
VectorNil = Bool
True
  VectorCons a
a Vector n a
as == VectorCons a
b Vector n a
bs = a
a forall a. Eq a => a -> a -> Bool
== a
b Bool -> Bool -> Bool
&& Vector n a
as forall a. Eq a => a -> a -> Bool
== Vector n a
bs

data Elem (rs :: [k]) (r :: k) where
  ElemHere :: Elem (r ': rs) r
  ElemThere :: Elem rs r -> Elem (s ': rs) r

type family (as :: [k]) ++ (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)
infixr 5 ++

data Rec :: forall (k :: Type). (k -> Type) -> [k] -> Type where
  RecNil :: Rec f '[]
  RecCons :: f r -> Rec f rs -> Rec f (r ': rs)

-- data BiRec :: (k -> Type) -> (j -> Type) -> [k] -> [j] -> Type where
--   BiRec :: Rec f ks -> Rec g js -> BiRec f g ks js

data NestRec :: forall (k :: Type). (k -> Type) -> Nest k -> Type where
  NestRec :: Rec f rs -> Rec (NestRec f) ns -> NestRec f ('Nest ns rs)

data Nest a = Nest [Nest a] [a]
newtype Fix f = Fix (f (Fix f))
newtype HFix h a = HFix (h (HFix h) a)

instance Semigroup1 f => Semigroup (Fix f) where
  Fix f (Fix f)
a <> :: Fix f -> Fix f -> Fix f
<> Fix f (Fix f)
b = forall (f :: * -> *). f (Fix f) -> Fix f
Fix (forall (f :: * -> *) a.
(Semigroup1 f, Semigroup a) =>
f a -> f a -> f a
append1 f (Fix f)
a f (Fix f)
b)

instance Monoid1 f => Monoid (Fix f) where
  mempty :: Fix f
mempty = forall (f :: * -> *). f (Fix f) -> Fix f
Fix (forall (f :: * -> *) a. Monoid1 f => a -> f a
liftEmpty forall a. Monoid a => a
mempty)
  mappend :: Fix f -> Fix f -> Fix f
mappend = forall a. Semigroup a => a -> a -> a
(SG.<>)

-- Think of a better name for this typeclass
class EqHetero h where
  eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool

instance EqHetero h => EqForall (HFix h) where
  eqForall :: forall (a :: k). HFix h a -> HFix h a -> Bool
eqForall (HFix h (HFix h) a
a) (HFix h (HFix h) a
b) = forall {k} {k} (h :: (k -> *) -> k -> *) (f :: k -> *) (a :: k).
EqHetero h =>
(forall (x :: k). f x -> f x -> Bool) -> h f a -> h f a -> Bool
eqHetero forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall h (HFix h) a
a h (HFix h) a
b 

instance EqHetero h => Eq (HFix h a) where
  == :: HFix h a -> HFix h a -> Bool
(==) = forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall

class TestEqualityHetero h where
  testEqualityHetero :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b)

instance TestEqualityHetero h => TestEquality (HFix h) where
  testEquality :: forall (a :: k) (b :: k). HFix h a -> HFix h b -> Maybe (a :~: b)
testEquality (HFix h (HFix h) a
a) (HFix h (HFix h) b
b) = forall {k} {k} (h :: (k -> *) -> k -> *) (f :: k -> *) (a :: k)
       (b :: k).
TestEqualityHetero h =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> h f a -> h f b -> Maybe (a :~: b)
testEqualityHetero forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality h (HFix h) a
a h (HFix h) b
b

instance TestEquality f => TestEquality (Rec f) where
  testEquality :: forall (a :: [k]) (b :: [k]). Rec f a -> Rec f b -> Maybe (a :~: b)
testEquality Rec f a
RecNil Rec f b
RecNil = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality (RecCons f r
x Rec f rs
xs) (RecCons f r
y Rec f rs
ys) = do
    r :~: r
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f r
x f r
y
    rs :~: rs
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec f rs
xs Rec f rs
ys
    forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Rec f a
_ Rec f b
_ = forall a. Maybe a
Nothing

instance TestCoercion f => TestCoercion (Rec f) where
  testCoercion :: forall (a :: [k]) (b :: [k]).
Rec f a -> Rec f b -> Maybe (Coercion a b)
testCoercion Rec f a
RecNil Rec f b
RecNil = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion (RecCons f r
x Rec f rs
xs) (RecCons f r
y Rec f rs
ys) = do
    Coercion r r
Coercion <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestCoercion f =>
f a -> f b -> Maybe (Coercion a b)
testCoercion f r
x f r
y
    Coercion rs rs
Coercion <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestCoercion f =>
f a -> f b -> Maybe (Coercion a b)
testCoercion Rec f rs
xs Rec f rs
ys
    forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion Rec f a
_ Rec f b
_ = forall a. Maybe a
Nothing

instance HashableForall f => HashableForall (Rec f) where
  hashWithSaltForall :: forall (a :: [k]). Int -> Rec f a -> Int
hashWithSaltForall Int
s0 = forall (a :: [k]). Int -> Rec f a -> Int
go Int
s0 where
    go :: Int -> Rec f rs -> Int
    go :: forall (a :: [k]). Int -> Rec f a -> Int
go !Int
s Rec f rs
x = case Rec f rs
x of
      Rec f rs
RecNil -> Int
s
      RecCons f r
b Rec f rs
bs -> forall (a :: [k]). Int -> Rec f a -> Int
go (forall {k} (f :: k -> *) (a :: k).
HashableForall f =>
Int -> f a -> Int
hashWithSaltForall Int
s f r
b) Rec f rs
bs

instance (EqForall f, HashableForall f) => Hashable (Rec f as) where
  hashWithSalt :: Int -> Rec f as -> Int
hashWithSalt = forall {k} (f :: k -> *) (a :: k).
HashableForall f =>
Int -> f a -> Int
hashWithSaltForall

instance ShowForall f => ShowForall (Rec f) where
  showsPrecForall :: forall (a :: [k]). Int -> Rec f a -> ShowS
showsPrecForall Int
p Rec f a
x = case Rec f a
x of
    RecCons f r
v Rec f rs
vs -> Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
      forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"RecCons "
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f r
v
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 Rec f rs
vs
    Rec f a
RecNil -> String -> ShowS
showString String
"RecNil"

instance ShowForall f => Show (Rec f as) where
  showsPrec :: Int -> Rec f as -> ShowS
showsPrec = forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall

instance ShowForeach f => ShowForeach (Rec f) where
  showsPrecForeach :: forall (a :: [k]). Sing a -> Int -> Rec f a -> ShowS
showsPrecForeach Sing a
SingList a
SingListNil Int
_ Rec f a
RecNil = String -> ShowS
showString String
"RecNil"
  showsPrecForeach (SingListCons Sing r
s SingList rs
ss) Int
p (RecCons f r
v Rec f rs
vs) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"RecCons "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing r
s Int
11 f r
v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach SingList rs
ss Int
11 Rec f rs
vs

instance EqForall f => Eq (Rec f as) where
  == :: Rec f as -> Rec f as -> Bool
(==) = forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall

instance EqForall f => EqForall (Rec f) where
  eqForall :: forall (a :: [k]). Rec f a -> Rec f a -> Bool
eqForall Rec f a
RecNil Rec f a
RecNil = Bool
True
  eqForall (RecCons f r
a Rec f rs
as) (RecCons f r
b Rec f rs
bs) =
    forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f r
a f r
b Bool -> Bool -> Bool
&& forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall Rec f rs
as Rec f rs
bs

instance EqForeach f => EqForeach (Rec f) where
  eqForeach :: forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Bool
eqForeach Sing a
SingList a
SingListNil Rec f a
RecNil Rec f a
RecNil = Bool
True
  eqForeach (SingListCons Sing r
s SingList rs
ss) (RecCons f r
a Rec f rs
as) (RecCons f r
b Rec f rs
bs) =
    forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing r
s f r
a f r
b Bool -> Bool -> Bool
&& forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach SingList rs
ss Rec f rs
as Rec f rs
bs

instance EqForallPoly f => EqForallPoly (Rec f) where
  eqForallPoly :: forall (a :: [k]) (b :: [k]).
Rec f a -> Rec f b -> WitnessedEquality a b
eqForallPoly Rec f a
RecNil Rec f b
RecNil = forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
  eqForallPoly Rec f a
RecNil (RecCons f r
_ Rec f rs
_) = forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  eqForallPoly (RecCons f r
_ Rec f rs
_) Rec f b
RecNil = forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  eqForallPoly (RecCons f r
x Rec f rs
xs) (RecCons f r
y Rec f rs
ys) = case forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly f r
x f r
y of
    WitnessedEquality r r
WitnessedEqualityUnequal -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
    WitnessedEquality r r
WitnessedEqualityEqual -> case forall {k} (f :: k -> *) (a :: k) (b :: k).
EqForallPoly f =>
f a -> f b -> WitnessedEquality a b
eqForallPoly Rec f rs
xs Rec f rs
ys of
      WitnessedEquality rs rs
WitnessedEqualityUnequal -> forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
      WitnessedEquality rs rs
WitnessedEqualityEqual -> forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual

instance OrdForall f => Ord (Rec f as) where
  compare :: Rec f as -> Rec f as -> Ordering
compare = forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall

instance OrdForall f => OrdForall (Rec f) where
  compareForall :: forall (a :: [k]). Rec f a -> Rec f a -> Ordering
compareForall Rec f a
RecNil Rec f a
RecNil = Ordering
EQ
  compareForall (RecCons f r
a Rec f rs
as) (RecCons f r
b Rec f rs
bs) =
    forall a. Monoid a => a -> a -> a
mappend (forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f r
a f r
b) (forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall Rec f rs
as Rec f rs
bs)

instance OrdForeach f => OrdForeach (Rec f) where
  compareForeach :: forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Ordering
compareForeach Sing a
SingList a
SingListNil Rec f a
RecNil Rec f a
RecNil = Ordering
EQ
  compareForeach (SingListCons Sing r
s SingList rs
ss) (RecCons f r
a Rec f rs
as) (RecCons f r
b Rec f rs
bs) =
    forall a. Monoid a => a -> a -> a
mappend (forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing r
s f r
a f r
b) (forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach SingList rs
ss Rec f rs
as Rec f rs
bs)


instance SemigroupForall f => Semigroup (Rec f as) where
  <> :: Rec f as -> Rec f as -> Rec f as
(<>) = forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
recZipWith forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall

instance SemigroupForeach f => SemigroupForeach (Rec f) where
  appendForeach :: forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Rec f a
appendForeach Sing a
SingList a
SingListNil Rec f a
RecNil Rec f a
RecNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
  appendForeach (SingListCons Sing r
s SingList rs
ss) (RecCons f r
x Rec f rs
xs) (RecCons f r
y Rec f rs
ys) =
    forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach Sing r
s f r
x f r
y) (forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach SingList rs
ss Rec f rs
xs Rec f rs
ys)

instance MonoidForeach f => MonoidForeach (Rec f) where
  emptyForeach :: forall (a :: [k]). Sing a -> Rec f a
emptyForeach Sing a
SingList a
SingListNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
  emptyForeach (SingListCons Sing r
s SingList rs
ss) = forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach Sing r
s) (forall {k} (f :: k -> *) (a :: k). MonoidForeach f => Sing a -> f a
emptyForeach SingList rs
ss)

instance SemigroupForall f => SemigroupForall (Rec f) where
  appendForall :: forall (a :: [k]). Rec f a -> Rec f a -> Rec f a
appendForall = forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
recZipWith forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall

instance ToJSONForall f => AE.ToJSON (Rec f as) where
  toJSON :: Rec f as -> Value
toJSON = forall {k} (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall

instance ToJSONForall f => ToJSONForall (Rec f) where
  toJSONForall :: forall (a :: [k]). Rec f a -> Value
toJSONForall = forall a. ToJSON a => a -> Value
AE.toJSON forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (g :: k -> *) (xs :: [k]).
ToJSONForall g =>
Rec g xs -> [Value]
go
    where
    go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]
    go :: forall {k} (g :: k -> *) (xs :: [k]).
ToJSONForall g =>
Rec g xs -> [Value]
go Rec g xs
RecNil = []
    go (RecCons g r
x Rec g rs
xs) = forall {k} (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall g r
x forall a. a -> [a] -> [a]
: forall {k} (g :: k -> *) (xs :: [k]).
ToJSONForall g =>
Rec g xs -> [Value]
go Rec g rs
xs

instance (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where
  parseJSON :: Value -> Parser (Rec f as)
parseJSON = forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach forall {k} (a :: k). Reify a => Sing a
reify

instance FromJSONForeach f => FromJSONForeach (Rec f) where
  parseJSONForeach :: forall (a :: [k]). Sing a -> Value -> Parser (Rec f a)
parseJSONForeach Sing a
s0 = forall a. String -> (Array -> Parser a) -> Value -> Parser a
AE.withArray String
"Rec" forall a b. (a -> b) -> a -> b
$ \Array
vs -> do
    let go :: SingList as -> Int -> AET.Parser (Rec f as)
        go :: forall (as :: [k]). SingList as -> Int -> Parser (Rec f as)
go SingList as
SingListNil !Int
ix = if forall a. Vector a -> Int
V.length Array
vs forall a. Eq a => a -> a -> Bool
== Int
ix
          then forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (f :: k -> *). Rec f '[]
RecNil
          else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"too many elements in array"
        go (SingListCons Sing r
s SingList rs
ss) !Int
ix = if Int
ix forall a. Ord a => a -> a -> Bool
< forall a. Vector a -> Int
V.length Array
vs
          then do
            f r
r <- forall {k} (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing r
s (Array
vs forall a. Vector a -> Int -> a
V.! Int
ix)
            Rec f rs
rs <- forall (as :: [k]). SingList as -> Int -> Parser (Rec f as)
go SingList rs
ss (Int
ix forall a. Num a => a -> a -> a
+ Int
1)
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
r Rec f rs
rs)
          else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not enough elements in array"
    forall (as :: [k]). SingList as -> Int -> Parser (Rec f as)
go Sing a
s0 Int
0

instance StorableForeach f => StorableForeach (Rec f) where
  sizeOfForeach :: forall (a :: [k]). Proxy (Rec f) -> Sing a -> Int
sizeOfForeach Proxy (Rec f)
_ Sing a
SingList a
SingListNil = Int
0
  sizeOfForeach Proxy (Rec f)
_ (SingListCons Sing r
s SingList rs
ss) =
    forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Sing r
s forall a. Num a => a -> a -> a
+ forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (forall {k} (t :: k). Proxy t
Proxy :: Proxy (Rec f)) SingList rs
ss
  peekForeach :: forall (a :: [k]). Sing a -> Ptr (Rec f a) -> IO (Rec f a)
peekForeach Sing a
SingList a
SingListNil Ptr (Rec f a)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (f :: k -> *). Rec f '[]
RecNil
  peekForeach (SingListCons Sing r
s SingList rs
ss) Ptr (Rec f a)
ptr = do
    f r
r <- forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach Sing r
s (forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f a)
ptr)
    Rec f rs
rs <- forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach SingList rs
ss (forall a b. Ptr a -> Int -> Ptr b
plusPtr Ptr (Rec f a)
ptr (forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Sing r
s))
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
r Rec f rs
rs)
  pokeForeach :: forall (a :: [k]). Sing a -> Ptr (Rec f a) -> Rec f a -> IO ()
pokeForeach Sing a
_ Ptr (Rec f a)
_ Rec f a
RecNil = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  pokeForeach (SingListCons Sing r
s SingList rs
ss) Ptr (Rec f a)
ptr (RecCons f r
r Rec f rs
rs) = do
    forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach Sing r
s (forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f a)
ptr) f r
r
    forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach SingList rs
ss (forall a b. Ptr a -> Int -> Ptr b
plusPtr Ptr (Rec f a)
ptr (forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Sing r
s)) Rec f rs
rs

instance (StorableForeach f, Reify as) => Storable (Rec f as) where
  sizeOf :: Rec f as -> Int
sizeOf Rec f as
_ = forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (forall {k} (t :: k). Proxy t
Proxy :: Proxy (Rec f)) (forall {k} (a :: k). Reify a => Sing a
reify :: SingList as)
  alignment :: Rec f as -> Int
alignment Rec f as
_ = forall a. Storable a => a -> Int
sizeOf (forall a. HasCallStack => a
undefined :: Rec f as)
  poke :: Ptr (Rec f as) -> Rec f as -> IO ()
poke = forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach (forall {k} (a :: k). Reify a => Sing a
reify :: SingList as)
  peek :: Ptr (Rec f as) -> IO (Rec f as)
peek = forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach (forall {k} (a :: k). Reify a => Sing a
reify :: SingList as)

instance BinaryForeach f => BinaryForeach (Rec f) where
  putForeach :: forall (a :: [k]). Sing a -> Rec f a -> Put
putForeach Sing a
SingList a
SingListNil Rec f a
RecNil = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  putForeach (SingListCons Sing r
s SingList rs
ss) (RecCons f r
r Rec f rs
rs) = do
    forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> f a -> Put
putForeach Sing r
s f r
r
    forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> f a -> Put
putForeach SingList rs
ss Rec f rs
rs
  getForeach :: forall (a :: [k]). Sing a -> Get (Rec f a)
getForeach Sing a
SingList a
SingListNil = forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (f :: k -> *). Rec f '[]
RecNil
  getForeach (SingListCons Sing r
s SingList rs
ss) =
    forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> Get (f a)
getForeach Sing r
s) (forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> Get (f a)
getForeach SingList rs
ss)

instance FromJSONExists f => FromJSONExists (Rec f) where
  parseJSONExists :: Value -> Parser (Exists (Rec f))
parseJSONExists = forall a. String -> (Array -> Parser a) -> Value -> Parser a
AE.withArray String
"Rec" forall a b. (a -> b) -> a -> b
$ \Array
vs -> 
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM forall {k} (g :: k -> *).
FromJSONExists g =>
Value -> Exists (Rec g) -> Parser (Exists (Rec g))
go (forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists forall {k} (f :: k -> *). Rec f '[]
RecNil) Array
vs
    where
    go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))
    go :: forall {k} (g :: k -> *).
FromJSONExists g =>
Value -> Exists (Rec g) -> Parser (Exists (Rec g))
go Value
v (Exists Rec g a
rs) = do
      Exists g a
r <- forall {k} (f :: k -> *).
FromJSONExists f =>
Value -> Parser (Exists f)
parseJSONExists Value
v :: AET.Parser (Exists g)
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons g a
r Rec g a
rs))

recZipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
recZipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
recZipWith forall (x :: k). f x -> g x -> h x
_ Rec f rs
RecNil Rec g rs
RecNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
recZipWith forall (x :: k). f x -> g x -> h x
f (RecCons f r
a Rec f rs
as) (RecCons g r
b Rec g rs
bs) =
  forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall (x :: k). f x -> g x -> h x
f f r
a g r
b) (forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
recZipWith forall (x :: k). f x -> g x -> h x
f Rec f rs
as Rec g rs
bs)