diff --git a/docs/user_manual.md b/docs/user_manual.md index a5d6cfdd93e..82745e1f917 100644 --- a/docs/user_manual.md +++ b/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) | diff --git a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md b/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md index 09a135fd322..a50bfea8040 100644 --- a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md +++ b/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 ``` diff --git a/k-distribution/k-tutorial/1_basic/11_casts/README.md b/k-distribution/k-tutorial/1_basic/11_casts/README.md index e2f8efeb354..a3270999c72 100644 --- a/k-distribution/k-tutorial/1_basic/11_casts/README.md +++ 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: diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_8/imp.md b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_8/imp.md index 603668dc003..8d26d310f61 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_8/imp.md +++ b/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 diff --git a/k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md b/k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md index 69346cc3b88..11da1f560d8 100644 --- a/k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md +++ b/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 diff --git a/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/simple-typed-static.md b/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/simple-typed-static.md index ecf6cabc513..56fededc707 100644 --- a/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/1_static/simple-typed-static.md +++ b/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] diff --git a/k-distribution/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/k-distribution/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md index 09be15de267..7d44affbcb0 100644 --- a/k-distribution/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md +++ b/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)]