mergeG.hs

{-# LANGUAGE GADTs #-}
import Reflex

import Data.Dependent.Map (DMap)
import qualified Data.Dependent.Map as DMap
import Data.Dependent.Sum (DSum(..))
import Data.GADT.Compare
import Data.Functor.Compose
import Data.Functor.Identity

data KComp k v a where
  KComp :: k a -> KComp k v (v a)

instance GEq k => GEq (KComp k v) where
  geq (KComp x) (KComp y) = case geq x y of
    Nothing -> Nothing
    Just Refl -> Just Refl

instance GCompare k => GCompare (KComp k v) where
  gcompare (KComp x) (KComp y) = case gcompare x y of
    GLT -> GLT
    GEQ -> GEQ
    GGT -> GGT

dmShift :: DMap k (Compose (Event t) v) -> DMap (KComp k v) (Event t)
dmShift m = DMap.fromDistinctAscList [ KComp k :=> e | k :=> Compose e <- DMap.toAscList m]

dmUnshift :: DMap (KComp k v) Identity -> DMap k v
dmUnshift m = DMap.fromDistinctAscList [ k :=> v | KComp k :=> (Identity v) <- DMap.toAscList m ]

mergeG :: (Reflex t, GCompare k) => DMap k (Compose (Event t) v) -> Event t (DMap k v)
mergeG = fmap dmUnshift . merge . dmShift