Add syntax for constructing and eliminating sum type values

quint/package.json

@@ -77,7 +77,7 @@
     "generate": "npm run antlr && npm run compile && npm link && npm run api-docs && npm run update-fixtures",
     "antlr": "antlr4ts -visitor ./src/generated/Quint.g4 && antlr4ts -visitor ./src/generated/Effect.g4",
     "api-docs": "quint docs ./src/builtin.qnt > ../doc/builtin.md",
-    "update-fixtures": "./scripts/update-fixtures.sh",
+    "update-fixtures": "npm run compile && ./scripts/update-fixtures.sh",
     "format-check": "npx prettier --check '**/*.ts' && npx eslint '**/*.ts'",
     "format": "npx prettier --write '**/*.ts' && npx eslint --fix '**/*.ts'",
     "debug": "npx ts-node ./src/cli.ts"

quint/src/IRTransformer.ts

@@ -58,6 +58,10 @@ export class IRTransformer {
   exitLambda?: (expr: ir.QuintLambda) => ir.QuintLambda
   enterLet?: (expr: ir.QuintLet) => ir.QuintLet
   exitLet?: (expr: ir.QuintLet) => ir.QuintLet
+  enterMatch?: (expr: ir.QuintMatch) => ir.QuintMatch
+  exitMatch?: (expr: ir.QuintMatch) => ir.QuintMatch
+  enterVariant?: (expr: ir.QuintVariant) => ir.QuintVariant
+  exitVariant?: (expr: ir.QuintVariant) => ir.QuintVariant
 
   /** Types */
   enterLiteralType?: (
@@ -448,6 +452,37 @@ function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.Q
         }
       }
       break
+    case 'match':
+      {
+        if (transformer.enterMatch) {
+          newExpr = transformer.enterMatch(newExpr)
+        }
+
+        newExpr.expr = transformExpression(transformer, newExpr.expr)
+        newExpr.cases = newExpr.cases.map(matchCase => ({
+          ...matchCase,
+          expr: transformExpression(transformer, matchCase.elim),
+        }))
+
+        if (transformer.exitMatch) {
+          newExpr = transformer.exitMatch(newExpr)
+        }
+      }
+      break
+
+    case 'variant':
+      {
+        if (transformer.enterVariant) {
+          newExpr = transformer.enterVariant(newExpr)
+        }
+
+        newExpr.expr = transformExpression(transformer, newExpr)
+
+        if (transformer.exitVariant) {
+          newExpr = transformer.exitVariant(newExpr)
+        }
+      }
+      break
 
     default:
       unreachable(newExpr)

quint/src/IRVisitor.ts

