{-# 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 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 (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 :: 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
eqHetero 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 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 :: 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)
testEqualityHetero 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 :: Rec f a -> Rec f b -> Maybe (a :~: b)
testEquality Rec f a
RecNil Rec f b
RecNil = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
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 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 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 :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
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 :: 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 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 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 :: 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 :: Int -> Rec f rs -> 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 k (f :: k -> *) (a :: k).
HashableForall f =>
Int -> f a -> Int
hashWithSaltForall Int
s f r
b) Rec f rs
bs

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

instance ShowForall f => ShowForall (Rec f) where
  showsPrecForall :: 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 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 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 k (f :: k -> *) (a :: k).
ShowForall f =>
Int -> f a -> ShowS
showsPrecForall

instance ShowForeach f => ShowForeach (Rec f) where
  showsPrecForeach :: Sing a -> Int -> Rec f a -> ShowS
showsPrecForeach Sing a
SingListNil Int
_ Rec f a
RecNil = String -> ShowS
showString String
"RecNil"
  showsPrecForeach (SingListCons s 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 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 k (f :: k -> *) (a :: k).
ShowForeach f =>
Sing a -> Int -> f a -> ShowS
showsPrecForeach Sing rs
SingList 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 k (f :: k -> *) (a :: k). EqForall f => f a -> f a -> Bool
eqForall

instance EqForall f => EqForall (Rec f) where
  eqForall :: 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 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 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 :: Sing a -> Rec f a -> Rec f a -> Bool
eqForeach Sing a
SingListNil Rec f a
RecNil Rec f a
RecNil = Bool
True
  eqForeach (SingListCons s 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 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 k (f :: k -> *) (a :: k).
EqForeach f =>
Sing a -> f a -> f a -> Bool
eqForeach Sing rs
SingList rs
ss Rec f rs
as Rec f rs
Rec f rs
bs

instance EqForallPoly f => EqForallPoly (Rec f) where
  eqForallPoly :: Rec f a -> Rec f b -> WitnessedEquality a b
eqForallPoly Rec f a
RecNil Rec f b
RecNil = 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 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 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 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 k (f :: k -> *) (a :: k).
OrdForall f =>
f a -> f a -> Ordering
compareForall

instance OrdForall f => OrdForall (Rec f) where
  compareForall :: 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 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 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 :: Sing a -> Rec f a -> Rec f a -> Ordering
compareForeach Sing a
SingListNil Rec f a
RecNil Rec f a
RecNil = Ordering
EQ
  compareForeach (SingListCons s 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 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 k (f :: k -> *) (a :: k).
OrdForeach f =>
Sing a -> f a -> f a -> Ordering
compareForeach Sing rs
SingList 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 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 :: Sing a -> Rec f a -> Rec f a -> Rec f a
appendForeach Sing a
SingListNil Rec f a
RecNil Rec f a
RecNil = Rec f a
forall k (f :: k -> *). Rec f '[]
RecNil
  appendForeach (SingListCons s 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 a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (Sing r -> f r -> f r -> f r
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 k (f :: k -> *) (a :: k).
SemigroupForeach f =>
Sing a -> f a -> f a -> f a
appendForeach Sing rs
SingList rs
ss Rec f rs
xs Rec f rs
Rec f rs
ys)

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

instance SemigroupForall f => SemigroupForall (Rec f) where
  appendForall :: 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 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 ToJSONForall f => AE.ToJSON (Rec f as) where
  toJSON :: Rec f as -> Value
toJSON = Rec f as -> Value
forall k (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall

instance ToJSONForall f => ToJSONForall (Rec f) where
  toJSONForall :: Rec f a -> Value
toJSONForall = [Value] -> Value
forall a. ToJSON a => a -> Value
AE.toJSON ([Value] -> Value) -> (Rec f a -> [Value]) -> Rec f a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f a -> [Value]
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 :: Rec g xs -> [Value]
go Rec g xs
RecNil = []
    go (RecCons g r
x Rec g rs
xs) = g r -> Value
forall k (f :: k -> *) (a :: k). ToJSONForall f => f a -> Value
toJSONForall g r
x Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: Rec g rs -> [Value]
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 = Sing as -> Value -> Parser (Rec f as)
forall k (f :: k -> *) (a :: k).
FromJSONForeach f =>
Sing a -> Value -> Parser (f a)
parseJSONForeach Sing as
forall k (a :: k). Reify a => Sing a
reify

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

instance StorableForeach f => StorableForeach (Rec f) where
  sizeOfForeach :: Proxy (Rec f) -> Sing a -> Int
sizeOfForeach Proxy (Rec f)
_ Sing a
SingListNil = Int
0
  sizeOfForeach Proxy (Rec f)
_ (SingListCons s ss) =
    Proxy f -> Sing r -> 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 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)) Sing rs
SingList rs
ss
  peekForeach :: Sing a -> Ptr (Rec f a) -> IO (Rec f a)
peekForeach Sing a
SingListNil Ptr (Rec f a)
_ = Rec f '[] -> IO (Rec f '[])
forall (m :: * -> *) a. Monad m => a -> m a
return Rec f '[]
forall k (f :: k -> *). Rec f '[]
RecNil
  peekForeach (SingListCons s ss) Ptr (Rec f a)
ptr = do
    f r
r <- Sing r -> Ptr (f r) -> IO (f r)
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 k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach Sing rs
SingList 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 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 (r : rs) -> IO (Rec f (r : rs))
forall (m :: * -> *) a. Monad m => a -> m a
return (f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
r Rec f rs
rs)
  pokeForeach :: Sing a -> Ptr (Rec f a) -> Rec f a -> IO ()
pokeForeach Sing a
_ Ptr (Rec f a)
_ Rec f a
RecNil = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  pokeForeach (SingListCons s ss) Ptr (Rec f a)
ptr (RecCons f r
r Rec f rs
rs) = do
    Sing r -> Ptr (f r) -> f r -> 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 k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach Sing rs
SingList 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 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 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
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 k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> f a -> IO ()
pokeForeach (SingList 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 k (f :: k -> *) (a :: k).
StorableForeach f =>
Sing a -> Ptr (f a) -> IO (f a)
peekForeach (SingList as
forall k (a :: k). Reify a => Sing a
reify :: SingList as)

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

instance FromJSONExists f => FromJSONExists (Rec f) where
  parseJSONExists :: Value -> Parser (Exists (Rec f))
parseJSONExists = String
-> (Array -> Parser (Exists (Rec f)))
-> Value
-> Parser (Exists (Rec f))
forall a. String -> (Array -> Parser a) -> Value -> Parser a
AE.withArray String
"Rec" ((Array -> Parser (Exists (Rec f)))
 -> Value -> Parser (Exists (Rec f)))
-> (Array -> Parser (Exists (Rec f)))
-> Value
-> Parser (Exists (Rec f))
forall a b. (a -> b) -> a -> b
$ \Array
vs -> 
    (Value -> Exists (Rec f) -> Parser (Exists (Rec f)))
-> Exists (Rec f) -> Array -> Parser (Exists (Rec f))
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM Value -> Exists (Rec f) -> Parser (Exists (Rec f))
forall k (g :: k -> *).
FromJSONExists g =>
Value -> Exists (Rec g) -> Parser (Exists (Rec g))
go (Rec f '[] -> Exists (Rec f)
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists Rec f '[]
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 :: Value -> Exists (Rec g) -> Parser (Exists (Rec g))
go Value
v (Exists Rec g a
rs) = do
      Exists g a
r <- Value -> Parser (Exists g)
forall k (f :: k -> *).
FromJSONExists f =>
Value -> Parser (Exists f)
parseJSONExists Value
v :: AET.Parser (Exists g)
      Exists (Rec g) -> Parser (Exists (Rec g))
forall (m :: * -> *) a. Monad m => a -> m a
return (Rec g (a : a) -> Exists (Rec g)
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (g a -> Rec g a -> Rec g (a : a)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
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 (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
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 a (f :: a -> *) (r :: a) (rs :: [a]).
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 forall (x :: k). f x -> g x -> h x
f Rec f rs
as Rec g rs
Rec g rs
bs)