{-# 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 a i -> K a j -> Bool
keq (K a
x) (K a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
instance KEq a => Eq (E a) where
E a i
x == :: E a -> E a -> Bool
== E a i
y = a i
x a i -> a i -> Bool
forall (f :: * -> *) i j. KEq f => f i -> f j -> Bool
`keq` a i
y
instance (EqHF f, EqHF g) => EqHF (f :+: g) where
eqHF :: (:+:) f g g i -> (:+:) f g g j -> Bool
eqHF (Inl f g i
x) (Inl f g j
y) = f g i -> f g j -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
eqHF f g i
x f g j
y
eqHF (Inr g g i
x) (Inr g g j
y) = g g i -> g g j -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
eqHF g g i
x g g j
y
eqHF (:+:) f g g i
_ (:+:) f g g j
_ = Bool
False
instance EqHF f => EqHF (Cxt h f) where
eqHF :: Cxt h f g i -> Cxt h f g j -> Bool
eqHF (Term f (Cxt h f g) i
e1) (Term f (Cxt h f g) j
e2) = f (Cxt h f g) i
e1 f (Cxt h f g) i -> f (Cxt h f g) j -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
`eqHF` f (Cxt h f g) j
e2
eqHF (Hole g i
h1) (Hole g j
h2) = g i
h1 g i -> g j -> Bool
forall (f :: * -> *) i j. KEq f => f i -> f j -> Bool
`keq` g j
h2
eqHF Cxt h f g i
_ Cxt h f g j
_ = Bool
False
instance (EqHF f, KEq a) => KEq (Cxt h f a) where
keq :: Cxt h f a i -> Cxt h f a j -> Bool
keq = Cxt h f a i -> Cxt h f a j -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
eqHF
instance (EqHF f, KEq a) => Eq (Cxt h f a i) where
== :: Cxt h f a i -> Cxt h f a i -> Bool
(==) = Cxt h f a i -> Cxt h f a i -> Bool
forall (f :: * -> *) i j. KEq f => f i -> f j -> Bool
keq
heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(E a, E b)]
heqMod :: f a i -> f b i -> Maybe [(E a, E b)]
heqMod f a i
s f b i
t
| f a i -> f (K ()) i
forall (f :: * -> *) i. f f i -> f (K ()) i
unit f a i
s f (K ()) i -> f (K ()) i -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
`eqHF` f b i -> f (K ()) i
forall (f :: * -> *) i. f f i -> f (K ()) i
unit' f b i
t = [(E a, E b)] -> Maybe [(E a, E b)]
forall a. a -> Maybe a
Just [(E a, E b)]
args
| Bool
otherwise = Maybe [(E a, E b)]
forall a. Maybe a
Nothing
where unit :: f f i -> f (K ()) i
unit = (f :-> K ()) -> forall i. f f i -> f (K ()) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (K () i -> f i -> K () i
forall a b. a -> b -> a
const (K () i -> f i -> K () i) -> K () i -> f i -> K () i
forall a b. (a -> b) -> a -> b
$ () -> K () i
forall a i. a -> K a i
K ())
unit' :: f f i -> f (K ()) i
unit' = (f :-> K ()) -> f f :-> f (K ())
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (K () i -> f i -> K () i
forall a b. a -> b -> a
const (K () i -> f i -> K () i) -> K () i -> f i -> K () i
forall a b. (a -> b) -> a -> b
$ () -> K () i
forall a i. a -> K a i
K ())
args :: [(E a, E b)]
args = f a i -> [E a]
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFoldable f =>
f a :=> [E a]
htoList f a i
s [E a] -> [E b] -> [(E a, E b)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` f b i -> [E b]
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFoldable f =>
f a :=> [E a]
htoList f b i
t