module Ivory.Stdlib.Memory
( resultInto
, into
, arrayCopy
) where
import Ivory.Language
import Ivory.Stdlib.Control
resultInto :: IvoryStore a =>
Ivory eff a -> Ref s ('Stored a) -> Ivory eff ()
resultInto a b = store b =<< a
into :: IvoryStore a =>
Ref s ('Stored a) -> Ref s' ('Stored a) -> Ivory eff ()
into a b = store b =<< deref a
arrayCopy ::
( ANat n, ANat m, IvoryRef r
, IvoryExpr (r s2 ('Array m ('Stored t)))
, IvoryExpr (r s2 ('Stored t))
, IvoryStore t
)
=> Ref s1 ('Array n ('Stored t))
-> r s2 ('Array m ('Stored t))
-> Sint32
-> Sint32
-> Ivory eff ()
arrayCopy to from toOffset end = do
assert (toOffset >=? 0 .&& toOffset <? toLen)
assert (end >=? 0 .&& end <=? frLen)
arrayMap $ go
where
go ix =
cond_
[
(fromIx ix >=? end)
==> return ()
,
(fromIx ix + toOffset >=? toLen)
==> return ()
, true
==> (deref (from ! ix) >>= store (to ! mkIx ix))
]
toLen = arrayLen to
frLen = arrayLen from
mkIx ix = toIx (toOffset + fromIx ix)