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.
7	import Base
8	import ../../paths.bend as Paths
9	import ../../role.bend as Role
10	import ../../src.bend as Src
11	import ../../finding.bend as F
12	import ../../syntax/tree.bend as Tree
13	import ../../lazy/lazy.bend as Lazy
14	import ../../syntax/bind.bend as Bind
15	
16	# does a law's body bind anything (a `for` or `exs` line)?
17	def binds(body: Tree.Node) -> Bool:
18	  match body:
19	    case Tree.NCons{Tree.Stmt{Tree.SFor{}, kids, b}, rest}:
20	      True{}
21	    case Tree.NCons{h, rest}:
22	      binds(rest)
23	    case other:
24	      False{}
25	
26	# a law's name, `?` when it has none
27	def name.of(mm: Maybe<&2, String>) -> String:
28	  match mm:
29	    case None{}:
30	      "?"
31	    case Some{n}:
32	      n
33	
34	def check.go(root: Tree.Node, +path: String) -> List<&2, F.Finding>:
35	  match root:
36	    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, +body}, rest}:
37	      +more = check.go(rest, path)
38	      Lazy.stop(List<&2, F.Finding>, binds(body), more,
39	        _u => F.Finding{path, Tree.line(kids), Tree.col(kids), 0, "closed",
40	          "Law " ++ name.of(Bind.declared(kids))
41	            ++ " has no `for` or `exs` binder, so it checks a single case; quantify it or delete it."} <> more)
42	    case Tree.NCons{h, rest}:
43	      check.go(rest, path)
44	    case other:
45	      Nil{}
46	
47	# the rule
48	def check(ss: Src.Src) -> List<&2, F.Finding>:
49	  Src.Src{+path, text, toks, tree, bound, items} = ss
50	  Lazy.stop(List<&2, F.Finding>, Bool.not(Paths.is_laws(path)), [], _u => check.go(tree, path))
51	
52	# the rule, told the file's role (src/role.bend): only a law file is checked
53	def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
54	  Src.Src{path, text, toks, tree, bound, items} = ss
55	  Lazy.stop(List<&2, F.Finding>, Bool.not(Role.is_laws(rr)), [], _u => check.go(tree, path))