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

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.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.Semigroup as SG

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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b Bool -> Bool -> Bool
&& Vector n a
as Vector n a -> Vector n a -> Bool
forall a. Eq a => a -> a -> Bool
== Vector n a
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 = f (Fix f) -> Fix f
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (f (Fix f) -> f (Fix f) -> f (Fix f)
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 = f (Fix f) -> Fix f
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Fix f -> f (Fix f)
forall a. a -> f a
forall (f :: * -> *) a. Monoid1 f => a -> f a
liftEmpty Fix f
forall a. Monoid a => a
mempty)
  mappend :: Fix f -> Fix f -> Fix f
mappend = Fix f -> Fix f -> Fix f
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 (a :: k). HFix h a -> HFix h a -> Bool)
-> h (HFix h) a -> h (HFix h) a -> Bool
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
forall (f :: k -> *) (a :: k).
(forall (x :: k). f x -> f x -> Bool) -> h f a -> h f a -> Bool
eqHetero HFix h x -> HFix h x -> Bool
forall (a :: k). HFix h a -> HFix h a -> Bool
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
(==) = HFix h a -> HFix h a -> Bool
forall (a :: k). 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 (a :: k) (b :: k). HFix h a -> HFix h b -> Maybe (a :~: b))
-> h (HFix h) a -> h (HFix h) b -> Maybe (a :~: 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)
forall (f :: k -> *) (a :: k) (b :: k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> h f a -> h f b -> Maybe (a :~: b)
testEqualityHetero HFix h x -> HFix h y -> Maybe (x :~: y)
forall (a :: k) (b :: k). HFix h a -> HFix h b -> Maybe (a :~: b)
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 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
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 <- f r -> f r -> Maybe (r :~: r)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
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 <- Rec f rs -> Rec f rs -> Maybe (rs :~: rs)
forall (a :: [k]) (b :: [k]). Rec f a -> Rec f b -> Maybe (a :~: b)
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
    (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Rec f a
_ Rec f b
_ = Maybe (a :~: 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 = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
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 <- f r -> f r -> Maybe (Coercion r r)
forall (a :: k) (b :: k). f a -> f b -> Maybe (Coercion a b)
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 <- Rec f rs -> Rec f rs -> Maybe (Coercion rs rs)
forall (a :: [k]) (b :: [k]).
Rec f a -> Rec f b -> Maybe (Coercion a b)
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
    Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion Rec f a
_ Rec f b
_ = Maybe (Coercion a 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 = Int -> Rec f a -> Int
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 -> Int -> Rec f rs -> Int
forall (a :: [k]). Int -> Rec f a -> Int
go (Int -> f r -> Int
forall (a :: k). Int -> f a -> Int
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 = Int -> Rec f as -> Int
forall (a :: [k]). Int -> Rec f a -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
      (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"RecCons "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f r -> ShowS
forall (a :: k). Int -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall Int
11 f r
v
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Rec f rs -> ShowS
forall (a :: [k]). Int -> Rec f a -> ShowS
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 = Int -> Rec f as -> ShowS
forall (a :: [k]). Int -> Rec f a -> ShowS
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 SingList a
Sing 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
    (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"RecCons "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing r -> Int -> f r -> ShowS
forall (a :: k). Sing a -> Int -> f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing r
Sing r
s Int
11 f r
v
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing rs -> Int -> Rec f rs -> ShowS
forall (a :: [k]). Sing a -> Int -> Rec f a -> ShowS
forall {k} (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach SingList rs
Sing rs
ss Int
11 Rec f rs
vs

instance EqForall f => Eq (Rec f as) where
  == :: Rec f as -> Rec f as -> Bool
(==) = Rec f as -> Rec f as -> Bool
forall (a :: [k]). Rec f a -> Rec f a -> 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) =
    f r -> f r -> Bool
forall (a :: k). f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall f r
a f r
f r
b Bool -> Bool -> Bool
&& Rec f rs -> Rec f rs -> Bool
forall (a :: [k]). Rec f a -> Rec f a -> Bool
forall {k} (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall Rec f rs
as Rec f rs
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 SingList a
Sing 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) =
    Sing r -> f r -> f r -> Bool
forall (a :: k). Sing a -> f a -> f a -> Bool
forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing r
Sing r
s f r
a f r
f r
b Bool -> Bool -> Bool
&& Sing rs -> Rec f rs -> Rec f rs -> Bool
forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Bool
forall {k} (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach SingList rs
Sing rs
ss Rec f rs
as Rec f rs
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 = WitnessedEquality a a
WitnessedEquality a b
forall {k} (a :: k). WitnessedEquality a a
WitnessedEqualityEqual
  eqForallPoly Rec f a
RecNil (RecCons f r
_ Rec f rs
_) = WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
  eqForallPoly (RecCons f r
_ Rec f rs
_) Rec f b
RecNil = WitnessedEquality a b
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 f r -> f r -> WitnessedEquality r r
forall (a :: k) (b :: k). f a -> f b -> WitnessedEquality a b
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 -> WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
    WitnessedEquality r r
WitnessedEqualityEqual -> case Rec f rs -> Rec f rs -> WitnessedEquality rs rs
forall (a :: [k]) (b :: [k]).
Rec f a -> Rec f b -> WitnessedEquality a b
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 -> WitnessedEquality a b
forall {k} (a :: k) (b :: k). WitnessedEquality a b
WitnessedEqualityUnequal
      WitnessedEquality rs rs
WitnessedEqualityEqual -> WitnessedEquality a a
WitnessedEquality a b
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 = Rec f as -> Rec f as -> Ordering
forall (a :: [k]). Rec f a -> Rec f a -> Ordering
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) =
    Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
mappend (f r -> f r -> Ordering
forall (a :: k). f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall f r
a f r
f r
b) (Rec f rs -> Rec f rs -> Ordering
forall (a :: [k]). Rec f a -> Rec f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall Rec f rs
as Rec f rs
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 SingList a
Sing 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) =
    Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
mappend (Sing r -> f r -> f r -> Ordering
forall (a :: k). Sing a -> f a -> f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing r
Sing r
s f r
a f r
f r
b) (Sing rs -> Rec f rs -> Rec f rs -> Ordering
forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Ordering
forall {k} (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach SingList rs
Sing rs
ss Rec f rs
as Rec f rs
Rec f rs
bs)


instance SemigroupForall f => Semigroup (Rec f as) where
  <> :: Rec f as -> Rec f as -> Rec f as
(<>) = (forall (x :: k). f x -> f x -> f x)
-> 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 f x -> f x -> f x
forall (x :: k). f x -> f x -> f x
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 SingList a
Sing a
SingListNil Rec f a
RecNil Rec f a
RecNil = Rec f a
Rec f '[]
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) =
    f r -> Rec f rs -> Rec f (r : rs)
forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (Sing r -> f r -> f r -> f r
forall (a :: k). Sing a -> f a -> f a -> f a
forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach Sing r
Sing r
s f r
x f r
f r
y) (Sing rs -> Rec f rs -> Rec f rs -> Rec f rs
forall (a :: [k]). Sing a -> Rec f a -> Rec f a -> Rec f a
forall {k} (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach SingList rs
Sing rs
ss Rec f rs
xs Rec f rs
Rec f rs
ys)

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

instance SemigroupForall f => SemigroupForall (Rec f) where
  appendForall :: forall (a :: [k]). Rec f a -> Rec f a -> Rec f a
appendForall = (forall (x :: k). f x -> f x -> f x)
-> Rec f a -> Rec f a -> Rec f a
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 f x -> f x -> f x
forall (x :: k). f x -> f x -> f x
forall {k} (f :: k -> *) (a :: k).
SemigroupForall f =>
f a -> f a -> f a
appendForall

instance StorableForeach f => StorableForeach (Rec f) where
  sizeOfForeach :: forall (a :: [k]). Proxy (Rec f) -> Sing a -> Int
sizeOfForeach Proxy (Rec f)
_ SingList a
Sing a
SingListNil = Int
0
  sizeOfForeach Proxy (Rec f)
_ (SingListCons Sing r
s SingList rs
ss) =
    Proxy f -> Sing r -> Int
forall (a :: k). Proxy f -> Sing a -> Int
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (Proxy f
forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Sing r
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy (Rec f) -> Sing rs -> Int
forall (a :: [k]). Proxy (Rec f) -> Sing a -> Int
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (Proxy (Rec f)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Rec f)) SingList rs
Sing rs
ss
  peekForeach :: forall (a :: [k]). Sing a -> Ptr (Rec f a) -> IO (Rec f a)
peekForeach SingList a
Sing a
SingListNil Ptr (Rec f a)
_ = Rec f a -> IO (Rec f a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Rec f a
Rec f '[]
forall {k} (f :: k -> *). Rec f '[]
RecNil
  peekForeach (SingListCons Sing r
s SingList rs
ss) Ptr (Rec f a)
ptr = do
    f r
r <- Sing r -> Ptr (f r) -> IO (f r)
forall (a :: k). Sing a -> Ptr (f a) -> IO (f a)
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach Sing r
s (Ptr (Rec f a) -> Ptr (f r)
forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f a)
ptr)
    Rec f rs
rs <- Sing rs -> Ptr (Rec f rs) -> IO (Rec f rs)
forall (a :: [k]). Sing a -> Ptr (Rec f a) -> IO (Rec f a)
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach SingList rs
Sing rs
ss (Ptr (Rec f a) -> Int -> Ptr (Rec f rs)
forall a b. Ptr a -> Int -> Ptr b
plusPtr Ptr (Rec f a)
ptr (Proxy f -> Sing r -> Int
forall (a :: k). Proxy f -> Sing a -> Int
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (Proxy f
forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Sing r
s))
    Rec f a -> IO (Rec f a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (f r -> Rec f rs -> Rec f (r : rs)
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 = () -> IO ()
forall a. a -> IO a
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
    Sing r -> Ptr (f r) -> f r -> IO ()
forall (a :: k). Sing a -> Ptr (f a) -> f a -> IO ()
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach Sing r
Sing r
s (Ptr (Rec f a) -> Ptr (f r)
forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f a)
ptr) f r
r
    Sing rs -> Ptr (Rec f rs) -> Rec f rs -> IO ()
forall (a :: [k]). Sing a -> Ptr (Rec f a) -> Rec f a -> IO ()
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach SingList rs
Sing rs
ss (Ptr (Rec f a) -> Int -> Ptr (Rec f rs)
forall a b. Ptr a -> Int -> Ptr b
plusPtr Ptr (Rec f a)
ptr (Proxy f -> Sing r -> Int
forall (a :: k). Proxy f -> Sing a -> Int
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (Proxy f
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
_ = Proxy (Rec f) -> Sing as -> Int
forall (a :: [k]). Proxy (Rec f) -> Sing a -> Int
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Proxy f -> Sing a -> Int
sizeOfForeach (Proxy (Rec f)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Rec f)) (SingList as
Sing as
forall {k} (a :: k). Reify a => Sing a
reify :: SingList as)
  alignment :: Rec f as -> Int
alignment Rec f as
_ = Rec f as -> Int
forall a. Storable a => a -> Int
sizeOf (Rec f as
forall a. HasCallStack => a
undefined :: Rec f as)
  poke :: Ptr (Rec f as) -> Rec f as -> IO ()
poke = Sing as -> Ptr (Rec f as) -> Rec f as -> IO ()
forall (a :: [k]). Sing a -> Ptr (Rec f a) -> Rec f a -> IO ()
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach (SingList as
Sing as
forall {k} (a :: k). Reify a => Sing a
reify :: SingList as)
  peek :: Ptr (Rec f as) -> IO (Rec f as)
peek = Sing as -> Ptr (Rec f as) -> IO (Rec f as)
forall (a :: [k]). Sing a -> Ptr (Rec f a) -> IO (Rec f a)
forall k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach (SingList as
Sing as
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 SingList a
Sing a
SingListNil Rec f a
RecNil = () -> Put
forall a. a -> PutM a
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
    Sing r -> f r -> Put
forall (a :: k). Sing a -> f a -> Put
forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> f a -> Put
putForeach Sing r
Sing r
s f r
r
    Sing rs -> Rec f rs -> Put
forall (a :: [k]). Sing a -> Rec f a -> Put
forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> f a -> Put
putForeach SingList rs
Sing rs
ss Rec f rs
rs
  getForeach :: forall (a :: [k]). Sing a -> Get (Rec f a)
getForeach SingList a
Sing a
SingListNil = Rec f a -> Get (Rec f a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Rec f a
Rec f '[]
forall {k} (f :: k -> *). Rec f '[]
RecNil
  getForeach (SingListCons Sing r
s SingList rs
ss) =
    (f r -> Rec f rs -> Rec f a)
-> Get (f r) -> Get (Rec f rs) -> Get (Rec f a)
forall a b c. (a -> b -> c) -> Get a -> Get b -> Get c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f r -> Rec f rs -> Rec f a
f r -> Rec f rs -> Rec f (r : rs)
forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (Sing r -> Get (f r)
forall (a :: k). Sing a -> Get (f a)
forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> Get (f a)
getForeach Sing r
s) (Sing rs -> Get (Rec f rs)
forall (a :: [k]). Sing a -> Get (Rec f a)
forall k (f :: k -> *) (a :: k).
BinaryForeach f =>
Sing a -> Get (f a)
getForeach SingList rs
Sing rs
ss)

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 = Rec h rs
Rec h '[]
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) =
  h r -> Rec h rs -> Rec h (r : rs)
forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (f r -> g r -> h r
forall (x :: k). f x -> g x -> h x
f f r
a g r
g r
b) ((forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
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 f x -> g x -> h x
forall (x :: k). f x -> g x -> h x
f Rec f rs
as Rec g rs
Rec g rs
bs)