Update documentation and tutorials for group(_) (#3487)

* user_manual.md: Document group(_) attribute

* Update k-tutorial to refer to group(_)

* Update pl-tutorial to refer to group(_)

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

docs/user_manual.md

@@ -743,25 +743,26 @@ For this purpose, we introduce the equivalent `syntax priorities`,
 example, the above grammar can be written equivalently as:
 
 ```k
-syntax Exp ::= Exp "*" Exp [mult]
-             | Exp "/" Exp [div]
-             | Exp "+" Exp [add]
-             | Exp "-" Exp [sub]
+syntax Exp ::= Exp "*" Exp [group(mult)]
+             | Exp "/" Exp [group(div)]
+             | Exp "+" Exp [group(add)]
+             | Exp "-" Exp [group(sub)]
 
 syntax priorities mult div > add sub
 syntax left mult div
 syntax right add sub
 ```
 
-Here we use user-defined attributes to refer to a group of sentences
-collectively. The sets are flattened together. We could equivalently have
-written:
+Here, the `group(_)` attribute is used to create user-defined groups of
+sentences. A particular group name collectively refers to the whole set of
+sentences within that group. The sets are flattened together, so we could
+equivalently have written:
 
 ```k
-syntax Exp ::= Exp "*" Exp [mult]
-             | Exp "/" Exp [mult]
-             | Exp "+" Exp [add]
-             | Exp "-" Exp [add]
+syntax Exp ::= Exp "*" Exp [group(mult)]
+             | Exp "/" Exp [group(mult)]
+             | Exp "+" Exp [group(add)]
+             | Exp "-" Exp [group(add)]
 
 syntax priorities mult > add
 syntax left mult
@@ -2867,10 +2868,10 @@ Attributes Reference
 
 ### Attribute Syntax Overview
 
-In K, many different syntactic categories accept _attributes_, an optional
-trailing list of keywords or user-defined identifiers. Attribute lists have two
-different syntaxes, depending on where they occur. Each attribute also has a
-type which describes where it may occur.
+In K, many different syntactic categories accept an optional trailing list of
+keywords known as _attributes_. Attribute lists have two different syntaxes,
+depending on where they occur. Each attribute also has a type which describes
+where it may occur.
 
 The first syntax is a square-bracketed (`[]`) list of words. This syntax is
 available for following attribute types:
@@ -2893,8 +2894,7 @@ available for the following attribute types:
 1.  `cell` attributes - may appear inside of the cell start tag in
     configuration declarations
 
-Note that, currently, *unknown* attributes are *ignored*. Essentially, this
-means that there is no such thing as an *invalid* attribute. When we talk about
+Unrecognized attributes are reported as an error. When we talk about
 the *type* of an attribute, we mean a syntactic category to which an attribute
 can be attached where the attribute has some semantic effect.
 
@@ -2925,6 +2925,7 @@ arguments. A legend describing how to interpret the index follows.
 | `format`              | prod  | all     | [`format` attribute](#format-attribute)                                                                                                         |
 | `freshGenerator`      | prod  | all     | [`freshGenerator` attribute](#freshgenerator-attribute)                                                                                         |
 | `function`            | prod  | all     | [`function` and `total` attributes](#function-and-total-attributes)                                                                             |
+| `group(_)`            | all   | all     | [Symbol priority and associativity](#symbol-priority-and-associativity)                                                                         |
 | `hook(_)`             | prod  | all     | No reference yet                                                                                                                                |
 | `hybrid(_)`           | prod  | all     | [`hybrid` attribute](#hybrid-attribute)                                                                                                         |
 | `hybrid`              | prod  | all     | [`hybrid` attribute](#hybrid-attribute)                                                                                                         |

k-distribution/k-tutorial/1_basic/04_disambiguation/README.md

@@ -214,21 +214,22 @@ module LESSON-04-D
 endmodule
 ```
 
-This introduces a couple of new features of K. First of all, we see a bunch of
-attributes we don't already recognize. These are actually not built-in
-attributes, but rather user-defined attributes that are used to group
-productions together conceptually. For example, `literal` in the
-`syntax priorities` sentence is used to refer to the productions with the
-`literal` attribute, i.e., `true` and `false`.
+This introduces a couple of new features of K. First, the `group(_)` attribute
+is used to conceptually group together sets of sentences under a common
+user-defined name. For example, `literal` in the `syntax priorities` sentence is
+used to refer to all the productions marked with the `group(literal)` attribute,
+i.e., `true` and `false`. A production can belong to multiple groups using
+syntax such as `group(myGrp1,myGrp2)`.
 
 Once we understand this, it becomes relatively straightforward to understand
 the meaning of this grammar. Each `syntax priorities` sentence defines a
-priority relation where each `>` separates a priority group containing all
-the productions with at least one of the attributes in that group, and each
-`syntax left`, `syntax right`, or `syntax non-assoc` sentence defines an
-associativity relation connecting all the productions with one of the target
-attributes together into a left-, right-, or non-associative grouping.
-Specifically, this means that:
+priority relation where `>` separates different priority groups. Each priority
+group is defined by a list of one or more group names, and consists of all
+productions which are members of at least one of those named groups.
+
+In the same way, a `syntax left`, `syntax right`, or `syntax non-assoc` sentence
+defines an associativity relation among left-, right-, or non-associative
+groups. Specifically, this means that:
 ```
 syntax left a b
 ```

k-distribution/k-tutorial/1_basic/11_casts/README.md

@@ -103,7 +103,7 @@ This grammar is a little ambiguous and contrived, but it serves to demonstrate
 how a semantic cast might be insufficient to disambiguate a term. If we were
 to write the term `(I1:Int + I2:Int):Exp2`, the term would be ambiguous,
 because the cast is not sufficiently strict to determine whether you mean
-to derive the "+" production tagged `exp`, or the one tagged `exp2`.
+to derive the "+" production in the group `exp` or the one in the group `exp2`.
 
 In this situation, there is a solution: the **strict cast**. For every sort
 `S` in your grammar, K also defines the following production:

k-distribution/pl-tutorial/1_k/4_imp++/lesson_8/imp.md

@@ -97,19 +97,17 @@ example, the syntax of the previous "statement" assignment which
 is now obtained by composing the new assignment expression, and the
 new expression statement constructs); go the last lesson of
 Tutorial 2 if you are interested in IMP's constructs. For execution
