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.Compounds
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 LetStrict b x1) x2)
= case step store x1 of
StepProgress store' x1'
-> StepProgress store' (XLet a (LLet LetStrict b x1') x2)
StepDone
-> StepProgress store (substituteXX b x1 x2)
err -> err
step store (XLet _ (LLet (LetLazy _w) b x1) x2)
= case typeOfExp (configOfProfile evalProfile)
(C.profilePrimKinds evalProfile)
(C.profilePrimTypes evalProfile)
x1
of
Left err -> StepMistyped err
Right t1
-> let (store1, l) = allocBind (Rgn 0) t1 (SThunk x1) store
x1' = xLoc l t1
in StepProgress store1 (substituteXX b x1' x2)
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 :: Type Name -> Maybe (Witness Name)
regionWitnessOfType tt
= case takeTyConApps tt of
Just (TyConWitness TwConGlobal , [r]) -> Just $ wGlobal r
Just (TyConWitness TwConMutable , [r]) -> Just $ wMutable r
Just (TyConWitness TwConConst , [r]) -> Just $ wConst r
Just (TyConWitness TwConLazy , [r]) -> Just $ wLazy r
Just (TyConWitness TwConManifest , [r]) -> Just $ wManifest r
Just (TyConWitness (TwConDistinct n), rs) -> Just $ wDistinct n rs
_ -> Nothing