ddc-core-eval-0.4.1.3: DDC/Core/Eval/Prim.hs
-- | Single step evaluation of primitive operators and constructors.
---
-- This should implements the proper operational semantics of the core language,
-- so we're careful to check all premises of the evaluation rules are satisfied.
module DDC.Core.Eval.Prim
( stepPrimCon
, stepPrimOp
, primNewRegion
, primDelRegion)
where
import DDC.Core.Eval.Compounds
import DDC.Core.Eval.Store
import DDC.Core.Eval.Name
import DDC.Core.Exp
import qualified DDC.Core.Eval.Store as Store
-------------------------------------------------------------------------------
-- | Step a primitive constructor, which allocates an object in the store.
stepPrimCon
:: DaCon Name -- ^ Data constructor to evaluate.
-> [Exp () Name] -- ^ Arguments to constructor.
-> Store -- ^ Current store.
-> Maybe ( Store
, Exp () Name) -- ^ New store and result expression,
-- if the operator steps, otherwise `Nothing`.
-- Redirect the unit constructor.
-- All unit values point to the same object in the store.
stepPrimCon dc xsArgs store
| DaConUnit <- dc
, [] <- xsArgs
= Just ( store
, xLoc locUnit tUnit )
stepPrimCon dc xsArgs store
------ Alloction of Ints ----------------------------------------
| Just _ <- takeIntDC dc
, [xR, xUnit'] <- xsArgs
-- unpack the args
, XType _ tR <- xR
, Just rgn <- takeHandleT tR
, isUnitOrLocX xUnit'
-- the store must contain the region we're going to allocate into.
, Store.hasRgn store rgn
-- add the binding to the store.
, (store1, l) <- Store.allocBind rgn
(tInt tR) (SObj dc []) store
= Just ( store1
, xLoc l (tInt tR))
------ Handle Pair specially until we have general data types --
| Just (NamePrimCon PrimDaConPr) <- takeNameOfDaCon dc
, [xR, xA, xB, x1, x2] <- xsArgs
-- unpack the args
, XType _ tR <- xR
, Just rgn <- takeHandleT tR
, XType _ tA <- xA
, XType _ tB <- xB
, Just l1 <- takeLocX x1
, Just l2 <- takeLocX x2
-- the store must contain the region we're going to allocate into.
, Store.hasRgn store rgn
-- add the binding to the store
, (store1, l) <- Store.allocBind rgn
(tPair tR tA tB) (SObj dc [l1, l2]) store
= Just ( store1
, xLoc l (tPair tR tA tB))
---- Handle Nil and Cons specially until we have general data types.
| Just (NamePrimCon PrimDaConNil) <- takeNameOfDaCon dc
, [xR, xA, xUnit'] <- xsArgs
-- unpack the args
, XType _ tR <- xR
, Just rgn <- takeHandleT tR
, XType _ tA <- xA
, isUnitOrLocX xUnit'
-- the store must contain the region we're going to allocate into.
, Store.hasRgn store rgn
-- add the binding to the store
, (store1, l) <- Store.allocBind rgn
(tList tR tA) (SObj dc []) store
= Just ( store1
, xLoc l (tList tR tA))
| Just (NamePrimCon PrimDaConCons) <- takeNameOfDaCon dc
, [xR, xA, xHead, xTail] <- xsArgs
-- unpack the args
, XType _ tR <- xR
, Just rgn <- takeHandleT tR
, XType _ tA <- xA
, Just lHead <- takeLocX xHead
, Just lTail <- takeLocX xTail
-- the store must contain the region we're going to allocate into.
, Store.hasRgn store rgn
-- add the binding to the store
, (store1, l) <- Store.allocBind rgn
(tList tR tA) (SObj dc [lHead, lTail]) store
= Just ( store1
, xLoc l (tList tR tA))
stepPrimCon _ _ _
= Nothing
-------------------------------------------------------------------------------
-- | Step a primitive operator.
stepPrimOp
:: Name -- ^ Name of operator to evaluate.
-> [Exp () Name] -- ^ Arguments to operator.
-> Store -- ^ Current store.
-> Maybe ( Store
, Exp () Name) -- ^ New store and result expression,
-- if the operator steps, otherwise `Nothing`.
-- Binary integer primop.
stepPrimOp (NamePrimOp op) [xR1, xR2, xR3, xL1, xL2] store
-- unpack the args
| Just fOp <- lookup op
[ (PrimOpAddInt, (+))
, (PrimOpSubInt, (-))
, (PrimOpMulInt, (*))
, (PrimOpDivInt, div)
, (PrimOpEqInt, (\x y -> if x == y then 1 else 0))]
, Just r1 <- takeHandleX xR1
, Just r2 <- takeHandleX xR2
, XType _ tR3 <- xR3
, Just r3 <- takeHandleX xR3
, Just l1 <- stripLocX xL1
, Just l2 <- stripLocX xL2
-- get the regions and values of each location
, Just (r1', _, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store
, Just i1 <- takeIntDC dc1
, Just (r2', _, SObj dc2 []) <- Store.lookupRegionTypeBind l2 store
, Just i2 <- takeIntDC dc2
-- the locations must be in the regions the args said they were in
, r1' == r1
, r2' == r2
-- the destination region must exist
, Store.hasRgn store r3
-- do the actual computation
, i3 <- i1 `fOp` i2
-- write the result to a new location in the store
, (store1, l3) <- Store.allocBind r3 (tInt tR3)
(SObj (dcInt i3) [])
store
= Just ( store1
, xLoc l3 (tInt tR3))
-- Update integer primop.
stepPrimOp (NamePrimOp PrimOpUpdateInt) [xR1, xR2, xMutR1, xL1, xL2] store
-- unpack the args
| Just r1 <- takeHandleX xR1
, Just r2 <- takeHandleX xR2
, Just r1W <- takeMutableX xMutR1
, Just l1 <- stripLocX xL1
, Just l2 <- stripLocX xL2
-- the witness must be for the destination region
, r1W == r1
-- get the regions and values of each location
, Just (r1L, tX1, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store
, Just _i1 <- takeIntDC dc1
, Just (r2L, _, SObj dc2 []) <- Store.lookupRegionTypeBind l2 store
, Just i2 <- takeIntDC dc2
-- the locations must be in the regions the args said they were in
, r1L == r1
, r2L == r2
-- update the destination
, store1 <- Store.addBind l1 r1 tX1 (SObj (dcInt i2) []) store
= Just ( store1
, xUnit ())
-- Unary integer operations
stepPrimOp (NamePrimOp op) [xR1, xR2, xL1] store
-- unpack the args
| Just fOp <- lookup op
[ (PrimOpCopyInt, id)
, (PrimOpNegInt, negate) ]
, Just r1 <- takeHandleX xR1
, XType _ tR2 <- xR2
, Just r2 <- takeHandleX xR2
, Just l1 <- stripLocX xL1
-- get the region and value of the int
, Just (r1L, _, SObj dc1 []) <- Store.lookupRegionTypeBind l1 store
, Just i1 <- takeIntDC dc1
-- the locations must be in the regions the args said they were in
, r1L == r1
-- the destination region must exist
, Store.hasRgn store r2
-- calculate
, i2 <- fOp i1
-- write the result to a new location in the store
, (store1, l2) <- Store.allocBind r2 (tInt tR2) (SObj (dcInt i2) []) store
= Just ( store1
, xLoc l2 (tInt tR2))
stepPrimOp _ _ _
= Nothing
-- Store ----------------------------------------------------------------------
-- | Like `Store.newRgn` but return the region handle wrapped in a `Bound`.
primNewRegion :: Store -> (Store, Bound Name)
primNewRegion store
= let (store', rgn) = Store.newRgn store
u = UPrim (NameRgn rgn) kRegion
in (store', u)
-- | Like `Store.delRgn` but accept a region handle wrapped in a `Bound`.
primDelRegion :: Bound Name -> Store -> Maybe Store
primDelRegion uu store
= case uu of
UPrim (NameRgn rgn) _ -> Just $ Store.delRgn rgn store
_ -> Nothing