@@ -62,6 +62,10 @@ export interface IRVisitor {
   exitLambda?: (_expr: ir.QuintLambda) => void
   enterLet?: (_expr: ir.QuintLet) => void
   exitLet?: (_expr: ir.QuintLet) => void
+  enterMatch?: (_expr: ir.QuintMatch) => void
+  exitMatch?: (_expr: ir.QuintMatch) => void
+  enterVariant?: (_expr: ir.QuintVariant) => void
+  exitVariant?: (_expr: ir.QuintVariant) => void
 
   /** Types */
   enterLiteralType?: (_type: t.QuintBoolType | t.QuintIntType | t.QuintStrType) => void
@@ -248,6 +252,9 @@ export function walkType(visitor: IRVisitor, type: t.QuintType): void {
 
     case 'sum':
       visitor.enterSumType?.(type)
+
+      walkRow(visitor, type.fields)
+
       visitor.exitSumType?.(type)
       break
 
@@ -301,6 +308,7 @@ export function walkDefinition(visitor: IRVisitor, def: ir.QuintDef): void {
       if (visitor.enterTypeDef) {
         visitor.enterTypeDef(def)
       }
+
       if (visitor.exitTypeDef) {
         visitor.exitTypeDef(def)
       }
@@ -404,6 +412,21 @@ function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {
         visitor.exitLet(expr)
       }
       break
+    case 'match':
+      visitor.enterMatch?.(expr)
+
+      walkExpression(visitor, expr.expr)
+      expr.cases.forEach(({ elim }) => walkExpression(visitor, elim))
+
+      visitor.exitMatch?.(expr)
+      break
+    case 'variant':
+      visitor.enterVariant?.(expr)
+      if (expr.expr) {
+        walkExpression(visitor, expr.expr)
+      }
+      visitor.exitVariant?.(expr)
+      break
     default:
       unreachable(expr)
   }

quint/src/IRprinting.ts

@@ -12,8 +12,8 @@
  * @module
  */
 
-import { OpQualifier, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr'
-import { EmptyRow, QuintSumType, QuintType, Row, RowField, VarRow, isTheUnit } from './quintTypes'
+import { MatchCase, OpQualifier, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr'
+import { EmptyRow, QuintSumType, QuintType, Row, RowField, VarRow, isUnitType } from './quintTypes'
 import { TypeScheme } from './types/base'
 import { typeSchemeToString } from './types/printing'
 
@@ -126,9 +126,24 @@ export function expressionToString(expr: QuintEx): string {
       return `((${expr.params.map(p => p.name).join(', ')}) => ${expressionToString(expr.expr)})`
     case 'let':
       return `${definitionToString(expr.opdef)} { ${expressionToString(expr.expr)} }`
+    case 'variant': {
+      const param = expr.expr ? `(${expressionToString(expr.expr)})` : ''
+      return `${expr.label}${param}`
+    }
+    case 'match':
+      return `match ${expressionToString(expr.expr)} { ${matchCasesToString(expr.cases)} }`
   }
 }
 
+function matchCasesToString(cases: MatchCase[]): string {
+  return cases
+    .map(({ label, elim }) => {
+      const param = elim.params.length === 0 ? '' : `(${elim.params[0].name})`
+      return `${label}${param} => ${expressionToString(elim.expr)}`
+    })
+    .join(' | ')
+}
+
 /**
  * Pretty prints a type
  *
@@ -194,13 +209,13 @@ export function rowToString(r: Row): string {
 export function sumToString(s: QuintSumType): string {
   return s.fields.fields
     .map((f: RowField) => {
-      if (isTheUnit(f.fieldType)) {
-        return `| ${f.fieldName}`
+      if (isUnitType(f.fieldType)) {
+        return `${f.fieldName}`
       } else {
-        return `| ${f.fieldName}(${typeToString(f.fieldType)})`
+        return `${f.fieldName}(${typeToString(f.fieldType)})`
       }
     })
-    .join('\n')
+    .join(' | ')
 }
 
 /**

quint/src/flattening.ts

@@ -22,6 +22,7 @@ import {
   QuintExport,
   QuintImport,
   QuintInstance,
+  QuintLambda,
   QuintModule,
   QuintOpDef,
   isAnnotatedDef,
@@ -343,23 +344,46 @@ class Flatenner {
         }
       }
       case 'lambda':
+        return this.addNamespaceToLambda(id, name, expr)
+      case 'let':
         return {
           ...expr,
-          params: expr.params.map(param => ({
-            name: this.namespacedName(name, param.name),
-            id: this.getNewIdWithSameData(param.id),
-          })),
+          opdef: this.addNamespaceToOpDef(name, expr.opdef),
           expr: this.addNamespaceToExpr(name, expr.expr),
           id,
         }
 
-      case 'let':
+      case 'match':
         return {
           ...expr,
-          opdef: this.addNamespaceToOpDef(name, expr.opdef),
           expr: this.addNamespaceToExpr(name, expr.expr),
+          cases: expr.cases.map(({ label, elim }) => ({
+            label: this.namespacedName(name, label),
+            elim: this.addNamespaceToLambda(this.getNewIdWithSameData(elim.id), name, elim),
+          })),
           id,
         }
+
+      case 'variant':
+        return {
+          ...expr,
+          label: this.namespacedName(name, expr.label),
+          expr: expr.expr ? this.addNamespaceToExpr(name, expr.expr) : expr.expr,
+        }
+    }
+  }
+
+  // Gives us a more narrowly typed transformation on lambdas, so we can use the same functionality for
+  // match exprssions.
+  private addNamespaceToLambda(id: bigint, name: string | undefined, lam: QuintLambda): QuintLambda {
+    return {
+      ...lam,
+      params: lam.params.map(param => ({
+        name: this.namespacedName(name, param.name),
+        id: this.getNewIdWithSameData(param.id),
+      })),
+      expr: this.addNamespaceToExpr(name, lam.expr),
+      id,
     }
   }
 

quint/src/generated/Quint.g4

@@ -157,6 +157,7 @@ expr:           // apply a built-in operator via the dot notation
         |       expr OR expr                                        # or
         |       expr IFF expr                                       # iff
         |       expr IMPLIES expr                                   # implies
+        |       matchSumExpr                                        # matchSum
         |       expr MATCH
                     ('|' STRING ':' parameter '=>' expr)+           # match
         |       'all' '{' expr (',' expr)* ','? '}'                 # actionAll
@@ -176,6 +177,12 @@ expr:           // apply a built-in operator via the dot notation
         |       '{' expr '}'                                        # braces
         ;
 
+// match e { A(a) => e1 | B => e2 | C(_)}
+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