{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
UndecidableInstances, GADTs #-}
module Data.Comp.Param.Equality
(
PEq(..),
EqD(..)
) where
import Data.Comp.Param.Term
import Data.Comp.Param.Sum
import Data.Comp.Param.Ops
import Data.Comp.Param.Difunctor
import Data.Comp.Param.FreshM
import Control.Monad (liftM)
class PEq a where
peq :: a -> a -> FreshM Bool
instance PEq a => PEq [a] where
peq l1 l2
| length l1 /= length l2 = return False
| otherwise = liftM or $ mapM (uncurry peq) $ zip l1 l2
instance {-# OVERLAPPABLE #-} Eq a => PEq a where
peq x y = return $ x == y
class EqD f where
eqD :: PEq a => f Name a -> f Name a -> FreshM Bool
instance (EqD f, EqD g) => EqD (f :+: g) where
eqD (Inl x) (Inl y) = eqD x y
eqD (Inr x) (Inr y) = eqD x y
eqD _ _ = return False
instance EqD f => EqD (Cxt h f) where
eqD (In e1) (In e2) = eqD e1 e2
eqD (Hole h1) (Hole h2) = peq h1 h2
eqD (Var p1) (Var p2) = peq p1 p2
eqD _ _ = return False
instance (EqD f, PEq a) => PEq (Cxt h f Name a) where
peq = eqD
instance (Difunctor f, EqD f) => Eq (Term f) where
(==) (Term x) (Term y) = evalFreshM $ eqD x y