updated files to support new tuple representation

quint/src/effects/builtinSignatures.ts

@@ -15,7 +15,6 @@
 import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature, effectNames, toScheme } from './base'
 import { parseEffectOrThrow } from './parser'
 import { range, times } from 'lodash'
-import { QuintBuiltinOpcode } from '../ir/quintIr'
 
 export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))
@@ -248,12 +247,12 @@ const otherOperators = [
   },
 ]
 
-const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [
+const multipleAritySignatures: [string, Signature][] = [
   ['List', standardPropagation],
   ['Set', standardPropagation],
   ['Map', standardPropagation],
   ['Rec', standardPropagation],
-  ['Tup', standardPropagation],
+  ['tuple', standardPropagation],
   ['tuples', standardPropagation],
   ['and', standardPropagation],
   ['or', standardPropagation],

quint/src/effects/inferrer.ts

@@ -29,6 +29,7 @@ import {
   QuintName,
   QuintOpDef,
   QuintStr,
+  QuintTup,
   QuintVar,
 } from '../ir/quintIr'
 import { Effect, EffectScheme, Signature, effectNames, entityNames, toScheme, unify } from './base'
@@ -139,72 +140,16 @@ export class EffectInferrer implements IRVisitor {
     this.addToResults(expr.id, this.effectForName(expr.name, expr.id, 2).map(toScheme))
   }
 
+  exitTuple(expr: QuintTup): void {
+    this.inferEffect(expr, expr.elements, expr.kind, expr.id, expr.elements.length)
+  }
+
   // { identifier: op, effect: E } ∈ Γ    Γ ⊢ p0:E0 ... Γ ⊢ pn:EN
   // Eres <- freshVar   S = unify(newInstance(E), (E0, ...,  EN) => Eres)
   // ------------------------------------------------------------------- (APP)
   //           Γ ⊢ op(p0, ..., pn): S(Eres)
   exitApp(expr: QuintApp): void {
-    if (this.errors.size > 0) {
-      // Don't try to infer application if there are errors with the args
-      return
-    }
-
-    this.location = `Trying to infer effect for operator application in ${expressionToString(expr)}`
-    const paramsResult = mergeInMany(
-      expr.args.map((a: QuintEx) => {
-        return this.fetchResult(a.id).map(e => this.newInstance(e))
-      })
-    )
-
-    const resultEffect: Effect = { kind: 'variable', name: this.freshVarGenerator.freshVar('_e') }
-    const arrowEffect = paramsResult
-      .map(params => {
-        const effect: Effect = {
-          kind: 'arrow',
-          params,
-          result: resultEffect,
-        }
-
-        return effect
-      })
-      .chain(e => applySubstitution(this.substitutions, e))
-
-    this.effectForName(expr.opcode, expr.id, expr.args.length)
-      .mapLeft(err => buildErrorTree(this.location, err))
-      .chain(signature => {
-        const substitution = arrowEffect.chain(effect =>
-          applySubstitution(this.substitutions, signature).chain(s => unify(s, effect))
-        )
-
-        const resultEffectWithSubs = substitution
-          .chain(s => compose(this.substitutions, s))
-          .chain(s => {
-            this.substitutions = s
-
-            paramsResult.map(effects =>
-              zip(
-                effects,
-                expr.args.map(a => a.id)
-              ).forEach(([effect, id]) => {
-                const r = applySubstitution(s, effect).map(toScheme)
-                this.addToResults(id, r)
-              })
-            )
-            // For every free name we are binding in the substitutions, the names occuring in the value of the
-            // substitution have to become free as well.
-            this.addBindingsToFreeNames(s)
-
-            return applySubstitution(s, resultEffect)
-          })
-
-        return resultEffectWithSubs
-      })
-      .map(effect => {
-        this.addToResults(expr.id, right(toScheme(effect)))
-      })
-      .mapLeft(err => {
-        this.addToResults(expr.id, left(err))
-      })
+    this.inferEffect(expr, expr.args, expr.opcode, expr.id, expr.args.length)
   }
 
   // Literals are always Pure
@@ -436,4 +381,66 @@ export class EffectInferrer implements IRVisitor {
       }
     })
   }
