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