Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update all K tests to use group(_) #3452

Merged
merged 3 commits into from
Jun 6, 2023
Merged

Update all K tests to use group(_) #3452

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1904227
Update tests to pass with --pedantic-attributes
Scott-Guest Jun 5, 2023
0e15279
issue-1169/Makefile: Remove not-yet-implemented --no-pedantic-attribu…
Scott-Guest Jun 6, 2023
7056fc2
Merge remote-tracking branch 'origin/develop' into pedantic-attributes
Scott-Guest Jun 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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