+
+  private inferEffect(expr: QuintEx, args: QuintEx[], name: string, id: bigint, arity: number): void {
+    if (this.errors.size > 0) {
+      return // Early exit if errors are present
+    }
+
+    this.location = `Trying to infer effect for operator application in ${expressionToString(expr)}`
+
+    const paramsResult = mergeInMany(args.map((a: QuintEx) => this.fetchResult(a.id).map(e => this.newInstance(e))))
+
+    const resultEffect: Effect = { kind: 'variable', name: this.freshVarGenerator.freshVar('_e') }
+    const arrowEffect = paramsResult
+      // paramsResult is an array.
+      // It iterates over each element in paramsResult, where each element is passed into the params parameter.
+      .map(params => {
+        const effect: Effect = {
+          kind: 'arrow',
+          params,
+          result: resultEffect,
+        }
+
+        return effect
+      })
+      .chain(e => applySubstitution(this.substitutions, e))
+
+    this.effectForName(name, id, arity)
+      .mapLeft(err => buildErrorTree(this.location, err))
+      .chain(signature => {
+        const substitution = arrowEffect.chain(effect =>
+          applySubstitution(this.substitutions, signature).chain(s => unify(s, effect))
+        )
+
+        const resultEffectWithSubs = substitution
+          .chain(s => compose(this.substitutions, s))
+          .chain(s => {
+            this.substitutions = s
+
+            paramsResult.map(effects =>
+              zip(
+                effects,
+                args.map(a => a.id)
+              ).forEach(([effect, id]) => {
+                const r = applySubstitution(s, effect).map(toScheme)
+                this.addToResults(id, r)
+              })
+            )
+            // For every free name we are binding in the substitutions, the names occuring in the value of the
+            // substitution have to become free as well.
+            this.addBindingsToFreeNames(s)
+
+            return applySubstitution(s, resultEffect)
+          })
+
+        return resultEffectWithSubs
+      })
+      .map(effect => {
+        this.addToResults(expr.id, right(toScheme(effect)))
+      })
+      .mapLeft(err => {
+        this.addToResults(expr.id, left(err))
+      })
+  }
 }

quint/src/graphics.ts

