Skip to content

Commit

Permalink
Update all K tests to use group(_) (#3452)
Browse files Browse the repository at this point in the history 
* Update tests to pass with --pedantic-attributes

* issue-1169/Makefile: Remove not-yet-implemented --no-pedantic-attributes flag.
  • Loading branch information
@Scott-Guest
Scott-Guest authored Jun 6, 2023
1 parent 4b0d9ea commit 0015827
Show file tree
Hide file tree
Showing 21 changed files with 135 additions and 135 deletions.
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down
6 changes: 3 additions & 3 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down Expand Up @@ -47,10 +47,10 @@ module IMP
// AExp
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0
rule I1 + I2 => I1 +Int I2
rule - I => 0 -Int I
Expand Down
6 changes: 3 additions & 3 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_4/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down Expand Up @@ -49,10 +49,10 @@ module IMP
// AExp
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
rule <k> read() => I ...</k>
<input> ListItem(I:Int) => .List ...</input>
rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0
Expand Down
6 changes: 3 additions & 3 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_5/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down Expand Up @@ -48,10 +48,10 @@ module IMP
// AExp
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
rule <k> read() => I ...</k>
<input> ListItem(I:Int) => .List ...</input>
rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0
Expand Down
12 changes: 6 additions & 6 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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})]
Expand Down Expand Up @@ -54,12 +54,12 @@ module IMP
// AExp
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
rule <k> read() => I ...</k>
<input> ListItem(I:Int) => .List ...</input> [read]
<input> ListItem(I:Int) => .List ...</input> [group(read)]
rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
rule I1 + I2 => I1 +Int I2
rule - I => 0 -Int I
Expand All @@ -76,7 +76,7 @@ module IMP
// Stmt
rule <k> X = I:Int; => . ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (_ => I) ...</store> [assignment]
<store>... N |-> (_ => I) ...</store> [group(assignment)]
rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
rule if (true) S else _ => S
rule if (false) _ else S => S
Expand All @@ -93,7 +93,7 @@ module IMP
syntax AExp ::= Printable
context print(HOLE:AExp, _AEs:AExps);
rule <k> print(P:Printable,AEs => AEs); ...</k>
<output>... .List => ListItem(P) </output> [print]
<output>... .List => ListItem(P) </output> [group(print)]
rule print(.AExps); => . [structural]

rule <k> halt; ~> _ => . </k>
Expand Down
12 changes: 6 additions & 6 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -55,12 +55,12 @@ module IMP
// AExp
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
rule <k> read() => I ...</k>
<input> ListItem(I:Int) => .List ...</input> [read]
<input> ListItem(I:Int) => .List ...</input> [group(read)]
rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
rule I1 + I2 => I1 +Int I2
rule - I => 0 -Int I
Expand All @@ -77,7 +77,7 @@ module IMP
rule _:Int; => .
rule <k> X = I:Int => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (_ => I) ...</store> [assignment]
<store>... N |-> (_ => I) ...</store> [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]
Expand All @@ -93,7 +93,7 @@ module IMP
syntax AExp ::= Printable
context print(HOLE:AExp, _AEs:AExps);
rule <k> print(P:Printable,AEs => AEs); ...</k>
<output>... .List => ListItem(P) </output> [print]
<output>... .List => ListItem(P) </output> [group(print)]
rule print(.AExps); => . [structural]

rule <k> halt; ~> _ => . </k>
Expand Down
12 changes: 6 additions & 6 deletions k-distribution/pl-tutorial/1_k/4_imp++/lesson_8/imp.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -312,7 +312,7 @@ them is chosen first.
```k
rule <k> X:Id => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> I ...</store> [lookup]
<store>... N |-> I ...</store> [group(lookup)]
```

### Arithmetic constructs
Expand Down Expand Up @@ -343,7 +343,7 @@ semantics of the two constructs:
rule _:Int; => .
rule <k> X = I:Int => I ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (_ => I) ...</store> [assignment]
<store>... N |-> (_ => I) ...</store> [group(assignment)]
```

### Sequential composition
Expand Down Expand Up @@ -400,7 +400,7 @@ Without abstraction, you would have to also include the `thread` and
```k
rule <k> ++X => I +Int 1 ...</k>
<env>... X |-> N ...</env>
<store>... N |-> (I => I +Int 1) ...</store> [increment]
<store>... N |-> (I => I +Int 1) ...</store> [group(increment)]
```

### Read
Expand All @@ -414,7 +414,7 @@ for the next transition can lead to different behaviors.

```k
rule <k> read() => I ...</k>
<input> ListItem(I:Int) => .List ...</input> [read]
<input> ListItem(I:Int) => .List ...</input> [group(read)]
```

### Print
Expand Down Expand Up @@ -444,7 +444,7 @@ count as a computational step.
context print(HOLE:AExp, _AEs:AExps);
rule <k> print(P:Printable,AEs => AEs); ...</k>
<output>... .List => ListItem(P) </output> [print]
<output>... .List => ListItem(P) </output> [group(print)]
rule print(.AExps); => . [structural]
```

