Clean up {...}<:S strict cast syntax (#3853)

This PR cleans up a few issues related to the `{...}<:S` syntax for
strict casts. Specifically,

- Add a section to Lesson 1.11 explaining the need for the braced strict
cast syntax
- Change the klabel from `#InnerCast` to `#SyntacticCastBraced`
   - `#InnerCast` was a holdover from prior to #2352 
- Opinionatedly, change the syntax from `{...}<:S` to `{...}::S`
- Makes it more obvious this is just an alternative syntax for strict
casts `::S`
- To me, the syntax `<:S` is misleading in that it reads as "subsort of
`S`", but the actual meaning is "exactly the sort `S` and not a proper
subsort".
- Minimal fallout - there is only one rule in `rv-match` and two tests
in `pyk` where this needs to be changed
(https://github.com/search?q=org%3Aruntimeverification+%7D%3C%3A&type=code)

The commit history is clean and I can just drop the last commit if we
don't want to change the syntax.

---------

Co-authored-by: rv-jenkins <[email protected]>

k-distribution/include/kframework/builtin/domains.md

@@ -1932,7 +1932,7 @@ module STRING-BUFFER-IN-K [symbolic]
   syntax StringBuffer ::= String
   syntax String ::= StringBuffer2String ( StringBuffer ) [function, total]
 
-  rule {SB:String +String S:String}<:StringBuffer => (SB +String S)::String
+  rule {SB:String +String S:String}::StringBuffer => (SB +String S)::String
   rule .StringBuffer => ""
   rule StringBuffer2String(S:String) => S
 endmodule

k-distribution/include/kframework/builtin/kast.md

@@ -387,7 +387,7 @@ module AUTO-CASTS
   // generates, for all sorts, productions of the form:
   // Sort  ::= Sort ":Sort"  // semantic cast - force the inner term to be `Sort` or a subsort
   // Sort  ::= Sort "::Sort" // strict cast - force the inner term to be exactly `Sort`. Useful for disambiguation
-  // Sort ::= "{" Sort "}" "<:Sort" // synonym for strict cast
+  // Sort ::= "{" Sort "}" "::Sort" // synonym for strict cast
   // Sort  ::= "{" K "}"    ":>Sort" // projection cast. Allows any term to be placed in a context that expects `Sort`
   // this is part of the mechanism that allows concrete user syntax in K
 endmodule

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

@@ -94,16 +94,18 @@ example, consider the following definition:
 module LESSON-11-C
   imports INT
 
-  syntax Exp ::= Int | Exp "+" Exp [group(exp)]
-  syntax Exp2 ::= Exp | Exp2 "+" Exp2 [group(exp2)]
+  syntax Exp ::= Int
+               | "add[" Exp "," Exp "]"   [group(exp)]
+  syntax Exp2 ::= Exp
+               | "add[" Exp2 "," Exp2 "]" [group(exp2)]
 endmodule
 ```
 
 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,
+to write the term `add[ 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 in the group `exp` or the one in the group `exp2`.
+to derive the "add" production defined in group `exp` or the one in 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:
@@ -120,9 +122,39 @@ in the **type system** of K: namely, the term inside the cast cannot be a
 `syntax S ::= S2` exists.
 
 As a result, if we were to write in the above grammar the term
-`(I1:Int + I2:Int)::Exp2`, then we would know that the second derivation above
+`add[ I1:Int , I2:Int ]::Exp2`, then we would know that the second derivation above
 should be chosen, whereas if we want the first derivation, we could write
-`(I1:Int + I2:Int)::Exp`.
+`add[ I1:Int , I2:Int ]::Exp`.
+
+Care must be taken when using a strict cast with brackets. For example, consider a
+similar grammar but using an infix "+":
+
+```k
+module LESSON-11-D
+  imports INT
+
+  syntax Exp ::= Int
+               | Exp "+" Exp   [group(exp)]
+  syntax Exp2 ::= Exp
+               | Exp2 "+" Exp2 [group(exp2)]
+               | "(" Exp2 ")"  [bracket]
+endmodule
+```
+
+The term `I1:Int + I2:Int` is ambiguous and could refer to either the production
+in group `exp` or the one in group `exp2`. To differentiate, you might try to write
+`(I1:Int + I2:Int)::Exp2` similarly to the previous example.
+
+Unfortunately though, this is still ambiguous. Here, the strict cast `::Exp2` applies
+directly to the brackets themselves rather than the underlying term within those brackets.
+As a result, it enforces that `(I1:Int + I2:Int)` cannot be a strict subsort of `Exp2`, but
+it has no effect on the sort of the subterm `I1:Int + I2:Int`.
+
+For cases like this, K provides an alternative syntax for strict casts:
+```
+  syntax S ::= "{" S "}::S"
+```
+The ambiguity can then be resolved with `{I1:Int + I2:Int}::Exp` or `{I1:Int + I2:Int}::Exp2`.
 
 ### Projection casts
 
@@ -162,7 +194,7 @@ inserted into the code that runs when the rule applies.
 For example, here is a module that makes use of projection casts:
 
 ```k
-module LESSON-11-D
+module LESSON-11-E
   imports INT
   imports BOOL
 
@@ -186,12 +218,12 @@ the projection cast will fail.
 
 ## Exercises
 
-1. Extend the `eval` function in `LESSON-11-D` to include Strings and add a `.`
+1. Extend the `eval` function in `LESSON-11-E` to include Strings and add a `.`
 operator which concatenates them.
 
 2. Modify your solution from Lesson 1.9, Exercise 2 by using an `Exp` sort to
 express the integer and Boolean expressions that it supports, in the same style
-as `LESSON-11-D`. Then write an `eval` function that evaluates all terms of
+as `LESSON-11-E`. Then write an `eval` function that evaluates all terms of
 sort `Exp` to either a `Bool` or an `Int`.
 
 ## Next lesson

k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md

@@ -117,7 +117,7 @@ Haskell Backend which performs **symbolic execution**.
 ### Exercise
 
 Pass a program containing no functions to `krun`. You can use a term of sort
-`Exp` from `LESSON-11-D`. Observe the output and try to understand why you get
+`Exp` from `LESSON-11-E`. Observe the output and try to understand why you get
 the output you do. Then write two rules that rewrite that program to another.
 Run `krun --search` on that program and observe both results. Then add a third
 rule that rewrites one of those results again. Test that that rule applies as

k-distribution/k-tutorial/1_basic/commands.sh

@@ -32,6 +32,7 @@ kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-B --syntax-module LESSON-11-B --output-definition build/11b
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-C --syntax-module LESSON-11-C --output-definition build/11c
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-D --syntax-module LESSON-11-D --output-definition build/11d
+kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-E --syntax-module LESSON-11-E --output-definition build/11e
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-A --output-definition build/12a
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-B --output-definition build/12b
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-C --syntax-module LESSON-12-C --output-definition build/12c

kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -783,18 +783,18 @@ private static Set<Sentence> makeCasts(
             castSort,
             Seq(NonTerminal(labelSort), Terminal("::" + castSort.toString())),
             attrs1.add(Att.FORMAT(), "%1%2")));
+    prods.add(
+        Production(
+            KLabel("#SyntacticCastBraced"),
+            castSort,
+            Seq(Terminal("{"), NonTerminal(labelSort), Terminal("}"), Terminal("::" + castSort)),
+            attrs1.add(Att.FORMAT(), "%1 %2 %3%4")));
     prods.add(
         Production(
             KLabel("#SemanticCastTo" + labelSort.toString()),
             labelSort,
             Seq(NonTerminal(labelSort), Terminal(":" + castSort)),
             attrs1.add(Att.FORMAT(), "%1%2")));
-    prods.add(
-        Production(
-            KLabel("#InnerCast"),
-            castSort,
-            Seq(Terminal("{"), NonTerminal(labelSort), Terminal("}"), Terminal("<:" + castSort)),
-            attrs1.add(Att.FORMAT(), "%1 %2 %3%4")));
     prods.add(
         Production(
             KLabel("#OuterCast"),

kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java

@@ -112,7 +112,7 @@ public Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> apply(TermCons
       // Never add a list wrapper between a sort annotation and the annotated term
       if (tcLabelName.equals("#SyntacticCast")
           || tcLabelName.startsWith("#SemanticCastTo")
-          || tcLabelName.equals("#InnerCast")) {
+          || tcLabelName.equals("#SyntacticCastBraced")) {
         return superApply(tc);
       }
     }

kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java

@@ -11,7 +11,7 @@ public class RemoveBracketVisitor extends SafeTransformer {
   public Term apply(TermCons tc) {
     if (tc.production().att().contains(Att.BRACKET())
         || tc.production().klabel().get().name().equals("#SyntacticCast")
-        || tc.production().klabel().get().name().equals("#InnerCast")) {
+        || tc.production().klabel().get().name().equals("#SyntacticCastBraced")) {
       return apply(tc.get(0));
     }
     return super.apply(tc);

kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java

@@ -260,7 +260,7 @@ public Either<Set<KEMException>, Term> apply(Term term) {
               castContext = CastContext.SEMANTIC;
             } else if (substituted.klabel().isDefined()
                 && (substituted.klabel().get().name().equals("#SyntacticCast")
-                    || substituted.klabel().get().name().equals("#InnerCast"))) {
+                    || substituted.klabel().get().name().equals("#SyntacticCastBraced"))) {
               castContext = CastContext.STRICT;
             } else {
               castContext = CastContext.NONE;

kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java

@@ -443,7 +443,7 @@ private static Sort getSortOfCast(TermCons tc) {
       case "#SyntacticCast":
       case "#OuterCast":
         return tc.production().sort();
-      case "#InnerCast":
+      case "#SyntacticCastBraced":
         return ((NonTerminal) tc.production().items().apply(1)).sort();
       default:
         if (tc.production().klabel().get().name().startsWith("#SemanticCastTo")) {
@@ -628,11 +628,11 @@ public String apply(Term t) {
             if (tc.production().klabel().isDefined()
                 && (tc.production().klabel().get().name().equals("#SyntacticCast")
                     || tc.production().klabel().get().name().startsWith("#SemanticCastTo")
-                    || tc.production().klabel().get().name().equals("#InnerCast"))) {
+                    || tc.production().klabel().get().name().equals("#SyntacticCastBraced"))) {
               expectedSort = getSortOfCast(tc);
               isStrictEquality =
                   tc.production().klabel().get().name().equals("#SyntacticCast")
-                      || tc.production().klabel().get().name().equals("#InnerCast");
+                      || tc.production().klabel().get().name().equals("#SyntacticCastBraced");
               if (tc.get(0) instanceof Constant child) {
                 if (child.production().sort().equals(Sorts.KVariable())
                     || child.production().sort().equals(Sorts.KConfigVar())) {

kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java

@@ -112,7 +112,7 @@ private static boolean hasStrictCast(Term t) {
     if (pr.production().klabel().isDefined()) {
       KLabel klabel = pr.production().klabel().get();
       String label = klabel.name();
-      if (label.equals("#SyntacticCast") || label.equals("#InnerCast")) {
+      if (label.equals("#SyntacticCast") || label.equals("#SyntacticCastBraced")) {
         return true;
       }
     }