Implement review suggestions

quint/src/flattening.ts

@@ -257,8 +257,8 @@ class Flatenner {
     return defsToFlatten.map(protoDef => this.copyDef(protoDef, qualifiedName))
   }
 
-  private copyDef(decl: QuintDef, qualifier: string | undefined): QuintDef {
-    const defWithQualifier = qualifier ? addNamespaceToDefinition(decl, qualifier, this.currentModuleNames) : decl
+  private copyDef(def: QuintDef, qualifier: string | undefined): QuintDef {
+    const defWithQualifier = qualifier ? addNamespaceToDefinition(def, qualifier, this.currentModuleNames) : def
     const defWithNewId = generateFreshIds(defWithQualifier, this.idGenerator, this.sourceMap, this.analysisOutput)
 
     return defWithNewId

quint/src/names/base.ts

@@ -23,15 +23,8 @@ export type DefinitionKind = 'module' | 'def' | 'val' | 'assumption' | 'param' |
 /**
  * A definition to be stored in `DefinitionsByName` and `LookupTable`. Either a `QuintDef`
  * or a `QuintLambdaParameter`, with additional metadata fields
- *
- * A definition can be hidden, meaning it
- *
- * A definition can also have a list of `namespaces` and a `importedFrom` reference, to be used
- * to track the origins of a definition. Namespaces are added to the definition's name when it
- * is copied over to a module with a qualified name. `importedFrom` is a reference to the import/instance/export
- * statement that originated the definition, when the definition was copied from another module.
  */
-export type Definition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter)) & {
+export type LookupDefinition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter)) & {
   /* Hidden definitions won't be copied over to a module when an
    * import/intance/export statement is resolved. `hidden` can be removed with
    * `export` statements for the hidden definitions. */
@@ -53,7 +46,7 @@ export type Definition = (QuintDef | ({ kind: 'param' } & QuintLambdaParameter))
 /**
  * A module's definitions, indexed by name.
  */
-export type DefinitionsByName = Map<string, Definition & { hidden?: boolean }>
+export type DefinitionsByName = Map<string, LookupDefinition & { hidden?: boolean }>
 
 /**
  * Definitions for each module
@@ -71,7 +64,7 @@ export type DefinitionsByModule = Map<string, DefinitionsByName>
  *
  * This should be created by `resolveNames` from `resolver.ts`
  */
-export type LookupTable = Map<bigint, Definition>
+export type LookupTable = Map<bigint, LookupDefinition>
 
 /**
  * Copy the names of a definitions table to a new one, ignoring hidden

quint/src/names/collector.ts

@@ -25,7 +25,7 @@ import {
   QuintTypeDef,
   QuintVar,
 } from '../ir/quintIr'
-import { Definition, DefinitionsByModule, DefinitionsByName, LookupTable, builtinNames, copyNames } from './base'
+import { LookupDefinition, DefinitionsByModule, DefinitionsByName, LookupTable, builtinNames, copyNames } from './base'
 import {
   moduleNotFoundError,
   nameNotFoundError,
@@ -236,7 +236,7 @@ export class NameCollector implements IRVisitor {
    * @param source - An optional source identifier for the definition, if the
    * source is different than `def.id` (i.e. in import-like statements).
    */
-  collectDefinition(def: Definition, name?: string, source?: bigint): void {
+  collectDefinition(def: LookupDefinition, name?: string, source?: bigint): void {
     const identifier = name ?? def.name
     if (identifier === '_') {
       // Don't collect underscores, as they are special identifiers that allow no usage
@@ -275,7 +275,7 @@ export class NameCollector implements IRVisitor {
    * @returns The definition object for the given identifier, or undefined if a
    * definitions with that identifier was never collected.
    */
-  getDefinition(identifier: string): Definition | undefined {
+  getDefinition(identifier: string): LookupDefinition | undefined {
     return this.definitionsByName.get(identifier)
   }
 

quint/src/types/aliasInliner.ts

@@ -14,7 +14,7 @@
  */
 
 import { IRTransformer, transformDefinition, transformModule, transformType } from '../ir/IRTransformer'
-import { Definition, LookupTable } from '../names/base'
+import { LookupDefinition, LookupTable } from '../names/base'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { QuintDef, QuintModule } from '../ir/quintIr'
 import { QuintType } from '../ir/quintTypes'
@@ -35,7 +35,7 @@ export function inlineTypeAliases(
 ): { modules: QuintModule[]; table: LookupTable; analysisOutput: AnalysisOutput } {
   const modulesWithInlinedAliases = modules.map(m => inlineAliasesInModule(m, table))
   const tableWithInlinedAliases = new Map(
-    [...table.entries()].map(([id, def]): [bigint, Definition] => {
+    [...table.entries()].map(([id, def]): [bigint, LookupDefinition] => {
       if (def.kind === 'param') {
         const typeAnnotation = def.typeAnnotation ? inlineAliasesInType(def.typeAnnotation, table) : undefined
         return [id, { ...def, typeAnnotation }]