run.bend

cli@0.2.0.0 · 139 lines · 20 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.2.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<List<&2, U32>>) -> List<&2, String>:
94  match args:
95    case Nil{}: Nil{}
96    case arg <> tail: Cli.arg_text(arg) <> argv_list(tail)
97
98# IO.args_bytes without its head, the program as invoked, each argument
99# decoded by Cli.arg_text, so Cli.arg_bytes gives back its bytes.
100def argv_of(args: List<List<&2, U32>>) -> List<&2, String>:
101  match args:
102    case Nil{}: Nil{}
103    case program <> tail: argv_list(tail)
104
105# §7.2 step 5: act's code, mapped by Cli.act_exit.
106def ended(r: (U32 & String)) -> IO(Unit):
107  match r:
108    case (code, err): finish(code, "", err)
109
110def stepped(~A: Type, ~act: @+t: Cli.Term -> A -> IO(U32),
111    s: Cli.Step<A>) -> IO(Unit):
112  match s:
113    case Cli.Quit{code, out, err}: finish(code, out, err)
114    case Cli.Go{a, t}:
115      do IO<Unit>:
116        n : U32 <- act(t, a)
117        ended(Cli.act_exit(n))
118
119# §7.2: an app's whole main.
120def main(~A: Type, ~decode: @+m: Cli.Matches -> Cli.Dec(A),
121    ~act: @+t: Cli.Term -> A -> IO(U32), +c: Cli.Cmd) -> IO(Unit):
122  do IO<Unit>:
123    args : List<List<&2, U32>> <- IO.args_bytes()
124    h : Cli.Host <- host(c)
125    stepped(~A, ~act, Cli.eval(~A, ~decode, c, h, argv_of(args)))
126
127def wrote(r: Cli.Ran) -> IO(Unit):
128  match r:
129    case Cli.Ran{code, out, err}: finish(code, out, err)
130
131# §7.2: the whole main of an app whose action is a pure plan: Cli.invoke's
132# run on the host and argv, written out, so a law on Cli.invoke states what
133# the app prints and exits with.
134def planned(~A: Type, ~decode: @+m: Cli.Matches -> Cli.Dec(A),
135    ~plan: @+t: Cli.Term -> A -> Cli.Ran, +c: Cli.Cmd) -> IO(Unit):
136  do IO<Unit>:
137    args : List<List<&2, U32>> <- IO.args_bytes()
138    h : Cli.Host <- host(c)
139    wrote(Cli.invoke(~A, ~decode, ~plan, c, h, argv_of(args)))