@@ -65,15 +65,18 @@ export function prettyQuintEx(ex: QuintEx): Doc {
     case 'str':
       return richtext(chalk.green, `"${ex.value}"`)
 
+    case 'tuple':
+      return nary(text('('), ex.elements.map(prettyQuintEx), text(')'))
+
     case 'app':
       switch (ex.opcode) {
         case 'Set':
           return group([richtext(chalk.green, 'Set'), nary(text('('), ex.args.map(prettyQuintEx), text(')'))])
 
         case 'Map': {
           const ps: Doc[] = ex.args.map(tup => {
-            if (tup.kind === 'app' && tup.opcode === 'Tup' && tup.args.length === 2) {
-              const [k, v] = tup.args
+            if (tup.kind === 'tuple' && tup.elements.length === 2) {
+              const [k, v] = tup.elements
               return group([prettyQuintEx(k), richtext(chalk.gray, ' ->'), nest('  ', [line(), prettyQuintEx(v)])])
             } else {
               return text('<expected-pair>')
@@ -82,9 +85,6 @@ export function prettyQuintEx(ex: QuintEx): Doc {
           return group([richtext(chalk.green, 'Map'), nary(text('('), ps, text(')'))])
         }
 
-        case 'Tup':
-          return nary(text('('), ex.args.map(prettyQuintEx), text(')'))
-
         case 'List': {
           return nary(text('['), ex.args.map(prettyQuintEx), text(']'))
         }
@@ -108,7 +108,7 @@ export function prettyQuintEx(ex: QuintEx): Doc {
 
           const valueExpr = ex.args[1]
           const value =
-            valueExpr.kind === 'app' && valueExpr.opcode === 'Tup' && valueExpr.args.length === 0
+            valueExpr.kind === 'tuple' && valueExpr.elements.length === 0
               ? [] // A payload with the empty tuple is shown as a bare label
               : [text('('), prettyQuintEx(valueExpr), text(')')]
 

quint/src/ir/IRTransformer.ts

@@ -62,6 +62,8 @@ export class IRTransformer {
   exitLambda?: (expr: ir.QuintLambda) => ir.QuintLambda
   enterLet?: (expr: ir.QuintLet) => ir.QuintLet
   exitLet?: (expr: ir.QuintLet) => ir.QuintLet
+  enterTuple?: (expr: ir.QuintTup) => ir.QuintTup
+  exitTuple?: (expr: ir.QuintTup) => ir.QuintTup
 
   /** Types */
   enterLiteralType?: (
@@ -522,6 +524,16 @@ function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.Q
       }
       break
 
+    case 'tuple':
+      if (transformer.enterTuple) {
+        newExpr = transformer.enterTuple(newExpr)
+      }
+      newExpr.elements = newExpr.elements.map(element => transformExpression(transformer, element))
+      if (transformer.exitTuple) {
+        newExpr = transformer.exitTuple(newExpr)
+      }
+      break
+
     default:
       unreachable(newExpr)
   }

quint/src/ir/IRVisitor.ts

@@ -71,6 +71,8 @@ export interface IRVisitor {
   exitLambda?: (_expr: ir.QuintLambda) => void
   enterLet?: (_expr: ir.QuintLet) => void
   exitLet?: (_expr: ir.QuintLet) => void
+  enterTuple?: (_expr: ir.QuintTup) => void
+  exitTuple?: (_expr: ir.QuintTup) => void
 
   /** Types */
   enterLiteralType?: (_type: t.QuintBoolType | t.QuintIntType | t.QuintStrType) => void
@@ -432,6 +434,17 @@ export function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {
         visitor.exitLiteral(expr)
       }
       break
+    case 'tuple': {
+      if (visitor.enterTuple) {
+        visitor.enterTuple(expr)
+      }
+      expr.elements.forEach(element => walkExpression(visitor, element))
+
+      if (visitor.exitTuple) {
+        visitor.exitTuple(expr)
+      }
+      break
+    }
     case 'app': {
       if (visitor.enterApp) {
         visitor.enterApp(expr)

quint/src/ir/IRprinting.ts

@@ -151,6 +151,10 @@ export function expressionToString(expr: QuintEx): string {
       return `((${expr.params.map(p => p.name).join(', ')}) => ${expressionToString(expr.expr)})`
     case 'let':
       return `${declarationToString(expr.opdef)} { ${expressionToString(expr.expr)} }`
+    case 'tuple':
+      return `(${expr.elements.map(expressionToString).join(', ')})`
+    default:
+      throw new Error(`Unknown expression kind: ${(expr as any).kind}`)
   }
 }
 

quint/src/ir/namespacer.ts

@@ -14,7 +14,7 @@
  */
 
 import { IRTransformer, transformDefinition } from './IRTransformer'
-import { QuintApp, QuintDef, QuintLambda, QuintName } from './quintIr'
+import { QuintApp, QuintDef, QuintLambda, QuintName, QuintTup } from './quintIr'
 import { QuintConstType } from './quintTypes'
 
 /**
@@ -63,6 +63,27 @@ class Namespacer implements IRTransformer {
     return expr
   }
 
+  exitTuple(tup: QuintTup): QuintTup {
+    // Process each element of the tuple
+    const namespacedElements = tup.elements.map(element => {
+      // If the element is a name, apply the namespace
+      if (element.kind === 'name' && typeof element.name === 'string') {
+        return {
+          ...element,
+          name: namespacedName(this.namespace, element.name), // Apply the namespace
+        }
+      }
+      // Otherwise, return the element as-is
+      return element
+    })
+
+    // Return a new tuple with namespaced elements
+    return {
+      ...tup,
+      elements: namespacedElements,
+    }
+  }
+
   exitApp(expr: QuintApp): QuintApp {
     if (!this.namesToPreserve.has(expr.opcode)) {
       return { ...expr, opcode: namespacedName(this.namespace, expr.opcode) }

quint/src/ir/quintIr.ts

@@ -108,6 +108,13 @@ export interface QuintApp extends WithId {
   args: QuintEx[]
 }
 
+export interface QuintTup extends WithId {
+  /** Expressions kind ('tuple' -- a collection where elements can have different types) */
+  kind: 'tuple'
+  /** A list of elements of the tuple */
+  elements: QuintEx[]
+}
+
 /** A subtype of `QuintApp` covering all quint builtin operators */
 export interface QuintBuiltinApp extends QuintApp {
   /** The name of the builtin being applied */
@@ -128,7 +135,6 @@ export const builtinOpCodes = [
   'Map',
   'Rec',
   'Set',
-  'Tup',
   'actionAll',
   'actionAny',
   'allLists',
@@ -247,7 +253,7 @@ export interface QuintLet extends WithId {
 /**
  * Discriminated union of Quint expressions.
  */
-export type QuintEx = QuintName | QuintBool | QuintInt | QuintStr | QuintApp | QuintLambda | QuintLet
+export type QuintEx = QuintName | QuintBool | QuintInt | QuintStr | QuintApp | QuintLambda | QuintLet | QuintTup
 
 /**
  * A user-defined operator that is defined via one of the qualifiers: