
   0 | module Data.Buffer.Core
   1 | 
   2 | import Data.Array.Index
   3 | import Data.Buffer
   4 | import Data.Linear.Token
   5 | import public Data.Fin
   6 | import public Data.Nat
   7 | 
   8 | import System.File
   9 | 
  10 | %default total
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | --          Raw Primitives
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | export
  17 | %foreign "scheme:(lambda (b o) (bytevector-u8-ref b o))"
  18 |          "javascript:lambda:(buf,offset)=>buf[Number(offset)]"
  19 | prim__getByte : Buffer -> (offset : Integer) -> Bits8
  20 | 
  21 | ||| This is an optimized version of `getByte` that allows us to read
  22 | ||| at an offset. On Chez, we can use the faster fixnum addition here,
  23 | ||| which can lead to a performance boost.
  24 | export
  25 | %foreign "scheme:(lambda (b a o) (bytevector-u8-ref b (+ a o)))"
  26 |          "scheme,chez:(lambda (b a o) (bytevector-u8-ref b (fx+ a o)))"
  27 |          "javascript:lambda:(buf,at,offset)=>buf[Number(offset) + Number(at)]"
  28 | prim__getByteOffset : Buffer -> (at, offset : Integer) -> Bits8
  29 | 
  30 | export
  31 | %foreign "scheme:(lambda (b o v) (bytevector-u8-set! b o v))"
  32 |          "javascript:lambda:(buf,offset,value,t)=>{buf[Number(offset)] = value; return t}"
  33 | prim__setByte : Buffer -> (offset : Integer) -> (val : Bits8) -> PrimIO ()
  34 | 
  35 | export
  36 | %foreign "scheme:(lambda (n) (make-bytevector n 0))"
  37 |          "javascript:lambda:(s,w)=>new Uint8Array(Number(s))"
  38 | prim__newBuf : Integer -> PrimIO Buffer
  39 | 
  40 | export
  41 | %foreign "scheme:blodwen-buffer-getstring"
  42 |          "javascript:lambda:(buf,offset,len)=> new TextDecoder().decode(buf.subarray(Number(offset), Number(offset+len)))"
  43 | prim__getString : Buffer -> (offset,len : Integer) -> String
  44 | 
  45 | export
  46 | %foreign "scheme:(lambda (v) (string->utf8 v))"
  47 |          "javascript:lambda:(v)=> new TextEncoder().encode(v)"
  48 | prim__fromString : (val : String) -> Buffer
  49 | 
  50 | export
  51 | %foreign "scheme:(lambda (b1 o1 len b2 o2) (bytevector-copy! b1 o1 b2 o2 len))"
  52 |          "javascript:lambda:(b1,bo1,blen,b2,bo2,t)=> {const o1 = Number(bo1); const len = Number(blen); const o2 = Number(bo2); for (let i = 0; i < len; i++) {b2[o2+i] = b1[o1+i];}; return t}"
  53 | prim__copy : (src : Buffer) -> (srcOffset, len : Integer) ->
  54 |              (dst : Buffer) -> (dstOffset : Integer) -> PrimIO ()
  55 | 
  56 | --------------------------------------------------------------------------------
  57 | --          Immutable Buffers
  58 | --------------------------------------------------------------------------------
  59 | 
  60 | ||| An immutable byte array of size `n`.
  61 | export
  62 | record IBuffer (n : Nat) where
  63 |   constructor IB
  64 |   buf : Buffer
  65 | 
  66 | ||| Safely access a value in an byte array at the given position.
  67 | export %inline
  68 | at : IBuffer n -> Fin n -> Bits8
  69 | at (IB buf) m = prim__getByte buf (cast $ finToNat m)
  70 | 
  71 | ||| Safely access a value in an immutable byte array at the given position
  72 | ||| and offset.
  73 | export %inline
  74 | atOffset : IBuffer n -> Fin m -> (off : Nat) -> (0 p : LTE (off+m) n) => Bits8
  75 | atOffset (IB buf) m off =
  76 |   prim__getByteOffset buf (cast $ finToNat m) (cast off)
  77 | 
  78 | ||| We can wrap a prefix of an immutable byte array in O(1) simply by giving it
  79 | ||| a new size index.
  80 | |||
  81 | ||| Note: If you only need a small portion of a potentially large
  82 | |||       byte array the rest of which you no longer need, consider to
  83 | |||       releasing the large byte array from memory by invoking `force`.
  84 | export
  85 | take : (0 m : Nat) -> IBuffer n -> {auto 0 lte : LTE m n} -> IBuffer m
  86 | take _ (IB buf) = IB buf
  87 | 
  88 | ||| Convert an UTF-8 string to an immutable byte array.
  89 | export %noinline
  90 | fromString : (s : String) -> IBuffer (cast $ stringByteLength s)
  91 | fromString s = IB (prim__fromString s)
  92 | 
  93 | ||| Convert a section of an immutable byte array to an UTF-8 string.
  94 | export
  95 | toString : IBuffer n -> (off,len : Nat) -> (0 _ : LTE (off + len) n) => String
  96 | toString (IB buf) off len = prim__getString buf (cast off) (cast len)
  97 | 
  98 | ||| Extracts the inner buffer held by an immutable byte array without copying.
  99 | |||
 100 | ||| This allows us to write efficiently write the data to a file
 101 | ||| without copying it first. This is a highly unsafe operation,
 102 | ||| and client code must make sure never ever to mutate the buffer!
 103 | export
 104 | unsafeGetBuffer : IBuffer n -> Buffer
 105 | unsafeGetBuffer (IB buf) = buf
 106 | 
 107 | ||| Wraps a bare mutable buffer in an `IBuffer`.
 108 | |||
 109 | ||| Client code is responsible to make sure the original buffer is no longer
 110 | ||| used.
 111 | export
 112 | unsafeMakeBuffer : Buffer -> IBuffer k
 113 | unsafeMakeBuffer = IB
 114 | 
 115 | public export
 116 | record AnyBuffer where
 117 |   constructor AB
 118 |   size : Nat
 119 |   ibuf : IBuffer size
 120 | 
 121 | --------------------------------------------------------------------------------
 122 | --          Mutable Byte Arrays
 123 | --------------------------------------------------------------------------------
 124 | 
 125 | ||| A mutable byte array.
 126 | export
 127 | data MBuffer : (s : Type) -> (n : Nat) -> Type where
 128 |   MB : (buf : Buffer) -> MBuffer s n
 129 | 
 130 | ||| Convenience alias for `MBuffer' RIO`
 131 | public export
 132 | 0 IOBuffer : Nat -> Type
 133 | IOBuffer = MBuffer World
 134 | 
 135 | ||| Wraps a `Buffer` in an `IOBuffer`. Use at your own risk.
 136 | export %inline
 137 | unsafeMBuffer : Buffer -> MBuffer s n
 138 | unsafeMBuffer = MB
 139 | 
 140 | ||| Extracts the `Buffer` from an `MBuffer`. Use at your own risk.
 141 | export %inline
 142 | unsafeFromMBuffer : MBuffer s n -> Buffer
 143 | unsafeFromMBuffer (MB buf) = buf
 144 | 
 145 | --------------------------------------------------------------------------------
 146 | -- Utilities
 147 | --------------------------------------------------------------------------------
 148 | 
 149 | ||| Creates a new mutable byte array bound to linear computation `s`.
 150 | export %inline
 151 | mbuffer1 : (n : Nat) -> F1 s (MBuffer s n)
 152 | mbuffer1 n t =
 153 |   let MkIORes b _ := prim__newBuf (cast n) %MkWorld
 154 |    in MB b # t
 155 | 
 156 | ||| Creates a new mutable byte array in `IO`.
 157 | export %inline
 158 | mbuffer : Lift1 s f => (n : Nat) -> f (MBuffer s n)
 159 | mbuffer n = lift1 (mbuffer1 n)
 160 | 
 161 | ||| Safely write a value to a mutable byte array.
 162 | export %inline
 163 | set : (r : MBuffer s n) -> Fin n -> Bits8 -> F1' s
 164 | set (MB buf) ix v = ffi (prim__setByte buf (cast $ finToNat ix) v)
 165 | 
 166 | ||| Safely read a value from a mutable byte array.
 167 | export %inline
 168 | get : (r : MBuffer s n) -> Fin n -> F1 s Bits8
 169 | get (MB buf) ix t = prim__getByte buf (cast $ finToNat ix) # t
 170 | 
 171 | ||| Safely modify a value in a mutable byte array.
 172 | export
 173 | modify : (r : MBuffer s n) -> Fin n -> (Bits8 -> Bits8) -> F1' s
 174 | modify r m f t = let v # t := get r m t in set r m (f v) t
 175 | 
 176 | ||| Extracts a string from a (possibly partially) filled mutable byte array.
 177 | export %inline
 178 | bufString : (r : MBuffer s n) -> (m : Nat) -> (0 lte : LTE m n) => F1 s String
 179 | bufString (MB buf) m t = prim__getString buf 0 (cast m) # t
 180 | 
 181 | ||| Like `bufString` but extracts a substring from position
 182 | ||| `from` up to but not including position `till`.
 183 | export
 184 | bufStringFromTill :
 185 |      (r : MBuffer s n)
 186 |   -> (from, till : Nat)
 187 |   -> {auto 0 lt1 : LTE from till}
 188 |   -> {auto 0 lt2 : LTE till n}
 189 |   -> F1 s String
 190 | bufStringFromTill (MB buf) from till t =
 191 |   prim__getString buf (cast from) (cast $ till `minus` from) # t
 192 | 
 193 | ||| Like `bufString` but extracts a substring from position
 194 | ||| `from` up to and including position `to`.
 195 | export
 196 | bufStringFromTo :
 197 |      (r : MBuffer s n)
 198 |   -> (from, to : Nat)
 199 |   -> {auto 0 lte : LTE from to}
 200 |   -> {auto 0 lt  : LT to n}
 201 |   -> F1 s String
 202 | bufStringFromTo buf from to = bufStringFromTill buf from (S to)
 203 | 
 204 | ||| Wraps a mutable byte array in a shorter one.
 205 | export %inline
 206 | mtake : MBuffer s n -> (0 m : Nat) -> (0 lte : LTE m n) => F1 s (MBuffer s m)
 207 | mtake (MB buf) _ t = MB buf # t
 208 | 
 209 | --------------------------------------------------------------------------------
 210 | -- Allocating Byte Vectors
 211 | --------------------------------------------------------------------------------
 212 | 
 213 | public export
 214 | 0 WithMBuffer : Nat -> (a : Type) -> Type
 215 | WithMBuffer n a = forall s . (r : MBuffer s n) -> F1 s a
 216 | 
 217 | ||| Allocate and potentially freeze a mutable byte array in a linear context.
 218 | export
 219 | alloc : (n : Nat) -> (fun : WithMBuffer n a) -> a
 220 | alloc n f = run1 $ \t => let r # t := mbuffer1 n t in f r t
 221 | 
 222 | --------------------------------------------------------------------------------
 223 | -- Utilities
 224 | --------------------------------------------------------------------------------
 225 | 
 226 | export %noinline
 227 | copy :
 228 |      MBuffer s m
 229 |   -> (srcOffset,dstOffset : Nat)
 230 |   -> (len : Nat)
 231 |   -> {auto 0 p1 : LTE (srcOffset + len) m}
 232 |   -> {auto 0 p2 : LTE (dstOffset + len) n}
 233 |   -> (r         : MBuffer s n)
 234 |   -> F1' s
 235 | copy (MB src) srcOffset dstOffset len (MB dst) =
 236 |   ffi (prim__copy src (cast srcOffset) (cast len) dst (cast dstOffset))
 237 | 
 238 | export %inline
 239 | icopy :
 240 |      IBuffer m
 241 |   -> (srcOffset,dstOffset : Nat)
 242 |   -> (len : Nat)
 243 |   -> {auto 0 p1 : LTE (srcOffset + len) m}
 244 |   -> {auto 0 p2 : LTE (dstOffset + len) n}
 245 |   -> (r         : MBuffer s n)
 246 |   -> F1' s
 247 | icopy (IB src) = copy {m} (MB src)
 248 | 
 249 | ||| Extracts an immutable sub-array from a mutable byte array.
 250 | export %inline
 251 | bufSubstring :
 252 |      (r : MBuffer s n)
 253 |   -> (off,len : Nat)
 254 |   -> {auto 0 lte : LTE (off+len) n}
 255 |   -> F1 s (IBuffer len)
 256 | bufSubstring (MB src) off len t =
 257 |  let MB dst # t := mbuffer1 len t
 258 |      _      # t := ffi (prim__copy src (cast off) (cast len) dst 0) t
 259 |   in IB dst # t
 260 | 
 261 | ||| Like `bufSubstring` but extracts a substring from position
 262 | ||| `from` up to but not including position `till`.
 263 | export
 264 | bufSubstringFromTill :
 265 |      (r : MBuffer s n)
 266 |   -> (from, till : Nat)
 267 |   -> {auto 0 lt1 : LTE from till}
 268 |   -> {auto 0 lt2 : LTE till n}
 269 |   -> F1 s (IBuffer (till `minus` from))
 270 | bufSubstringFromTill r f t =
 271 |   bufSubstring r f (t `minus` f) @{transitive (plusMinusLTE _ _ lt1) lt2}
 272 | 
 273 | ||| Like `bufSubstring` but extracts a substring from position
 274 | ||| `from` up to and including position `to`.
 275 | export %inline
 276 | bufSubstringFromTo :
 277 |      (r : MBuffer s n)
 278 |   -> (from, to : Nat)
 279 |   -> {auto 0 lte : LTE from to}
 280 |   -> {auto 0 lt  : LT to n}
 281 |   -> F1 s (IBuffer (S to `minus` from))
 282 | bufSubstringFromTo r f t = bufSubstringFromTill r f (S t)
 283 | 
 284 | ||| Copy the content of an immutable byte array to a new byte array.
 285 | export
 286 | thaw : {n : _} -> IBuffer n -> F1 s (MBuffer s n)
 287 | thaw src t =
 288 |     let r # t := mbuffer1 n t
 289 |         _ # t := icopy src 0 0 n @{reflexive} @{reflexive} r t
 290 |      in r # t
 291 | 
 292 | ||| Wrap a mutable byte array in an immutable byte array without copying.
 293 | |||
 294 | ||| In order to make this safe, the associated linear token has to
 295 | ||| be discarded.
 296 | |||
 297 | ||| It is safe to only use a prefix of a properly constructed array,
 298 | ||| therefore we are free to give the resulting array a smaller size.
 299 | ||| Most of the time, we'd like to use the whole buffer, in which case
 300 | ||| we can just use `freezeBufAt`.
 301 | |||
 302 | ||| Note: For reasons of efficiency, this does not copy the buffer,
 303 | |||       and therefore, it must no longer be modified after calling
 304 | |||       this function.
 305 | export %inline
 306 | unsafeFreezeLTE :
 307 |      MBuffer s n
 308 |   -> (0 m : Nat)
 309 |   -> {auto 0 _ : LTE m n}
 310 |   -> F1 s (IBuffer m)
 311 | unsafeFreezeLTE (MB buf) _ t = IB buf # t
 312 | 
 313 | ||| Convenience alias for `unsafeFreezeLTE @{reflexive}`
 314 | export %inline
 315 | unsafeFreeze : (r : MBuffer s n) -> F1 s (IBuffer n)
 316 | unsafeFreeze r = unsafeFreezeLTE @{reflexive} r n
 317 | 
 318 | ||| Copy a prefix of a mutable byte arrya into an immutable byte array.
 319 | export
 320 | freezeLTE : MBuffer s n -> (m : Nat) -> (0 p : LTE m n) => F1 s (IBuffer m)
 321 | freezeLTE src m t =
 322 |   let r@(MB buf) # t := mbuffer1 m t
 323 |       _          # t := copy src 0 0 m @{p} @{reflexive} r t
 324 |    in IB buf     # t
 325 | 
 326 | ||| Copy a mutable byte array into an immutable byte array.
 327 | export %inline
 328 | freeze : {n : _} -> MBuffer s n -> F1 s (IBuffer n)
 329 | freeze src = freezeLTE src n @{reflexive}
 330 | 
 331 | --------------------------------------------------------------------------------
 332 | --          Reading and Writing Files
 333 | --------------------------------------------------------------------------------
 334 | 
 335 | ||| Read up to `n` bytes from a file into an immutable byte array.
 336 | export
 337 | readIBuffer :
 338 |      {auto has : HasIO io}
 339 |   -> Nat
 340 |   -> File
 341 |   -> io (Either FileError (n ** IBuffer n))
 342 | readIBuffer max f = do
 343 |   buf <- primIO (prim__newBuf (cast max))
 344 |   Right r <- readBufferData f buf 0 (cast max) | Left x => pure (Left x)
 345 |   if r >= 0
 346 |      then pure (Right (cast r ** IB buf))
 347 |      else pure (Left FileReadError)
 348 | 
 349 | ||| Write up to `len` bytes from an immutable byte array to a file, starting
 350 | ||| at the given offset.
 351 | export
 352 | writeIBuffer :
 353 |      {auto has : HasIO io}
 354 |   -> File
 355 |   -> (offset,len : Nat)
 356 |   -> IBuffer n
 357 |   -> {auto 0 prf : LTE (offset + len) n}
 358 |   -> io (Either (FileError,Int) ())
 359 | writeIBuffer h o s (IB buf) = writeBufferData h buf (cast o) (cast s)
 360 | 
 361 | ||| Write up to `len` bytes from a mutable byte array to a file, starting
 362 | ||| at the given offset.
 363 | export
 364 | writeMBuffer :
 365 |      {auto has : HasIO io}
 366 |   -> File
 367 |   -> (offset,len : Nat)
 368 |   -> {auto 0 prf : LTE (offset + len) n}
 369 |   -> (r : MBuffer s n)
 370 |   -> io (Either (FileError,Int) ())
 371 | writeMBuffer h o s (MB b) =
 372 |   writeBufferData h b (cast o) (cast s)
 373 |