src/Fs.bend
mylsm-lsm-store@0.3.1.0 · 75 lines · 0 definitions
1import Base
2
3# Audited host effects (spec §3.3). Thin syscall wrappers with .c + .js
4# twins and matching intended semantics. No laws — validated empirically.
5
6def fsync(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
7 import "./effs/fsync.c"
8 import "./effs/fsync.js"
9
10def rename(old: String, new: String) -> IO(Result<&1, &1, U32 & String, Unit>):
11 import "./effs/rename.c"
12 import "./effs/rename.js"
13
14def remove(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
15 import "./effs/remove.c"
16 import "./effs/remove.js"
17
18def read_dir_count(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
19 import "./effs/read_dir.c"
20 import "./effs/read_dir.js"
21
22def read_dir_at(path: String, idx: Nat) -> IO(Result<&1, &1, U32 & String, String>):
23 import "./effs/read_dir.c"
24 import "./effs/read_dir.js"
25
26def make_dir(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
27 import "./effs/make_dir.c"
28 import "./effs/make_dir.js"
29
30def chmod(path: String, bits: U32) -> IO(Result<&1, &1, U32 & String, Unit>):
31 import "./effs/chmod.c"
32 import "./effs/chmod.js"
33
34def exists(path: String) -> IO(Result<&1, &1, U32 & String, Bool>):
35 import "./effs/exists.c"
36 import "./effs/exists.js"
37
38# Read-only byte size for Bend-side accounting (no shell wc needed).
39def file_size(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
40 import "./effs/file_size.c"
41 import "./effs/file_size.js"
42
43# Returns `<byte-count>;<text>` for a positional chunk whose end is adjusted to
44# a complete UTF-8 boundary. The byte count advances the next positional read.
45def read_utf8_chunk(path: String, offset: Nat, max_bytes: Nat) -> IO(Result<&1, &1, U32 & String, String>):
46 import "./effs/read_utf8_chunk.c"
47 import "./effs/read_utf8_chunk.js"
48
49# Pure accumulator step (leaf: matches structurally, never recurses).
50# Past-end fetches answer "" (SNil{}), which is skipped.
51
52def grab_name(nm: String, acc: List<String>) -> List<String>:
53 match nm:
54 case SNil{}:
55 acc
56 case SCon{_, _}:
57 Con{nm, acc}
58
59# Fuel-bounded sweep 0..count-1. Startup-only use (spec §10 below): the
60# directory is stable during recovery, so count-then-fetch is exact.
61
62def read_go(fuel: Nat, +path: String, +idx: Nat, acc: List<String>) -> IO(List<String>):
63 match fuel:
64 case 0n:
65 IO.pure(List<String>, List.reverse(&1, String, acc))
66 case 1n+f:
67 do IO<List<String>>:
68 nm : String <- IO.try(String, read_dir_at(path, idx))
69 read_go(f, path, Nat.add(idx, 1n), grab_name(nm, acc))
70
71def read_dir(+path: String) -> IO(Result<&1, &1, U32 & String, List<String>>):
72 do IO<Result<&1, &1, U32 & String, List<String>>>:
73 n : Nat <- IO.try(Nat, read_dir_count(path))
74 names : List<String> <- read_go(Nat.add(n, 1n), path, 0n, Nil{})
75 return Done{names}