src/rules/style/param.bend source

src/rules/style/param.bend on the hub · documented module

# rule param: a parameter name shorter than 2 characters. A single uppercase# letter is a type parameter (`A`, `T`), and a bare parameter or one typed# `Quant` is a quantity. Locals, pattern binders and a law's `for` names are# not parameters. A PROOF.bend's parameters are the names the law bound.import Baseimport ../../paths.bend as Pathsimport ../../src.bend as Srcimport ../../finding.bend as Fimport ../../syntax/bind.bend as Bindimport ../../lazy/lazy.bend as Lazyimport ../tokens.bend as T# one character, and a capital: a type parameterdef check.letter(cs: List<&2, Char>) -> Bool:  match cs:    case Con{c, Nil{}}:      Char.is_upper(c)    case other:      False{}# `A`, `T`, `H`def check.upper(+nm: String) -> Bool:  check.letter(String.to_list(nm))# no type, or `: Quant`: a quantity parameter (`a` in `List<a, A>`). The# note is read with its string literals cut to their quote: a `:` inside a# string is no typedef check.quant(+note: String) -> Bool:  +cn = T.code(note)  Bool.or(Bool.not(String.contains(cn, ":")), String.ends_with(cn, ": Quant"))# shorter than 2def check.short(+nm: String) -> Bool:  Nat.is_lt(String.length(nm), 2n)# a parameter, not a local or a patterndef check.is_param(kk: Bind.BindKind) -> Bool:  match kk:    case Bind.KParam{}:      True{}    case other:      False{}# a type parameter or a quantity, which are allowed to be one letterdef check.allowed(+nm: String, +note: String) -> Bool:  Bool.or(check.upper(nm), check.quant(note))def check.go(binds: List<&2, Bind.Bind>, +path: String) -> List<&2, F.Finding>:  match binds:    case Nil{}:      Nil{}    case Con{Bind.Bind{+nm, +line, +col, +kind, +note}, rest}:      +more = check.go(rest, path)      +hit = Bool.and(check.is_param(kind), Bool.and(check.short(nm), Bool.not(check.allowed(nm, note))))      Bool.pick(List<&2, F.Finding>, hit,        F.Finding{path, line, col, U32.from_nat(String.length(nm)), "param",          "Parameter " ++ nm ++ " is too short; use at least 2 characters."} <> more, more)def check.on(binds: List<&2, Bind.Bind>, +path: String) -> List<&2, F.Finding>:  Lazy.stop(List<&2, F.Finding>, Paths.is_proof(path), [], _u => check.go(binds, path))# the rule; a proof's parameters stay the law's namesdef check(ss: Src.Src) -> List<&2, F.Finding>:  Src.Src{path, text, toks, tree, bound, items} = ss  Bind.Bound{binds, uses, scopes} = bound  check.on(binds, path)