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