content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE TypeFamilies #-}
  
  module Ivory.Stdlib.Memory
    ( resultInto
    , into
    , arrayCopy
    ) where
  
  import Ivory.Language
  import Ivory.Stdlib.Control
  
  -- | handy shorthand for transfering members
  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
  
  -- XXX Belongs with Pack.hs and SafePack.hs.
  
  -- | Copies a prefix of an array into a postfix of another array.  That is, copy
  -- from array @from@ (either a 'Ref' or a 'ConstRef') into array @to@ starting
  -- at index @toOffset@ in @to@.  Copying continues until either the from array
  -- is fully copied, the @to@ array is full, or index @end@ in the @from@ array
  -- is reached (index @end@ is not copied).  to copy the full @from@ array, let
  -- @end@ equal 'arrayLen from'.
  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
    -- The index is w.r.t. the from array.
    go ix =
      cond_
        [   -- We've reached the @end@ index: stop copying.
            (fromIx ix >=? end)
        ==> return ()
        ,   -- We've reached the end of the @to@ array: stop copying.
            (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)
  