{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
  UndecidableInstances, IncoherentInstances, GADTs #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Param.Equality
-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines equality for signatures, which lifts to equality for
-- terms.
--
--------------------------------------------------------------------------------
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

-- |Equality on parametric values. The equality test is performed inside the
-- 'FreshM' monad for generating fresh identifiers.
class PEq a where
    peq :: a -> a -> FreshM Bool

instance Eq a => PEq a where
    peq x y = return $ x == y

{-| Signature equality. An instance @EqD f@ gives rise to an instance
  @Eq (Term f)@. The equality test is performed inside the 'FreshM' monad for
  generating fresh identifiers. -}
class EqD f where
    eqD :: PEq a => f Var a -> f Var a -> FreshM Bool

{-| 'EqD' is propagated through sums. -}
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

{-| From an 'EqD' difunctor an 'Eq' instance of the corresponding term type can
  be derived. -}
instance EqD f => EqD (Cxt h f) where
    eqD (Term e1) (Term e2) = eqD e1 e2
    eqD (Hole h1) (Hole h2) = peq h1 h2
    eqD (Place p1) (Place p2) = peq p1 p2
    eqD _ _ = return False

instance (EqD f, PEq a) => PEq (Cxt h f Var a) where
    peq = eqD

{-| Equality on terms. -}
instance (Difunctor f, EqD f) => Eq (Term f) where
    (==) x y = evalFreshM $ eqD (coerceCxt x) (coerceCxt y)