diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k index 39f955666da..390511a1414 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX // remove division tag when we have proper search strategies | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k index e97f915dd0c..67f7d5fe427 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k @@ -7,7 +7,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k index d8590fe2dc1..a2dd1e8e165 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k @@ -7,7 +7,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] @@ -47,10 +47,10 @@ module IMP // AExp rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_4/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_4/imp.k index c45ba6d325e..290d5720edf 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_4/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_4/imp.k @@ -7,7 +7,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] @@ -49,10 +49,10 @@ module IMP // AExp rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] rule read() => I ... ListItem(I:Int) => .List ... rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_5/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_5/imp.k index 5d5b10beaf7..76b39076b16 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_5/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_5/imp.k @@ -6,7 +6,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] @@ -48,10 +48,10 @@ module IMP // AExp rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] rule read() => I ... ListItem(I:Int) => .List ... rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/imp.k index af60d9454b7..d43dbefe4e2 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/imp.k @@ -7,7 +7,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] syntax BExp ::= Bool | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] @@ -54,12 +54,12 @@ module IMP // AExp rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] rule read() => I ... - ListItem(I:Int) => .List ... [read] + ListItem(I:Int) => .List ... [group(read)] rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I @@ -76,7 +76,7 @@ module IMP // Stmt rule X = I:Int; => . ... ... X |-> N ... - ... N |-> (_ => I) ... [assignment] + ... N |-> (_ => I) ... [group(assignment)] rule S1:Stmt S2:Stmt => S1 ~> S2 [structural] rule if (true) S else _ => S rule if (false) _ else S => S @@ -93,7 +93,7 @@ module IMP syntax AExp ::= Printable context print(HOLE:AExp, _AEs:AExps); rule print(P:Printable,AEs => AEs); ... - ... .List => ListItem(P) [print] + ... .List => ListItem(P) [group(print)] rule print(.AExps); => . [structural] rule halt; ~> _ => . diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/imp.k b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/imp.k index fe8bdd0a245..2772d0ec76a 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/imp.k +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/imp.k @@ -7,7 +7,7 @@ module IMP-SYNTAX | "read" "(" ")" | "-" Int | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] > "spawn" Block > Id "=" AExp [strict(2)] @@ -55,12 +55,12 @@ module IMP // AExp rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] rule read() => I ... - ListItem(I:Int) => .List ... [read] + ListItem(I:Int) => .List ... [group(read)] rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I @@ -77,7 +77,7 @@ module IMP rule _:Int; => . rule X = I:Int => I ... ... X |-> N ... - ... N |-> (_ => I) ... [assignment] + ... N |-> (_ => I) ... [group(assignment)] rule if (true) S else _ => S rule if (false) _ else S => S rule while (B) S => if (B) {S while (B) S} else {.Stmts} [structural] @@ -93,7 +93,7 @@ module IMP syntax AExp ::= Printable context print(HOLE:AExp, _AEs:AExps); rule print(P:Printable,AEs => AEs); ... - ... .List => ListItem(P) [print] + ... .List => ListItem(P) [group(print)] rule print(.AExps); => . [structural] rule halt; ~> _ => . 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 a801ff94b88..603668dc003 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 @@ -126,7 +126,7 @@ of statements surrounded by curly brackets. | "read" "(" ")" | "-" AExp [strict] | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] > "spawn" Block > Id "=" AExp [strict(2)] @@ -312,7 +312,7 @@ them is chosen first. ```k rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] ``` ### Arithmetic constructs @@ -343,7 +343,7 @@ semantics of the two constructs: rule _:Int; => . rule X = I:Int => I ... ... X |-> N ... - ... N |-> (_ => I) ... [assignment] + ... N |-> (_ => I) ... [group(assignment)] ``` ### Sequential composition @@ -400,7 +400,7 @@ Without abstraction, you would have to also include the `thread` and ```k rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] ``` ### Read @@ -414,7 +414,7 @@ for the next transition can lead to different behaviors. ```k rule read() => I ... - ListItem(I:Int) => .List ... [read] + ListItem(I:Int) => .List ... [group(read)] ``` ### Print @@ -444,7 +444,7 @@ count as a computational step. context print(HOLE:AExp, _AEs:AExps); rule print(P:Printable,AEs => AEs); ... - ... .List => ListItem(P) [print] + ... .List => ListItem(P) [group(print)] rule print(.AExps); => . [structural] ``` 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 b0a6411ce3c..69346cc3b88 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 @@ -572,7 +572,7 @@ store, then we rewrite `X` into `V`: ```k rule X:Id => V ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] ``` Note that the rule above excludes reading `⊥`, because `⊥` is not a value and `V` is checked at runtime to be a value. @@ -591,7 +591,7 @@ integers. ```k context ++(HOLE => lvalue(HOLE)) rule ++loc(L) => I +Int 1 ... - ... L |-> (I => I +Int 1) ... [increment] + ... L |-> (I => I +Int 1) ... [group(increment)] ``` ## Arithmetic operators @@ -739,7 +739,7 @@ input value, at the same time discarding the input value from the `in` cell. ```k - rule read() => I ... ListItem(I:Int) => .List ... [read] + rule read() => I ... ListItem(I:Int) => .List ... [group(read)] ``` ## Assignment @@ -757,7 +757,7 @@ resulting location: context (HOLE => lvalue(HOLE)) = _ rule loc(L) = V:Val => V ... ... L |-> (_ => V) ... - [assignment] + [group(assignment)] ``` ## Statements @@ -876,7 +876,7 @@ its evaluated arguments to the output buffer, and discard the residual `print` statement with an empty list of arguments. ```k rule print(V:Val, Es => Es); ... ... .List => ListItem(V) - [print] + [group(print)] rule print(.Vals); => . [structural] ``` @@ -1010,7 +1010,7 @@ by the two rules below: rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - requires (notBool(V in Busy)) [acquire] + requires (notBool(V in Busy)) [group(acquire)] rule acquire V; => . ... ... V:Val |-> (N => N +Int 1) ... @@ -1052,7 +1052,7 @@ actual configuration of SIMPLE is to include each `k` cell in a `thread` cell. ```k rule rendezvous V:Val; => . ... - rendezvous V; => . ... [rendezvous] + rendezvous V; => . ... [group(rendezvous)] ``` ## Auxiliary declarations and operations @@ -1079,7 +1079,7 @@ both rules will be considered transitions when we include the `lookup` tag in the transition option of `kompile`. ```k syntax Exp ::= lookup(Int) - rule lookup(L) => V ... ... L |-> V:Val ... [lookup] + rule lookup(L) => V ... ... L |-> V:Val ... [group(lookup)] ``` ## Environment recovery diff --git a/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md b/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md index 68db3354599..d7c6f65751b 100644 --- a/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md +++ b/k-distribution/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md @@ -295,7 +295,7 @@ When done with the first pass, call `main()`. ```k rule X:Id => V ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] ``` ### Variable/Array increment @@ -303,7 +303,7 @@ When done with the first pass, call `main()`. ```k context ++(HOLE => lvalue(HOLE)) rule ++loc(L) => I +Int 1 ... - ... L |-> (I:Int => I +Int 1) ... [increment] + ... L |-> (I:Int => I +Int 1) ... [group(increment)] ``` ### Arithmetic operators @@ -387,7 +387,7 @@ completed to return the `nothing` value tagged as expected. ### Read ```k - rule read() => I ... ListItem(I:Int) => .List ... [read] + rule read() => I ... ListItem(I:Int) => .List ... [group(read)] ``` ### Assignment @@ -398,7 +398,7 @@ preserved: context (HOLE => lvalue(HOLE)) = _ rule loc(L) = V:Val => V ... ... L |-> (V' => V) ... - when typeOf(V) ==K typeOf(V') [assignment] + when typeOf(V) ==K typeOf(V') [group(assignment)] ``` ### Statements @@ -440,7 +440,7 @@ preserved: We only allow printing integers and strings: ```k rule print(V:Val, Es => Es); ... ... .List => ListItem(V) - when typeOf(V) ==K int orBool typeOf(V) ==K string [print] + when typeOf(V) ==K int orBool typeOf(V) ==K string [group(print)] rule print(.Vals); => . [structural] ``` @@ -511,7 +511,7 @@ values, in which case our semantics below works fine: rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - when (notBool(V in Busy:Set)) [acquire] + when (notBool(V in Busy:Set)) [group(acquire)] rule acquire V; => . ... ... V:Val |-> (N:Int => N +Int 1) ... @@ -532,7 +532,7 @@ values, in which case our semantics below works fine: ```k rule rendezvous V:Val; => . ... - rendezvous V; => . ... [rendezvous] + rendezvous V; => . ... [group(rendezvous)] ``` ### Auxiliary declarations and operations @@ -548,7 +548,7 @@ into a list of variable declarations. Location lookup. ```k syntax Exp ::= lookup(Int) // see NOTES.md for why Exp instead of KItem - rule lookup(L) => V ... ... L |-> V:Val ... [lookup] + rule lookup(L) => V ... ... L |-> V:Val ... [group(lookup)] ``` Environment recovery. ```k diff --git a/k-distribution/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md b/k-distribution/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md index cc3b0a0c1e8..ea2da2b423e 100644 --- a/k-distribution/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md +++ b/k-distribution/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md @@ -414,12 +414,12 @@ definition. rule X:Id => V ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] context ++(HOLE => lvalue(HOLE)) rule ++loc(L) => I +Int 1 ... - ... L |-> (I:Int => I +Int 1) ... [increment] + ... L |-> (I:Int => I +Int 1) ... [group(increment)] rule I1 + I2 => I1 +Int I2 @@ -469,13 +469,13 @@ interestingly, the semantics of return stays unchanged. rule return; => return nothing; - rule read() => I ... ListItem(I:Int) => .List ... [read] + rule read() => I ... ListItem(I:Int) => .List ... [group(read)] context (HOLE => lvalue(HOLE)) = _ rule loc(L) = V:Val => V ... ... L |-> (_ => V) ... - [assignment] + [group(assignment)] rule {} => . [structural] @@ -492,7 +492,7 @@ interestingly, the semantics of return stays unchanged. rule while (E) S => if (E) {S while(E)S} [structural] rule print(V:Val, Es => Es); ... ... .List => ListItem(V) - [print] + [group(print)] rule print(.Vals); => . [structural] @@ -539,7 +539,7 @@ from SIMPLE unchanged. rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - when (notBool(V in Busy:Set)) [acquire] + when (notBool(V in Busy:Set)) [group(acquire)] rule acquire V; => . ... ... V:Val |-> (N:Int => N +Int 1) ... @@ -552,7 +552,7 @@ from SIMPLE unchanged. ... SetItem(V) => .Set ... rule rendezvous V:Val; => . ... - rendezvous V; => . ... [rendezvous] + rendezvous V; => . ... [group(rendezvous)] ``` ## Unchanged auxiliary operations from untyped SIMPLE @@ -567,7 +567,7 @@ from SIMPLE unchanged. /* syntax KItem ::= lookup(Int) */ - rule lookup(L) => V ... ... L |-> V:Val ... [lookup] + rule lookup(L) => V ... ... L |-> V:Val ... [group(lookup)] syntax KItem ::= setEnv(Map) rule setEnv(Env) => . ... _ => Env [structural] @@ -922,7 +922,7 @@ method call or the array access. ```k rule (X:Id => V)(_:Exps) ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] rule (X:Id => this . X)(_:Exps) ... Env @@ -963,7 +963,7 @@ task as a replacement for the method. When that happens, we just lookup the value at location `L`: ```k rule (lookup(L) => V)(_:Exps) ... ... L |-> V:Val ... - [lookup] + [group(lookup)] ``` The value `V` looked up above is expected to be a method closure, in which case the semantics of method application given above will diff --git a/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md b/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md index 5e26f0a3123..249d75efbb3 100644 --- a/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md +++ b/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md @@ -280,12 +280,12 @@ KOOL). rule X:Id => V ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] context ++(HOLE => lvalue(HOLE)) rule ++loc(L) => I +Int 1 ... - ... L |-> (I:Int => I +Int 1) ... [increment] + ... L |-> (I:Int => I +Int 1) ... [group(increment)] rule I1 + I2 => I1 +Int I2 @@ -322,7 +322,7 @@ KOOL). [structural] - rule read() => I ... ListItem(I:Int) => .List ... [read] + rule read() => I ... ListItem(I:Int) => .List ... [group(read)] context (HOLE => lvalue(HOLE)) = _ @@ -346,7 +346,7 @@ KOOL). rule print(V:Val, Es => Es); ... ... .List => ListItem(V) - requires typeOf(V) ==K int orBool typeOf(V) ==K string [print] + requires typeOf(V) ==K int orBool typeOf(V) ==K string [group(print)] rule print(.Vals); => . [structural] @@ -360,7 +360,7 @@ KOOL). rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - requires (notBool(V in Busy:Set)) [acquire] + requires (notBool(V in Busy:Set)) [group(acquire)] rule acquire V; => . ... ... V:Val |-> (N:Int => N +Int 1) ... @@ -373,7 +373,7 @@ KOOL). ... SetItem(V) => .Set ... rule rendezvous V:Val; => . ... - rendezvous V; => . ... [rendezvous] + rendezvous V; => . ... [group(rendezvous)] ``` ## Unchanged auxiliary operations from dynamically typed SIMPLE @@ -385,7 +385,7 @@ KOOL). rule mkDecls(.Params,.Vals) => {} syntax Exp ::= lookup(Int) - rule lookup(L) => V ... ... L |-> V:Val ... [lookup] + rule lookup(L) => V ... ... L |-> V:Val ... [group(lookup)] syntax KItem ::= setEnv(Map) rule setEnv(Env) => . ... _ => Env [structural] @@ -518,7 +518,7 @@ values are allowed to be stored in each location. => subtype(typeOf(V),typeOf(V')) ~> true? ~> unsafeCast(V, typeOf(V')) ... ... L |-> (V' => unsafeCast(V, typeOf(V'))) ... - [assignment] + [group(assignment)] ``` ## Typed exceptions @@ -714,7 +714,7 @@ The method lookup is the same as in untyped KOOL. ```k rule (X:Id => V)(_:Exps) ... ... X |-> L ... - ... L |-> V:Val ... [lookup] + ... L |-> V:Val ... [group(lookup)] rule (X:Id => this . X)(_:Exps) ... Env @@ -751,7 +751,7 @@ The method lookup is the same as in untyped KOOL. */ rule (lookup(L) => V)(_:Exps) ... ... L |-> V:Val ... - [lookup] + [group(lookup)] ``` ## Instance of diff --git a/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md index c0cab4c7c34..cc286f91d89 100644 --- a/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md +++ b/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md @@ -646,7 +646,7 @@ checks for cycles. ... => .Bag) ... .List => ListItem("Class \"" +String Id2String(C) +String "\" is in a cycle!\n") - [inheritance-cycle, priority(25)] + [group(inheritance-cycle), priority(25)] ``` ## New 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 ed4546200f8..09be15de267 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 @@ -170,27 +170,27 @@ 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). ```k syntax Exp ::= left: - Exp "*" Exp [strict, arith] - | Exp "/" Exp [strict, arith] - | Exp "%" Exp [strict, arith] + Exp "*" Exp [strict, group(arith)] + | Exp "/" Exp [strict, group(arith)] + | Exp "%" Exp [strict, group(arith)] > left: - Exp "+" Exp [strict, left, arith] - | Exp "^" Exp [strict, left, arith] + Exp "+" Exp [strict, left, group(arith)] + | Exp "^" Exp [strict, left, group(arith)] // left attribute should not be necessary; currently a parsing bug - | Exp "-" Exp [strict, prefer, arith] + | Exp "-" Exp [strict, prefer, group(arith)] // the "prefer" attribute above is to not parse x-1 as x(-1) // Due to some parsing problems, we currently cannot add unary minus: - | "-" Exp [strict, arith] + | "-" Exp [strict, group(arith)] > non-assoc: - Exp "<" Exp [strict, arith] - | Exp "<=" Exp [strict, arith] - | Exp ">" Exp [strict, arith] - | Exp ">=" Exp [strict, arith] - | Exp "==" Exp [strict, arith] - | Exp "!=" Exp [strict, arith] - > "!" Exp [strict, arith] - > Exp "&&" Exp [strict(1), left, arith] - > Exp "||" Exp [strict(1), left, arith] + Exp "<" Exp [strict, group(arith)] + | Exp "<=" Exp [strict, group(arith)] + | Exp ">" Exp [strict, group(arith)] + | Exp ">=" Exp [strict, group(arith)] + | Exp "==" Exp [strict, group(arith)] + | Exp "!=" Exp [strict, group(arith)] + > "!" Exp [strict, group(arith)] + > Exp "&&" Exp [strict(1), left, group(arith)] + > Exp "||" Exp [strict(1), left, group(arith)] ``` The conditional construct has the expected evaluation strategy, stating that only the first argument is evaluate: diff --git a/k-distribution/tests/regression-new/imp++-llvm/imp.md b/k-distribution/tests/regression-new/imp++-llvm/imp.md index 346841fb954..1868a1af444 100644 --- a/k-distribution/tests/regression-new/imp++-llvm/imp.md +++ b/k-distribution/tests/regression-new/imp++-llvm/imp.md @@ -126,7 +126,7 @@ of statements surrounded by curly brackets. | "read" "(" ")" | "-" AExp [strict] | "(" AExp ")" [bracket] - > AExp "/" AExp [left, strict, division] + > AExp "/" AExp [left, strict, group(division)] > AExp "+" AExp [left, strict] > "spawn" Block > Id "=" AExp [strict(2)] @@ -312,7 +312,7 @@ them is chosen first. ```k rule X:Id => I ... ... X |-> N ... - ... N |-> I ... [lookup] + ... N |-> I ... [group(lookup)] ``` ### Arithmetic constructs @@ -343,7 +343,7 @@ semantics of the two constructs: rule _:Int; => . rule X = I:Int => I ... ... X |-> N ... - ... N |-> (_ => I) ... [assignment] + ... N |-> (_ => I) ... [group(assignment)] ``` ### Sequential composition @@ -400,7 +400,7 @@ Without abstraction, you would have to also include the `thread` and ```k rule ++X => I +Int 1 ... ... X |-> N ... - ... N |-> (I => I +Int 1) ... [increment] + ... N |-> (I => I +Int 1) ... [group(increment)] ``` ### Read @@ -414,7 +414,7 @@ for the next transition can lead to different behaviors. ```k rule read() => I ... - ListItem(I:Int) => .List ... [read] + ListItem(I:Int) => .List ... [group(read)] ``` ### Print @@ -444,7 +444,7 @@ count as a computational step. context print(HOLE:AExp, _AEs:AExps); rule print(P:Printable,AEs => AEs); ... - ... .List => ListItem(P) [print] + ... .List => ListItem(P) [group(print)] rule print(.AExps); => . [structural] ``` diff --git a/k-distribution/tests/regression-new/issue-1372/test.k b/k-distribution/tests/regression-new/issue-1372/test.k index fda622e72f9..40815b33104 100644 --- a/k-distribution/tests/regression-new/issue-1372/test.k +++ b/k-distribution/tests/regression-new/issue-1372/test.k @@ -1,6 +1,6 @@ // Copyright (c) K Team. All Rights Reserved. module TEST - configuration .K + configuration .K .K syntax KItem ::= "foo" diff --git a/k-distribution/tests/regression-new/issue-1760/test.k b/k-distribution/tests/regression-new/issue-1760/test.k index 1c9aed2ae8d..09992bc4f9e 100644 --- a/k-distribution/tests/regression-new/issue-1760/test.k +++ b/k-distribution/tests/regression-new/issue-1760/test.k @@ -18,11 +18,11 @@ module TEST // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), boolOperation, latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), boolOperation, latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), boolOperation, latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] + > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] + | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)] - //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), boolOperation, hook(KAT.implies)] + //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)] diff --git a/k-distribution/tests/regression-new/issue-1760/test.k.out b/k-distribution/tests/regression-new/issue-1760/test.k.out index 1435e188e69..a5da92020be 100644 --- a/k-distribution/tests/regression-new/issue-1760/test.k.out +++ b/k-distribution/tests/regression-new/issue-1760/test.k.out @@ -5,16 +5,16 @@ . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `notKat_`(_) Source(test.k) - Location(21,19,21,167) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), boolOperation, latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,174) + 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(test.k) - Location(22,19,22,179) - 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), boolOperation, latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(22,19,22,186) + 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_orKat__TEST_Kat_Kat_Kat`(_,_) Source(test.k) - Location(23,19,23,166) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), boolOperation, latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(23,19,23,173) + 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/k-distribution/tests/regression-new/issue-999/kat.k b/k-distribution/tests/regression-new/issue-999/kat.k index 9b4c2c71a20..adea4d946e7 100644 --- a/k-distribution/tests/regression-new/issue-999/kat.k +++ b/k-distribution/tests/regression-new/issue-999/kat.k @@ -18,11 +18,11 @@ module KAT // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), boolOperation, latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), boolOperation, latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), boolOperation, latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] + > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] + | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)] - //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), boolOperation, hook(KAT.implies)] + //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)] diff --git a/k-distribution/tests/regression-new/issue-999/kat.k.out b/k-distribution/tests/regression-new/issue-999/kat.k.out index 86960f10d16..04d446fee84 100644 --- a/k-distribution/tests/regression-new/issue-999/kat.k.out +++ b/k-distribution/tests/regression-new/issue-999/kat.k.out @@ -5,16 +5,16 @@ . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `notKat_`(_) Source(kat.k) - Location(21,19,21,167) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), boolOperation, latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,174) + 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(kat.k) - Location(22,19,22,179) - 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), boolOperation, latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(22,19,22,186) + 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_orKat__KAT_Kat_Kat_Kat`(_,_) Source(kat.k) - Location(23,19,23,166) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), boolOperation, latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(23,19,23,173) + 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/k-distribution/tests/regression-new/parse-c/c18-syntax.k b/k-distribution/tests/regression-new/parse-c/c18-syntax.k index ad2fef9e6bd..d5ac70196ae 100644 --- a/k-distribution/tests/regression-new/parse-c/c18-syntax.k +++ b/k-distribution/tests/regression-new/parse-c/c18-syntax.k @@ -84,29 +84,29 @@ module C18-COMMON > right: Exp "?" Exp ":" Exp > right: - Exp "=" Exp [assign] - | Exp "*=" Exp [assign] - | Exp "/=" Exp [assign] - | Exp "%=" Exp [assign] - | Exp "+=" Exp [assign] - | Exp "-=" Exp [assign] - | Exp "<<=" Exp [assign] - | Exp ">>=" Exp [assign] - | Exp "&=" Exp [assign] - | Exp "^=" Exp [assign] - | Exp "|=" Exp [assign] + Exp "=" Exp [group(assign)] + | Exp "*=" Exp [group(assign)] + | Exp "/=" Exp [group(assign)] + | Exp "%=" Exp [group(assign)] + | Exp "+=" Exp [group(assign)] + | Exp "-=" Exp [group(assign)] + | Exp "<<=" Exp [group(assign)] + | Exp ">>=" Exp [group(assign)] + | Exp "&=" Exp [group(assign)] + | Exp "^=" Exp [group(assign)] + | Exp "|=" Exp [group(assign)] > left: - Exp "," Exp [comma] + Exp "," Exp [group(comma)] syntax priorities assignExp > comma syntax priorities constantExp > assign syntax GenericAssocs ::= NeList{GenericAssoc,","} - syntax GenericAssoc ::= TypeName ":" Exp [assignExp] - | "default" ":" Exp [assignExp] + syntax GenericAssoc ::= TypeName ":" Exp [group(assignExp)] + | "default" ":" Exp [group(assignExp)] - syntax Exps ::= Exp [klabel(arg), assignExp] - | Exps "," Exp [assignExp] + syntax Exps ::= Exp [klabel(arg), group(assignExp)] + | Exps "," Exp [group(assignExp)] // \section(A.2.2) @@ -175,13 +175,13 @@ module C18-COMMON syntax StructDeclarators ::= NeList{StructDeclarator,","} syntax StructDeclarator ::= Declarator - | Declarator ":" Exp [constantExp] - | ":" Exp [constantExp] + | Declarator ":" Exp [group(constantExp)] + | ":" Exp [group(constantExp)] syntax Enumerators ::= NeList{Enumerator,","} syntax Enumerator ::= Identifier - | Identifier "=" Exp [constantExp] + | Identifier "=" Exp [group(constantExp)] syntax TypeQualifier ::= "const" | "restrict" | "volatile" | "_Atomic" syntax FunctionSpecifier ::= "inline" | "_Noreturn" @@ -257,7 +257,7 @@ module C18-COMMON | DirectAbstractDeclarator "(" ")" | DirectAbstractDeclarator "(" ParamTypeList ")" - syntax Init ::= Exp [klabel(initExp), assignExp] + syntax Init ::= Exp [klabel(initExp), group(assignExp)] | "{" Inits "}" | "{" Inits "," "}"