Expand Down
16 changes: 8 additions & 8 deletions k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -572,7 +572,7 @@ store, then we rewrite `X` into `V`:
```k
rule <k> X:Id => V ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
<store>... L |-> V:Val ...</store> [group(lookup)]
```
Note that the rule above excludes reading `⊥`, because `⊥` is not
a value and `V` is checked at runtime to be a value.
Expand All @@ -591,7 +591,7 @@ integers.
```k
context ++(HOLE => lvalue(HOLE))
rule <k> ++loc(L) => I +Int 1 ...</k>
<store>... L |-> (I => I +Int 1) ...</store> [increment]
<store>... L |-> (I => I +Int 1) ...</store> [group(increment)]
```

## Arithmetic operators
Expand Down Expand Up @@ -739,7 +739,7 @@ input value, at the same time discarding the input value from the
`in` cell.

```k
rule <k> read() => I ...</k> <input> ListItem(I:Int) => .List ...</input> [read]
rule <k> read() => I ...</k> <input> ListItem(I:Int) => .List ...</input> [group(read)]
```

## Assignment
Expand All @@ -757,7 +757,7 @@ resulting location:
context (HOLE => lvalue(HOLE)) = _
rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (_ => V) ...</store>
[assignment]
[group(assignment)]
```

## Statements
Expand Down Expand Up @@ -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 <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
[print]
[group(print)]
rule print(.Vals); => . [structural]
```

Expand Down Expand Up @@ -1010,7 +1010,7 @@ by the two rules below:
rule <k> acquire V:Val; => . ...</k>
<holds>... .Map => V |-> 0 ...</holds>
<busy> Busy (.Set => SetItem(V)) </busy>
requires (notBool(V in Busy)) [acquire]
requires (notBool(V in Busy)) [group(acquire)]
rule <k> acquire V; => . ...</k>
<holds>... V:Val |-> (N => N +Int 1) ...</holds>
Expand Down Expand Up @@ -1052,7 +1052,7 @@ actual configuration of SIMPLE is to include each `k` cell in a
`thread` cell.
```k
rule <k> rendezvous V:Val; => . ...</k>
<k> rendezvous V; => . ...</k> [rendezvous]
<k> rendezvous V; => . ...</k> [group(rendezvous)]
```

## Auxiliary declarations and operations
Expand All @@ -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 <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [lookup]
rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [group(lookup)]
```

## Environment recovery
Expand Down
16 changes: 8 additions & 8 deletions ...tion/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -295,15 +295,15 @@ When done with the first pass, call `main()`.
```k
rule <k> X:Id => V ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
<store>... L |-> V:Val ...</store> [group(lookup)]
```

### Variable/Array increment

```k
context ++(HOLE => lvalue(HOLE))
rule <k> ++loc(L) => I +Int 1 ...</k>
<store>... L |-> (I:Int => I +Int 1) ...</store> [increment]
<store>... L |-> (I:Int => I +Int 1) ...</store> [group(increment)]
```

### Arithmetic operators
Expand Down Expand Up @@ -387,7 +387,7 @@ completed to return the `nothing` value tagged as expected.
### Read

```k
rule <k> read() => I ...</k> <input> ListItem(I:Int) => .List ...</input> [read]
rule <k> read() => I ...</k> <input> ListItem(I:Int) => .List ...</input> [group(read)]
```

### Assignment
Expand All @@ -398,7 +398,7 @@ preserved:
context (HOLE => lvalue(HOLE)) = _
rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (V' => V) ...</store>
when typeOf(V) ==K typeOf(V') [assignment]
when typeOf(V) ==K typeOf(V') [group(assignment)]
```

### Statements
Expand Down Expand Up @@ -440,7 +440,7 @@ preserved:
We only allow printing integers and strings:
```k
rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
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]
```

Expand Down Expand Up @@ -511,7 +511,7 @@ values, in which case our semantics below works fine:
rule <k> acquire V:Val; => . ...</k>
<holds>... .Map => V |-> 0 ...</holds>
<busy> Busy (.Set => SetItem(V)) </busy>
when (notBool(V in Busy:Set)) [acquire]
when (notBool(V in Busy:Set)) [group(acquire)]
rule <k> acquire V; => . ...</k>
<holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
Expand All @@ -532,7 +532,7 @@ values, in which case our semantics below works fine:

```k
rule <k> rendezvous V:Val; => . ...</k>
<k> rendezvous V; => . ...</k> [rendezvous]
<k> rendezvous V; => . ...</k> [group(rendezvous)]
```

### Auxiliary declarations and operations
Expand All @@ -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 <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [lookup]
rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [group(lookup)]
```
Environment recovery.
```k
Expand Down
Loading

0 comments on commit 0015827

Please sign in to comment.