module DDC.Core.Eval.Step
( StepResult(..)
, force
, step
, isValue
, isWeakValue)
where
import DDC.Core.Eval.Profile
import DDC.Core.Eval.Store
import DDC.Core.Eval.Name
import DDC.Core.Eval.Prim
import DDC.Core.Eval.Env
import DDC.Core.Eval.Compounds
import DDC.Core.Transform.SubstituteWX
import DDC.Core.Transform.SubstituteXX
import DDC.Core.Transform.SubstituteTX
import DDC.Core.Check
import DDC.Core.Predicates
import DDC.Core.Exp
import qualified DDC.Core.Fragment as C
import qualified Data.Set as Set
data StepResult
= StepProgress Store (Exp () Name)
| StepDone
| StepStuck
| StepMistyped (Error () Name)
deriving (Show)
force :: Store
-> Exp () Name
-> StepResult
force store xx
| (casts, xx') <- unwrapCasts xx
, XCon _ dc <- xx'
, Just (NameLoc l) <- takeNameOfDaCon dc
, Just (rgn, t, SThunk x) <- lookupRegionTypeBind l store
= case force store x of
StepProgress store' x'
-> let store2 = addBind l rgn t (SThunk x') store'
in StepProgress store2 (wrapCasts casts xx)
StepDone
-> StepProgress store x
err -> err
| otherwise
= step store xx
step :: Store
-> Exp () Name
-> StepResult
step store xx
| (casts, xp) <- unwrapCasts xx
, isLambdaX xp
= case typeOfExp
(configOfProfile evalProfile)
(C.profilePrimKinds evalProfile)
(C.profilePrimTypes evalProfile)
xp
of Left err -> StepMistyped err
Right t
-> let Just (bs, xBody) = takeXLamFlags xp
(store', l) = allocBind (Rgn 0) t (SLams bs xBody) store
x' = xLoc l t
in StepProgress store' (wrapCasts casts x')
step store xx
| Just (dc, xs) <- takeXConApps xx
, and $ map (isWeakValue store) xs
, Just (store', x') <- stepPrimCon dc xs store
= StepProgress store' x'
step store xx
| Just (x1@(XVar _ (UPrim p _)), xs) <- takeXApps xx
, Just arity <- arityOfName p
= let
stepArg i _acc []
| i == arity
, Just (store', x') <- stepPrimOp p xs store
= Right (store', x')
| otherwise
= Left StepStuck
stepArg i acc (ax:axs)
= case force store ax of
StepProgress store' x'
-> Right (store', xApps () x1 (reverse acc ++ (x' : axs)))
StepDone
-> case stepArg (i + 1) (ax : acc) axs of
Left err -> Left err
result -> result
err -> Left err
in case stepArg 0 [] xs of
Left err -> err
Right (store', x') -> StepProgress store' x'
step store xx
| Just (x1, xsArgs) <- takeXApps xx
, Just l1 <- takeLocX x1
, Just (Rgn 0, _, SLams bs _xBody) <- lookupRegionTypeBind l1 store
, arity <- length bs
, wnfs <- map (isWeakValue store) xsArgs
, or (take arity $ map not wnfs)
= let
stepArg _ []
= error "stepArg: no more args"
stepArg [] xs
= Right (store, xs)
stepArg (True:ws) (x:xs)
= case stepArg ws xs of
Right (store', xs') -> Right (store', x : xs')
Left err -> Left err
stepArg (False:_) (x:xs)
= case step store x of
StepProgress store' x' -> Right (store', x' : xs)
err -> Left err
in case stepArg wnfs xsArgs of
Left err -> err
Right (store2, xsArgs')
-> StepProgress store2 (xApps () x1 xsArgs')
step store xx
| Just (x1, xsArgs) <- takeXApps xx
, (casts, xL1) <- unwrapCasts x1
, Just l1 <- takeLocX xL1
, Just (Rgn 0, _, SLams fbs xBody) <- lookupRegionTypeBind l1 store
, arity <- length fbs
, (wnfs, nonWnfs) <- span (isWeakValue store) xsArgs
, not $ null wnfs
= let argsToSubst = take arity wnfs
argsOverApplied = drop (length argsToSubst) wnfs
argsLeftover = argsOverApplied ++ nonWnfs
bs = map snd fbs
bsToSubst = take (length argsToSubst) bs
bsLeftover = drop (length bsToSubst) fbs
xResult = substituteXArgs (zip bsToSubst argsToSubst)
$ makeXLamFlags () bsLeftover xBody
in StepProgress store
$ wrapCasts casts (xApps () xResult argsLeftover)
step store (XApp a x1 x2)
| (casts, x1p) <- unwrapCasts x1
= case force store x1p of
StepProgress store' x1p'
-> StepProgress store' (XApp a (wrapCasts casts x1p') x2)
StepDone
-> case step store x2 of
StepProgress store' x2'
-> StepProgress store' (XApp a x1 x2')
err -> err
err -> err
step store (XLet a (LLet b x1) x2)
= case step store x1 of
StepProgress store' x1'
-> StepProgress store' (XLet a (LLet b x1') x2)
StepDone
-> StepProgress store (substituteXX b x1 x2)
err -> err
step store (XLet _ (LRec bxs) x2)
= let (bs, xs) = unzip bxs
ts = map typeOfBind bs
(store1, ls) = newLocs (length bs) store
xls = [xLoc l t | (l, t) <- zip ls ts]
xs' = map (substituteXXs (zip bs xls)) xs
mos = map (\x -> case takeXLamFlags x of
Just (fbs', xBody) -> Just $ SLams fbs' xBody
_ -> Nothing)
xs'
in case sequence mos of
Nothing -> StepStuck
Just os
-> let
store2 = foldr (\(l, t, o) -> addBind l (Rgn 0) t o) store1
$ zip3 ls ts os
x2' = substituteXXs (zip bs xls) x2
in StepProgress store2 x2'
step store (XLet a (LLetRegions bRegions bws) x)
| uRegions <- takeSubstBoundsOfBinds bRegions
, (store1, uHandle@(UPrim (NameRgn rgn) _))
<- primNewRegion store
, tHandle <- TCon $ TyConBound uHandle kRegion
, bws' <- concatMap
(\uRegion -> map (substituteBoundTX uRegion tHandle) bws)
uRegions
, Just wits <- sequence
$ map (regionWitnessOfType ())
$ map typeOfBind bws'
= let
substituteBoundTX' xx u
= substituteBoundTX u tHandle xx
x' = substituteWXs (zip bws' wits) x
x'' = foldl substituteBoundTX' x' uRegions
isGlobalBind b
= case typeOfBind b of
TApp (TCon (TyConWitness TwConGlobal)) _
-> True
_ -> False
store2 = if or $ map isGlobalBind bws
then setGlobal rgn store1
else store1
in StepProgress store2 (XLet a (LWithRegion uHandle) x'')
| otherwise
= let (store', _) = primNewRegion store
in StepProgress store' x
step store (XLet _ (LWithRegion r@(UPrim (NameRgn rgn) _)) x)
| isWeakValue store x
, Set.member rgn (storeGlobal store)
= StepProgress store x
| isWeakValue store x
, Just store' <- primDelRegion r store
= StepProgress store' x
step store (XLet a (LWithRegion uRegion) x)
= case step store x of
StepProgress store' x'
-> StepProgress store' (XLet a (LWithRegion uRegion) x')
err -> err
step store (XCase a xDiscrim alts)
= case force store xDiscrim of
StepProgress store' xDiscrim'
-> StepProgress store' (XCase a xDiscrim' alts)
StepDone
| (casts, xDiscrim') <- unwrapCasts xDiscrim
, Just lDiscrim <- takeLocX xDiscrim'
, Just (SObj dc lsArgs) <- lookupBind lDiscrim store
, Just nTag <- takeNameOfDaCon dc
, Just tsArgs <- sequence $ map (\l -> lookupTypeOfLoc l store) lsArgs
, AAlt pat xBody : _ <- filter (tagMatchesAlt nTag) alts
-> case pat of
PDefault
-> StepProgress store xBody
PData _ bsArgs
| bxsArgs <- [ (b, wrapCasts casts (xLoc l t))
| l <- lsArgs
| t <- tsArgs
| b <- bsArgs]
-> StepProgress store
(substituteXXs bxsArgs xBody)
| otherwise
-> StepStuck
err -> err
step store (XCast _ (CastPurify _) x)
| isWeakValue store x
= StepProgress store x
step store (XCast a cc x)
= case step store x of
StepProgress store' x'
-> StepProgress store' (XCast a cc x')
StepDone
-> case cc of
CastWeakenEffect _
-> StepProgress store x
CastWeakenClosure _
-> StepProgress store x
_ -> StepDone
err -> err
step store xx
| isWeakValue store xx = StepDone
| otherwise = StepStuck
unwrapCasts :: Exp () n -> ([Cast () n], Exp () n)
unwrapCasts xx
= case xx of
XCast _ c x
-> let (cs, x') = unwrapCasts x
in (c : cs, x')
_ -> ([], xx)
wrapCasts :: [Cast () n] -> Exp () n -> Exp () n
wrapCasts cc xx
= case cc of
[] -> xx
c : cs -> XCast () c (wrapCasts cs xx)
tagMatchesAlt :: Name -> Alt a Name -> Bool
tagMatchesAlt n (AAlt p _)
= tagMatchesPat n p
tagMatchesPat :: Name -> Pat Name -> Bool
tagMatchesPat _ PDefault = True
tagMatchesPat n (PData dc _)
= case takeNameOfDaCon dc of
Just n' -> n == n'
_ -> False
isValue :: Store -> Exp a Name -> Bool
isValue store xx
= isSomeValue False store xx
isWeakValue :: Store -> Exp a Name -> Bool
isWeakValue store xx
= isSomeValue True store xx
isSomeValue :: Bool -> Store -> Exp a Name -> Bool
isSomeValue weak store xx
= case xx of
XVar{} -> True
XCon _ dc
| Just (NameLoc l) <- takeNameOfDaCon dc
, Just SThunk{} <- lookupBind l store
-> weak
XCon{} -> True
XLAM{} -> False
XLam{} -> False
XLet{} -> False
XCase{} -> False
XCast _ (CastPurify _) _
-> False
XCast _ _ x
-> isSomeValue weak store x
XType{} -> True
XWitness{} -> True
XApp _ x1 x2
| Just (n, xs) <- takeXPrimApps xx
, and $ map (isSomeValue weak store) xs
, Just a <- arityOfName n
, length xs >= a
-> False
| Just (dc, _xs) <- takeXConApps xx
, Just (NameLoc l) <- takeNameOfDaCon dc
, Just SLams{} <- lookupBind l store
-> False
| Just (dc, xs) <- takeXConApps xx
, and $ map (isSomeValue weak store) xs
, Just n <- takeNameOfDaCon dc
, Just a <- arityOfName n
, length xs >= a
-> False
| otherwise
-> isSomeValue weak store x1
&& isSomeValue weak store x2
regionWitnessOfType :: a -> Type Name -> Maybe (Witness a Name)
regionWitnessOfType a tt
= case takeTyConApps tt of
Just (TyConWitness TwConGlobal , [r]) -> Just $ wGlobal a r
Just (TyConWitness TwConMutable , [r]) -> Just $ wMutable a r
Just (TyConWitness TwConConst , [r]) -> Just $ wConst a r
Just (TyConWitness TwConLazy , [r]) -> Just $ wLazy a r
Just (TyConWitness TwConManifest , [r]) -> Just $ wManifest a r
Just (TyConWitness (TwConDistinct n), rs) -> Just $ wDistinct a n rs
_ -> Nothing