-----------------------------------------------------------------------------
-- |
-- 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