module DDC.Type.Equiv
(equivT)
where
import DDC.Type.Exp
import DDC.Type.Compounds
import DDC.Type.Transform.Crush
import DDC.Type.Transform.Trim
import DDC.Base.Pretty
import Data.Maybe
import qualified DDC.Type.Sum as Sum
equivT :: (Ord n, Pretty n) => Type n -> Type n -> Bool
equivT t1 t2
= equivT' [] 0 [] 0 t1 t2
equivT' :: (Ord n, Pretty n)
=> [Bind n] -> Int
-> [Bind n] -> Int
-> Type n -> Type n
-> Bool
equivT' stack1 depth1 stack2 depth2 t1 t2
= let t1' = unpackSumT $ crushSomeT t1
t2' = unpackSumT $ crushSomeT t2
in case (t1', t2') of
(TVar u1, TVar u2)
| u1 == u2 -> True
| depth1 == depth2
, Just (ix1, t1a) <- getBindType stack1 u1
, Just (ix2, t2a) <- getBindType stack2 u2
, ix1 == ix2
-> equivT' stack1 depth1 stack2 depth2 t1a t2a
(TCon tc1, TCon tc2)
-> tc1 == tc2
(TForall b11 t12, TForall b21 t22)
| equivT (typeOfBind b11) (typeOfBind b21)
-> equivT' (b11 : stack1) (depth1 + 1)
(b21 : stack2) (depth2 + 1)
t12 t22
(TApp t11 t12, TApp t21 t22)
-> equivT' stack1 depth1 stack2 depth2 t11 t21
&& equivT' stack1 depth1 stack2 depth2 t12 t22
(TSum ts1, TSum ts2)
-> let ts1' = Sum.toList ts1
ts2' = Sum.toList ts2
equiv = equivT' stack1 depth1 stack2 depth2
checkFast = and $ zipWith equiv ts1' ts2'
checkSlow = and [ or (map (equiv t1c) ts2') | t1c <- ts1' ]
&& and [ or (map (equiv t2c) ts1') | t2c <- ts2' ]
in (length ts1' == length ts2')
&& (checkFast || checkSlow)
(_, _) -> False
unpackSumT :: Type n -> Type n
unpackSumT (TSum ts)
| [t] <- Sum.toList ts = t
unpackSumT tt = tt
crushSomeT :: (Ord n, Pretty n) => Type n -> Type n
crushSomeT tt
= case tt of
(TApp (TCon tc) _)
-> case tc of
TyConSpec TcConDeepRead -> crushEffect tt
TyConSpec TcConDeepWrite -> crushEffect tt
TyConSpec TcConDeepAlloc -> crushEffect tt
TyConSpec TcConDeepUse -> fromMaybe tt (trimClosure tt)
TyConWitness TwConDeepGlobal -> crushEffect tt
_ -> tt
_ -> tt
getBindType :: Eq n => [Bind n] -> Bound n -> Maybe (Int, Type n)
getBindType bs' u
= go 0 bs'
where go n (BName n1 t : bs)
| UName n2 _ <- u
, n1 == n2 = Just (n, t)
| otherwise = go (n + 1) bs
go n (BAnon t : bs)
| UIx i _ <- u
, i == 0 = Just (n, t)
| UIx i _ <- u
, i < 0 = Nothing
| otherwise = go (n + 1) bs
go n (BNone _ : bs)
= go (n + 1) bs
go _ [] = Nothing