src/rules/correctness/arms.bend
bolt@1.22.0.0 · 139 lines · 0 definitions
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.
9import Base
10import bolt@1.22.0.0/src/src.bend as Src
11import bolt@1.22.0.0/src/finding.bend as F
12import bolt@1.22.0.0/src/syntax/lex.bend as Lex
13import bolt@1.22.0.0/src/syntax/tree.bend as Tree
14import bolt@1.22.0.0/src/lazy/lazy.bend as Lazy
15import bolt@1.22.0.0/src/rules/tokens.bend as T
16
17# what an arm matches: from k up (text is its pattern), exactly k, or other
18type 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
24type Wide is Data:
25 Wide{k: U32, text: String}
26
27# a lone binder, inside `Succ{..}` or after `kn+`: a name or `_`
28def 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:`
38def 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
50def 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
58def 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
70def 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
80def 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
98def 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
106def 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
117def 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
126def 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
137def check(ss: Src.Src) -> List<&2, F.Finding>:
138 Src.Src{path, text, toks, tree, bound, items} = ss
139 walk(tree, path)