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	
8	import Base
9	import ./cli.bend as Cli
10	
11	# 1 if fd is a terminal, else 0.
12	def 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.
17	def Sys.columns(fd: U32) -> IO(U32):
18	  import "./sys.c"
19	  import "./sys.js"
20	
21	def 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.
28	def exit(+code: U32) -> IO(Unit):
29	  exit_when(U32.is_eq(code, 0), code)
30	
31	def 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".
37	def 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.
43	def chomp(s: String) -> String:
44	  match s:
45	    case SNil{}: SNil{}
46	    case SCon{c, t}: chomp_from(t, c)
47	
48	def 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	
53	def 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.
59	def 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	
65	def 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.
72	def 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.
83	def 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	
93	def 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.
100	def 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.
106	def ended(r: (U32 & String)) -> IO(Unit):
107	  match r:
108	    case (code, err): finish(code, "", err)
109	
110	def 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.
120	def 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	
127	def 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.
134	def 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)))