{-# 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(..)
, 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 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.<>)
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)