1	# rule arms: a Nat arm no value can reach. `case kn+p:` matches every Nat
2	# from k up, so a later `case jn+q:` with j >= k, or a later `case mn:` with
3	# m >= k, never runs. The checker accepts it and the match quietly returns
4	# the earlier arm (nohzafk pat_bad: 0n, 1n+p, 2n+p gives f(2n) = 1; bend
5	# 2.0.16 still does). Put the narrower arms first: the literals, then the
6	# larger n+p. `Succ{p}` and `Succ{_}` count as 1n+p. Only a
7	# single-scrutinee match is read: a column of a multi-scrutinee match is
8	# skipped.
9	import Base
10	import ../../src.bend as Src
11	import ../../finding.bend as F
12	import ../../syntax/lex.bend as Lex
13	import ../../syntax/tree.bend as Tree
14	import ../../lazy/lazy.bend as Lazy
15	import ../tokens.bend as T
16	
17	# what an arm matches: from k up (text is its pattern), exactly k, or other
18	type Arm is Data:
19	  APlus{k: U32, text: String, line: U32, col: U32, len: U32}
20	  ALit{k: U32, line: U32, col: U32, len: U32}
21	  AOther{}
22	
23	# the widest n+p arm so far: its k and its pattern
24	type Wide is Data:
25	  Wide{k: U32, text: String}
26	
27	# a lone binder, inside `Succ{..}` or after `kn+`: a name or `_`
28	def binder(kk: Lex.TokKind) -> Bool:
29	  match kk:
30	    case Lex.TName{}:
31	      True{}
32	    case Lex.TWild{}:
33	      True{}
34	    case other:
35	      False{}
36	
37	# `kn+p:` (p a name or `_`) or `kn:`
38	def lit.shape(rest: Tree.Node, +kk: U32, +tt: String, +line: U32, +col: U32) -> Arm:
39	  match rest:
40	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, +o, l, c}},
41	        Tree.NCons{Tree.Leaf{Lex.Tok{b, +p, l2, c2}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, s, l3, c3}}, more}}}:
42	      Bool.pick(Arm, Bool.and(String.eq(o, "+"), binder(b)), APlus{kk, tt ++ "+" ++ p, line, col,
43	        T.width(tt)}, AOther{})
44	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, s, l, c}}, more}:
45	      ALit{kk, line, col, T.width(tt)}
46	    case other:
47	      AOther{}
48	
49	# a Nat literal token's arm, once its value is read
50	def lit.of(mm: Maybe<&2, U32>, +tt: String, +rest: Tree.Node, +line: U32, +col: U32) -> Arm:
51	  match mm:
52	    case None{}:
53	      AOther{}
54	    case Some{+k}:
55	      lit.shape(rest, k, tt, line, col)
56	
57	# a case pattern's arm
58	def arm(pat: Tree.Node) -> Arm:
59	  match pat:
60	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, rest}:
61	      lit.of(T.nat_value(t), t, rest, l, c)
62	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, +t, l, c}},
63	        Tree.NCons{Tree.Group{open, Tree.NCons{Tree.Leaf{Lex.Tok{k, +p, l2, c2}}, Tree.NNil{}}, close},
64	          more}}:
65	      Bool.pick(Arm, Bool.and(String.eq(t, "Succ"), binder(k)), APlus{1, "Succ{" ++ p ++ "}", l, c, 4}, AOther{})
66	    case other:
67	      AOther{}
68	
69	# the widest n+p arm after this one
70	def widen(ww: Maybe<&2, Wide>, aa: Arm) -> Maybe<&2, Wide>:
71	  match ww aa:
72	    case None{} APlus{k, text, l, c, n}:
73	      Some{Wide{k, text}}
74	    case Some{Wide{+k, +text}} APlus{+j, +t2, l, c, n}:
75	      Bool.pick(Maybe<&2, Wide>, U32.is_lt(j, k), Some{Wide{j, t2}}, Some{Wide{k, text}})
76	    case w2 a2:
77	      w2
78	
79	# a finding when the arm is inside the widest one above
80	def verdict.on(+kk: U32, +text: String, aa: Arm, +path: String, +more: List<&2, F.Finding>) -> List<&2, F.Finding>:
81	  match aa:
82	    case APlus{+j, t, l, c, n}:
83	      Bool.pick(List<&2, F.Finding>, U32.is_ge(j, kk),
84	        F.Finding{path, l, c, n, "arms",
85	          "Unreachable: the case " ++ text ++ " above already matches everything from " ++ U32.show(j)
86	            ++ "n up; put narrower arms first."} <> more,
87	        more)
88	    case ALit{+m, l, c, n}:
89	      Bool.pick(List<&2, F.Finding>, U32.is_ge(m, kk),
90	        F.Finding{path, l, c, n, "arms",
91	          "Unreachable: the case " ++ text ++ " above already matches " ++ U32.show(m) ++ "n; put narrower arms first."}
92	          <> more,
93	        more)
94	    case AOther{}:
95	      more
96	
97	# the arm against the widest one above, if any
98	def verdict(ww: Maybe<&2, Wide>, aa: Arm, +path: String, more: List<&2, F.Finding>) -> List<&2, F.Finding>:
99	  match ww:
100	    case None{}:
101	      more
102	    case Some{Wide{k, text}}:
103	      verdict.on(k, text, aa, path, more)
104	
105	# a match's arms in order, against the widest n+p arm above each
106	def arms(body: Tree.Node, +wide: Maybe<&2, Wide>, +path: String) -> List<&2, F.Finding>:
107	  match body:
108	    case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, b}, rest}:
109	      +a = arm(T.pattern(kids))
110	      verdict(wide, a, path, arms(rest, widen(wide, a), path))
111	    case Tree.NCons{h, rest}:
112	      arms(rest, wide, path)
113	    case other:
114	      Nil{}
115	
116	# `match x:`: one scrutinee
117	def single(kids: Tree.Node) -> Bool:
118	  match kids:
119	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TKey{}, +t, l, c}},
120	        Tree.NCons{x, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, s, l2, c2}}, Tree.NNil{}}}}:
121	      String.eq(t, "match")
122	    case other:
123	      False{}
124	
125	# every statement, at any depth; a single-scrutinee match's arms are read
126	def walk(nn: Tree.Node, +path: String) -> List<&2, F.Finding>:
127	  match nn:
128	    case Tree.NCons{Tree.Stmt{kind, kids, +body}, rest}:
129	      +mine = Lazy.stop(List<&2, F.Finding>, Bool.not(single(kids)), [], _u => arms(body, None{}, path))
130	      List.concat(&2, F.Finding, [mine, walk(body, path), walk(rest, path)])
131	    case Tree.NCons{h, rest}:
132	      walk(rest, path)
133	    case other:
134	      Nil{}
135	
136	# the rule
137	def check(ss: Src.Src) -> List<&2, F.Finding>:
138	  Src.Src{path, text, toks, tree, bound, items} = ss
139	  walk(tree, path)