src/rules/style/param.bend
bolt@1.23.0.0 · 73 lines · 0 definitions
1# rule param: a parameter name shorter than 2 characters. A single uppercase
2# letter is a type parameter (`A`, `T`), and a bare parameter or one typed
3# `Quant` is a quantity. Locals, pattern binders and a law's `for` names are
4# not parameters. A PROOF.bend's parameters are the names the law bound.
5import Base
6import bolt@1.23.0.0/src/paths.bend as Paths
7import bolt@1.23.0.0/src/role.bend as Role
8import bolt@1.23.0.0/src/src.bend as Src
9import bolt@1.23.0.0/src/finding.bend as F
10import bolt@1.23.0.0/src/syntax/bind.bend as Bind
11import bolt@1.23.0.0/src/lazy/lazy.bend as Lazy
12import bolt@1.23.0.0/src/rules/tokens.bend as T
13
14# one character, and a capital: a type parameter
15def check.letter(cs: List<&2, Char>) -> Bool:
16 match cs:
17 case Con{c, Nil{}}:
18 Char.is_upper(c)
19 case other:
20 False{}
21
22# `A`, `T`, `H`
23def check.upper(+nm: String) -> Bool:
24 check.letter(String.to_list(nm))
25
26# no type, or `: Quant`: a quantity parameter (`a` in `List<a, A>`). The
27# note is read with its string literals cut to their quote: a `:` inside a
28# string is no type
29def check.quant(+note: String) -> Bool:
30 +cn = T.code(note)
31 Bool.or(Bool.not(String.contains(cn, ":")), String.ends_with(cn, ": Quant"))
32
33# shorter than 2
34def check.short(+nm: String) -> Bool:
35 Nat.is_lt(String.length(nm), 2n)
36
37# a parameter, not a local or a pattern
38def check.is_param(kk: Bind.BindKind) -> Bool:
39 match kk:
40 case Bind.KParam{}:
41 True{}
42 case other:
43 False{}
44
45# a type parameter or a quantity, which are allowed to be one letter
46def check.allowed(+nm: String, +note: String) -> Bool:
47 Bool.or(check.upper(nm), check.quant(note))
48
49def check.go(binds: List<&2, Bind.Bind>, +path: String) -> List<&2, F.Finding>:
50 match binds:
51 case Nil{}:
52 Nil{}
53 case Con{Bind.Bind{+nm, +line, +col, +kind, +note}, rest}:
54 +more = check.go(rest, path)
55 +hit = Bool.and(check.is_param(kind), Bool.and(check.short(nm), Bool.not(check.allowed(nm, note))))
56 Bool.pick(List<&2, F.Finding>, hit,
57 F.Finding{path, line, col, U32.from_nat(String.length(nm)), "param",
58 "Parameter " ++ nm ++ " is too short; use at least 2 characters."} <> more, more)
59
60def check.on(binds: List<&2, Bind.Bind>, +path: String) -> List<&2, F.Finding>:
61 Lazy.stop(List<&2, F.Finding>, Paths.is_proof(path), [], _u => check.go(binds, path))
62
63# the rule; a proof's parameters stay the law's names
64def check(ss: Src.Src) -> List<&2, F.Finding>:
65 Src.Src{path, text, toks, tree, bound, items} = ss
66 Bind.Bound{binds, uses, scopes} = bound
67 check.on(binds, path)
68
69# the rule, told the file's role (src/role.bend): a proof file is skipped
70def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
71 Src.Src{path, text, toks, tree, bound, items} = ss
72 Bind.Bound{binds, uses, scopes} = bound
73 Lazy.stop(List<&2, F.Finding>, Role.is_proof(rr), [], _u => check.go(binds, path))