Add support for the variant operator in the type and effect system

doc/lang.md

@@ -1295,131 +1295,6 @@ with discriminated unions.
 
 *Mode:* Stateless, State. Other modes are not allowed.
 
-### Discriminated unions (work-in-progress)
-
-**WARNING:** *We are redesigning discriminated unions*, see
-[#539](https://github.com/informalsystems/quint/issues/539). *As they are not
-fully implemented, please avoid using discriminated unions for now*.
-
-Quint has provides the user with special syntax for constructing and destructing
-discriminated unions.  For the type syntax of discriminated unions, see
-[Types](#types).
-
-**Constructors.** Construct a tagged record by using the record syntax, e.g.:
-
-```scala
-  { tag: "Cat", name: "Ours", year: 2019 }
-```
-
-Note that the above record has the field `tag`. Hence, this record is assigned
-a union type of one element:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-Records of different union types may be mixed in a single set. For example:
-
-```scala
-val Entries =
-  Set(
-    { tag: "Cat", name: "Ours", year: 2019  },
-    { tag: "Cat", name: "Murka", year: 1950 },
-    { tag: "Date", day: 16, month: 11, year: 2021 }
-  )
-```
-
-In the above example, the set elements have the following union type:
-
-```scala
-type ENTRY_TYPE =
-  | { tag: "Cat", name: str, year: int }
-  | { tag: "Date", day: int, month: int, year: int }
-```
-
-When we construct the individual records, they still have singleton union
-types.  For instance, the entry  `{ tag: "Date", day: 16, month: 11, year: 2021
-}` has the type:
-
-```scala
-type DATE_TYPE =
-  { tag: "Date", day: int, month: int, year: int }
-```
-
-**Set filters.** The most common pattern over discriminated union is to filter
-set elements by their tag. Using the above definition of `Entries`, we can
-filter it as follows:
-
-```scala
-Entries.filter(e => e.tag == "Cat")
-```
-
-As expected from the semantics of `filter`, the above set is equal to:
-
-```
-Set(
-  { tag: "Cat", name: "Ours", year: 2019  },
-  { tag: "Cat", name: "Murka", year: 1950 }
-)
-```
-
-Importantly, its elements have the type:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-**Destructors.** Sometimes, we have a value of a union type that is not stored
-in a set. For this case, Quint has the union destructor syntax.  For example,
-given an entry from `Entries`, we can compute the predicate `isValid` by case
-distinction over tags:
-
-```scala
-pure def isValid(entry): ENTRY_TYPE => bool =
-  entry match
-     | "Cat": cat =>
-       name != "" and cat.year > 0
-     | "Date": date =>
-       date.day.in(1 to 31) and date.month.in(1.to(12)) and date.year > 0
-```
-
-In the above example, the names `cat` and `date` have the singleton union types
-of `CAT_TYPE` and `DATE_TYPE`, respectively. Note that the expressions after
-the tag name (e.g., `"Cat":` and `"Date":`) follow the syntax of
-single-argument lambda expressions. As a result, we can use `_` as a name,
-which means that the name is omitted.
-
-Match expressions require all possible values of `tag` to be enumerated. This is
-ensured by the type checker.
-
-We do not introduce parentheses in the syntax of `match`. If you feel uncomfortable
-about it, wrap the whole match-expression with `(...)`.
-
-*Grammar*:
-
-```bnf
-  expr "match" ("|" string ":" (identifier | "_") "=>" expr)+
-```
-
-*Normal form*: Consider the match operator:
-
-```scala
-  ex match
-    | tag_1: x_1 => ex_1
-    ...
-    | tag_n: x_n => ex_n
-```
-
-Its normal form is `unionMatch(ex, tag_1, (x_1 => ex_1), ..., (x_n => ex_n))`.
-
-*Mode:* Stateless, State. Other modes are not allowed.
-
-**Discussion.** In TLA+, there is no separation between discriminated unions
-and records. It is common to use tagged records to distinguish between different
-cases of records. Quint makes this pattern explicit.
-
 ### Tuples
 
 In contrast to TLA+, Quint tuples have length of at least 2.

quint/src/builtin.qnt

@@ -1024,26 +1024,4 @@ module builtin {
   // /// run test = (x' = 0).then(any { x' = 1, x' = 2 }).then(assert(or { x == 1, x == 2 }))
   // /// ```
   // pure def actionAny(a*): (bool*) => bool
-
-  // /// `unionMatch(m, (t0, e0), ..., (tn, en))` is the expression `ei` when `ti` is the tag of `m`.
-  // ///
-  // /// The behavior of this operator is undefined if the tag isn't one of the `ti`s.
-  // ///
-  // /// This is the pattern matching operator.
-  // ///
-  // /// Can also be written as `m match | t0: e0, ..., | tn: en }`.
-  // ///
-  // /// ### Examples
-  // ///
-  // /// ```
-  // /// pure val total(w) = w match
-  // ///   // this pattern binds some_w to the "some" version of w, if w.tag == "some"
-  // ///   | "some": some_w => some_w.value
-  // ///   // this pattern
-  // ///   | "none": _ => 0
-  // ///
-  // /// assert(total({ tag = "some", value = 1 }) == 1)
-  // /// assert(total({ tag = "none" }) == 0)
-  // /// ```
-  // pure def unionMatch(m, (t, e)*): (a, (b, ((b) => c))*) => c
 }

quint/src/effects/builtinSignatures.ts

@@ -226,6 +226,10 @@ const otherOperators = [
     name: 'ite',
     effect: parseAndQuantify('(Read[r1], Read[r2] & Update[u], Read[r3] & Update[u]) => Read[r1, r2, r3] & Update[u]'),
   },
+  {
+    name: 'variant',
+    effect: parseAndQuantify('(Pure, Read[r] & Update[u]) => Read[r] & Update[u]'),
+  },
 ]
 
 const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
@@ -238,7 +242,7 @@ const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
   ['and', standardPropagation],
   ['or', standardPropagation],
   [
-    'unionMatch',
+    'match',
     (arity: number) => {
       const readVars = times((arity - 1) / 2, i => `r${i}`)
       const args = readVars.map(r => `Pure, (Pure) => Read[${r}]`)

quint/src/graphics.ts

@@ -29,7 +29,7 @@ import {
 import { QuintDeclaration, QuintEx, isAnnotatedDef } from './ir/quintIr'
 import { ExecutionFrame } from './runtime/trace'
 import { zerog } from './idGenerator'
-import { ConcreteFixedRow, QuintType, Row } from './ir/quintTypes'
+import { ConcreteRow, QuintType, Row, isUnitType } from './ir/quintTypes'
 import { TypeScheme } from './types/base'
 import { canonicalTypeScheme } from './types/printing'
 import { declarationToString, qualifierToString, rowToString } from './ir/IRprinting'
@@ -220,20 +220,23 @@ function prettyRow(r: Row, showFieldName = true): Doc {
   return group([nest('  ', [linebreak, docJoin([text(','), line()], fieldsDocs)]), ...otherDoc, linebreak])
 }
 
-function prettySumRow(r: ConcreteFixedRow): Doc {
+function prettySumRow(r: ConcreteRow): Doc {
   const row = simplifyRow(r)
   const fields = row.kind === 'row' ? row.fields : []
   const other = row.kind === 'row' ? row.other : undefined
 
   const fieldsDocs = fields.map(f => {
     if (other?.kind === 'empty') {
       return group(text(f.fieldName))
+    } else if (isUnitType(f.fieldType)) {
+      // Print the variant `Foo({})`
+      return group([text(`${f.fieldName}`)])
     } else {
       return group([text(`${f.fieldName}(`), prettyQuintType(f.fieldType), text(')')])
     }
   })
 
-  return group([nest('  ', [linebreak, docJoin([text(','), line()], fieldsDocs)]), linebreak])
+  return group([nest('  ', [linebreak, docJoin([text('|'), line()], fieldsDocs)]), linebreak])
 }
 
 /**

quint/src/ir/IRprinting.ts

@@ -216,15 +216,19 @@ export function rowToString(r: Row): string {
  * @returns a string with the pretty printed sum
  */
 export function sumToString(s: QuintSumType): string {
-  return s.fields.fields
-    .map((f: RowField) => {
-      if (isUnitType(f.fieldType)) {
-        return `| ${f.fieldName}`
-      } else {
-        return `| ${f.fieldName}(${typeToString(f.fieldType)})`
-      }
-    })
-    .join('\n')
+  return (
+    '(' +
+    s.fields.fields
+      .map((f: RowField) => {
+        if (isUnitType(f.fieldType)) {
+          return `${f.fieldName}`
+        } else {
+          return `${f.fieldName}(${typeToString(f.fieldType)})`
+        }
+      })
+      .join(' | ') +
+    ')'
+  )
 }
 
 /**

quint/src/ir/quintIr.ts

@@ -209,7 +209,6 @@ export const builtinOpCodes = [
   'to',
   'tuples',
   'union',
-  'unionMatch',
   'variant',
   'weakFair',
   'with',

quint/src/ir/quintTypes.ts

@@ -89,7 +89,13 @@ export function isUnitType(r: QuintType): Boolean {
 
 export interface QuintSumType extends WithOptionalId {
   kind: 'sum'
-  fields: ConcreteFixedRow
+  fields: ConcreteRow
+}
+
+export function sumType(labelTypePairs: [string, QuintType][], rowVar?: string, id?: bigint): QuintSumType {
+  const fields = labelTypePairs.map(([fieldName, fieldType]) => ({ fieldName, fieldType }))
+  const other: Row = rowVar ? { kind: 'var', name: rowVar } : { kind: 'empty' }
+  return { kind: 'sum', fields: { kind: 'row', fields, other }, id }
 }
 
 export interface QuintUnionType extends WithOptionalId {

quint/src/names/base.ts

@@ -226,7 +226,6 @@ export const builtinNames = [
   'field',
   'fieldNames',
   'item',
-  'unionMatch',
   'assign',
   'of',
   'eq',

quint/src/parsing/ToIrListener.ts

@@ -17,7 +17,16 @@ import {
   QuintOpDef,
   QuintStr,
 } from '../ir/quintIr'
-import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, isUnitType, unitType } from '../ir/quintTypes'
+import {
+  ConcreteFixedRow,
+  QuintConstType,
+  QuintSumType,
+  QuintType,
+  Row,
+  RowField,
+  isUnitType,
+  unitType,
+} from '../ir/quintTypes'
 import { strict as assert } from 'assert'
 import { SourceMap } from './quintParserFrontend'
 import { compact, zipWith } from 'lodash'
@@ -382,6 +391,7 @@ export class ToIrListener implements QuintListener {
     const fields: RowField[] = popMany(this.variantStack, this.variantStack.length)
     const row: ConcreteFixedRow = { kind: 'row', fields, other: { kind: 'empty' } }
     const type: QuintSumType = { id, kind: 'sum', fields: row }
+    const typeName: QuintConstType = { id, kind: 'const', name }
     const def: QuintTypeDef = {
       id: id,
       name,
@@ -418,32 +428,56 @@ export class ToIrListener implements QuintListener {
         // This shouldn't be visible to users
         const paramName = `__${fieldName}Param`
 
-        let params: QuintLambdaParameter[]
-        let expr: QuintEx
         let qualifier: OpQualifier
+        let expr: QuintEx
+        let typeAnnotation: QuintType
 
+        const label: QuintStr = { id: this.getId(variantCtx), kind: 'str', value: fieldName }
         if (isUnitType(fieldType)) {
+          // Its a `val` cause it has no parameters
+          //
+          // E.g., for B we will produce
+          //
+          // ```
+          // val B: T = variant("B", {})
+          // ```
+          qualifier = 'val'
+
           // The nullary variant constructor is actualy
           // a variant pairing a label with the unit.
-          params = []
-          expr = unitValue(this.getId(variantCtx._sumLabel))
-          // Its a `val` cause it takes no arguments
-          qualifier = 'val'
+          const wrappedExpr = unitValue(this.getId(variantCtx._sumLabel))
+
+          typeAnnotation = typeName
+          expr = {
+            id: this.getId(variantCtx),
+            kind: 'app',
+            opcode: 'variant',
+            args: [label, wrappedExpr],
+          }
         } else {
           // Otherwise we will build a constructor that takes one parameter
-          params = [{ id: this.getId(variantCtx.type()!), name: paramName }]
-          expr = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) }
+          //
+          // E.g., for A(int) we will produce a
+          //
+          // ```
+          // def A(x:int): T = variant("A", x)
+          // ```
           qualifier = 'def'
+
+          const params = [{ id: this.getId(variantCtx.type()!), name: paramName }]
+          const wrappedExpr: QuintName = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) }
+          const variant: QuintBuiltinApp = {
+            id: this.getId(variantCtx),
+            kind: 'app',
+            opcode: 'variant',
+            args: [label, wrappedExpr],
+          }
+
+          typeAnnotation = { kind: 'oper', args: [fieldType], res: typeName }
+          expr = { id: this.getId(variantCtx), kind: 'lambda', params, qualifier, expr: variant }
         }
-        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 }
+
+        return { id: this.getId(variantCtx), kind: 'def', name: fieldName, qualifier, typeAnnotation, expr }
       }
     )
 

quint/src/runtime/impl/compilerImpl.ts

@@ -930,7 +930,6 @@ export class CompilerVisitor implements IRVisitor {
           break
 
         // 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':