src/args.bend
bolt@1.25.0.0 · 186 lines · 0 definitions
1# src/args: bolt's command line, parsed by shake. `bolt [lint] [file..]`,
2# `bolt check file..`, `bolt lsp`, `bolt --version`. A rest positional at the root (and on
3# `lint` / `check`) takes every leftover word, so `bolt a.bend b.bend` lints
4# those files. `help` is shake's usage page, and `--help` asks for the same
5# page (`line`). IO.args gives the program as invoked first, then its
6# arguments (bend 2.0.32); `argv` drops the program. A compiled binary passes
7# its whole line through except its runtime options, which stand between
8# `+RTS` and `-RTS` (bend 2.0.38): `--threads` and `--gpu` outside that
9# bracket reach the program, and `--RTS` hands everything after it to the
10# program. `--help` reaches the program (bend 2.0.29).
11# `out` is every decision the line makes, as data: what to print, where, and
12# the exit code, or the subcommand to run and its files. main only does it.
13# Only shake's interface (main.bend) is read here; what `parse` answers for a
14# given argv is shake's guarantee, not bolt's: shake v0.6.0, pinned by hash,
15# proves it in its own gate, and the laws naming an argv take shake's answer as
16# a premise and prove what bolt does with it. Of shake's assumptions bolt
17# trusts one: the words a compiled bolt's argv holds are the runtime's (its
18# options, between `+RTS` and `-RTS`, never reach it), which no law reaches.
19import Base
20import shake@0.6.0.0/main.bend as Shake
21import bolt@1.25.0.0/src/version.bend as Ver
22import bolt@1.25.0.0/src/build_rev.bend as Rev
23import bolt@1.25.0.0/src/lazy/lazy.bend as Lazy
24
25# the line at the quantity the rest of bolt reads it at (IO.args gives each
26# argument once)
27def widen(ss: List<&1, String>) -> List<&2, String>:
28 match ss:
29 case Nil{}:
30 Nil{}
31 case Con{s, t}:
32 s <> widen(t)
33
34# the arguments of IO.args's line: the program as invoked comes first, and is
35# dropped
36def args_of(ss: List<&1, String>) -> List<&2, String>:
37 match ss:
38 case Nil{}:
39 Nil{}
40 case Con{_prog, t}:
41 widen(t)
42
43# bolt's command line: its arguments, without the program
44def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv
45 do IO<List<&2, String>>:
46 ss : List<&1, String> <- IO.args()
47 return args_of(ss)
48
49# whether a word names a subcommand
50def is_cmd(+ww: String) -> Bool:
51 Bool.or(String.eq(ww, "lint"), Bool.or(String.eq(ww, "check"), String.eq(ww, "lsp")))
52
53# whether `--help` stands among the words before the first `--` (after it,
54# every word is a file); the search stops at either
55def asks_help(ws: List<&2, String>) -> Bool:
56 match ws:
57 case Nil{}:
58 False{}
59 case Con{+ww, rest}:
60 Lazy.and_then(Bool.not(String.eq(ww, "--")), _u => Lazy.or_else(String.eq(ww, "--help"), _v => asks_help(rest)))
61
62# the command path `--help` asks about: the first word other than `--help`,
63# when it names a subcommand, else the root's
64def help_path(ws: List<&2, String>) -> List<&2, String>:
65 match ws:
66 case Nil{}:
67 Nil{}
68 case Con{+ww, rest}:
69 Lazy.either(List<&2, String>, String.eq(ww, "--help"), _u => help_path(rest),
70 _u => Bool.pick(List<&2, String>, is_cmd(ww), [ww], []))
71
72# the line, given whether it asks for `--help`
73def line.at(ask: Bool, +ws: List<&2, String>) -> List<&2, String>:
74 match ask:
75 case True{}:
76 "help" <> help_path(ws)
77 case False{}:
78 ws
79
80# the line shake parses: one that asks for `--help` is `help` for its command
81# path, the page `bolt help` prints; any other is itself
82def line(+ws: List<&2, String>) -> List<&2, String>:
83 line.at(asks_help(ws), ws)
84
85# the files rest, optional, last among positionals
86def spec.files(+help: String) -> Shake.Arg:
87 Shake.rest("files", help, False{}, None{}, [])
88
89# the release, with the short commit in parentheses when it is present
90def version.at(+rel: String, +rev: String) -> String:
91 Bool.pick(String, String.is_empty(rev), rel, rel ++ " (" ++ rev ++ ")")
92
93# the release, and the short commit when the build has one
94def version() -> String:
95 version.at(Ver.text(), Rev.text())
96
97# bolt's program spec
98def spec() -> Shake.Cli:
99 Shake.app("bolt", "A linter, checker and language server for Bend 2.", Some{version()},
100 [Shake.flag("version", None{}, Some{"version"}, "Print the version"),
101 spec.files("Files to lint")],
102 [Shake.sub("lint", "Lint files", [spec.files("Files to lint")], []),
103 Shake.sub("check", "Check files", [spec.files("Files to check")], []),
104 Shake.sub("lsp", "Serve an editor over stdio", [], [])])
105
106# argv against bolt's spec
107def parse(av: List<&2, String>) -> Result<&2, &2, Shake.ParseErr, Shake.Matched>:
108 Shake.parse(spec(), av)
109
110# usage for a command path
111def help_text(path: List<&2, String>) -> String:
112 Shake.help(spec(), path)
113
114# a parse error as the text the binary prints
115def err_text(ee: Shake.ParseErr) -> String:
116 Shake.err_text(spec(), ee)
117
118# a subcommand
119type Cmd is Data:
120 CLint{}
121 CCheck{}
122 CLsp{}
123
124# a subcommand by its name; the empty name (no subcommand) is `lint`
125def command(+name: String) -> Cmd:
126 Bool.pick(Cmd, String.eq(name, "check"), CCheck{},
127 Bool.pick(Cmd, String.eq(name, "lsp"), CLsp{}, CLint{}))
128
129# where a line that stops puts its text
130type Stream is Data:
131 Line{}
132 Page{}
133 Err{}
134
135# what a parsed line does: print a text and exit with a code, or run a
136# subcommand over files (which then exits as that command decides)
137type Out is Data:
138 Stop{to: Stream, text: String, code: U32}
139 Go{cmd: Cmd, paths: List<&2, String>}
140
141# the files the selected command bound: each command keeps its own
142# bindings, so they are read from the Matched at the end of the selected
143# path, which is the root's own when no subcommand was selected
144def files.at(sel: Maybe<&2, Shake.Matched>, +mm: Shake.Matched) -> List<&2, String>:
145 match sel:
146 case Some{ss}:
147 Shake.get_all(ss, "files")
148 case None{}:
149 Shake.get_all(mm, "files")
150
151# the files a successful parse bound, to the command it selected
152def files(+mm: Shake.Matched) -> List<&2, String>:
153 files.at(Shake.at(mm, Shake.path_of(mm)), mm)
154
155# a successful parse: the version, or the selected command and its files
156def out.run(ask: Bool, +mm: Shake.Matched) -> Out:
157 match ask:
158 case True{}:
159 Stop{Line{}, "bolt " ++ version(), 0}
160 case False{}:
161 Go{command(String.join(Shake.path_of(mm), "/")), files(mm)}
162
163# a failed parse, given whether it asked for usage: that usage page, or the
164# error
165def out.fail.at(asked: Maybe<&2, List<&2, String>>, +ee: Shake.ParseErr) -> Out:
166 match asked:
167 case Some{path}:
168 Stop{Page{}, help_text(path), 0}
169 case None{}:
170 Stop{Err{}, err_text(ee), 1}
171
172# a failed parse: help text, or an error
173def out.fail(+ee: Shake.ParseErr) -> Out:
174 out.fail.at(Shake.help_path(ee), ee)
175
176# a successful parse, read once for the version flag
177def out.done(+mm: Shake.Matched) -> Out:
178 out.run(Shake.on(mm, "version"), mm)
179
180# what a parse result does
181def out(rr: Result<&2, &2, Shake.ParseErr, Shake.Matched>) -> Out:
182 match rr:
183 case Fail{e}:
184 out.fail(e)
185 case Done{m}:
186 out.done(m)