module DDC.Core.Call
(
Cons (..)
, isConsType
, isConsValue
, isConsBox
, takeCallConsFromExp
, takeCallConsFromType
, splitStdCallCons
, takeStdCallConsFromTypeArity
, Elim (..)
, isElimType
, isElimValue
, isElimRun
, takeCallElim
, applyElim
, splitStdCallElims
, elimForCons
, dischargeConsWithElims
, dischargeTypeWithElims)
where
import DDC.Core.Exp.Annot
import DDC.Type.Transform.SubstituteT
data Cons n
=
ConsType (Bind n)
| ConsValue (Type n)
| ConsBox
deriving (Show)
isConsType :: Cons n -> Bool
isConsType cc
= case cc of
ConsType{} -> True
_ -> False
isConsValue :: Cons n -> Bool
isConsValue cc
= case cc of
ConsValue{} -> True
_ -> False
isConsBox :: Cons n -> Bool
isConsBox cc
= case cc of
ConsBox{} -> True
_ -> False
takeCallConsFromExp :: Exp a n -> [Cons n]
takeCallConsFromExp xx
= case xx of
XLAM _ b x
-> ConsType b : takeCallConsFromExp x
XLam _ b x
-> let t = typeOfBind b
in ConsValue t : takeCallConsFromExp x
XCast _ CastBox x
-> ConsBox : takeCallConsFromExp x
_ -> []
takeCallConsFromType :: Type n -> [Cons n]
takeCallConsFromType tt
| TForall bParam tBody <- tt
= ConsType bParam : takeCallConsFromType tBody
| Just (tParam, tResult) <- takeTFun tt
= ConsValue tParam : takeCallConsFromType tResult
| Just (_, tResult) <- takeTSusp tt
= ConsBox : takeCallConsFromType tResult
| otherwise
= []
splitStdCallCons
:: [Cons n]
-> Maybe ([Cons n], [Cons n], [Cons n])
splitStdCallCons cs
= eatTypes [] cs
where
eatTypes accTs (e@ConsType{} : es)
= eatTypes (e : accTs) es
eatTypes accTs es
= eatValues (reverse accTs) [] es
eatValues accTs accVs (e@ConsValue{} : es)
= eatValues accTs (e : accVs) es
eatValues accTs accVs es
= eatRuns accTs (reverse accVs) [] es
eatRuns accTs accVs accRs (e@ConsBox{} : es)
= eatRuns accTs accVs (e : accRs) es
eatRuns accTs accVs accRs []
= Just (accTs, accVs, reverse accRs)
eatRuns _accTs _accVs _accRs _
= Nothing
takeStdCallConsFromTypeArity
:: Type n
-> Int
-> Int
-> Int
-> Maybe [Cons n]
takeStdCallConsFromTypeArity tt0 nTypes0 nValues0 nBoxes0
= eatTypes [] tt0 nTypes0
where
eatTypes !accTs !tt !nTypes
| nTypes > 0
= case tt of
TForall b tBody
-> eatTypes (ConsType b : accTs) tBody (nTypes 1)
_ -> Nothing
| otherwise
= eatValues (reverse accTs) [] tt nValues0
eatValues !accTs !accVs !tt !nValues
| nValues > 0
= case takeTFun tt of
Just (t1, t2)
-> eatValues accTs (ConsValue t1 : accVs) t2 (nValues 1)
_ -> Nothing
| otherwise
= eatBoxes accTs (reverse accVs) [] tt nBoxes0
eatBoxes !accTs !accVs !accBs tt nBoxes
| nBoxes > 0
= case takeTSusp tt of
Just (_eff, tBody)
-> eatBoxes accTs accVs (ConsBox : accBs) tBody (nBoxes 1)
_ -> Nothing
| otherwise
= return (accTs ++ accVs ++ reverse accBs)
data Elim a n
=
ElimType a a (Type n)
| ElimValue a (Exp a n)
| ElimRun a
deriving (Show)
isElimType :: Elim a n -> Bool
isElimType ee
= case ee of
ElimType{} -> True
_ -> False
isElimValue :: Elim a n -> Bool
isElimValue ee
= case ee of
ElimValue{} -> True
_ -> False
isElimRun :: Elim a n -> Bool
isElimRun ee
= case ee of
ElimRun{} -> True
_ -> False
applyElim :: Exp a n -> Elim a n -> Exp a n
applyElim xx e
= case e of
ElimType a at t -> XApp a xx (XType at t)
ElimValue a x -> XApp a xx x
ElimRun a -> XCast a CastRun xx
takeCallElim :: Exp a n -> (Exp a n, [Elim a n])
takeCallElim xx
= case xx of
XApp a x1 (XType at t2)
-> let (xF, xArgs) = takeCallElim x1
in (xF, xArgs ++ [ElimType a at t2])
XApp a x1 x2
-> let (xF, xArgs) = takeCallElim x1
in (xF, xArgs ++ [ElimValue a x2])
XCast a CastRun x1
-> let (xF, xArgs) = takeCallElim x1
in (xF, xArgs ++ [ElimRun a])
_ -> (xx, [])
splitStdCallElims
:: [Elim a n]
-> Maybe ([Elim a n], [Elim a n], [Elim a n])
splitStdCallElims ee
= eatTypes [] ee
where
eatTypes accTs (e@ElimType{} : es)
= eatTypes (e : accTs) es
eatTypes accTs es
= eatValues (reverse accTs) [] es
eatValues accTs accVs (e@ElimValue{} : es)
= eatValues accTs (e : accVs) es
eatValues accTs accVs es
= eatRuns accTs (reverse accVs) [] es
eatRuns accTs accVs accRs (e@ElimRun{} : es)
= eatRuns accTs accVs (e : accRs) es
eatRuns accTs accVs accRs []
= Just (accTs, accVs, reverse accRs)
eatRuns _accTs _accVs _accRs _
= Nothing
elimForCons :: Elim a n -> Cons n -> Bool
elimForCons e c
= case (e, c) of
(ElimType{}, ConsType{}) -> True
(ElimValue{}, ConsValue{}) -> True
(ElimRun{}, ConsBox{}) -> True
_ -> False
dischargeConsWithElims
:: Ord n
=> [Cons n]
-> [Elim a n]
-> ([Cons n], [Elim a n])
dischargeConsWithElims (c : cs) (e : es)
= case (c, e) of
(ConsType b1, ElimType _ _ t2)
-> dischargeConsWithElims
(map (instantiateConsT b1 t2) cs)
es
(ConsValue _t1, ElimValue _ _x2)
-> dischargeConsWithElims cs es
(ConsBox, ElimRun _)
-> dischargeConsWithElims cs es
_ -> (c : cs, e : es)
dischargeConsWithElims cs es
= (cs, es)
instantiateConsT :: Ord n => Bind n -> Type n -> Cons n -> Cons n
instantiateConsT b t cc
= case cc of
ConsType{} -> cc
ConsValue t' -> ConsValue (substituteT b t t')
ConsBox{} -> cc
dischargeTypeWithElims
:: Ord n
=> Type n
-> [Elim a n]
-> Maybe (Type n)
dischargeTypeWithElims tt (ElimType _ _ tArg : es)
| TForall b tBody <- tt
= dischargeTypeWithElims
(substituteT b tArg tBody)
es
dischargeTypeWithElims tt (ElimValue _ _xArg : es)
| Just (_tParam, tResult) <- takeTFun tt
= dischargeTypeWithElims tResult es
dischargeTypeWithElims tt (ElimRun _ : es)
| Just (_, tBody) <- takeTSusp tt
= dischargeTypeWithElims tBody es
dischargeTypeWithElims tt []
= Just tt
dischargeTypeWithElims _tt _es
= Nothing