1	# src/syntax/tree: a source as a concrete syntax tree over its significant tokens:
2	# statements by line and indentation, groups by brackets. Built by one stack
3	# machine over the token list, so a half-written file still yields a tree:
4	#   - a bracket that never closes is closed by the next line at column 0
5	#     (so damage stays inside one item), or by the end of the file;
6	#   - a close bracket that matches nothing on the stack is a stray leaf;
7	#   - `<` opens type arguments only when glued to a name (`List<`, `Maybe<&`);
8	#     a `>`-only operator closes as many angle groups as it has `>`s, each
9	#     only while an angle group is the innermost open one: in
10	#     `List<f(a > b)>` the first `>` is an operator inside `(..)`.
11	# Trivia (spaces, newlines, comments) is not in the tree: read the tokens for
12	# that. The cells (NNil, NCons) live inside the type, as json/value does, so
13	# every walk is a structural recursion on one argument.
14	import Base
15	import ../lazy/lazy.bend as Lazy
16	import ./lex.bend as Lex
17	
18	# what a statement is, by its shape: SDef `def f(..)` (also `@unsafe def`),
19	# SType, SLaw, SImport, SCase `case p:`, SFor `for x: T` / `exs x: T`, SLet
20	# (a `=` or `<-` among its own tokens), else STerm (`match x:`, `do M<T>:`,
21	# `return e`, a call, and a dependent arrow `@x: A -> B` or `@+x: A -> B`,
22	# which an `@` does not make a def)
23	type StmtKind is Data:
24	  SDef{}
25	  SType{}
26	  SLaw{}
27	  SImport{}
28	  SCase{}
29	  SFor{}
30	  SLet{}
31	  STerm{}
32	
33	# a leaf holds one token; a group its bracket, what is inside, and its close
34	# (None when it never closed); a statement its own tokens and the statements
35	# under it; NNil and NCons chain nodes
36	type Node is Data:
37	  Leaf{tok: Lex.Tok}
38	  Group{open: Lex.Tok, kids: Node, close: Maybe<&2, Lex.Tok>}
39	  Stmt{kind: StmtKind, kids: Node, body: Node}
40	  NNil{}
41	  NCons{head: Node, tail: Node}
42	
43	# cells
44	# -----
45	
46	# a chain, reversed onto acc
47	def reverse(cells: Node, acc: Node) -> Node:
48	  match cells:
49	    case NCons{h, t}:
50	      reverse(t, NCons{h, acc})
51	    case other:
52	      acc
53	
54	# the token a leaf holds; a group's open, a statement's first token
55	def first(nn: Node) -> Maybe<&2, Lex.Tok>:
56	  match nn:
57	    case Leaf{tok}:
58	      Some{tok}
59	    case Group{open, kids, close}:
60	      Some{open}
61	    case Stmt{kind, kids, body}:
62	      first(kids)
63	    case NNil{}:
64	      None{}
65	    case NCons{h, t}:
66	      first(h)
67	
68	def line.of(mm: Maybe<&2, Lex.Tok>) -> U32:
69	  match mm:
70	    case None{}:
71	      0
72	    case Some{Lex.Tok{k, t, l, c}}:
73	      l
74	
75	# the line of a node's first token (0 for none)
76	def line(nn: Node) -> U32:
77	  line.of(first(nn))
78	
79	def col.of(mm: Maybe<&2, Lex.Tok>) -> U32:
80	  match mm:
81	    case None{}:
82	      0
83	    case Some{Lex.Tok{k, t, l, c}}:
84	      c
85	
86	# the column of a node's first token (0 for none)
87	def col(nn: Node) -> U32:
88	  col.of(first(nn))
89	
90	# is it a group opened by this bracket?
91	def opens(nn: Node, +ss: String) -> Bool:
92	  match nn:
93	    case Group{Lex.Tok{k, t, l, c}, kids, close}:
94	      String.eq(t, ss)
95	    case other:
96	      False{}
97	
98	# the leaves of a tree, in order: the significant tokens
99	def leaf_close(close: Maybe<&2, Lex.Tok>, acc: List<&2, Lex.Tok>) -> List<&2, Lex.Tok>:
100	  match close:
101	    case None{}:
102	      acc
103	    case Some{tok}:
104	      tok <> acc
105	
106	def leaves.go(nn: Node, acc: List<&2, Lex.Tok>) -> List<&2, Lex.Tok>:
107	  match nn:
108	    case Leaf{tok}:
109	      tok <> acc
110	    case Group{open, kids, close}:
111	      leaf_close(close, leaves.go(kids, open <> acc))
112	    case Stmt{kind, kids, body}:
113	      leaves.go(body, leaves.go(kids, acc))
114	    case NNil{}:
115	      acc
116	    case NCons{h, t}:
117	      leaves.go(t, leaves.go(h, acc))
118	
119	# the leaves of a tree, in order: the significant tokens when the tree is faithful
120	def leaves(nn: Node) -> List<&2, Lex.Tok>:
121	  List.reverse(&2, Lex.Tok, leaves.go(nn, []))
122	
123	# building
124	# --------
125	
126	# an open group (its kids reversed), or an open statement (its kids and the
127	# finished statements under it, both reversed); the root holds the items
128	type Frame is Data:
129	  FGroup{open: Lex.Tok, kids: Node}
130	  FStmt{indent: U32, kids: Node, body: Node}
131	  FRoot{body: Node}
132	
133	# fresh: the next significant token starts a line
134	type B is Data:
135	  B{fresh: Bool, stack: List<&2, Frame>}
136	
137	# the bracket that closes an opener (`>` for `<` and `<&`)
138	def closer(+oo: String) -> String:
139	  Bool.pick(String, String.eq(oo, "("), ")",
140	    Bool.pick(String, String.eq(oo, "["), "]",
141	      Bool.pick(String, String.eq(oo, "{"), "}", ">")))
142	
143	# is every char a `>`?
144	def all_gt(cs: List<&2, Char>) -> Bool:
145	  match cs:
146	    case Nil{}:
147	      True{}
148	    case Con{+c, t}:
149	      Lazy.and_then(Char.is_eq(c, '>'), _u => all_gt(t))
150	
151	# a token that closes a group: `)`, `]`, `}` or a run of `>`
152	def closes_with(kk: Lex.TokKind, +tt: String) -> Bool:
153	  match kk:
154	    case Lex.TClose{}:
155	      True{}
156	    case Lex.TOp{}:
157	      Bool.and(Bool.not(String.is_empty(tt)), all_gt(String.to_list(tt)))
158	    case other:
159	      False{}
160	
161	# `<` or `<&` right after a name opens type arguments
162	def opens_angle(kk: Lex.TokKind, +tt: String, glued: Bool) -> Bool:
163	  match kk:
164	    case Lex.TOp{}:
165	      Bool.and(glued, Bool.or(String.eq(tt, "<"), String.eq(tt, "<&")))
166	    case other:
167	      False{}
168	
169	# a finished node lands in the frame below
170	def put(stack: List<&2, Frame>, nn: Node) -> List<&2, Frame>:
171	  match stack:
172	    case Nil{}:
173	      Nil{}
174	    case Con{FGroup{open, kids}, rest}:
175	      FGroup{open, NCons{nn, kids}} <> rest
176	    case Con{FStmt{indent, kids, body}, rest}:
177	      FStmt{indent, NCons{nn, kids}, body} <> rest
178	    case Con{FRoot{body}, rest}:
179	      FRoot{NCons{nn, body}} <> rest
180	
181	# the innermost open group, closed by close (None: never closed)
182	def close_one(stack: List<&2, Frame>, close: Maybe<&2, Lex.Tok>) -> List<&2, Frame>:
183	  match stack:
184	    case Con{FGroup{open, kids}, rest}:
185	      put(rest, Group{open, reverse(kids, NNil{}), close})
186	    case other:
187	      other
188	
189	# one more group above the one found below, when one was
190	def depth_to.up(below: Nat) -> Nat:
191	  match below:
192	    case Zero{}:
193	      0n
194	    case Succ{p}:
195	      Succ{Succ{p}}
196	
197	# how many groups sit open above the one that c closes (counting it); 0 when
198	# none does. A `>` closes only an angle group on top: inside `(..)`, `[..]`
199	# or `{..}` it is an operator, even within `<..>`
200	def depth_to(stack: List<&2, Frame>, +cc: String) -> Nat:
201	  match stack:
202	    case Nil{}:
203	      0n
204	    case Con{FGroup{Lex.Tok{k, +t, l, c2}, kids}, rest}:
205	      Lazy.stop(Nat, String.eq(closer(t), cc), 1n,
206	        _u => Lazy.stop(Nat, String.eq(cc, ">"), 0n, _v => depth_to.up(depth_to(rest, cc))))
207	    case Con{other, rest}:
208	      0n
209	
210	# how many groups sit open on top of the stack
211	def groups(stack: List<&2, Frame>) -> Nat:
212	  match stack:
213	    case Con{FGroup{open, kids}, rest}:
214	      Succ{groups(rest)}
215	    case other:
216	      0n
217	
218	# n groups close, innermost first; only the last gets the close token
219	def close_n(nn: Nat, stack: List<&2, Frame>, close: Maybe<&2, Lex.Tok>) -> List<&2, Frame>:
220	  match nn:
221	    case Zero{}:
222	      stack
223	    case Succ{Zero{}}:
224	      close_one(stack, close)
225	    case Succ{p}:
226	      close_n(p, close_one(stack, None{}), close)
227	
228	# every open group closes, unclosed
229	def close_all(+stack: List<&2, Frame>) -> List<&2, Frame>:
230	  close_n(groups(stack), stack, None{})
231	
232	# a close bracket: to its match if it has one, else a stray leaf
233	def close_tok(+stack: List<&2, Frame>, +close: Lex.Tok) -> List<&2, Frame>:
234	  Lex.Tok{k, +t, l, c} = close
235	  +n = depth_to(stack, t)
236	  Lazy.stop(List<&2, Frame>, Nat.is_eq(n, 0n), put(stack, Leaf{close}), _u => close_n(n, stack, Some{close}))
237	
238	# `>>` closes two angle groups
239	def close_gts(cs: List<&2, Char>, stack: List<&2, Frame>, +ll: U32, +cc: U32) -> List<&2, Frame>:
240	  match cs:
241	    case Nil{}:
242	      stack
243	    case Con{ch, t}:
244	      close_gts(t, close_tok(stack, Lex.Tok{Lex.TOp{}, ">", ll, cc}), ll, (cc + 1 : U32))
245	
246	# the close a bracket makes, given whether it is a run of `>`: a match, so
247	# only the side taken runs
248	def close_any.at(
249	  +gt: Bool,
250	  +stack: List<&2, Frame>,
251	  +close: Lex.Tok,
252	  +tt: String,
253	  +ll: U32,
254	  +cc: U32
255	) -> List<&2, Frame>:
256	  match gt:
257	    case True{}:
258	      close_gts(String.to_list(tt), stack, ll, cc)
259	    case False{}:
260	      close_tok(stack, close)
261	
262	# a close bracket, or a run of `>`, closes what it can
263	def close_any(+stack: List<&2, Frame>, +close: Lex.Tok) -> List<&2, Frame>:
264	  Lex.Tok{k, +t, +l, +c} = close
265	  close_any.at(String.starts_with(t, ">"), stack, close, t, l, c)
266	
267	# a finished statement lands in the body of the frame below
268	def put_stmt(stack: List<&2, Frame>, nn: Node) -> List<&2, Frame>:
269	  match stack:
270	    case Con{FStmt{indent, kids, body}, rest}:
271	      FStmt{indent, kids, NCons{nn, body}} <> rest
272	    case Con{FRoot{body}, rest}:
273	      FRoot{NCons{nn, body}} <> rest
274	    case other:
275	      other
276	
277	# a `=` or `<-` among a statement's own tokens
278	def binds_in(kids: Node) -> Bool:
279	  match kids:
280	    case NCons{Leaf{Lex.Tok{Lex.TEq{}, t, l, c}}, rest}:
281	      True{}
282	    case NCons{Leaf{Lex.Tok{Lex.TBind{}, t, l, c}}, rest}:
283	      True{}
284	    case NCons{h, rest}:
285	      binds_in(rest)
286	    case other:
287	      False{}
288	
289	# the kind of a statement led by this keyword
290	def keyword_kind(+tt: String) -> StmtKind:
291	  Bool.pick(StmtKind, String.eq(tt, "def"), SDef{},
292	    Bool.pick(StmtKind, String.eq(tt, "type"), SType{},
293	      Bool.pick(StmtKind, String.eq(tt, "law"), SLaw{},
294	        Bool.pick(StmtKind, String.eq(tt, "import"), SImport{},
295	          Bool.pick(StmtKind, String.eq(tt, "case"), SCase{},
296	            Bool.pick(StmtKind, Bool.or(String.eq(tt, "for"), String.eq(tt, "exs")), SFor{}, STerm{}))))))
297	
298	# does the chain after an `@` start with a binder's name and a `:`?
299	def arrow.named(rest: Node) -> Bool:
300	  match rest:
301	    case NCons{Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}}, NCons{Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}:
302	      True{}
303	    case NCons{Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}}, NCons{Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}:
304	      True{}
305	    case _other:
306	      False{}
307	
308	# does the chain after an `@` bind a name, `@x:` or with a quantity mark
309	# `@+x:`, as a dependent arrow does, rather than name an attribute (`@unsafe`)?
310	def arrow(rest: Node) -> Bool:
311	  match rest:
312	    case NCons{Leaf{Lex.Tok{Lex.TOp{}, _t, _l, _c}}, more}:
313	      arrow.named(more)
314	    case other:
315	      arrow.named(other)
316	
317	# a statement's kind from its own tokens
318	def classify(kids: Node) -> StmtKind:
319	  match kids:
320	    case NCons{Leaf{Lex.Tok{Lex.TKey{}, t, l, c}}, rest}:
321	      keyword_kind(t)
322	    case NCons{Leaf{Lex.Tok{Lex.TAll{}, t, l, c}}, rest}:
323	      Bool.pick(StmtKind, arrow(rest), STerm{}, SDef{})
324	    case other:
325	      Bool.pick(StmtKind, binds_in(other), SLet{}, STerm{})
326	
327	# the innermost open statement is finished and lands in its parent
328	def end_stmt(stack: List<&2, Frame>) -> List<&2, Frame>:
329	  match stack:
330	    case Con{FStmt{indent, kids, body}, rest}:
331	      +ks = reverse(kids, NNil{})
332	      put_stmt(rest, Stmt{classify(ks), ks, reverse(body, NNil{})})
333	    case other:
334	      other
335	
336	# n statements finish, innermost first
337	def end_n(nn: Nat, stack: List<&2, Frame>) -> List<&2, Frame>:
338	  match nn:
339	    case Zero{}:
340	      stack
341	    case Succ{p}:
342	      end_n(p, end_stmt(stack))
343	
344	# the statements a line at column col ends: those not shallower than it
345	def deeper(stack: List<&2, Frame>, +col: U32) -> Nat:
346	  match stack:
347	    case Con{FStmt{+indent, kids, body}, rest}:
348	      +below = deeper(rest, col)
349	      Bool.pick(Nat, U32.is_ge(indent, col), Succ{below}, 0n)
350	    case other:
351	      0n
352	
353	# how many statements sit open on the stack
354	def stmts(stack: List<&2, Frame>) -> Nat:
355	  match stack:
356	    case Con{FStmt{indent, kids, body}, rest}:
357	      Succ{stmts(rest)}
358	    case other:
359	      0n
360	
361	# is the innermost frame an open group?
362	def in_group(stack: List<&2, Frame>) -> Bool:
363	  match stack:
364	    case Con{FGroup{open, kids}, rest}:
365	      True{}
366	    case other:
367	      False{}
368	
369	# a new statement at column c, once the ones it ends are finished; inside a
370	# group a line is just more tokens
371	def open_stmt(+stack: List<&2, Frame>, +cc: U32) -> List<&2, Frame>:
372	  Lazy.stop(List<&2, Frame>, in_group(stack), stack,
373	    _u => FStmt{cc, NNil{}, NNil{}} <> end_n(deeper(stack, cc), stack))
374	
375	# a significant token that starts a line: at column 0 it closes every open
376	# group (unless it is a bracket closing one of them); outside a group it opens
377	# a statement
378	def fresh(+stack: List<&2, Frame>, +tok: Lex.Tok) -> List<&2, Frame>:
379	  Lex.Tok{k, t, l, +c} = tok
380	  +cuts = Bool.and(Bool.and(in_group(stack), U32.is_eq(c, 0)), Nat.is_eq(depth_to(stack, t), 0n))
381	  open_stmt(Lazy.stop(List<&2, Frame>, Bool.not(cuts), stack, _u => close_all(stack)), c)
382	
383	# an open bracket or a leaf into the innermost frame
384	def push(+stack: List<&2, Frame>, +tok: Lex.Tok, glued: Bool) -> List<&2, Frame>:
385	  Lex.Tok{+k, +t, l, c} = tok
386	  Lazy.stop(List<&2, Frame>, Bool.not(closes_with(k, t)),
387	    Bool.pick(List<&2, Frame>, Bool.or(Lex.is_open(k), opens_angle(k, t, glued)), FGroup{tok, NNil{}} <> stack,
388	      put(stack, Leaf{tok})),
389	    _u => close_any(stack, tok))
390	
391	# glued: the previous token was a name with nothing between
392	def step(+tok: Lex.Tok, st: B, glued: Bool) -> B:
393	  Lex.Tok{+k, t, l, c} = tok
394	  B{+fr, +stack} = st
395	  Lazy.stop(B, Bool.not(Lex.significant(k)), B{Bool.or(fr, Lex.is_nl(k)), stack},
396	    _u => B{False{}, push(Lazy.stop(List<&2, Frame>, Bool.not(fr), stack, _u2 => fresh(stack, tok)), tok, glued)})
397	
398	# an identifier of any kind (what `<` glues to)
399	def is_name_tok(tok: Lex.Tok) -> Bool:
400	  Lex.Tok{k, t, l, c} = tok
401	  Lex.is_name(k)
402	
403	# every token, in order
404	def run(toks: List<&2, Lex.Tok>, st: B, glued: Bool) -> B:
405	  match toks:
406	    case Nil{}:
407	      st
408	    case Con{+tok, t}:
409	      +g = is_name_tok(tok)
410	      run(t, step(tok, st, glued), g)
411	
412	# the items gathered in the root frame
413	def root(stack: List<&2, Frame>) -> Node:
414	  match stack:
415	    case Con{FRoot{body}, rest}:
416	      reverse(body, NNil{})
417	    case other:
418	      NNil{}
419	
420	# the tree once the tokens are over: every group and statement closes
421	def finish(st: B) -> Node:
422	  B{fr, stack} = st
423	  +closed = close_all(stack)
424	  root(end_n(stmts(closed), closed))
425	
426	# the items of a source: a chain of statements
427	def of_tokens(toks: List<&2, Lex.Tok>) -> Node:
428	  finish(run(toks, B{True{}, [FRoot{NNil{}}]}, False{}))
429	
430	# the items of a source: a chain of statements
431	def parse(source: String) -> Node:
432	  of_tokens(Lex.tokens(source))
433	
434	# showing
435	# -------
436	
437	# a group's close bracket, `..` when it never closed
438	def show_close(close: Maybe<&2, Lex.Tok>) -> String:
439	  match close:
440	    case None{}:
441	      ".."
442	    case Some{Lex.Tok{k, t, l, c}}:
443	      t
444	
445	# `[def f (x : U32) -> U32 : {[match x {[case A {} : {[1]}]}]}]`: a statement
446	# in brackets, its body in braces, a group as its brackets (an unclosed one
447	# ends in `..`)
448	def show(nn: Node) -> String:
449	  match nn:
450	    case Leaf{Lex.Tok{k, t, l, c}}:
451	      t
452	    case Group{Lex.Tok{k, t, l, c}, kids, close}:
453	      t ++ show(kids) ++ show_close(close)
454	    case Stmt{kind, kids, body}:
455	      +b = show(body)
456	      "[" ++ show(kids) ++ Bool.pick(String, String.is_empty(b), "", " {" ++ b ++ "}") ++ "]"
457	    case NNil{}:
458	      ""
459	    case NCons{h, t}:
460	      +rest = show(t)
461	      show(h) ++ Bool.pick(String, String.is_empty(rest), "", " " ++ rest)