module DDC.Type.Equiv
( equivT
, equivWithBindsT
, equivTyCon
, crushSomeT
, crushEffect)
where
import DDC.Type.Predicates
import DDC.Type.Compounds
import DDC.Type.Bind
import DDC.Type.Exp
import DDC.Type.Env (TypeEnv)
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Sum as Sum
import qualified Data.Map as Map
equivT :: Ord n => Type n -> Type n -> Bool
equivT t1 t2
= equivWithBindsT [] [] t1 t2
equivWithBindsT
:: Ord n
=> [Bind n]
-> [Bind n]
-> Type n
-> Type n
-> Bool
equivWithBindsT stack1 stack2 t1 t2
= let t1' = unpackSumT $ crushSomeT Env.empty t1
t2' = unpackSumT $ crushSomeT Env.empty t2
in case (t1', t2') of
(TVar u1, TVar u2)
| Nothing <- getBindType stack1 u1
, Nothing <- getBindType stack2 u2
, u1 == u2 -> checkBounds u1 u2 True
| Just (ix1, t1a) <- getBindType stack1 u1
, Just (ix2, t2a) <- getBindType stack2 u2
, ix1 == ix2
-> checkBounds u1 u2
$ equivWithBindsT stack1 stack2 t1a t2a
| otherwise
-> checkBounds u1 u2
$ False
(TCon tc1, TCon tc2)
-> equivTyCon tc1 tc2
(TForall b11 t12, TForall b21 t22)
| equivT (typeOfBind b11) (typeOfBind b21)
-> equivWithBindsT
(b11 : stack1)
(b21 : stack2)
t12 t22
(TApp t11 t12, TApp t21 t22)
-> equivWithBindsT stack1 stack2 t11 t21
&& equivWithBindsT stack1 stack2 t12 t22
(TSum ts1, TSum ts2)
-> let ts1' = Sum.toList ts1
ts2' = Sum.toList ts2
checkFast = and $ zipWith (equivWithBindsT stack1 stack2) ts1' ts2'
checkSlow = and [ or (map (equivWithBindsT stack1 stack2 t1c) ts2')
| t1c <- ts1' ]
&& and [ or (map (equivWithBindsT stack2 stack1 t2c) ts1')
| t2c <- ts2' ]
in (length ts1' == length ts2')
&& (checkFast || checkSlow)
(_, _) -> False
checkBounds :: Eq n => Bound n -> Bound n -> a -> a
checkBounds u1 u2 x
= case (u1, u2) of
(UName n2, UPrim n1 _)
| n1 == n2 -> die
(UPrim n1 _, UName n2)
| n1 == n2 -> die
_ -> x
where
die = error $ unlines
[ "DDC.Type.Equiv"
, " Found a primitive and non-primitive bound variable with the same name."]
unpackSumT :: Type n -> Type n
unpackSumT (TSum ts)
| [t] <- Sum.toList ts = t
unpackSumT tt = tt
equivTyCon :: Eq n => TyCon n -> TyCon n -> Bool
equivTyCon tc1 tc2
= case (tc1, tc2) of
(TyConBound u1 _, TyConBound u2 _) -> u1 == u2
_ -> tc1 == tc2
crushSomeT :: Ord n => TypeEnv n -> Type n -> Type n
crushSomeT caps tt
=
case tt of
TApp (TCon tc) _
-> case tc of
TyConSpec TcConDeepRead -> crushEffect caps tt
TyConSpec TcConDeepWrite -> crushEffect caps tt
TyConSpec TcConDeepAlloc -> crushEffect caps tt
_ -> tt
_ -> tt
crushEffect
:: Ord n
=> TypeEnv n
-> Effect n
-> Effect n
crushEffect caps tt
=
case tt of
TVar{} -> tt
TCon{} -> tt
TForall b t
-> TForall b $ crushEffect caps t
TSum ts
-> TSum
$ Sum.fromList (Sum.kindOfSum ts)
$ map (crushEffect caps)
$ Sum.toList ts
TApp{}
| or [equivT tt t | (_, t) <- Map.toList $ Env.envMap caps]
-> tSum kEffect []
TApp t1 t2
| Just (TyConSpec TcConHeadRead, [t]) <- takeTyConApps tt
-> case takeTyConApps t of
Just (TyConBound _ k, (tR : _))
| (k1 : _, _) <- takeKFuns k
, isRegionKind k1
-> tRead tR
Just (TyConSpec TcConUnit, [])
-> tBot kEffect
Just (TyConBound _ _, _)
-> tBot kEffect
_ -> tt
| Just (TyConSpec TcConDeepRead, [t]) <- takeTyConApps tt
-> case takeTyConApps t of
Just (TyConBound _ k, ts)
| (ks, _) <- takeKFuns k
, length ks == length ts
, Just effs <- sequence $ zipWith makeDeepRead ks ts
-> crushEffect caps $ TSum $ Sum.fromList kEffect effs
_ -> tt
| Just (TyConSpec TcConDeepWrite, [t]) <- takeTyConApps tt
-> case takeTyConApps t of
Just (TyConBound _ k, ts)
| (ks, _) <- takeKFuns k
, length ks == length ts
, Just effs <- sequence $ zipWith makeDeepWrite ks ts
-> crushEffect caps $ TSum $ Sum.fromList kEffect effs
_ -> tt
| Just (TyConSpec TcConDeepAlloc, [t]) <- takeTyConApps tt
-> case takeTyConApps t of
Just (TyConBound _ k, ts)
| (ks, _) <- takeKFuns k
, length ks == length ts
, Just effs <- sequence $ zipWith makeDeepAlloc ks ts
-> crushEffect caps $ TSum $ Sum.fromList kEffect effs
_ -> tt
| otherwise
-> TApp (crushEffect caps t1) (crushEffect caps t2)
makeDeepRead :: Kind n -> Type n -> Maybe (Effect n)
makeDeepRead k t
| isRegionKind k = Just $ tRead t
| isDataKind k = Just $ tDeepRead t
| isClosureKind k = Just $ tBot kEffect
| isEffectKind k = Just $ tBot kEffect
| otherwise = Nothing
makeDeepWrite :: Kind n -> Type n -> Maybe (Effect n)
makeDeepWrite k t
| isRegionKind k = Just $ tWrite t
| isDataKind k = Just $ tDeepWrite t
| isClosureKind k = Just $ tBot kEffect
| isEffectKind k = Just $ tBot kEffect
| otherwise = Nothing
makeDeepAlloc :: Kind n -> Type n -> Maybe (Effect n)
makeDeepAlloc k t
| isRegionKind k = Just $ tAlloc t
| isDataKind k = Just $ tDeepAlloc t
| isClosureKind k = Just $ tBot kEffect
| isEffectKind k = Just $ tBot kEffect
| otherwise = Nothing