{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Multi.Equality
(
EqHF(..),
KEq(..),
heqMod
) where
import Data.Comp.Multi.HFoldable
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
class KEq f where
keq :: f i -> f j -> Bool
class EqHF f where
eqHF :: KEq g => f g i -> f g j -> Bool
instance Eq a => KEq (K a) where
keq (K x) (K y) = x == y
instance KEq a => Eq (E a) where
E x == E y = x `keq` y
instance (EqHF f, EqHF g) => EqHF (f :+: g) where
eqHF (Inl x) (Inl y) = eqHF x y
eqHF (Inr x) (Inr y) = eqHF x y
eqHF _ _ = False
instance EqHF f => EqHF (Cxt h f) where
eqHF (Term e1) (Term e2) = e1 `eqHF` e2
eqHF (Hole h1) (Hole h2) = h1 `keq` h2
eqHF _ _ = False
instance (EqHF f, KEq a) => KEq (Cxt h f a) where
keq = eqHF
instance (EqHF f, KEq a) => Eq (Cxt h f a i) where
(==) = keq
heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(E a, E b)]
heqMod s t
| unit s `eqHF` unit' t = Just args
| otherwise = Nothing
where unit = hfmap (const $ K ())
unit' = hfmap (const $ K ())
args = htoList s `zip` htoList t