src/rules/laws/closed.bend

bolt@1.20.0.0 · 49 lines · 0 definitions

1# rule closed: a law in a LAWS.bend with no `for`/`exs` binder. A law with no
2# binder holds for the one input it names, which makes it a unit test the
3# checker runs, not a guarantee, and that is so for an equality (`{lhs == rhs
4# : T}`, including `IO(T)`) as much as for anything else. Nothing exempts a
5# closed law: quantify it, or delete it. Laws outside LAWS.bend are not held
6# to it.
7import Base
8import bolt@1.20.0.0/src/paths.bend as Paths
9import bolt@1.20.0.0/src/src.bend as Src
10import bolt@1.20.0.0/src/finding.bend as F
11import bolt@1.20.0.0/src/syntax/tree.bend as Tree
12import bolt@1.20.0.0/src/lazy/lazy.bend as Lazy
13import bolt@1.20.0.0/src/syntax/bind.bend as Bind
14
15# does a law's body bind anything (a `for` or `exs` line)?
16def binds(body: Tree.Node) -> Bool:
17  match body:
18    case Tree.NCons{Tree.Stmt{Tree.SFor{}, kids, b}, rest}:
19      True{}
20    case Tree.NCons{h, rest}:
21      binds(rest)
22    case other:
23      False{}
24
25# a law's name, `?` when it has none
26def name.of(mm: Maybe<&2, String>) -> String:
27  match mm:
28    case None{}:
29      "?"
30    case Some{n}:
31      n
32
33def check.go(root: Tree.Node, +path: String) -> List<&2, F.Finding>:
34  match root:
35    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, +body}, rest}:
36      +more = check.go(rest, path)
37      Lazy.stop(List<&2, F.Finding>, binds(body), more,
38        _u => F.Finding{path, Tree.line(kids), Tree.col(kids), 0, "closed",
39          "Law " ++ name.of(Bind.declared(kids))
40            ++ " has no `for` or `exs` binder, so it checks a single case; quantify it or delete it."} <> more)
41    case Tree.NCons{h, rest}:
42      check.go(rest, path)
43    case other:
44      Nil{}
45
46# the rule
47def check(ss: Src.Src) -> List<&2, F.Finding>:
48  Src.Src{+path, text, toks, tree, bound, items} = ss
49  Lazy.stop(List<&2, F.Finding>, Bool.not(Paths.is_laws(path)), [], _u => check.go(tree, path))