0 | module Data.Buffer.Builder
2 | import Data.Array.Index
6 | import Data.Buffer.Indexed
8 | import public Data.Buffer.Core
9 | import public Data.Linear.Token
17 | %foreign "scheme:(lambda (n) (cons (make-bytevector (max n 32) 0) 0))"
18 | "javascript:lambda:(sz,w)=> {const buf = new ArrayBuffer(sz); return {buffer:buf, view: new DataView(buf), pos: 0};}"
19 | prim__builder : Bits32 -> PrimIO AnyPtr
21 | %foreign "scheme:(lambda (n b) (let ((sz (bytevector-length (car b))) (tgt (+ n (cdr b)))) (if (> tgt sz) (let ((bv (make-bytevector (+ sz (max sz n)) 0))) (bytevector-copy! (car b) 0 bv 0 (cdr b)) (set-car! b bv)))))"
22 | "javascript:lambda:(n,b,w) => {const tgt = n + b.pos; const sz = b.buffer.byteLength; if (tgt > sz) {const newSize = Math.max(2 * sz, tgt); const newBuffer = new ArrayBuffer(newSize); new Uint8Array(newBuffer).set(new Uint8Array(b.buffer)); b.buffer = newBuffer; b.view = new DataView(newBuffer);}}"
23 | prim__checksize : Bits32 -> AnyPtr -> PrimIO ()
25 | %foreign "scheme:(lambda (off sz buf b) (bytevector-copy! buf off (car b) (cdr b) sz) (set-cdr! b (+ sz (cdr b))))"
26 | "javascript:lambda:(o,len,buf,b,t)=> {new Uint8Array(b.buffer).set(buf.slice(o,o+len), b.pos); b.pos += len;}"
27 | prim__putbytes : (offset, len : Bits32) -> Buffer -> AnyPtr -> PrimIO ()
29 | %foreign "scheme:(lambda (v b) (bytevector-u8-set! (car b) (cdr b) v) (set-cdr! b (+ 1 (cdr b))))"
30 | "javascript:lambda:(n,b,w) => {b.view.setUint8(b.pos, n); b.pos += 1;}"
31 | prim__putbits8 : Bits8 -> AnyPtr -> PrimIO ()
33 | %foreign "scheme:(lambda (v b) (bytevector-u16-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 2 (cdr b))))"
34 | "javascript:lambda:(n,b,w) => {b.view.setUint16(b.pos, n, true); b.pos += 2;}"
35 | prim__putbits16le : Bits16 -> AnyPtr -> PrimIO ()
37 | %foreign "scheme:(lambda (v b) (bytevector-u16-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 2 (cdr b))))"
38 | "javascript:lambda:(n,b,w) => {b.view.setUint16(b.pos, n, false); b.pos += 2;}"
39 | prim__putbits16be : Bits16 -> AnyPtr -> PrimIO ()
41 | %foreign "scheme:(lambda (v b) (bytevector-u32-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 4 (cdr b))))"
42 | "javascript:lambda:(n,b,w) => {b.view.setUint32(b.pos, n, true); b.pos += 4;}"
43 | prim__putbits32le : Bits32 -> AnyPtr -> PrimIO ()
45 | %foreign "scheme:(lambda (v b) (bytevector-u32-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 4 (cdr b))))"
46 | "javascript:lambda:(n,b,w) => {b.view.setUint32(b.pos, n, false); b.pos += 4;}"
47 | prim__putbits32be : Bits32 -> AnyPtr -> PrimIO ()
49 | %foreign "scheme:(lambda (v b) (bytevector-u64-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 8 (cdr b))))"
50 | "javascript:lambda:(n,b,w) => {const nx = Number(n & 0xffffffffn); const ny = Number((n >> 32n) & 0xffffffffn); b.view.setUint32(b.pos, nx, true); b.pos += 4; b.view.setUint32(b.pos, ny, true); b.pos += 4;}"
51 | prim__putbits64le : Bits64 -> AnyPtr -> PrimIO ()
53 | %foreign "scheme:(lambda (v b) (bytevector-u64-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 8 (cdr b))))"
54 | "javascript:lambda:(n,b,w) => {const nx = Number(n & 0xffffffffn); const ny = Number((n >> 32n) & 0xffffffffn); b.view.setUint32(b.pos, ny, false); b.pos += 4; b.view.setUint32(b.pos, nx, false); b.pos += 4;}"
55 | prim__putbits64be : Bits64 -> AnyPtr -> PrimIO ()
57 | %foreign "scheme:(lambda (v b) (bytevector-s8-set! (car b) (cdr b) v) (set-cdr! b (+ 1 (cdr b))))"
58 | "javascript:lambda:(n,b,w) => {b.view.setInt8(b.pos, n); b.pos += 1;}"
59 | prim__putint8 : Int8 -> AnyPtr -> PrimIO ()
61 | %foreign "scheme:(lambda (v b) (bytevector-s16-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 2 (cdr b))))"
62 | "javascript:lambda:(n,b,w) => {b.view.setInt16(b.pos, n, true); b.pos += 2;}"
63 | prim__putint16le : Int16 -> AnyPtr -> PrimIO ()
65 | %foreign "scheme:(lambda (v b) (bytevector-s16-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 2 (cdr b))))"
66 | "javascript:lambda:(n,b,w) => {b.view.setInt16(b.pos, n, false); b.pos += 2;}"
67 | prim__putint16be : Int16 -> AnyPtr -> PrimIO ()
69 | %foreign "scheme:(lambda (v b) (bytevector-s32-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 4 (cdr b))))"
70 | "javascript:lambda:(n,b,w) => {b.view.setInt32(b.pos, n, true); b.pos += 4;}"
71 | prim__putint32le : Int32 -> AnyPtr -> PrimIO ()
73 | %foreign "scheme:(lambda (v b) (bytevector-s32-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 4 (cdr b))))"
74 | "javascript:lambda:(n,b,w) => {b.view.setInt32(b.pos, n, false); b.pos += 4;}"
75 | prim__putint32be : Int32 -> AnyPtr -> PrimIO ()
77 | %foreign "scheme:(lambda (v b) (bytevector-s64-set! (car b) (cdr b) v 'little) (set-cdr! b (+ 8 (cdr b))))"
78 | "javascript:lambda:(x,b,w) => {const n = BigInt.asUintN(64,x); const nx = Number(n & 0xffffffffn); const ny = Number((n >> 32n) & 0xffffffffn); b.view.setUint32(b.pos, nx, true); b.pos += 4; b.view.setUint32(b.pos, ny, true); b.pos += 4;}"
79 | prim__putint64le : Int64 -> AnyPtr -> PrimIO ()
81 | %foreign "scheme:(lambda (v b) (bytevector-s64-set! (car b) (cdr b) v 'big) (set-cdr! b (+ 8 (cdr b))))"
82 | "javascript:lambda:(x,b,w) => {const n = BigInt.asUintN(64,x); const nx = Number(n & 0xffffffffn); const ny = Number((n >> 32n) & 0xffffffffn); b.view.setUint32(b.pos, ny, false); b.pos += 4; b.view.setUint32(b.pos, nx, false); b.pos += 4;}"
83 | prim__putint64be : Int64 -> AnyPtr -> PrimIO ()
85 | %foreign "scheme:(lambda (b) (cdr b))"
86 | "javascript:lambda:(b,w) => b.pos"
87 | prim__buildersize : AnyPtr -> PrimIO Bits32
89 | %foreign "scheme:(lambda (b) (let ((bv (make-bytevector (cdr b) 0))) (bytevector-copy! (car b) 0 bv 0 (cdr b)) (set-cdr! b 0) bv))"
90 | "javascript:lambda:(b,w) => {const res = new Uint8Array(b.buffer.slice(0, b.pos)); b.pos = 0; return res;}"
91 | prim__builderbytes : AnyPtr -> PrimIO Buffer
98 | record Builder q where
104 | builder : {default 128 size : Bits32} -> F1 q (Builder q)
105 | builder t = let p # t := ffi (prim__builder size) t in B p # t
109 | {default 128 size : Bits32}
110 | -> (run : forall q . Builder q => F1 q a)
113 | run1 $
\t => let b # t := builder t in run @{b} t
115 | parameters {auto b : Builder q}
118 | checksize : Bits32 -> F1' q
119 | checksize n = ffi $
prim__checksize n b.ptr
122 | putBits8 : Bits8 -> F1' q
123 | putBits8 v t = let _ # t := checksize 1 t in ffi (prim__putbits8 v b.ptr) t
126 | putBits16LE : Bits16 -> F1' q
127 | putBits16LE v t = let _ # t := checksize 2 t in ffi (prim__putbits16le v b.ptr) t
130 | putBits16BE : Bits16 -> F1' q
131 | putBits16BE v t = let _ # t := checksize 2 t in ffi (prim__putbits16be v b.ptr) t
134 | putBits32LE : Bits32 -> F1' q
135 | putBits32LE v t = let _ # t := checksize 4 t in ffi (prim__putbits32le v b.ptr) t
138 | putBits32BE : Bits32 -> F1' q
139 | putBits32BE v t = let _ # t := checksize 4 t in ffi (prim__putbits32be v b.ptr) t
142 | putBits64LE : Bits64 -> F1' q
143 | putBits64LE v t = let _ # t := checksize 8 t in ffi (prim__putbits64le v b.ptr) t
146 | putBits64BE : Bits64 -> F1' q
147 | putBits64BE v t = let _ # t := checksize 8 t in ffi (prim__putbits64be v b.ptr) t
150 | putInt8 : Int8 -> F1' q
151 | putInt8 v t = let _ # t := checksize 1 t in ffi (prim__putint8 v b.ptr) t
154 | putInt16LE : Int16 -> F1' q
155 | putInt16LE v t = let _ # t := checksize 2 t in ffi (prim__putint16le v b.ptr) t
158 | putInt16BE : Int16 -> F1' q
159 | putInt16BE v t = let _ # t := checksize 2 t in ffi (prim__putint16be v b.ptr) t
162 | putInt32LE : Int32 -> F1' q
163 | putInt32LE v t = let _ # t := checksize 4 t in ffi (prim__putint32le v b.ptr) t
166 | putInt32BE : Int32 -> F1' q
167 | putInt32BE v t = let _ # t := checksize 4 t in ffi (prim__putint32be v b.ptr) t
170 | putInt64LE : Int64 -> F1' q
171 | putInt64LE v t = let _ # t := checksize 8 t in ffi (prim__putint64le v b.ptr) t
174 | putInt64BE : Int64 -> F1' q
175 | putInt64BE v t = let _ # t := checksize 8 t in ffi (prim__putint64be v b.ptr) t
179 | (offset, len : Nat)
181 | -> {auto 0 lte : LTE (offset+len) n}
183 | putBytesFrom offset len buf t =
185 | _ # t := checksize sz t
186 | in ffi (prim__putbytes (cast offset) sz (unsafeGetBuffer buf) b.ptr) t
189 | putBytes : {n : _} -> IBuffer n -> F1' q
192 | _ # t := checksize sz t
193 | in ffi (prim__putbytes 0 sz (unsafeGetBuffer buf) b.ptr) t
196 | putAnyBytes : AnyBuffer -> F1' q
197 | putAnyBytes (AB _ ib) = putBytes ib
200 | putString : String -> F1' q
201 | putString s = putBytes (fromString s)
204 | putChar : Char -> F1' q
205 | putChar = putString . singleton
208 | putMBytes : {n : _} -> MBuffer q n -> F1' q
209 | putMBytes m t = let ib # t := unsafeFreeze m t in putBytes ib t
212 | getBytes : F1 q AnyBuffer
214 | let sz # t := ffi (prim__buildersize b.ptr) t
215 | buf # t := ffi (prim__builderbytes b.ptr) t
216 | in AB (cast sz) (unsafeMakeBuffer buf) # t
219 | getString : F1 q String
220 | getString t = let ab # t := getBytes t in cast ab # t
223 | fastConcat : List AnyBuffer -> AnyBuffer
224 | fastConcat bs = withBuilder (go bs)
226 | go : Builder q => List AnyBuffer -> F1 q AnyBuffer
227 | go [] t = getBytes t
228 | go (x :: xs) t = let _ # t := putAnyBytes x t in go xs t