module DDC.Type.Transform.Crush
( crushSomeT
, crushEffect )
where
import DDC.Type.Predicates
import DDC.Type.Compounds
import DDC.Type.Transform.Trim
import DDC.Type.Exp
import qualified DDC.Type.Sum as Sum
import Data.Maybe
crushSomeT :: Ord 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
crushEffect :: Ord n => Effect n -> Effect n
crushEffect tt
=
case tt of
TVar{} -> tt
TCon{} -> tt
TForall b t
-> TForall b (crushEffect t)
TSum ts
-> TSum
$ Sum.fromList (Sum.kindOfSum ts)
$ map crushEffect
$ Sum.toList ts
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 $ 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 $ 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 $ TSum $ Sum.fromList kEffect effs
_ -> tt
| Just (TyConWitness TwConDeepGlobal, [t]) <- takeTyConApps tt
-> case takeTyConApps t of
Just (TyConBound _ k, ts)
| (ks, _) <- takeKFuns k
, length ks == length ts
, Just props <- sequence $ zipWith makeDeepGlobal ks ts
-> crushEffect $ TSum $ Sum.fromList kWitness props
_ -> tt
| otherwise
-> TApp (crushEffect t1) (crushEffect 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
makeDeepGlobal :: Kind n -> Type n -> Maybe (Type n)
makeDeepGlobal k t
| isRegionKind k = Just $ tGlobal t
| isDataKind k = Just $ tDeepGlobal t
| isClosureKind k = Nothing
| isEffectKind k = Just $ tBot kEffect
| otherwise = Nothing