diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 72df2bc186c..c2b669330e9 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/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 diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md index 9a02996946c..da392abe46a 100644 --- a/k-distribution/include/kframework/builtin/kast.md +++ b/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 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 a3270999c72..6480a37a990 100644 --- a/k-distribution/k-tutorial/1_basic/11_casts/README.md +++ b/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 diff --git a/k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md b/k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md index c7385ab24ca..0694980e6a1 100644 --- a/k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md +++ b/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 diff --git a/k-distribution/k-tutorial/1_basic/commands.sh b/k-distribution/k-tutorial/1_basic/commands.sh index 66ca5cf6aae..f15ab6e30fa 100644 --- a/k-distribution/k-tutorial/1_basic/commands.sh +++ b/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 diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java index 130ed27f176..35f20d563f7 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -783,18 +783,18 @@ private static Set 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"), diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java index 885565d9c97..b4d4589e62d 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java @@ -112,7 +112,7 @@ public Tuple2, Term>, Set> 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); } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java index 1d914cb360c..3dcf0aace10 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java +++ b/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); diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java index 2a4cf418f1e..f4972b8b99d 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java @@ -260,7 +260,7 @@ public Either, 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; diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java index 8798ac1151d..71e01fe0099 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java +++ b/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())) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java index 2de3668a55a..7c88927d511 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java +++ b/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; } }