Add parsing of sum type declarations (#1088)

* Add syntax for sum type declarations

* Add parser generator updates

* Adapt flattening and graphics for sum types

* Add unit test for sum type declaration parsing

* Update the super spec

Not sure why this updating. Tests succeed whether this file is updated
or not. But, well, it's up to date now :)

* Add test for IRPrinting

quint/src/IRprinting.ts

@@ -13,7 +13,7 @@
  */
 
 import { OpQualifier, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr'
-import { EmptyRow, QuintType, Row, VarRow } from './quintTypes'
+import { EmptyRow, QuintSumType, QuintType, Row, RowField, VarRow, isTheUnit } from './quintTypes'
 import { TypeScheme } from './types/base'
 import { typeSchemeToString } from './types/printing'
 
@@ -160,6 +160,9 @@ export function typeToString(type: QuintType): string {
     case 'rec': {
       return rowToString(type.fields)
     }
+    case 'sum': {
+      return sumToString(type)
+    }
     case 'union': {
       const records = type.records.map(rec => {
         return `| { ${type.tag}: "${rec.tagValue}", ${rowFieldsToString(rec.fields)} }`
@@ -181,6 +184,25 @@ export function rowToString(r: Row): string {
   return fields === '' ? '{}' : `{ ${fields} }`
 }
 
+/**
+ * Pretty prints a sum type. Standard sum printing used in error reporting
+ *
+ * @param r the sum type to be formatted
+ *
+ * @returns a string with the pretty printed sum
+ */
+export function sumToString(s: QuintSumType): string {
+  return s.fields.fields
+    .map((f: RowField) => {
+      if (isTheUnit(f.fieldType)) {
+        return `| ${f.fieldName}`
+      } else {
+        return `| ${f.fieldName}(${typeToString(f.fieldType)})`
+      }
+    })
+    .join('\n')
+}
+
 /**
  * Pretty prints an operator qualifier.
  *

quint/src/flattening.ts

@@ -28,7 +28,7 @@ import {
   isFlat,
 } from './quintIr'
 import { definitionToString } from './IRprinting'
-import { QuintType, Row } from './quintTypes'
+import { ConcreteFixedRow, QuintType, Row } from './quintTypes'
 import { Loc, parsePhase3importAndNameResolution } from './parsing/quintParserFrontend'
 import { compact, uniqBy } from 'lodash'
 import { AnalysisOutput } from './quintAnalyzer'
@@ -398,6 +398,12 @@ class Flatenner {
           fields: this.addNamespaceToRow(name, type.fields),
           id,
         }
+      case 'sum':
+        return {
+          ...type,
+          fields: this.addNamespaceToSumRow(name, type.fields),
+          id,
+        }
       case 'union':
         return {
           ...type,
@@ -428,6 +434,18 @@ class Flatenner {
     }
   }
 
+  private addNamespaceToSumRow(name: string | undefined, row: ConcreteFixedRow): ConcreteFixedRow {
+    return {
+      ...row,
+      fields: row.fields.map(field => {
+        return {
+          ...field,
+          fieldType: this.addNamespaceToType(name, field.fieldType),
+        }
+      }),
+    }
+  }
+
   private namespacedName(namespace: string | undefined, name: string): string {
     return namespace ? `${namespace}::${name}` : name
   }

quint/src/generated/Quint.g4

@@ -52,10 +52,16 @@ operDef : qualifier normalCallName
         ;
 
 typeDef
-    : 'type' qualId          # typeAbstractDef
-    | 'type' qualId '=' type # typeAliasDef
+    : 'type' qualId                                                         # typeAbstractDef
+    | 'type' qualId '=' type                                                # typeAliasDef
+    | 'type' typeName=qualId '=' '|'? typeSumVariant ('|' typeSumVariant)*  # typeSumDef
     ;
 
+// A single variant case in a sum type definition.
+//
+// E.g., `A(t)` or `A`.
+typeSumVariant : sumLabel=simpleId["variant label"] ('(' type ')')? ;
+
 nondetOperDef : 'nondet' qualId (':' type)? '=' expr ';'?;
 
 qualifier : 'val'