Clean up CheckAtt (#3943)

This PR refactors `CheckAtt` to more clearly separate the checks on
different attributes.

Most of the change here is just shuffling code between functions, but we
additionally
- Implemented `HasAtt` and `HasLocation` for `Module` so we can use the
same `checkUnrecognizedAtts` and `checkRestrictedAtts` functions for
both modules and sentences
- In doing so, fixed a bug where we failed to check restricted
attributes on modules at all
- Corrected the whitelist to allow `one-path` and `all-path` on `Module`
as well as `Claim`
- Slightly changed a few error messages
- Removed a manual check for attribute values on `binder`, as this is
now covered by the general check

k-distribution/tests/regression-new/checks/binder.k

@@ -6,8 +6,6 @@ module BINDER
 
   syntax Error ::= foo() [binder]
 
-  syntax Error ::= foo(KVar, Error) [binder(1 -> 2)]
-
   syntax Error ::= foo(Error, Error) [binder]
 
   syntax Correct ::= foo(KVar, Error) [binder]

k-distribution/tests/regression-new/checks/binder.k.out

@@ -3,14 +3,9 @@
 	Location(7,20,7,34)
 	7 |	  syntax Error ::= foo() [binder]
 	  .	                   ^~~~~~~~~~~~~~
-[Error] Compiler: Attribute value for 'binder' attribute is not supported.
-	Source(binder.k)
-	Location(9,20,9,53)
-	9 |	  syntax Error ::= foo(KVar, Error) [binder(1 -> 2)]
-	  .	                   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 [Error] Compiler: First child of binder must have a sort with the 'KVAR.KVar' hook attribute.
 	Source(binder.k)
-	Location(11,20,11,46)
-	11 |	  syntax Error ::= foo(Error, Error) [binder]
-	   .	                   ^~~~~~~~~~~~~~~~~~~~~~~~~~
-[Error] Compiler: Had 3 structural errors.
+	Location(9,20,9,46)
+	9 |	  syntax Error ::= foo(Error, Error) [binder]
+	  .	                   ^~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 2 structural errors.

k-distribution/tests/regression-new/checks/checkModuleAtts.k.out

@@ -1,3 +1,9 @@
-[Error] Compiler: Had 1 structural errors.
-[Error] Compiler: Unrecognized attributes on module CHECKMODULEATTS: [baz, foo]
+[Error] Compiler: Unrecognized attributes: [baz, foo]
 Hint: User-defined groups can be added with the group(_) attribute.
+	Source(checkModuleAtts.k)
+	Location(2,1,3,10)
+	  .	v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+	2 |	module CHECKMODULEATTS [foo, group(bar), baz]
+	3 |	endmodule
+	  .	~~~~~~~~^
+[Error] Compiler: Had 1 structural errors.

k-distribution/tests/regression-new/checks/invalidLabel.k.out

@@ -1,14 +1,14 @@
-[Error] Compiler: Rule label 'INVALIDLABEL.foo`bar' cannot contain whitespace or backticks.
+[Error] Compiler: Label 'INVALIDLABEL.foo`bar' cannot contain whitespace or backticks.
 	Source(invalidLabel.k)
 	Location(6,19,6,32)
 	6 |	  rule [foo`bar]: true => false
 	  .	                  ^~~~~~~~~~~~~
-[Error] Compiler: Rule label 'foo bar' cannot contain whitespace or backticks.
+[Error] Compiler: Label 'foo bar' cannot contain whitespace or backticks.
 	Source(invalidLabel.k)
 	Location(7,8,7,21)
 	7 |	  rule false => true [label(foo bar)]
 	  .	       ^~~~~~~~~~~~~
-[Error] Compiler: Rule label 'foo`bar' cannot contain whitespace or backticks.
+[Error] Compiler: Label 'foo`bar' cannot contain whitespace or backticks.
 	Source(invalidLabel.k)
 	Location(8,8,8,14)
 	8 |	  rule 0 => 1 [label(foo`bar)]

k-distribution/tests/regression-new/checks/restrictedAtts.k.out

@@ -1,9 +1,9 @@
-[Error] Compiler: Production sentences can not have the following attributes: [cool, kore]
+[Error] Compiler: Production cannot have the following attributes: [cool, kore]
 	Source(restrictedAtts.k)
 	Location(4,19,4,41)
 	4 |	  syntax Foo  ::= a() [cool, kore, left]
 	  .	                  ^~~~~~~~~~~~~~~~~~~~~~
-[Error] Compiler: Rule sentences can not have the following attributes: [idem]
+[Error] Compiler: Rule cannot have the following attributes: [idem]
 	Source(restrictedAtts.k)
 	Location(5,8,5,17)
 	5 |	  rule a() => .K [idem, owise]