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 ../../src.bend as Src
10	import ../../finding.bend as F
11	import ../../syntax/tree.bend as Tree
12	import ../../lazy/lazy.bend as Lazy
13	import ../../syntax/bind.bend as Bind
14	
15	# does a law's body bind anything (a `for` or `exs` line)?
16	def 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
26	def name.of(mm: Maybe<&2, String>) -> String:
27	  match mm:
28	    case None{}:
29	      "?"
30	    case Some{n}:
31	      n
32	
33	def 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
47	def 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))