-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Equal
-- Copyright   :  (c) 2010 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Rewrite:
-- automatic transformation system for point-free programs
-- 
-- Implementation of type and function equality at the value-level.
--
-----------------------------------------------------------------------------

module Data.Equal where

import Data.Type
import Data.Spine

import Control.Monad hiding (Functor(..))
import Unsafe.Coerce

import Generics.Pointless.Functors

data Equal a b where
    Eq :: Equal a a

teq :: MonadPlus m => Type a -> Type b -> m (Equal a b)
teq Any _ = return (unsafeCoerce Eq)
teq _ Any = return (unsafeCoerce Eq)
teq (Id a) b = teq a b
teq a (Id b) = teq a b
teq One One = return Eq
teq Int Int = return Eq
teq Bool Bool = return Eq
teq Char Char = return Eq
teq (Prod a b) (Prod c d) = do
	Eq <- teq a c
	Eq <- teq b d
	return Eq
teq (Either a b) (Either c d) = do
	Eq <- teq a c
	Eq  <- teq b d
	return Eq
teq (Data s fx) (Data s' fy) = do
    guard (s == s')
    Eq <- feq fx fy
    return (unsafeCoerce Eq)
teq (Fun a b) (Fun c d) = do
    Eq <- teq a c
    Eq <- teq b d
    return Eq
teq (Lns a b) (Lns c d) = do
    Eq <- teq a c
    Eq <- teq b d
    return Eq
teq (Pf a) (Pf b) = do
    Eq <- teq a b
    return Eq
teq Dynamic Dynamic = error "dynamic equality"
teq TP TP = return Eq
teq (TU a) (TU b) = do
    Eq <- teq a b
    return Eq
teq _ _ = mzero

feq :: MonadPlus m => Fctr f -> Fctr g -> m (Equal (Fix f) (Fix g))
feq I I = return Eq
feq (K a) (K b) = do
    Eq <- teq a b
    return Eq
feq L L = return Eq
feq (f :*!: g) (h :*!: i) = do
    Eq <- feq f h
    Eq <- feq g i
    return Eq
feq (f :+!: g) (h :+!: i) = do
    Eq <- feq f h
    Eq <- feq g i
    return Eq
feq (f :@!: g) (h :@!: i) = do
    Eq <- feq f h
    Eq <- feq g i
    return Eq
feq _ _ = mzero

-- | Syntactic equality, with the exception of protected values.
geq :: Type a -> a -> a -> Bool
geq (Pf t) (PROTECT x) y = geq (Pf t) x y
geq (Pf t) x (PROTECT y) = geq (Pf t) x y
geq (Pf t) (PROTECT_LNS x) y = geq (Pf t) x y
geq (Pf t) x (PROTECT_LNS y) = geq (Pf t) x y
geq t x y = geq' t x t y

geq' :: Type a -> a -> Type b -> b -> Bool
geq' a x b y = aux a b x y
    where aux :: Type a -> Type b -> a -> b -> Bool
          aux t1 t2 x y = aux' t1 (toSpine t1 x) t2 (toSpine t2 y)
          aux' :: Type a -> Spine a -> Type b -> Spine b -> Bool
          aux' _ (_ `As` c1) _ (_ `As` c2) = name c1 == name c2
          aux' t (f1 `Ap` (t1 :| a1)) t' (f2 `Ap` (t2 :| a2)) = aux' (Fun t1 t) f1 (Fun t2 t') f2 && aux t1 t2 a1 a2
          aux' _ _ _ _ = False

-- | Clone of |geq| with a specific case for top.
geqt :: Type a -> a -> a -> Bool
geqt (Pf t) (PROTECT x) y = geqt (Pf t) x y
geqt (Pf t) x (PROTECT y) = geqt (Pf t) x y
geqt (Pf t) (PROTECT_LNS x) y = geqt (Pf t) x y
geqt (Pf t) x (PROTECT_LNS y) = geqt (Pf t) x y
geqt t x y = geqt' t x t y

geqt' :: Type a -> a -> Type b -> b -> Bool
geqt' a x b y = aux a b x y
    where aux :: Type a -> Type b -> a -> b -> Bool
          aux t1 t2 x y = aux' t1 (toSpine t1 x) t2 (toSpine t2 y)
          aux' :: Type a -> Spine a -> Type b -> Spine b -> Bool
          aux' _ _ (Pf _) (TOP `As` _) = True
          aux' (Pf _) (As TOP _) _ _ = True
          aux' _ (_ `As` c1) _ (_ `As` c2) = name c1 == name c2
          aux' t (f1 `Ap` (t1 :| a1)) t' (f2 `Ap` (t2 :| a2)) = aux' (Fun t1 t) f1 (Fun t2 t') f2 && aux t1 t2 a1 a2
          aux' _ _ _ _ = False

coerce :: MonadPlus m => Type a -> Type b -> a -> m b
coerce a b x = do Eq <- teq a b
                  return x

find :: Type b -> b -> Type a -> a -> Bool
find b y a x = findSpine a (toSpine a x)
    where findSpine :: Type a -> Spine a -> Bool
          findSpine t (As v con) = case teq t b of {
              Just Eq   -> geqt t v y;
              otherwise -> False
              }
          findSpine t s@(Ap f (a :| v)) = (case teq t b of {
              Just Eq   -> geqt b y (spineVal s);
              otherwise -> False
              })
              || findSpine (Fun a t) f
              || findSpine a (toSpine a v)
          spineVal :: Spine a -> a
          spineVal (As v con) = v
          spineVal (Ap f (t :| v)) = spineVal f v