module DDC.Core.Salt.Compounds.PrimStore
( xStoreSize, xStoreSize2
, xCreate
, xRead, xWrite
, xPeek, xPeekBounded, xPoke, xPokeBounded
, xCastPtr
, typeOfPrimStore)
where
import DDC.Core.Salt.Compounds.PrimTyCon
import DDC.Core.Salt.Name
import DDC.Core.Exp.Annot
xPrimStore a p
= XVar a (UPrim (NamePrimOp $ PrimStore p) (typeOfPrimStore p))
xStoreSize :: a -> Type Name -> Exp a Name
xStoreSize a tElem
= xApps a (xPrimStore a PrimStoreSize)
[XType a tElem]
xStoreSize2 :: a -> Type Name -> Exp a Name
xStoreSize2 a tElem
= xApps a (xPrimStore a PrimStoreSize2)
[XType a tElem]
xCreate :: a -> Exp a Name -> Exp a Name
xCreate a xLength
= xApps a (xPrimStore a PrimStoreCreate)
[xLength]
xRead :: a -> Type Name -> Exp a Name -> Exp a Name -> Exp a Name
xRead a tField xAddr xOffset
= xApps a (xPrimStore a PrimStoreRead)
[ XType a tField, xAddr, xOffset ]
xWrite :: a -> Type Name -> Exp a Name -> Exp a Name -> Exp a Name -> Exp a Name
xWrite a tField xAddr xOffset xVal
= xApps a (xPrimStore a PrimStoreWrite)
[ XType a tField, xAddr, xOffset, xVal ]
xPeek :: a -> Type Name -> Type Name -> Exp a Name -> Exp a Name -> Exp a Name
xPeek a r t xPtr xOffset
= xApps a (xPrimStore a PrimStorePeek)
[ XType a r, XType a t, xPtr, xOffset ]
xPeekBounded
:: a -> Type Name -> Type Name
-> Exp a Name -> Exp a Name -> Exp a Name -> Exp a Name
xPeekBounded a r t xPtr xOffset xLimit
= xApps a (xPrimStore a PrimStorePeekBounded)
[ XType a r, XType a t, xPtr, xOffset, xLimit ]
xPoke :: a -> Type Name -> Type Name
-> Exp a Name -> Exp a Name -> Exp a Name -> Exp a Name
xPoke a r t xPtr xOffset xVal
= xApps a (xPrimStore a PrimStorePoke)
[ XType a r, XType a t, xPtr, xOffset, xVal]
xPokeBounded
:: a -> Type Name -> Type Name
-> Exp a Name -> Exp a Name -> Exp a Name -> Exp a Name -> Exp a Name
xPokeBounded a r t xPtr xOffset xLimit xVal
= xApps a (xPrimStore a PrimStorePokeBounded)
[ XType a r, XType a t, xPtr, xOffset, xLimit, xVal]
xCastPtr :: a -> Type Name -> Type Name -> Type Name -> Exp a Name -> Exp a Name
xCastPtr a r toType fromType xPtr
= xApps a (xPrimStore a PrimStoreCastPtr)
[ XType a r, XType a toType, XType a fromType, xPtr ]
typeOfPrimStore :: PrimStore -> Type Name
typeOfPrimStore jj
= case jj of
PrimStoreSize
-> tForall kData $ \_ -> tNat
PrimStoreSize2
-> tForall kData $ \_ -> tNat
PrimStoreCreate
-> tNat `tFun` tVoid
PrimStoreCheck
-> tNat `tFun` tBool
PrimStoreRecover
-> tNat `tFun` tVoid
PrimStoreAlloc
-> tNat `tFun` tAddr
PrimStoreRead
-> tForall kData
$ \t -> tAddr `tFun` tNat `tFun` t
PrimStoreWrite
-> tForall kData
$ \t -> tAddr `tFun` tNat `tFun` t `tFun` tVoid
PrimStorePlusAddr
-> tAddr `tFun` tNat `tFun` tAddr
PrimStoreMinusAddr
-> tAddr `tFun` tNat `tFun` tAddr
PrimStorePeek
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` t
PrimStorePoke
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` t `tFun` tVoid
PrimStorePeekBounded
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` tNat `tFun` t
PrimStorePokeBounded
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` tNat `tFun` t `tFun` tVoid
PrimStorePlusPtr
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` tPtr r t
PrimStoreMinusPtr
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tNat `tFun` tPtr r t
PrimStoreMakePtr
-> tForalls [kRegion, kData]
$ \[r,t] -> tAddr `tFun` tPtr r t
PrimStoreTakePtr
-> tForalls [kRegion, kData]
$ \[r,t] -> tPtr r t `tFun` tAddr
PrimStoreCastPtr
-> tForalls [kRegion, kData, kData]
$ \[r,t1,t2] -> tPtr r t2 `tFun` tPtr r t1