ddc-core-eval-0.2.0.1: DDC/Core/Eval/Step.hs
-- | Single step evalation for the Disciple Core language.
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
-- StepResult -----------------------------------------------------------------
-- | The result of stepping some expression.
data StepResult
-- | Expression progressed to a new state.
= StepProgress Store (Exp () Name)
-- | Expression cannot step and is a (weak) value.
-- We're done already.
| StepDone
-- | Expression cannot step, and is not a (weak) value.
-- The original expression was mistyped,
-- or something is wrong with the interpreter.
| StepStuck
-- | Expression is stuck, and we know for sure it's mistyped.
| StepStuckMistyped (Error () Name)
deriving (Show)
-- force ----------------------------------------------------------------------
-- | Single step a core expression to a value.
--
-- As opposed to `step`, if the provided expression is the location of a
-- Thunk, then the thunk will be forced.
--
force :: Store -- ^ Current store.
-> Exp () Name -- ^ Expression to force.
-> StepResult -- ^ Result of forcing it.
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 -----------------------------------------------------------------------
-- | Single step a code expression to a weak value.
--
-- As opposed to `force`, if the provided expression is the location of a
-- Thunk, then the thunk is not forced.
--
step :: Store -- ^ Current store.
-> Exp () Name -- ^ Expression to step.
-> StepResult -- ^ Result of stepping it.
-- (EvLam)
-- Add abstractions to the heap.
-- We need the type of the expression to attach to the location
-- This fakes the store typing from the formal typing rules.
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))
-- (EvAlloc)
-- Construct some data in the heap.
step store xx
| Just (u, xs) <- takeXConApps xx
, case u of
-- Unit constructors are not allocated into the store.
UPrim (NamePrimCon PrimDaConUnit) _ -> False
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'
-- (EvPrim)
-- Step a primitive operator or constructor defined by the client.
step store xx
| x1@(XVar _ (UPrim p _)) : xs <- takeXApps xx
, Just arity <- arityOfName p
= let
-- TODO: we're not allowing over-applied primops
stepArg i _acc []
| i == arity
, Just (store', x') <- stepPrimOp p xs store
= Right (store', x')
-- The arguments are all values, but the primop didn't step.
| 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'
-- (EvAppArgs)
-- Step the left-most non-wnf argument of a lambda.
step store xx
| x1 : xsArgs <- takeXApps xx
, Just l1 <- takeLocX x1
, Just (Rgn 0, _, SLams bs _xBody) <- lookupRegionTypeBind l1 store
-- See if an arg to any of the lambdas needs to be stepped.
, arity <- length bs
, wnfs <- map (isWeakValue store) xsArgs
, or (take arity $ map not wnfs)
= let -- Step the first non-wnf argument.
-- This should never error, as we took as many args
-- as we had wnf flags.
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')
-- (EvAppSubst)
-- Substitute wnf arguments into an abstraction.
step store xx
| x1 : xsArgs <- takeXApps xx
, (casts, xL1) <- unwrapCasts x1
, Just l1 <- takeLocX xL1
, Just (Rgn 0, _, SLams fbs xBody) <- lookupRegionTypeBind l1 store
-- Take as many wnfs as possible to satisfy binders.
, arity <- length fbs
, (wnfs, nonWnfs) <- span (isWeakValue store) xsArgs
-- If we have any wnfs at all, then we can do a substitution.
, 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)
-- (EvApp1 / EvApp2)
-- Evaluate the components of an application.
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
-- (EvLetStrictStep / EvLetStrictSubst)
-- Substitute in a bound value in a let expression.
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
-- (EvLetLazyAlloc)
-- Allocate a lazy binding in the heap.
step store (XLet _ (LLet (LetLazy _w) b x1) x2)
-- We need the type of the expression to attach to the location
-- This fakes the store typing from the formal typing rules.
= 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)
-- (EvLetRec)
-- Add recursive bindings to the store.
step store (XLet _ (LRec bxs) x2)
= let (bs, xs) = unzip bxs
ts = map typeOfBind bs
-- Allocate new locations in the store to hold the expressions.
(store1, ls) = newLocs (length bs) store
xls = [XCon () (UPrim (NameLoc l) t) | (l, t) <- zip ls ts]
-- Substitute locations into all the bindings.
xs' = map (substituteXXs (zip bs xls)) xs
-- Create store objects for each of the bindings.
mos = map (\x -> case takeXLamFlags x of
Just (fbs', xBody) -> Just $ SLams fbs' xBody
_ -> Nothing)
xs'
-- If this fails then some of the bindings did not have lambdas out the
-- front. We don't support plain value recursion yet.
in case sequence mos of
Nothing -> StepStuck
Just os
-> let -- Add all the objects to the store.
store2 = foldr (\(l, t, o) -> addBind l (Rgn 0) t o) store1
$ zip3 ls ts os
-- Substitute locations into the body expression.
x2' = substituteXXs (zip bs xls) x2
in StepProgress store2 x2'
-- (EvCreateRegion)
-- Create a new region.
step store (XLet a (LLetRegion bRegion bws) x)
| Just uRegion <- takeSubstBoundOfBind bRegion
-- Allocate a new region handle for the bound region.
, (store1, uHandle@(UPrim (NameRgn rgn) _))
<- primNewRegion store
, tHandle <- TCon $ TyConBound uHandle
-- Substitute handle into the witness types.
, bws' <- map (substituteBoundTX uRegion tHandle) bws
-- Build witnesses for each of the witness types.
-- This can fail if the set of witness signatures is malformed.
, Just wits <- sequence
$ map regionWitnessOfType
$ map typeOfBind bws'
= let -- Substitute handle and witnesses into body.
x' = substituteBoundTX uRegion tHandle
$ substituteWXs (zip bws' wits) x
isGlobalBind b
= case typeOfBind b of
TApp (TCon (TyConWitness TwConGlobal)) _
-> True
_ -> False
-- Set region to global if there is a witness for it.
store2 = if or $ map isGlobalBind bws
then setGlobal rgn store1
else store1
in StepProgress store2 (XLet a (LWithRegion uHandle) x')
-- Region binder was a wildcard, so we can't create the region handle.
-- No witness sigs can be in the set, because any sig would need
-- to reference the region variable. Just create a dummy region in the
-- store to simulate what would happen if there was a real binder.
| otherwise
= let (store', _) = primNewRegion store
in StepProgress store' x
-- (EvEjectRegion)
-- Eject completed value from the region context, and delete the region.
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
-- (EvWithRegion)
-- Reduction within a region context.
step store (XLet a (LWithRegion uRegion) x)
= case step store x of
StepProgress store' x'
-> StepProgress store' (XLet a (LWithRegion uRegion) x')
err -> err
-- (EvCaseStep / EvCaseMatch)
-- Case branching.
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
-- (EvPurifyEject)
-- Eject values from purify casts as there are no more effects to be had.
step store (XCast _ (CastPurify _) x)
| isWeakValue store x
= StepProgress store x
-- (EvCast)
-- Evaluate under casts.
step store (XCast a cc x)
= case step store x of
StepProgress store' x'
-> StepProgress store' (XCast a cc x')
err -> err
-- (Done/Stuck)
-- Either already a value, or expression is stuck.
step store xx
| isWeakValue store xx = StepDone
| otherwise = StepStuck
-- Casts ----------------------------------------------------------------------
-- Unwrap casts from the front of an expression.
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)
-- Wrap casts around an expression.
wrapCasts :: [Cast n] -> Exp () n -> Exp () n
wrapCasts cc xx
= case cc of
[] -> xx
c : cs -> XCast () c (wrapCasts cs xx)
-- Alternatives ---------------------------------------------------------------
-- | See if a constructor tag matches a case alternative.
tagMatchesAlt :: Name -> Alt a Name -> Bool
tagMatchesAlt n (AAlt p _)
= tagMatchesPat n p
-- | See if a constructor tag matches a pattern.
tagMatchesPat :: Name -> Pat Name -> Bool
tagMatchesPat _ PDefault = True
tagMatchesPat n (PData u' _)
= case takeNameOfBound u' of
Just n' -> n == n'
_ -> False
-- isValue ----------------------------------------------------------------
-- | Check if an expression is a value.
-- Values can't be progressed any further, with either `force` or `step`.
isValue :: Store -> Exp a Name -> Bool
isValue store xx
= isSomeValue False store xx
-- | Check if an expression is a weak values.
-- These are all the values, and locations that point to thunks.
--
-- Weak values can be progressed with `force`, but not `step`.
isWeakValue :: Store -> Exp a Name -> Bool
isWeakValue store xx
= isSomeValue True store xx
-- | Check if an expression is a weak value.
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
-- Plain lambdas aren't weak values because we always add them
-- to the store. The resulting store location is then a value.
XLAM{} -> False
XLam{} -> False
XLet{} -> False
XCase{} -> False
XCast _ (CastPurify _) _
-> False
XCast _ _ x
-> isSomeValue weak store x
XType{} -> True
XWitness{} -> True
XApp _ x1 x2
-- Application if a primop to enough args is not wnf.
| Just (n, xs) <- takeXPrimApps xx
, and $ map (isSomeValue weak store) xs
, Just a <- arityOfName n
, length xs >= a
-> False
-- Application of a lambda in the store is not wnf.
| Just (u, _xs) <- takeXConApps xx
, UPrim (NameLoc l) _ <- u
, Just SLams{} <- lookupBind l store
-> False
-- Application of a data constructor to enough args is not wnf.
| Just (u, xs) <- takeXConApps xx
, and $ map (isSomeValue weak store) xs
, UPrim n _ <- u
, Just a <- arityOfName n
, length xs >= a
-> False
-- Application of some other expression,
-- maybe an under-applied primop or data constructor.
| otherwise
-> isSomeValue weak store x1
&& isSomeValue weak store x2
-- | Get the region witness corresponding to one of the witness types that are
-- permitted in a letregion.
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