Replace unsupported union match with sum match

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(_)}
+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

quint/src/graphics.ts

@@ -187,7 +187,7 @@ export function prettyQuintType(type: QuintType): Doc {
       return group([text('{ '), prettyRow(type.fields), text('}')])
     }
     case 'sum': {
-      return group([text('{ '), prettySumRow(type.fields), text('}')])
+      return prettySumRow(type.fields)
     }
     case 'union': {
       const records = type.records.map(rec => {

quint/src/ir/IRprinting.ts

@@ -13,7 +13,7 @@
  */
 
 import { OpQualifier, QuintDeclaration, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr'
-import { QuintSumType, QuintType, Row, RowField, isTheUnit } from './quintTypes'
+import { QuintSumType, QuintType, Row, RowField, isUnitType } from './quintTypes'
 import { TypeScheme } from '../types/base'
 import { typeSchemeToString } from '../types/printing'
 
@@ -218,7 +218,7 @@ export function rowToString(r: Row): string {
 export function sumToString(s: QuintSumType): string {
   return s.fields.fields
     .map((f: RowField) => {
-      if (isTheUnit(f.fieldType)) {
+      if (isUnitType(f.fieldType)) {
         return `| ${f.fieldName}`
       } else {
         return `| ${f.fieldName}(${typeToString(f.fieldType)})`

quint/src/ir/quintIr.ts

@@ -131,7 +131,7 @@ export function isQuintBuiltin(app: QuintApp): app is QuintBuiltinApp {
 }
 
 // This should be the source of truth for all builtin opcodes
-const builtinOpCodes = [
+export const builtinOpCodes = [
   'List',
   'Map',
   'Rec',
@@ -187,6 +187,7 @@ const builtinOpCodes = [
   'length',
   'map',
   'mapBy',
+  'match',
   'mustChange',
   'neq',
   'next',
@@ -217,6 +218,7 @@ const builtinOpCodes = [
   'tuples',
   'union',
   'unionMatch',
+  'variant',
   'weakFair',
   'with',
 ] as const

quint/src/ir/quintTypes.ts

@@ -75,15 +75,15 @@ export interface QuintRecordType extends WithOptionalId {
 }
 
 // A value of the unit type, i.e. an empty record
-export function unitValue(id: bigint): QuintRecordType {
+export function unitType(id: bigint): QuintRecordType {
   return {
     id,
     kind: 'rec',
     fields: { kind: 'row', fields: [], other: { kind: 'empty' } },
   }
 }
 
-export function isTheUnit(r: QuintType): Boolean {
+export function isUnitType(r: QuintType): Boolean {
   return r.kind === 'rec' && r.fields.kind === 'row' && r.fields.fields.length === 0 && r.fields.other.kind === 'empty'
 }
 

quint/src/names/base.ts

@@ -12,7 +12,7 @@
  * @module
  */
 
-import { QuintDef, QuintExport, QuintImport, QuintInstance, QuintLambdaParameter } from '../ir/quintIr'
+import { QuintDef, QuintExport, QuintImport, QuintInstance, QuintLambdaParameter, builtinOpCodes } from '../ir/quintIr'
 import { QuintType } from '../ir/quintTypes'
 
 /**
@@ -232,4 +232,6 @@ export const builtinNames = [
   'ite',
   'cross',
   'difference',
+  'match',
+  'variant',
 ]

quint/src/parsing/ToIrListener.ts

@@ -5,22 +5,26 @@ import { QuintListener } from '../generated/QuintListener'
 import {
   OpQualifier,
   QuintApp,
+  QuintBuiltinApp,
   QuintDeclaration,
   QuintDef,
   QuintEx,
+  QuintLambda,
   QuintLambdaParameter,
   QuintLet,
   QuintModule,
   QuintName,
   QuintOpDef,
+  QuintStr,
 } from '../ir/quintIr'
-import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, unitValue } from '../ir/quintTypes'
+import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, isUnitType, unitType } from '../ir/quintTypes'
 import { strict as assert } from 'assert'
 import { ErrorMessage, Loc } from './quintParserFrontend'
 import { compact, zipWith } from 'lodash'
 import { Maybe, just, none } from '@sweet-monads/maybe'
 import { TerminalNode } from 'antlr4ts/tree/TerminalNode'
 import { QuintTypeDef } from '../ir/quintIr'
+import { zip } from '../../test/util'
 
 /**
  * An ANTLR4 listener that constructs QuintIr objects out of the abstract
@@ -373,44 +377,69 @@ export class ToIrListener implements QuintListener {
   // type T = | A | B(t1) | C(t2)
   exitTypeSumDef(ctx: p.TypeSumDefContext) {
     const name = ctx._typeName!.text!
-    const defId = this.idGen.nextId()
-    this.sourceMap.set(defId, this.loc(ctx))
-
-    const typeId = this.idGen.nextId()
-    this.sourceMap.set(typeId, this.loc(ctx))
+    const id = this.getId(ctx)
 
+    // Build the type declaraion
     const fields: RowField[] = popMany(this.variantStack, this.variantStack.length)
     const row: ConcreteFixedRow = { kind: 'row', fields, other: { kind: 'empty' } }
-    const type: QuintSumType = { id: defId, kind: 'sum', fields: row }
-
+    const type: QuintSumType = { id, kind: 'sum', fields: row }
     const def: QuintTypeDef = {
-      id: defId,
+      id: id,
       name,
       kind: 'typedef',
       type,
     }
 
-    this.declarationStack.push(def)
+    // Generate all the variant constructors
+    // a variant constructor is an operator that injects an exprssion
+    // into the sum type by wrapping it in a label
+    const constructors: QuintOpDef[] = zip(fields, ctx.typeSumVariant()).map(
+      ([{ fieldName, fieldType }, variantCtx]) => {
+        // Mangle the parameter name to avoid clashes
+        // This shouldn't be visible to users
+        const paramName = `__${fieldName}Param`
+
+        let params: QuintLambdaParameter[]
+        let expr: QuintEx
+        let qualifier: OpQualifier
+
+        if (isUnitType(fieldType)) {
+          // The nullary variant constructor is actual
+          // variant pairint a label with the unit.
+          params = []
+          expr = unitValue(this.getId(variantCtx._sumLabel))
+          // Its a `val` cause it takes no arguments
+          qualifier = 'val'
+        } else {
+          // Oherwise we will build constructor that takes one parameter
+          // and wraps it in a `variaint`
+          params = [{ id: this.getId(variantCtx.type()!), name: paramName }]
+          expr = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) }
+          qualifier = 'def'
+        }
+        const label: QuintStr = { id: this.getId(variantCtx), kind: 'str', value: fieldName }
+        const variant: QuintBuiltinApp = {
+          id: this.getId(variantCtx),
+          kind: 'app',
+          opcode: 'variant',
+          args: [label, expr],
+        }
+        const lam: QuintLambda = { id: this.getId(variantCtx), kind: 'lambda', params, qualifier, expr: variant }
+        return { id: this.getId(variantCtx), kind: 'def', name: fieldName, qualifier, expr: lam }
+      }
+    )
+
+    this.declarationStack.push(def, ...constructors)
   }
 
   exitTypeSumVariant(ctx: p.TypeSumVariantContext) {
     const fieldName = ctx._sumLabel!.text!
     const poppedType = this.popType().value
-
-    let fieldType: QuintType
-
     // Check if we have an accompanying type, and if not, then synthesize the
     // unit type.
-    //
-    // I.e., we interpert a variant `A` as `A({})`.
-    if (poppedType === undefined) {
-      const id = this.idGen.nextId()
-      this.sourceMap.set(id, this.loc(ctx))
-      fieldType = unitValue(id)
-    } else {
-      fieldType = poppedType
-    }
-
+    //   const poppedType = this.popType().value
+    // I.e., we interpret a variant `A` as `A({})`.
+    const fieldType: QuintType = poppedType ? poppedType : unitType(this.getId(ctx))
     this.variantStack.push({ fieldName, fieldType })
   }
 
@@ -887,45 +916,68 @@ export class ToIrListener implements QuintListener {
   }
 
   // if (p) e1 else e2
-  exitIfElse(ctx: any) {
+  exitIfElse(ctx: p.IfElseContext) {
     const args = popMany(this.exprStack, 3)
     this.pushApplication(ctx, 'ite', args)
   }
 
-  // entry match
-  //   | "Cat": cat => cat.name != ""
-  //   | "Dog": dog => dog.year > 0
-  exitMatch(ctx: p.MatchContext) {
-    const options = ctx.STRING().map(opt => opt.text.slice(1, -1))
-    const noptions = options.length
-    // expressions in the right-hand sides, e.g., dog.year > 0
-    const rhsExprs = popMany(this.exprStack, noptions)
-    // parameters in the right-hand side
-    const params = popMany(this.paramStack, noptions)
-    // matched expressionm e.g., entry
-    const exprToMatch = popMany(this.exprStack, 1)![0]
-    const matchArgs: QuintEx[] = [exprToMatch]
-    // push the tag value and the corresponding lambda in matchArgs
-    for (let i = 0; i < noptions; i++) {
-      const tagId = this.getId(ctx)
-      const tag: QuintEx = {
-        id: tagId,
-        kind: 'str',
-        value: options[i],
-      }
-      const lamId = this.getId(ctx)
-      const lam: QuintEx = {
-        id: lamId,
-        kind: 'lambda',
-        params: [params[i]],
-        qualifier: 'def',
-        expr: rhsExprs[i],
+  // match expr {
+  //    | Variant1(var1) => expr1
+  //    | Variantk(_) => exprk    // a hole in the payload
+  //    | ...
+  //    | Variantn(varn) => exprn
+  //    | _ => exprm              // A wildcard match, acting as a catchall
+  // }
+  //
+  // The above is represented in the UFC using an exotic `match` operator of the form
+  //
+  // match(epxr, label1, (var1) => expr1, ..., labeln, (varn) => exprn, "_", (_) => exprm)
+  exitMatchSumExpr(ctx: p.MatchSumExprContext) {
+    const matchId = this.getId(ctx)
+    // We will have one expression for each match case, plus the
+    const exprs = popMany(this.exprStack, ctx._matchCase.length + 1)
+    // The first expression is the one we are matching on
+    // the syntax rules ensure that at least this expression is given
+    const expr = exprs.shift()!
+    const gatherCase: (
+      acc: (QuintStr | QuintLambda)[],
+      matchCase: [QuintEx, p.MatchSumCaseContext]
+    ) => (QuintStr | QuintLambda)[] = (acc, [caseExpr, caseCtx]) => {
+      const caseId = this.getId(caseCtx)
+      let label: string
+      let params: QuintLambdaParameter[]
+      if (caseCtx._wildCardMatch) {
+        // a wildcard case: _ => expr
+        label = '_'
+        params = []
+      } else if (caseCtx._variantMatch) {
+        const variant = caseCtx._variantMatch
+        let name: string
+        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) }]
+      } else {
+        throw new Error('impossible: either _wildCardMatch or _variantMatch must be present')
       }
-      matchArgs.push(tag)
-      matchArgs.push(lam)
+      const labelStr: QuintStr = { id: caseId, kind: 'str', value: label }
+      const elim: QuintLambda = { id: caseId, kind: 'lambda', qualifier: 'def', expr: caseExpr, params }
+      return acc.concat([labelStr, elim])
+    }
+
+    // after  shifting off the match expr, the remaing exprs are in each case
+    const cases: (QuintStr | QuintLambda)[] = zip(exprs, ctx._matchCase).reduce(gatherCase, [])
+    const matchExpr: QuintBuiltinApp = {
+      id: matchId,
+      kind: 'app',
+      opcode: 'match',
+      args: [expr].concat(cases),
     }
-    // construct the match expression and push it in exprStack
-    this.pushApplication(ctx, 'unionMatch', matchArgs)
+    this.exprStack.push(matchExpr)
   }
 
   /** ******************* translate types ********************************/
@@ -1238,3 +1290,13 @@ function popMany<T>(stack: T[], n: number): T[] {
 function getDocText(doc: TerminalNode[]): string {
   return doc.map(l => l.text.slice(4, -1)).join('\n')
 }
+
+// Helper to construct an empty record (the unit value)
+function unitValue(id: bigint): QuintBuiltinApp {
+  return {
+    id,
+    kind: 'app',
+    opcode: 'Rec',
+    args: [],
+  }
+}

quint/src/runtime/impl/compilerImpl.ts

@@ -919,6 +919,8 @@ export class CompilerVisitor implements IRVisitor {
 
         // builtin operators that are not handled by REPL
         case 'unionMatch':
+        case 'variant': // TODO: https://github.com/informalsystems/quint/issues/1033
+        case 'match': // TODO: https://github.com/informalsystems/quint/issues/1033
         case 'orKeep':
         case 'mustChange':
         case 'weakFair':

quint/test/ir/IRprinting.test.ts

@@ -9,7 +9,7 @@ import {
   typeToString,
 } from '../../src/ir/IRprinting'
 import { toScheme } from '../../src/types/base'
-import { QuintSumType, unitValue } from '../../src'
+import { QuintSumType, unitType } from '../../src'
 
 describe('moduleToString', () => {
   const quintModule = buildModuleWithDecls(['var S: Set[int]', 'val f = S.filter(x => x + 1)'])
@@ -241,7 +241,7 @@ describe('typeToString', () => {
         kind: 'row',
         fields: [
           { fieldName: 'A', fieldType: { kind: 'int', id: 0n } },
-          { fieldName: 'B', fieldType: unitValue(0n) },
+          { fieldName: 'B', fieldType: unitType(0n) },
         ],
         other: { kind: 'empty' },
       },