-- | Vectors are arrays of unboxed values.
module Vector
imports {
        allocRaw     :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj;
        payloadOfRaw :: [r : Region]. Ptr# r Obj -> Addr#;
} 
with letrec


-- Allocation -----------------------------------------------------------------
-- | Alloc a vector of the given length.
-- 
--   typedef struct
--   {  nat_t   length
--      uint8_t payload[] 
--   } Vector8
--
allocVector8 [r : Region] (length : Nat#) : Ptr# r Obj
 = do   
        -- total size of object payload.
        bytes   = add# [Nat#] (bytesNat# V#) length
        obj     = allocRaw [r] TAG0# bytes

        -- write the length field.
        payload = payloadOfRaw [r] obj
        write# [Nat#] payload 0# length

        -- zero fill vector
        fillVector8 [r] obj 0w8#

        obj


-- Projections ----------------------------------------------------------------
-- | Get the length of a vector.
lengthVector8 [r : Region] (obj : Ptr# r Obj) : Nat#
 = do   payload = payloadOfRaw [r] obj
        read# [Nat#] payload 0#


-- | Unsafely read a byte from a vector.
indexVector8 [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Word8#
 = do   payload = payloadOfRaw [r] obj
        offset  = add# [Nat#] (bytesNat# V#) index
        read# [Word8#] payload offset 


-- Update ---------------------------------------------------------------------
-- | Unsafely write a byte into a vector.
updateVector8 
        [r : Region]
        (obj : Ptr# r Obj)
        (index : Nat#) (val : Word8#)
        : Void#
 = do   payload = payloadOfRaw [r] obj
        offset  = add# [Nat#] (bytesNat# V#) index
        write# [Word8#] payload offset val


-- Fill -----------------------------------------------------------------------
-- | Fill a vector with the given value.
fillVector8 
        [r : Region]
        (obj : Ptr# r Obj) (val : Word8#)
        : Void#
 = do   payload = payloadOfRaw [r] obj
        length  = read# [Nat#] payload 0#

        buf     = plusPtr# [r] [Word8#] (makePtr# [r] [Word8#] payload) (bytesNat# V#)
        max     = plusPtr# [r] [Word8#] buf length
        fillPtr8 [r] buf max val


-- | Fill a range of bytes with the given value.
fillPtr8 
        [r : Region] 
        (cur : Ptr# r Word8#) 
        (top : Ptr# r Word8#) (val : Word8#)
        : Void#
 = do   
        curAddr = takePtr# [r] [Word8#] cur
        topAddr = takePtr# [r] [Word8#] top
        case ge# [Addr#] curAddr topAddr of
         True#  -> V#
         False#  
          -> do poke# [r] [Word8#] cur 0# val
                next    = plusPtr# [r] [Word8#] cur 1#
                fillPtr8 [r] next top val


-- Copy -----------------------------------------------------------------------
-- | Copy a vector into a fresh buffer.
copyVector8 
        [r1 r2 : Region]
        (vec1 : Ptr# r1 Obj)
        : Ptr# r2 Obj
 = do   
        len     = lengthVector8 [r1] vec1
        vec2    = allocVector8  [r2] len

        src     = plusPtr# [r1] [Word8#]
                        (makePtr#  [r1] [Word8#] (payloadOfRaw [r1] vec1))
                        (bytesNat# V#)

        dst     = plusPtr# [r2] [Word8#]
                        (makePtr#  [r2] [Word8#] (payloadOfRaw [r2] vec2))
                        (bytesNat# V#)

        copyPtr8 [:r1 r2:] 0# len src dst
        vec2


copyPtr8
        [r1 r2 : Region]
        (offset : Nat#)
        (length : Nat#)
        (src : Ptr# r1 Word8#)
        (dst : Ptr# r2 Word8#)
        : Void#
 = do   
        case gt# [Nat#] offset length of
         True#   -> V#
         False#
          -> do x1       = peek# [r1] [Word8#] src offset
                poke# [r2] [Word8#] dst offset x1
                
                copyPtr8 [:r1 r2:] 
                        (add# [Nat#] offset 1#)
                        length src dst