-purposes, we tag the addition and division operations with the
-`addition` and `division` tags. These attributes have
-no theoretical significance, in that they do not affect the semantics
-of the language in any way. They only have practical relevance,
-specific to our implementation of the **K** tool. Specifically, we can
-tell the **K** tool (using its `superheat` and `supercool`
+purposes, we tag the addition and division operations as members of the
+`addition` and `division` groups. These groups have no theoretical significance,
+in that they do not affect the semantics of the language in any way. They only
+have practical relevance, specific to our implementation of the **K** tool.
+Specifically, we can tell the **K** tool (using its `superheat` and `supercool`
 options) that we want to exhaustively explore all the non-deterministic
 behaviors (due to strictness) of these language constructs. For performance
 reasons, by default the **K** tool chooses an arbitrary but fixed order to
-evaluate the arguments of the strict language constructs, thus possibly
-losing behaviors due to missed interleavings. This aspect was irrelevant in
-IMP, because its expressions had no side effects, but it becomes relevant
-in IMP++.
+evaluate the arguments of the strict language constructs, thus possibly losing
+behaviors due to missed interleavings. This aspect was irrelevant in IMP,
+because its expressions had no side effects, but it becomes relevant in IMP++.
 
 The syntax of the IMP++ constructs is self-explanatory. Note that assignment
 is now an expression construct. Also, `print` is variadic, taking a
@@ -293,7 +291,7 @@ configuration.
 Below we list the semantics of the old IMP constructs, referring the
 reader to the **K** semantics of IMP for their meaning. Like we tagged the
 addition and the division rules above in the syntax, we also tag the lookup
-and the assignment rules below (with tags `lookup` and
+and the assignment rules below (as members of the groups `lookup` and
 `assignment`), because we want to refer to them when we generate the
 language model (with the `kompile` tool), basically to allow them to
 generate (possibly non-deterministic) transitions. Indeed, these two rules,
@@ -405,7 +403,7 @@ Without abstraction, you would have to also include the `thread` and
 
 ### Read
 The `read()` construct evaluates to the first integer in the
-input buffer, which it consumes. Note that this rule is tagged
+input buffer, which it consumes. Note that this rule is put in the group
 `increment`. This is because we will include it in the set of
 potentially non-deterministic transitions when we kompile the definition;
 we want to do that because two or more threads can "compete" on
@@ -587,7 +585,7 @@ with the command:
 kompile imp.k --transition="addition division lookup assignment increment read print"
 ```
 
-As already mentioned, the syntax and rule tags play no theoretical or
+As already mentioned, the syntax and rule groups play no theoretical or
 foundational role in **K**. They are only a means to allow `kompile` to
 refer to them in its options, like we did above. By default, `kompile`'s
 transition option is empty, because this yields the fastest language model when

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md

@@ -1073,8 +1073,8 @@ declarations.
 
 ## Location lookup
 
-The operation below is straightforward.  Note that we tag it with the same
-`lookup` tag as the variable lookup rule defined above.  This way,
+The operation below is straightforward.  Note that we place it in the same
+`lookup` group as the variable lookup rule defined above.  This way,
 both rules will be considered transitions when we include the `lookup`
 tag in the transition option of `kompile`.
 ```k
@@ -1170,7 +1170,7 @@ definition with the right options in order to generate the desired model.
 No kompile options are needed if you only only want to execute the definition
 (and thus get an interpreter), but if you want to search for a different
 program behaviors then you need to kompile with the transition option
-including rule tags such as lookup, increment, acquire, etc.  See the
+including rule groups such as lookup, increment, acquire, etc.  See the
 IMP++ tutorial for what the transition option means how to use it.
 ```k
 endmodule

k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/simple-typed-static.md

@@ -509,7 +509,7 @@ Array access requires each index to type to an integer, and the
 array type to be at least as deep as the number of indexes:
 ```k
 // NOTE:
-// We used to need parentheses in the RHS, to avoid capturing Ts as rule tag.
+// We used to need parentheses in the RHS, to avoid capturing Ts as an attribute
 // Let's hope that is not a problem anymore.
 
   rule (T[])[int, Ts:Types] => T[Ts]

k-distribution/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md

@@ -166,8 +166,8 @@ the list is on a position which can be evaluated:
 ```
 We next define the syntax of arithmetic constructs, together with
 their relative priorities and left-/non-associativities.  We also
-tag all these rules with a new tag, "arith", so we can more easily
-define global syntax priirities later (at the end of the syntax module).
+tag all these rules as members of a new group, "arith", so we can more easily
+define global syntax priorities later (at the end of the syntax module).
 ```k
   syntax Exp ::= left:
                  Exp "*" Exp                       [strict, group(arith)]