src/lsp/files/disk.bend
bolt@1.17.0.0 · 87 lines · 0 definitions
1# files/disk: the real file system. Reads bytes and decodes them itself, as a
2# chunk may end inside a UTF-8 char.
3import Base
4import bolt@1.17.0.0/src/lsp/files/service.bend as S
5import bolt@1.17.0.0/src/lsp/frame.bend as Frame
6import bolt@1.17.0.0/src/walk/disk.bend as WalkDisk
7
8def slurp.end(file: File, acc: List<&2, U32>) -> IO(Maybe<&2, String>):
9 do IO<Maybe<&2, String>>:
10 File.close(file)
11 return Some{Frame.decode(acc)}
12
13def slurp.cut(
14 bytes: List<&2, U32>,
15 file: File,
16 acc: List<&2, U32>,
17 rest: File -> List<&2, U32> -> IO(Maybe<&2, String>)
18) -> IO(Maybe<&2, String>):
19 match bytes:
20 case Nil{}:
21 slurp.end(file, acc)
22 case Con{b, t}:
23 rest(file, List.append(&2, U32, acc, b <> t))
24
25def slurp.more(
26 rr: Result<&1, &1, U32 & String, List<&2, U32>>,
27 file: File,
28 acc: List<&2, U32>,
29 rest: File -> List<&2, U32> -> IO(Maybe<&2, String>)
30) -> IO(Maybe<&2, String>):
31 match rr:
32 case Fail{e}:
33 slurp.end(file, acc)
34 case Done{bytes}:
35 slurp.cut(bytes, file, acc, rest)
36
37def slurp.next(
38 got: File & Result<&1, &1, U32 & String, List<&2, U32>>,
39 acc: List<&2, U32>,
40 rest: File -> List<&2, U32> -> IO(Maybe<&2, String>)
41) -> IO(Maybe<&2, String>):
42 (file, r) = got
43 slurp.more(r, file, acc, rest)
44
45# the whole file, read in chunks until one is empty, or the fuel is
46def slurp(fuel: Nat, file: File, acc: List<&2, U32>) -> IO(Maybe<&2, String>): # noqa: L001 disk effect
47 match fuel:
48 case 0n:
49 slurp.end(file, acc)
50 case 1n+f:
51 do IO<Maybe<&2, String>>:
52 got : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_bytes(file, 65536)
53 slurp.next(got, acc, fl => a => slurp(f, fl, a))
54
55def read.opened(rr: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
56 match rr:
57 case Fail{e}:
58 IO.pure(Maybe<&2, String>, None{})
59 case Done{file}:
60 slurp(U32.to_nat(100000), file, [])
61
62# a file's text, or None when it cannot be opened
63def read(path: String) -> IO(Maybe<&2, String>): # noqa: L001 disk effect
64 do IO<Maybe<&2, String>>:
65 r : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
66 read.opened(r)
67
68def base_path.of(rr: Result<&1, &1, U32 & String, String>) -> IO(String):
69 match rr:
70 case Fail{e}:
71 IO.pure(String, "")
72 case Done{home}:
73 IO.pure(String, home ++ "/.bend/current/bend2/base.bend")
74
75# Base, where bend's installer puts it
76def base_path(_u: Unit) -> IO(String): # noqa: L001 disk effect
77 do IO<String>:
78 r : Result<&1, &1, U32 & String, String> <- IO.get_env("HOME")
79 base_path.of(r)
80
81# the working directory, as the lint's walk names it
82def cwd(_u: Unit) -> IO(String): # noqa: L001 disk effect
83 WalkDisk.cwd()
84
85# the real file system
86def new() -> S.Files: # noqa: L001 effect record
87 S.Files{read, base_path, cwd}