module DDC.Core.Eval.Step
( StepResult(..)
, force
, step
, isValue
, isWeakValue)
where
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.Compounds
import DDC.Core.Predicates
import DDC.Core.Exp
import DDC.Type.Compounds
import qualified Data.Set as Set
data StepResult
= StepProgress Store (Exp () Name)
| StepDone
| StepStuck
| StepStuckMistyped (Error () Name)
deriving (Show)
force :: Store
-> Exp () Name
-> StepResult
force store xx
| (casts, xx') <- unwrapCasts xx
, XCon _ (UPrim (NameLoc l) _) <- xx'
, 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 primDataDefs xp of
Left err -> StepStuckMistyped err
Right t
-> let Just (bs, xBody) = takeXLamFlags xp
(store', l) = allocBind (Rgn 0) t (SLams bs xBody) store
in StepProgress store' (wrapCasts casts $ XCon () (UPrim (NameLoc l) t))
step store xx
| Just (u, xs) <- takeXConApps xx
, case u of
UPrim NamePrimCon{} _ -> True
UPrim NameInt{} _ -> True
UPrim NameCon{} _ -> True
_ -> False
, UPrim n _ <- u
, Just arity <- arityOfName n
, length xs == arity
, and $ map (isWeakValue store) xs
, Just (store', x') <- stepPrimCon n xs store
= StepProgress store' x'
step store xx
| 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', makeXApps () 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
| 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 (makeXApps () x1 xsArgs')
step store xx
| 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 (makeXApps () 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 primDataDefs x1 of
Left err -> StepStuckMistyped err
Right t1
-> let (store1, l) = allocBind (Rgn 0) t1 (SThunk x1) store
x1' = XCon () (UPrim (NameLoc 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 = [XCon () (UPrim (NameLoc 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 (LLetRegion bRegion bws) x)
| Just uRegion <- takeSubstBoundOfBind bRegion
, (store1, uHandle@(UPrim (NameRgn rgn) _))
<- primNewRegion store
, tHandle <- TCon $ TyConBound uHandle
, bws' <- map (substituteBoundTX uRegion tHandle) bws
, Just wits <- sequence
$ map regionWitnessOfType
$ map typeOfBind bws'
= let
x' = substituteBoundTX uRegion tHandle
$ substituteWXs (zip bws' wits) x
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 nTag lsArgs) <- lookupBind lDiscrim store
, 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 (XCon a (UPrim (NameLoc 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')
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 u' _)
= case takeNameOfBound u' 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 _ (UPrim (NameLoc l) _)
| 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 (u, _xs) <- takeXConApps xx
, UPrim (NameLoc l) _ <- u
, Just SLams{} <- lookupBind l store
-> False
| Just (u, xs) <- takeXConApps xx
, and $ map (isSomeValue weak store) xs
, UPrim n _ <- u
, 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 tt of
TApp (TCon (TyConWitness TwConGlobal)) r -> Just $ wGlobal r
TApp (TCon (TyConWitness TwConMutable)) r -> Just $ wMutable r
TApp (TCon (TyConWitness TwConConst)) r -> Just $ wConst r
TApp (TCon (TyConWitness TwConLazy)) r -> Just $ wLazy r
TApp (TCon (TyConWitness TwConManifest)) r -> Just $ wManifest r
_ -> Nothing