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

Add syntax for match and variant operators #1206

Merged
merged 15 commits into from
Oct 5, 2023
Merged

Add syntax for match and variant operators #1206

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
fe8f55a
Replace unsupported union match with sum match
Oct 5, 2023
16d7075
Add generated files
Oct 5, 2023
d8c6cc0
Add test fixtures
Oct 5, 2023
5fc4698
Remove unused import
Oct 5, 2023
1c5bfce
Clean up ToIrListener
Oct 5, 2023
abfb0e0
Fix comment
Oct 5, 2023
382e90c
Use sum syntax in the option example
Oct 5, 2023
9272a76
Remove CLI test for typecheck of option.qnt
Oct 5, 2023
f29276d
Update examples entry for option.qnt
Oct 5, 2023
2ab35d6
Move `zip` util into src
Oct 5, 2023
fcd5ba5
Fix order of actual and expected values
Oct 5, 2023
d9ffe10
Walk the row of a sum type
Oct 5, 2023
0f187c0
Fix documentation of sum type ir listener
Oct 5, 2023
3768598
Fix comments
Oct 5, 2023
ba946ad
Remove commented out code
Oct 5, 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 examples/.scripts/run-example.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ result () {
printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then
elif [[ "$file" == "language-features/option.qnt" && "$cmd" =~ (typecheck|test|verify) ]] ; then
printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
printf "<sup>https://github.com/informalsystems/quint/issues/1019</sup>"
Expand Down
2 changes: 1 addition & 1 deletion examples/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ listed without any additional command line arguments.
| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
| [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
Expand Down
29 changes: 6 additions & 23 deletions examples/language-features/option.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,8 @@ module option {
// An option type for values.
// This type declaration is not required. It only defines an alias.
type Vote_option =
| { tag: "none" }
| { tag: "some", value: int }

def Some(v) = { tag: "some", value: v }

val None = { tag: "none" }
| None
| Some(int)

var votes: List[Vote_option]
var outcome: int
Expand All @@ -29,24 +25,11 @@ module option {
}

val SumVotes =
def sum_one(sum, w): (int, Vote_option) => int =
// deconstruct a discriminate union.
w match
// this pattern binds some_w to the "some" version of w, if w.tag == "some"
| "some": some_w => sum + some_w.value
// this pattern
| "none": _ => sum

/* // this is how you would do that in typescript
if (w.tag == "some") {
// w has the type { tag: "some", value: int }
sum + w.value
} else {
sum
votes.foldl(0, (sum, vote) => match vote {
| Some(v) => sum + v
| None => sum
}
*/

votes.foldl(0, sum_one)
)

action Next = all {
any {
Expand Down
5 changes: 0 additions & 5 deletions quint/cli-tests.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,11 +117,6 @@ Temporarily disabled.
<!-- !test check option -->
quint parse ../examples/language-features/option.qnt

### OK on typecheck option

<!-- !test check option - Types & Effects -->
quint typecheck ../examples/language-features/option.qnt

### OK on parse BinSearch

<!-- !test check BinSearch -->
Expand Down
12 changes: 8 additions & 4 deletions quint/src/generated/Quint.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,7 @@ typeDef
| 'type' typeName=qualId '=' '|'? typeSumVariant ('|' typeSumVariant)* # typeSumDef
;

// A single variant case in a sum type definition.
//
// A single variant case in a sum type definition or match statement.
// E.g., `A(t)` or `A`.
typeSumVariant : sumLabel=simpleId["variant label"] ('(' type ')')? ;

Expand Down Expand Up @@ -157,8 +156,7 @@ expr: // apply a built-in operator via the dot notation
| expr OR expr # or
| expr IFF expr # iff
| expr IMPLIES expr # implies
| expr MATCH
('|' STRING ':' parameter '=>' expr)+ # match
| matchSumExpr # match
| 'all' '{' expr (',' expr)* ','? '}' # actionAll
| 'any' '{' expr (',' expr)* ','? '}' # actionAny
| ( qualId | INT | BOOL | STRING) # literalOrId
Expand All @@ -176,6 +174,12 @@ expr: // apply a built-in operator via the dot notation
| '{' expr '}' # braces
;

// match e { A(a) => e1 | B => e2 | C(_) => e3 | ... | _ => en }
matchSumExpr: MATCH expr '{' '|'? matchCase+=matchSumCase ('|' matchCase+=matchSumCase)* '}' ;
matchSumCase: (variantMatch=matchSumVariant | wildCardMatch='_') '=>' expr ;
matchSumVariant
: (variantLabel=simpleId["variant label"]) ('(' (variantParam=simpleId["match case parameter"] | '_') ')')? ;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How are these labels used? I see they have spaces, so I suppose it's only for error reporting to users? If so, that's really great - we should really use them more.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep, the string arguments are used for error reporting in

quint/quint/src/generated/Quint.g4

Lines 243 to 254 in ba946ad

// An unqualified identifier that raises an error if a qualId is supplied
simpleId[context: string]
: IDENTIFIER
| qualId {
const err = quintErrorToString(
{ code: 'QNT008',
message: "Identifiers in a " + $context + " cannot be qualified with '::'. Found " + $qualId.text + "."
},
)
this.notifyErrorListeners(err)
}
;

To produce messages like

>>> {A::B::c: 3}
syntax error: error: [QNT008] Identifiers in a record cannot be qualified with '::'. Found A::B::c.
{A::B::c: 3}
        ^


>>> type T = A::B(int)
syntax error: error: [QNT008] Identifiers in a variant label cannot be qualified with '::'. Found A::B.
type T = A::B(int)
             ^

The ANTLR labels like variantLabel and variantParam, on the other hand, are used to provide named accessors for the parsed data on the rhs of the =, used in

quint/quint/src/parsing/ToIrListener.ts

Lines 996 to 1003 in ba946ad

if (variant._variantParam) {
name = variant._variantParam.text
} else {
// We either have a hole or no param specified, in which case our lambda only needs a hole
name = '_'
}
label = variant._variantLabel.text
params = [{ name, id: this.getId(variant) }]


// A probing rule for REPL.
// Note that a top-level declaration has priority over an expression.
// For example, see: https://github.com/informalsystems/quint/issues/394
Expand Down
5 changes: 4 additions & 1 deletion quint/src/generated/Quint.interp
View file
Open in desktop

Large diffs are not rendered by default.

36 changes: 36 additions & 0 deletions quint/src/generated/QuintListener.ts
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading