src/Fs.bend
mylsm-lsm-store@0.4.0.0 · 137 lines · 0 definitions
1import Base
2import bend-kit-bytes@0.3.2.0/bytes.bend as StorageBytes
3import bend-kit-files@0.1.1.0/files.bend as PackedFiles
4
5# Audited host effects (spec §3.3). Thin syscall wrappers with .c + .js
6# twins and matching intended semantics. No laws — validated empirically.
7
8# Read at most 1 MiB as packed words. Short reads are valid progress; zero is EOF.
9def read_words(
10 file: File,
11 max: U32
12) ->
13 IO(File & Result<&1, &1, U32 & String, U32 & Array<U32>>):
14 PackedFiles.read.words(file, max)
15
16# Write all bytes from a packed word array, retaining the file handle on errors.
17def write_words(
18 file: File,
19 len: U32,
20 words: Array<U32>
21) ->
22 IO(File & Result<&1, &1, U32 & String, Unit>):
23 PackedFiles.write.words(file, len, words)
24
25def read_bytes.wrap(
26 result: Result<&1, &1, U32 & String, U32 & Array<U32>>
27) ->
28 Result<&1, &1, U32 & String, StorageBytes.Bytes>:
29 match result:
30 case Fail{err}:
31 Fail{err}
32 case Done{(len, words)}:
33 Done{StorageBytes.Bytes{len, words}}
34
35def read_bytes.pair(
36 pair: File & Result<&1, &1, U32 & String, U32 & Array<U32>>
37) ->
38 File & Result<&1, &1, U32 & String, StorageBytes.Bytes>:
39 match pair:
40 case (handle, result):
41 (handle, read_bytes.wrap(result))
42
43# Read one bounded packed chunk; nonempty short reads are not EOF.
44def read_bytes(
45 file: File,
46 max: U32
47) ->
48 IO(File & Result<&1, &1, U32 & String, StorageBytes.Bytes>):
49 do IO<File & Result<&1, &1, U32 & String, StorageBytes.Bytes>>:
50 pair : File & Result<&1, &1, U32 & String, U32 & Array<U32>> <- read_words(file, max)
51 return read_bytes.pair(pair)
52
53# Write the significant bytes of a packed buffer through the pinned host effect.
54def write_bytes(
55 file: File,
56 bytes: StorageBytes.Bytes
57) ->
58 IO(File & Result<&1, &1, U32 & String, Unit>):
59 StorageBytes.Bytes{len, buf} = bytes
60 write_words(file, len, buf)
61
62# Sync file contents to stable storage.
63def fsync(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
64 import "./effs/fsync.c"
65 import "./effs/fsync.js"
66
67# Handle truncate in the filesystem effects.
68def truncate(path: String, offset: Nat) -> IO(Result<&1, &1, U32 & String, Unit>):
69 import "./effs/truncate.c"
70 import "./effs/truncate.js"
71
72# Atomically rename a filesystem path.
73def rename(old: String, new: String) -> IO(Result<&1, &1, U32 & String, Unit>):
74 import "./effs/rename.c"
75 import "./effs/rename.js"
76
77# Remove a file or empty directory.
78def remove(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
79 import "./effs/remove.c"
80 import "./effs/remove.js"
81
82# Return the number of entries available through the indexed directory API.
83def read_dir_count(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
84 import "./effs/read_dir.c"
85 import "./effs/read_dir.js"
86
87# Fetch one directory entry by index.
88def read_dir_at(path: String, idx: Nat) -> IO(Result<&1, &1, U32 & String, String>):
89 import "./effs/read_dir.c"
90 import "./effs/read_dir.js"
91
92# Create one directory.
93def make_dir(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
94 import "./effs/make_dir.c"
95 import "./effs/make_dir.js"
96
97# Set POSIX permission bits.
98def chmod(path: String, bits: U32) -> IO(Result<&1, &1, U32 & String, Unit>):
99 import "./effs/chmod.c"
100 import "./effs/chmod.js"
101
102# Check whether a filesystem path exists.
103def exists(path: String) -> IO(Result<&1, &1, U32 & String, Bool>):
104 import "./effs/exists.c"
105 import "./effs/exists.js"
106
107# Read-only byte size for Bend-side accounting (no shell wc needed).
108def file_size(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
109 import "./effs/file_size.c"
110 import "./effs/file_size.js"
111
112# Pure accumulator step (leaf: matches structurally, never recurses).
113# Past-end fetches answer "" (SNil{}), which is skipped.
114def grab_name(nm: String, acc: List<String>) -> List<String>:
115 match nm:
116 case SNil{}:
117 acc
118 case SCon{_, _}:
119 Con{nm, acc}
120
121# Fuel-bounded sweep 0..count-1. Startup-only use (spec §10 below): the
122# directory is stable during recovery, so count-then-fetch is exact.
123def read_go(fuel: Nat, +path: String, +idx: Nat, acc: List<String>) -> IO(List<String>):
124 match fuel:
125 case 0n:
126 IO.pure(List<String>, List.reverse(&1, String, acc))
127 case 1n+f:
128 do IO<List<String>>:
129 nm : String <- IO.try(String, read_dir_at(path, idx))
130 read_go(f, path, Nat.add(idx, 1n), grab_name(nm, acc))
131
132# List directory names using the bounded count-then-fetch host API.
133def read_dir(+path: String) -> IO(Result<&1, &1, U32 & String, List<String>>):
134 do IO<Result<&1, &1, U32 & String, List<String>>>:
135 n : Nat <- IO.try(Nat, read_dir_count(path))
136 names : List<String> <- read_go(Nat.add(n, 1n), path, 0n, Nil{})
137 return Done{names}