run.bend
cli@0.1.0.0 · 124 lines · 0 definitions
1# Purpose: the public IO shell: probes the host, runs Cli.eval, writes its
2# output, calls act and exits (§7). The host effects live in sys.c and
3# sys.js; no law imports this file (F1).
4# Expected output: SOME PROOFS FAIL, listing only the defs that rely on
5# sys.c and sys.js (F1, G2).
6# Run: bend run.bend --check-only
7
8import Base
9import cli@0.1.0.0/cli.bend as Cli
10
11# 1 if fd is a terminal, else 0.
12def Sys.isatty(fd: U32) -> IO(U32):
13 import "./sys.c"
14 import "./sys.js"
15
16# fd's terminal width in columns, or 0 if it has none.
17def Sys.columns(fd: U32) -> IO(U32):
18 import "./sys.c"
19 import "./sys.js"
20
21def exit_when(zero: Bool, code: U32) -> IO(Unit):
22 match zero:
23 case True{}: IO.pure(Unit, Unit{})
24 case False{}: IO.exit(code)
25
26# 0 returns, so work started with IO.fork can finish; any other code
27# flushes stdout and ends the process at once.
28def exit(+code: U32) -> IO(Unit):
29 exit_when(U32.is_eq(code, 0), code)
30
31def chomp_end(newline: Bool, c: Char) -> String:
32 match newline:
33 case True{}: SNil{}
34 case False{}: SCon{c, SNil{}}
35
36# c then t, less one final "\n".
37def chomp_from(t: String, +c: Char) -> String:
38 match t:
39 case SNil{}: chomp_end(Char.is_eq(c, '\n'), c)
40 case SCon{d, u}: SCon{c, chomp_from(u, d)}
41
42# s less one final "\n": IO.print_err adds it back.
43def chomp(s: String) -> String:
44 match s:
45 case SNil{}: SNil{}
46 case SCon{c, t}: chomp_from(t, c)
47
48def write_out(empty: Bool, out: String) -> IO(Unit):
49 match empty:
50 case True{}: IO.pure(Unit, Unit{})
51 case False{}: IO.write(out)
52
53def write_err(empty: Bool, err: String) -> IO(Unit):
54 match empty:
55 case True{}: IO.pure(Unit, Unit{})
56 case False{}: IO.print_err(chomp(err))
57
58# §7.2 step 4: out to stdout and err to stderr, each if not empty, then exit.
59def finish(code: U32, +out: String, +err: String) -> IO(Unit):
60 do IO<Unit>:
61 write_out(String.is_empty(out), out)
62 write_err(String.is_empty(err), err)
63 exit(code)
64
65def var_found(name: String,
66 got: Result<&1, &1, U32 & String, String>) -> List<&2, Cli.Var>:
67 match got:
68 case Done{value}: [Cli.Var{name, value}]
69 case Fail{e}: []
70
71# Each set variable among names, in order.
72def read_vars(names: List<&2, String>) -> IO(List<&2, Cli.Var>):
73 match names:
74 case Nil{}: IO.pure(List<&2, Cli.Var>, [])
75 case +name <> tail:
76 do IO<List<&2, Cli.Var>>:
77 got : Result<&1, &1, U32 & String, String> <- IO.get_env(name)
78 rest : List<&2, Cli.Var> <- read_vars(tail)
79 return List.append(&2, Cli.Var, var_found(name, got), rest)
80
81# §7.3: the variables c reads, whether stdout and stderr are TTYs, and their
82# columns; Cli.probe decides the rest.
83def host(c: Cli.Cmd) -> IO(Cli.Host):
84 do IO<Cli.Host>:
85 vars : List<&2, Cli.Var> <- read_vars(Cli.vars(c))
86 out_tty : U32 <- Sys.isatty(1)
87 err_tty : U32 <- Sys.isatty(2)
88 out_cols : U32 <- Sys.columns(1)
89 err_cols : U32 <- Sys.columns(2)
90 return Cli.probe(vars, U32.is_eq(out_tty, 1), U32.is_eq(err_tty, 1),
91 out_cols, err_cols)
92
93def argv_list(args: List<String>) -> List<&2, String>:
94 match args:
95 case Nil{}: Nil{}
96 case arg <> tail: arg <> argv_list(tail)
97
98# IO.args without its head, the program as invoked.
99def argv_of(args: List<String>) -> List<&2, String>:
100 match args:
101 case Nil{}: Nil{}
102 case program <> tail: argv_list(tail)
103
104# §7.2 step 5: act's code, mapped by Cli.act_exit.
105def ended(r: (U32 & String)) -> IO(Unit):
106 match r:
107 case (code, err): finish(code, "", err)
108
109def stepped(~A: Type, ~act: @+t: Cli.Term -> A -> IO(U32),
110 s: Cli.Step<A>) -> IO(Unit):
111 match s:
112 case Cli.Quit{code, out, err}: finish(code, out, err)
113 case Cli.Go{a, t}:
114 do IO<Unit>:
115 n : U32 <- act(t, a)
116 ended(Cli.act_exit(n))
117
118# §7.2: an app's whole main.
119def main(~A: Type, ~decode: @+m: Cli.Matches -> Cli.Dec(A),
120 ~act: @+t: Cli.Term -> A -> IO(U32), +c: Cli.Cmd) -> IO(Unit):
121 do IO<Unit>:
122 args : List<String> <- IO.args()
123 h : Cli.Host <- host(c)
124 stepped(~A, ~act, Cli.eval(~A, ~decode, c, h, argv_of(args)))