src/rules/laws/closed.bend source

src/rules/laws/closed.bend on the hub · documented module

# rule closed: a law in a LAWS.bend with no `for`/`exs` binder. A law with no# binder holds for the one input it names, which makes it a unit test the# checker runs, not a guarantee, and that is so for an equality (`{lhs == rhs# : T}`, including `IO(T)`) as much as for anything else. Nothing exempts a# closed law: quantify it, or delete it. Laws outside LAWS.bend are not held# to it.import Baseimport ../../paths.bend as Pathsimport ../../src.bend as Srcimport ../../finding.bend as Fimport ../../syntax/tree.bend as Treeimport ../../lazy/lazy.bend as Lazyimport ../../syntax/bind.bend as Bind# does a law's body bind anything (a `for` or `exs` line)?def binds(body: Tree.Node) -> Bool:  match body:    case Tree.NCons{Tree.Stmt{Tree.SFor{}, kids, b}, rest}:      True{}    case Tree.NCons{h, rest}:      binds(rest)    case other:      False{}# a law's name, `?` when it has nonedef name.of(mm: Maybe<&2, String>) -> String:  match mm:    case None{}:      "?"    case Some{n}:      ndef check.go(root: Tree.Node, +path: String) -> List<&2, F.Finding>:  match root:    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, +body}, rest}:      +more = check.go(rest, path)      Lazy.stop(List<&2, F.Finding>, binds(body), more,        _u => F.Finding{path, Tree.line(kids), Tree.col(kids), 0, "closed",          "Law " ++ name.of(Bind.declared(kids))            ++ " has no `for` or `exs` binder, so it checks a single case; quantify it or delete it."} <> more)    case Tree.NCons{h, rest}:      check.go(rest, path)    case other:      Nil{}# the ruledef check(ss: Src.Src) -> List<&2, F.Finding>:  Src.Src{+path, text, toks, tree, bound, items} = ss  Lazy.stop(List<&2, F.Finding>, Bool.not(Paths.is_laws(path)), [], _u => check.go(tree, path))