Allow shadowing by keeping a list of definitions in the

`definitionsByName` map

Author: bugarela

quint/src/names/base.ts

@@ -12,6 +12,7 @@
  * @module
  */
 
+import { cloneDeep, compact } from 'lodash'
 import { QuintDef, QuintExport, QuintImport, QuintInstance, QuintLambdaParameter } from '../ir/quintIr'
 import { QuintType } from '../ir/quintTypes'
 import { QuintError } from '../quintError'
@@ -49,7 +50,7 @@ export type LookupDefinition = (QuintDef | ({ kind: 'param' } & QuintLambdaParam
 /**
  * A module's definitions, indexed by name.
  */
-export type DefinitionsByName = Map<string, LookupDefinition & { hidden?: boolean }>
+export type DefinitionsByName = Map<string, (LookupDefinition & { hidden?: boolean })[]>
 
 /**
  * Definitions for each module
@@ -83,6 +84,10 @@ export type NameResolutionResult = {
   errors: QuintError[]
 }
 
+export function getTopLevelDef(defs: DefinitionsByName, name: string): LookupDefinition | undefined {
+  return defs.get(name)?.at(0)
+}
+
 /**
  * Copy the names of a definitions table to a new one, ignoring hidden
  * definitions, and optionally adding a namespace.
@@ -100,11 +105,15 @@ export function copyNames(
 ): DefinitionsByName {
   const table = new Map()
 
-  originTable.forEach((def, identifier) => {
+  originTable.forEach((defs, identifier) => {
     const name = namespace ? [namespace, identifier].join('::') : identifier
-    if (!def.hidden || def.kind === 'const') {
-      table.set(name, copyAsHidden ? { ...def, hidden: copyAsHidden } : def)
-    }
+    const newDefs = defs.map(def => {
+      if (!def.hidden || def.kind === 'const') {
+        return cloneDeep(copyAsHidden ? { ...def, hidden: copyAsHidden } : def)
+      }
+    })
+
+    table.set(name, compact(newDefs))
   })
 
   return table

quint/src/names/collector.ts

@@ -34,6 +34,7 @@ import {
   addNamespacesToDef,
   builtinNames,
   copyNames,
+  getTopLevelDef,
 } from './base'
 import {
   moduleNotFoundError,
@@ -42,7 +43,7 @@ import {
   paramNotFoundError,
   selfReferenceError,
 } from './importErrors'
-import { compact } from 'lodash'
+import { cloneDeep, compact } from 'lodash'
 
 /**
  * Collects all top-level definitions in Quint modules. Used internally by
@@ -118,7 +119,7 @@ export class NameCollector implements IRVisitor {
       return
     }
 
-    const instanceTable = new Map([...moduleTable.entries()])
+    const instanceTable = cloneDeep(moduleTable)
     if (decl.qualifiedName) {
       // Add the qualifier to `definitionsMyModule` map with a copy of the
       // definitions, so if there is an export of that qualifier, we know which
@@ -129,7 +130,8 @@ export class NameCollector implements IRVisitor {
     // For each override, check if the name exists in the instantiated module and is a constant.
     // If so, update the value definition to point to the expression being overriden
     decl.overrides.forEach(([param, ex]) => {
-      const constDef = instanceTable.get(param.name)
+      // Constants are always top-level
+      const constDef = getTopLevelDef(instanceTable, param.name)
 
       if (!constDef) {
         this.errors.push(paramNotFoundError(decl, param))
@@ -142,13 +144,14 @@ export class NameCollector implements IRVisitor {
       }
 
       // Update the definition to point to the expression being overriden
-      instanceTable.set(param.name, { ...constDef, id: ex.id })
+      constDef.id = ex.id
+      constDef.hidden = false
     })
 
     // All names from the instanced module should be acessible with the instance namespace
     // So, copy them to the current module's lookup table
     const newDefs = copyNames(instanceTable, decl.qualifiedName, true)
-    this.collectDefinitions(newDefs, decl)
+    this.collectTopLevelDefinitions(newDefs, decl)
   }
 
   enterImport(decl: QuintImport): void {
@@ -158,7 +161,7 @@ export class NameCollector implements IRVisitor {
       return
     }
 
-    const moduleTable = this.definitionsByModule.get(decl.protoName)
+    const moduleTable = cloneDeep(this.definitionsByModule.get(decl.protoName))
 
     if (!moduleTable) {
       // Importing non-existing module
@@ -178,12 +181,12 @@ export class NameCollector implements IRVisitor {
 
     if (!decl.defName || decl.defName === '*') {
       // Imports all definitions
-      this.collectDefinitions(importableDefinitions, decl)
+      this.collectTopLevelDefinitions(importableDefinitions, decl)
       return
     }
 
     // Tries to find a specific definition, reporting an error if not found
-    const newDef = importableDefinitions.get(decl.defName)
+    const newDef = getTopLevelDef(importableDefinitions, decl.defName)
     if (!newDef) {
       this.errors.push(nameNotFoundError(decl))
       return
@@ -203,7 +206,7 @@ export class NameCollector implements IRVisitor {
       return
     }
 
-    const moduleTable = this.definitionsByModule.get(decl.protoName)
+    const moduleTable = cloneDeep(this.definitionsByModule.get(decl.protoName))
     if (!moduleTable) {
       // Exporting non-existing module
       this.errors.push(moduleNotFoundError(decl))
@@ -214,12 +217,12 @@ export class NameCollector implements IRVisitor {
 
     if (!decl.defName || decl.defName === '*') {
       // Export all definitions
-      this.collectDefinitions(exportableDefinitions, decl)
+      this.collectTopLevelDefinitions(exportableDefinitions, decl)
       return
     }
 
     // Tries to find a specific definition, reporting an error if not found
-    const newDef = exportableDefinitions.get(decl.defName)
+    const newDef = getTopLevelDef(exportableDefinitions, decl.defName)
 
     if (!newDef) {
       this.errors.push(nameNotFoundError(decl))
@@ -257,14 +260,36 @@ export class NameCollector implements IRVisitor {
       return
     }
 
-    if (this.definitionsByName.has(identifier) && this.definitionsByName.get(identifier)!.id != def.id) {
-      // Conflict with a previous definition
-      this.recordConflict(identifier, this.definitionsByName.get(identifier)!.id, source)
+    def.depth ??= 0
+    const namespaces = importedFrom ? this.namespaces(importedFrom) : []
+
+    if (!this.definitionsByName.has(identifier)) {
+      // No existing defs with this name. Create an entry with a single def.
+      this.definitionsByName.set(identifier, [{ ...addNamespacesToDef(def, namespaces), importedFrom }])
       return
     }
 
-    const namespaces = importedFrom ? this.namespaces(importedFrom) : []
-    this.definitionsByName.set(identifier, { ...addNamespacesToDef(def, namespaces), importedFrom })
+    // Else: There are exiting defs. We need to check for conflicts
+    const existingEntries = this.definitionsByName.get(identifier)!
+    // Entries conflict if they have different ids, but the same depth.
+    // Entries with different depths are ok, because one is shadowing the
+    // other.
+    const conflictingEntries = existingEntries.filter(entry => entry.id !== def.id && entry.depth === def.depth)
+
+    // Record potential errors and move on
+    conflictingEntries.forEach(existingEntry => {
+      this.recordConflict(identifier, existingEntry.id, source)
+    })
+
+    // Keep entries with different ids. DON'T keep the whole
+    // `existingEntries` since those may contain the same exact defs, but
+    // hidden.
+    this.definitionsByName.set(
+      identifier,
+      existingEntries
+        .filter(entry => entry.id !== def.id)
+        .concat([{ ...addNamespacesToDef(def, namespaces), importedFrom }])
+    )
   }
 
   /**
@@ -273,19 +298,25 @@ export class NameCollector implements IRVisitor {
    * @param identifier - The identifier of the definition to delete.
    */
   deleteDefinition(identifier: string): void {
-    this.definitionsByName.delete(identifier)
+    this.definitionsByName.get(identifier)?.pop()
+    return
   }
 
   /**
-   * Obtains a collected definition.
+   * Gets the definition with the given name, in the current (visiting) scope
    *
    * @param identifier - The identifier of the definition to retrieve.
    *
    * @returns The definition object for the given identifier, or undefined if a
    * definitions with that identifier was never collected.
    */
   getDefinition(identifier: string): LookupDefinition | undefined {
-    return this.definitionsByName.get(identifier)
+    const defs = this.definitionsByName.get(identifier)
+    if (defs === undefined || defs.length === 0) {
+      return
+    }
+
+    return defs[defs.length - 1]
   }
 
   private namespaces(decl: QuintImport | QuintInstance | QuintExport): string[] {
@@ -297,18 +328,33 @@ export class NameCollector implements IRVisitor {
     return namespace ? [namespace] : []
   }
 
-  private collectDefinitions(
+  private collectTopLevelDefinitions(
     newDefs: DefinitionsByName,
     importedFrom?: QuintImport | QuintExport | QuintInstance
   ): void {
     const namespaces = importedFrom ? this.namespaces(importedFrom) : []
-    const newEntries: [string, LookupDefinition][] = [...newDefs.entries()].map(([identifier, def]) => {
-      const existingEntry = this.definitionsByName.get(identifier)
-      if (existingEntry && existingEntry.id !== def.id) {
-        this.recordConflict(identifier, existingEntry.id, def.id)
-      }
-      return [identifier, { ...addNamespacesToDef(def, namespaces), importedFrom }]
-    })
+    const newEntries: [string, LookupDefinition[]][] = compact(
+      [...newDefs.keys()].map(identifier => {
+        const def = getTopLevelDef(newDefs, identifier)
+        if (!def) {
+          return
+        }
+
+        const existingEntries = this.definitionsByName.get(identifier)
+        if (existingEntries) {
+          const conflictingEntries = existingEntries.filter(entry => entry.id !== def.id)
+          conflictingEntries.forEach(existingEntry => {
+            this.recordConflict(identifier, existingEntry.id, def.id)
+          })
+
+          // Keep conflicting entries and add the new one. DON'T keep the whole
+          // `existingEntries` since those may contain the same exact defs, but
+          // hidden.
+          return [identifier, conflictingEntries.concat([{ ...addNamespacesToDef(def, namespaces), importedFrom }])]
+        }
+        return [identifier, [{ ...addNamespacesToDef(def, namespaces), importedFrom }]]
+      })
+    )
 
     this.definitionsByName = new Map([...this.definitionsByName.entries(), ...newEntries])
   }

quint/src/names/resolver.ts

@@ -58,8 +58,8 @@ class NameResolver implements IRVisitor {
   unusedDefinitions: UnusedDefinitions = moduleName => {
     const definitions: LookupDefinition[] = Array.from(
       this.collector.definitionsByModule.get(moduleName)?.values() || []
-    )
-    const usedDefinitions = [...this.table.values()]
+    ).flat()
+    const usedDefinitions = [...this.table.values()].flat()
 
     return new Set(difference(definitions, usedDefinitions))
   }