{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Equality
(
EqF(..),
eqMod,
) where
import Control.Monad hiding (mapM_)
import Data.Comp.Derive.Equality
import Data.Comp.Derive.Utils
import Data.Comp.Ops
import Data.Comp.Term
import Data.Foldable
import Prelude hiding (all, mapM_)
instance (EqF f, Eq a) => Eq (Cxt h f a) where
== :: Cxt h f a -> Cxt h f a -> Bool
(==) = Cxt h f a -> Cxt h f a -> Bool
forall (f :: * -> *) a. (EqF f, Eq a) => f a -> f a -> Bool
eqF
instance (EqF f) => EqF (Cxt h f) where
eqF :: Cxt h f a -> Cxt h f a -> Bool
eqF (Term f (Cxt h f a)
e1) (Term f (Cxt h f a)
e2) = f (Cxt h f a)
e1 f (Cxt h f a) -> f (Cxt h f a) -> Bool
forall (f :: * -> *) a. (EqF f, Eq a) => f a -> f a -> Bool
`eqF` f (Cxt h f a)
e2
eqF (Hole a
h1) (Hole a
h2) = a
h1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
h2
eqF Cxt h f a
_ Cxt h f a
_ = Bool
False
instance (EqF f, EqF g) => EqF (f :+: g) where
eqF :: (:+:) f g a -> (:+:) f g a -> Bool
eqF (Inl f a
x) (Inl f a
y) = f a -> f a -> Bool
forall (f :: * -> *) a. (EqF f, Eq a) => f a -> f a -> Bool
eqF f a
x f a
y
eqF (Inr g a
x) (Inr g a
y) = g a -> g a -> Bool
forall (f :: * -> *) a. (EqF f, Eq a) => f a -> f a -> Bool
eqF g a
x g a
y
eqF (:+:) f g a
_ (:+:) f g a
_ = Bool
False
eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a,b)]
eqMod :: f a -> f b -> Maybe [(a, b)]
eqMod f a
s f b
t
| f a -> f ()
forall b. f b -> f ()
unit f a
s f () -> f () -> Bool
forall (f :: * -> *) a. (EqF f, Eq a) => f a -> f a -> Bool
`eqF` f b -> f ()
forall b. f b -> f ()
unit' f b
t = [(a, b)] -> Maybe [(a, b)]
forall a. a -> Maybe a
Just [(a, b)]
args
| Bool
otherwise = Maybe [(a, b)]
forall a. Maybe a
Nothing
where unit :: f b -> f ()
unit = (b -> ()) -> f b -> f ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> b -> ()
forall a b. a -> b -> a
const ())
unit' :: f b -> f ()
unit' = (b -> ()) -> f b -> f ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> b -> ()
forall a b. a -> b -> a
const ())
args :: [(a, b)]
args = f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f a
s [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` f b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f b
t
$(derive [makeEqF] $ [''Maybe, ''[]] ++ tupleTypes 2 10)