module Generics.MultiRec.Binary where
import Control.Applicative
import Control.Monad
import Data.Binary
import Generics.MultiRec.Base
import Generics.MultiRec.TEq
class HBinary phi f where
hput :: (forall ix'. phi ix' -> r ix' -> Put) -> phi ix -> f r ix -> Put
hget :: (forall ix'. El phi ix' => phi ix' -> Get (r ix')) -> phi ix -> Get (f r ix)
instance El phi xi => HBinary phi (I xi) where
hput t _ (I x) = t proof x
hget g _ = I <$> g proof
instance Binary a => HBinary phi (K a) where
hput _ _ (K x) = put x
hget _ _ = K <$> get
instance HBinary phi U where
hput _ _ U = put ()
hget _ _ = return U
instance (HBinary phi f, HBinary phi g) => HBinary phi (f :+: g) where
hput t p (L x) = put True >> hput t p x
hput t p (R y) = put False >> hput t p y
hget t p = get >>= \v -> if v then L <$> hget t p else R <$> hget t p
instance (HBinary phi f, HBinary phi g) => HBinary phi (f :*: g) where
hput t p (x :*: y) = hput t p x >> hput t p y
hget t p = (:*:) <$> hget t p <*> hget t p
instance (EqS phi, El phi ix, HBinary phi f) => HBinary phi (f :>: ix) where
hput t p (Tag x) = hput t p x
hget t p =
case eqS (proof :: phi ix) p of
Nothing -> error "decoding error"
Just Refl -> Tag <$> hget t p
instance (Constructor c, HBinary phi f) => HBinary phi (C c f) where
hput t p (C x) = hput t p x
hget t p = C <$> hget t p
gput :: (Fam phi, HBinary phi (PF phi)) => phi ix -> ix -> Put
gput p = hput (\q -> gput q . unI0) p . from p
gget :: (Fam phi, HBinary phi (PF phi)) => phi ix -> Get ix
gget p = to p <$> hget (fmap I0 . gget) p