Merge pull request #1206 from informalsystems/1082/sum-type-syntax

Add syntax for match and variant operators

examples/.scripts/run-example.sh

@@ -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>"

examples/README.md

@@ -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: |

examples/language-features/option.qnt

@@ -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
@@ -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 {

quint/cli-tests.md

@@ -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 -->

quint/src/generated/Quint.g4

@@ -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 ')')? ;
 
@@ -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
@@ -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"] | '_') ')')? ;
+
 // 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