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).
8	import Base
9	
10	def 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
21	def 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	
30	def 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	
38	type Gr is Type:
39	  Gr{src: Array<U32>, dst: Array<U32>}
40	
41	def 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	
45	def 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	
52	def gr_dst(st: Gr) -> Array<U32>:
53	  match st:
54	    case Gr{src, dst}:
55	      dst
56	
57	def 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
61	def 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	
70	def 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	
79	def 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	
83	def 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
88	def 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	
91	def 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
96	def 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	
107	def 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	
111	def 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	
115	def 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	
119	def 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	
123	def 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	
127	def 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	
131	def 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	
135	def 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	
139	def fail(what: String, e: U32 & String) -> IO(Unit):
140	  (code, msg) = e
141	  IO.die(Unit, 1, what ++ ": " ++ msg)
142	
143	def 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	
152	def 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	
157	def 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	
166	def 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
177	def 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	
182	def 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	
187	def drop(a: Array<U32>) -> IO(Unit):
188	  IO.pure(Unit, Unit{})
189	
190	def 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	
199	def 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	
204	def 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
211	def 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	
218	type Chunk is Type:
219	  Chunk{file: File, a: Array<U32>, n: U32}
220	
221	def 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	
232	def 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	
246	def 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	
258	type Sink is Type:
259	  Sink{a: Array<U32>, cap: U32, pos: U32}
260	
261	def 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	
268	def sink_new() -> Sink:
269	  Sink{Array.new(U32, 16n, 0), 65536, 0}
270	
271	def 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
276	def ob_room(a: Array<U32>, +cap: U32, +pos: U32, +need: U32) -> Sink:
277	  ob_fit(room(a, cap, ((need >> 2n) + 4 : U32)), pos)
278	
279	def 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	
283	def 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	
289	def 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	
295	def 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	
302	def 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.
309	def 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	
317	def 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
324	def 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
332	def skip(st: Sink, +n: U32) -> Sink:
333	  match st:
334	    case Sink{a, cap, pos}:
335	      Sink{a, cap, (pos + n : U32)}
336	
337	def 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	
343	def 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))