words.bend

gralha-byte-words@0.1.0.0 · 344 lines · 55 definitions

1# gralha-byte-words: bytes packed four to a U32 word, little-endian, in an
2# Array<U32>, the layer the gralha codecs share. byte_at and le32_at read
3# a byte or a four-byte window at any offset; Sink is a growing output
4# buffer (put_byte, put_str, put_le32, put_zeros, reserve, skip); the
5# effects under effs/ move packed words to and from files without a
6# byte-per-cell detour (read, write, fill_at, append, copy_range,
7# file_read_at, sink_write, open_out, file_size).
8import Base
9
10def b2u(b: Bool) -> U32:
11  match b:
12    case False{}:
13      0
14    case True{}:
15      1
16
17# Arrays
18# ------
19
20# the smallest depth d with 2^d >= need
21def fit(n: Nat, +d: U32, +need: U32, ok: Bool) -> U32:
22  match n, ok:
23    case k, True{}:
24      d
25    case 0n, False{}:
26      d
27    case 1n+p, False{}:
28      fit(p, (d + 1 : U32), need, U32.is_ge(U32.shln(1, U32.to_nat((d + 1 : U32))), need))
29
30def depth_for(+need: U32) -> Nat:
31  U32.to_nat(fit(31n, 0, need, U32.is_le(need, 1)))
32
33# Output growth
34# -------------
35# the output doubles when a write would pass its capacity, so the size
36# need not be known up front (bsdtar pads a piped archive past its trailer)
37
38type Gr is Type:
39  Gr{src: Array<U32>, dst: Array<U32>}
40
41def gr_put(r: Array<U32> & U32, dst: Array<U32>, +i: U32) -> Gr:
42  (src, v) = r
43  Gr{src, Array.set(U32, dst, i, v)}
44
45def gr_loop(n: Nat, st: Gr, +i: U32) -> Gr:
46  match n, st:
47    case 0n, r:
48      r
49    case 1n+p, Gr{src, dst}:
50      gr_loop(p, gr_put(Array.get(U32, src, i), dst, i), (i + 1 : U32))
51
52def gr_dst(st: Gr) -> Array<U32>:
53  match st:
54    case Gr{src, dst}:
55      dst
56
57def grow(out: Array<U32>, +cap: U32) -> Array<U32>:
58  gr_dst(gr_loop(U32.to_nat(cap), Gr{out, Array.new(U32, depth_for((cap * 2 : U32)), 0)}, 0))
59
60# (out, cap) with cap >= need; ok says it already is
61def ensure(n: Nat, out: Array<U32>, +cap: U32, +need: U32, ok: Bool) -> Array<U32> & U32:
62  match n, ok:
63    case k, True{}:
64      (out, cap)
65    case 0n, False{}:
66      (out, cap)
67    case 1n+p, False{}:
68      ensure(p, grow(out, cap), (cap * 2 : U32), need, U32.is_ge((cap * 2 : U32), need))
69
70def room(out: Array<U32>, +cap: U32, +need: U32) -> Array<U32> & U32:
71  ensure(32n, out, cap, need, U32.is_ge(cap, need))
72
73# Packed input
74# ------------
75# the input packed four bytes to a word, little-endian: a byte is one
76# read and a shift, the window at any byte offset two reads combined.
77# The memory is a byte per byte.
78
79def w4_hi(r: Array<U32> & U32, +lo: U32, +sh: U32) -> Array<U32> & U32:
80  (a, v) = r
81  (a, (lo .|. (U32.shln(v, U32.to_nat((24 - sh : U32))) << 8n) : U32))
82
83def w4_lo(r: Array<U32> & U32, +q: U32, +sh: U32) -> Array<U32> & U32:
84  (a, v) = r
85  w4_hi(Array.get(U32, a, (q + 1 : U32)), U32.shrn(v, U32.to_nat(sh)), sh)
86
87# the four bytes from j, j lowest
88def le32_at(a: Array<U32>, +j: U32) -> Array<U32> & U32:
89  w4_lo(Array.get(U32, a, (j >> 2n : U32)), (j >> 2n : U32), ((j .&. 3) << 3n : U32))
90
91def wb_of(r: Array<U32> & U32, +sh: U32) -> Array<U32> & U32:
92  (a, v) = r
93  (a, (U32.shrn(v, U32.to_nat(sh)) .&. 255 : U32))
94
95# the byte at j
96def byte_at(a: Array<U32>, +j: U32) -> Array<U32> & U32:
97  wb_of(Array.get(U32, a, (j >> 2n : U32)), ((j .&. 3) << 3n : U32))
98
99# Files
100# -----
101# a file's bytes come and go as words: four bytes to a word,
102# little-endian, zero padded past the end with three spare words, so
103# the codec's windows never fall off. The effects are foreign C and JS
104# under effs/. A `_raw` effect answers its Result; its plain twin exits
105# the program with the error instead.
106
107def read_raw(path: String) -> IO(Result<&1, &1, U32 & String, Array<U32> & U32>):
108  import "./effs/words_read.c"
109  import "./effs/words_read.js"
110
111def write_raw(path: String, a: Array<U32>, +start: U32, +n: U32) -> IO(Array<U32> & Result<&1, &1, U32 & String, Unit>):
112  import "./effs/words_write.c"
113  import "./effs/words_write.js"
114
115def fill_at_raw(path: String, +file_off: U32, a: Array<U32>, +start: U32, +n: U32) -> IO(Array<U32> & Result<&1, &1, U32 & String, Unit>):
116  import "./effs/words_fill_at.c"
117  import "./effs/words_fill_at.js"
118
119def append_raw(path: String, a: Array<U32>, +header_n: U32, input: String, +pad_n: U32, +first: U32) -> IO(Array<U32> & Result<&1, &1, U32 & String, Unit>):
120  import "./effs/stream_append.c"
121  import "./effs/stream_append.js"
122
123def copy_range(src: Array<U32>, +src_at: U32, dst: Array<U32>, +dst_at: U32, +n: U32) -> IO(Array<U32> & Array<U32>):
124  import "./effs/words_copy_range.c"
125  import "./effs/words_copy_range.js"
126
127def file_write_raw(file: File, a: Array<U32>, +start: U32, +n: U32) -> IO(File & Array<U32> & Result<&1, &1, U32 & String, Unit>):
128  import "./effs/file_words_write.c"
129  import "./effs/file_words_write.js"
130
131def file_read_at_raw(file: File, +offset: U32, +max: U32) -> IO(File & Result<&1, &1, U32 & String, Array<U32> & U32>):
132  import "./effs/file_words_read_at.c"
133  import "./effs/file_words_read_at.js"
134
135def open_out_raw(path: String) -> IO(Result<&1, &1, U32 & String, File>):
136  import "./effs/output_open.c"
137  import "./effs/output_open.js"
138
139def fail(what: String, e: U32 & String) -> IO(Unit):
140  (code, msg) = e
141  IO.die(Unit, 1, what ++ ": " ++ msg)
142
143def read_got(what: String, r: Result<&1, &1, U32 & String, Array<U32> & U32>) -> IO(Array<U32> & U32):
144  match r:
145    case Done{v}:
146      IO.pure(Array<U32> & U32, v)
147    case Fail{e}:
148      do IO<Array<U32> & U32>:
149        Unit <- fail(what, e)
150        IO.die(Array<U32> & U32, 1, "unreachable")
151
152def read(+path: String) -> IO(Array<U32> & U32):
153  do IO<Array<U32> & U32>:
154    r : Result<&1, &1, U32 & String, Array<U32> & U32> <- read_raw(path)
155    read_got(path, r)
156
157def size_got(what: String, r: Result<&1, &1, U32 & String, U32>) -> IO(U32):
158  match r:
159    case Done{n}:
160      IO.pure(U32, n)
161    case Fail{e}:
162      do IO<U32>:
163        Unit <- fail(what, e)
164        IO.die(U32, 1, "unreachable")
165
166def wr_done(what: String, r: Array<U32> & Result<&1, &1, U32 & String, Unit>) -> IO(Array<U32>):
167  (a, w) = r
168  match w:
169    case Done{u}:
170      IO.pure(Array<U32>, a)
171    case Fail{e}:
172      do IO<Array<U32>>:
173        Unit <- fail(what, e)
174        return a
175
176# n bytes of a from byte start; the words come back
177def write(+path: String, a: Array<U32>, +start: U32, +n: U32) -> IO(Array<U32>):
178  do IO<Array<U32>>:
179    r : Array<U32> & Result<&1, &1, U32 & String, Unit> <- write_raw(path, a, start, n)
180    wr_done(path, r)
181
182def fill_at(+path: String, +file_off: U32, a: Array<U32>, +start: U32, +n: U32) -> IO(Array<U32>):
183  do IO<Array<U32>>:
184    r : Array<U32> & Result<&1, &1, U32 & String, Unit> <- fill_at_raw(path, file_off, a, start, n)
185    wr_done(path, r)
186
187def drop(a: Array<U32>) -> IO(Unit):
188  IO.pure(Unit, Unit{})
189
190def open_got(what: String, r: Result<&1, &1, U32 & String, File>) -> IO(File):
191  match r:
192    case Done{file}:
193      IO.pure(File, file)
194    case Fail{e}:
195      do IO<File>:
196        Unit <- fail(what, e)
197        IO.die(File, 1, "unreachable")
198
199def open_out(+path: String) -> IO(File):
200  do IO<File>:
201    r : Result<&1, &1, U32 & String, File> <- open_out_raw(path)
202    open_got(path, r)
203
204def size_close(what: String, r: File & Result<&1, &1, U32 & String, U32>) -> IO(U32):
205  (file, v) = r
206  do IO<U32>:
207    Unit <- File.close(file)
208    size_got(what, v)
209
210# a member's byte count, read off its open handle
211def file_size(+path: String) -> IO(U32):
212  do IO<U32>:
213    opened : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
214    file : File <- open_got(path, opened)
215    r : File & Result<&1, &1, U32 & String, U32> <- File.size(file)
216    size_close(path, r)
217
218type Chunk is Type:
219  Chunk{file: File, a: Array<U32>, n: U32}
220
221def file_read_got(what: String, r: File & Result<&1, &1, U32 & String, Array<U32> & U32>) -> IO(Chunk):
222  (file, v) = r
223  match v:
224    case Done{(a, n)}:
225      IO.pure(Chunk, Chunk{file, a, n})
226    case Fail{e}:
227      do IO<Chunk>:
228        Unit <- File.close(file)
229        Unit <- fail(what, e)
230        IO.die(Chunk, 1, "unreachable")
231
232def file_write_got(what: String, r: File & Array<U32> & Result<&1, &1, U32 & String, Unit>) -> IO(File):
233  (file, a, v) = r
234  match v:
235    case Done{u}:
236      do IO<File>:
237        Unit <- drop(a)
238        return file
239    case Fail{e}:
240      do IO<File>:
241        Unit <- drop(a)
242        Unit <- File.close(file)
243        Unit <- fail(what, e)
244        IO.die(File, 1, "unreachable")
245
246def append(+path: String, a: Array<U32>, +header_n: U32, +input: String, +pad_n: U32, first: Bool) -> IO(Unit):
247  do IO<Unit>:
248    r : Array<U32> & Result<&1, &1, U32 & String, Unit> <- append_raw(path, a, header_n, input, pad_n, b2u(first))
249    a2 : Array<U32> <- wr_done(path, r)
250    drop(a2)
251
252# Output
253# ------
254# a growing byte sink over packed words: cap counts words, pos bytes.
255# A byte lands by read-modify-write of its word; a run of zeros and a
256# word-aligned block of words go in whole.
257
258type Sink is Type:
259  Sink{a: Array<U32>, cap: U32, pos: U32}
260
261def sink_write(+path: String, file: File, st: Sink) -> IO(File):
262  match st:
263    case Sink{a, cap, pos}:
264      do IO<File>:
265        r : File & Array<U32> & Result<&1, &1, U32 & String, Unit> <- file_write_raw(file, a, 0, pos)
266        file_write_got(path, r)
267
268def sink_new() -> Sink:
269  Sink{Array.new(U32, 16n, 0), 65536, 0}
270
271def ob_fit(r: Array<U32> & U32, +pos: U32) -> Sink:
272  (a, cap) = r
273  Sink{a, cap, pos}
274
275# room for bytes up to need
276def ob_room(a: Array<U32>, +cap: U32, +pos: U32, +need: U32) -> Sink:
277  ob_fit(room(a, cap, ((need >> 2n) + 4 : U32)), pos)
278
279def ob_or(r: Array<U32> & U32, +cap: U32, +pos: U32, +b: U32) -> Sink:
280  (a, w) = r
281  Sink{Array.set(U32, a, (pos >> 2n : U32), (w .|. U32.shln(b, U32.to_nat(((pos .&. 3) << 3n : U32))) : U32)), cap, (pos + 1 : U32)}
282
283def ob_byte_at(st: Sink, +b: U32) -> Sink:
284  match st:
285    case Sink{a, cap, pos}:
286      +p = pos
287      ob_or(Array.get(U32, a, (p >> 2n : U32)), cap, p, b)
288
289def put_byte(st: Sink, +b: U32) -> Sink:
290  match st:
291    case Sink{a, cap, pos}:
292      +p = pos
293      ob_byte_at(ob_room(a, cap, p, (p + 1 : U32)), b)
294
295def ow_split(a: Array<U32>, +q: U32, +v: U32, +sh: U32, split: Bool) -> Array<U32>:
296  match split:
297    case True{}:
298      Array.set(U32, a, (q + 1 : U32), U32.shrn(v, U32.to_nat((32 - sh : U32))))
299    case False{}:
300      a
301
302def ob_word_got(r: Array<U32> & U32, +cap: U32, +pos: U32, +q: U32, +sh: U32, +v: U32) -> Sink:
303  (a, old) = r
304  Sink{ow_split(Array.set(U32, a, q, (old .|. U32.shln(v, U32.to_nat(sh)) : U32)), q, v, sh, U32.is_ne(sh, 0)), cap, (pos + 4 : U32)}
305
306# Four bytes into a previously reserved output range. The destination may be
307# unaligned; its already-written low bytes are preserved and the high spill
308# becomes the prefix of the next word.
309def put_word_at(st: Sink, +v: U32) -> Sink:
310  match st:
311    case Sink{a, cap, pos}:
312      +p = pos
313      +q = (p >> 2n : U32)
314      +sh = ((p .&. 3) << 3n : U32)
315      ob_word_got(Array.get(U32, a, q), cap, p, q, sh, v)
316
317def reserve(st: Sink, +n: U32) -> Sink:
318  match st:
319    case Sink{a, cap, pos}:
320      +p = pos
321      ob_room(a, cap, p, (p + n : U32))
322
323# n bytes of a string
324def put_str(s: String, st: Sink) -> Sink:
325  match s:
326    case SNil{}:
327      st
328    case SCon{Chr{c}, t}:
329      put_str(t, put_byte(st, c))
330
331# n zero bytes: the room is zero already
332def skip(st: Sink, +n: U32) -> Sink:
333  match st:
334    case Sink{a, cap, pos}:
335      Sink{a, cap, (pos + n : U32)}
336
337def put_zeros(st: Sink, +n: U32) -> Sink:
338  match st:
339    case Sink{a, cap, pos}:
340      +p = pos
341      skip(ob_room(a, cap, p, (p + n : U32)), n)
342
343def put_le32(ob: Sink, +v: U32) -> Sink:
344  put_byte(put_byte(put_byte(put_byte(ob, (v .&. 255 : U32)), ((v >> 8n) .&. 255 : U32)), ((v >> 16n) .&. 255 : U32)), (v >> 24n : U32))