Merge pull request #1104 from informalsystems/gabriela/definition-upd…

…ate-procedure-extraction

Namespacer and ID Refresher

quint/src/cliCommands.ts

@@ -27,7 +27,7 @@ import { Either, left, right } from '@sweet-monads/either'
 import { EffectScheme } from './effects/base'
 import { LookupTable } from './names/base'
 import { ReplOptions, quintRepl } from './repl'
-import { OpQualifier, QuintEx, QuintModule } from './quintIr'
+import { OpQualifier, QuintEx, QuintModule } from './ir/quintIr'
 import { TypeScheme } from './types/base'
 import lineColumn from 'line-column'
 import { formatError } from './errorReporter'

quint/src/docs.ts

@@ -14,8 +14,8 @@
  */
 
 import { compact } from 'lodash'
-import { definitionToString } from './IRprinting'
-import { QuintModule } from './quintIr'
+import { definitionToString } from './ir/IRprinting'
+import { QuintModule } from './ir/quintIr'
 
 /**
  * A documentation entry for a definition, compatible with LSP responses for signature help

quint/src/effects/builtinSignatures.ts

@@ -15,7 +15,7 @@
 import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature, effectNames, toScheme } from './base'
 import { parseEffectOrThrow } from './parser'
 import { range, times } from 'lodash'
-import { QuintBuiltinOpcode } from '../quintIr'
+import { QuintBuiltinOpcode } from '../ir/quintIr'
 
 export function getSignatures(): Map<string, Signature> {
   return new Map<string, Signature>(fixedAritySignatures.concat(multipleAritySignatures))

quint/src/effects/inferrer.ts

@@ -15,8 +15,8 @@
 
 import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { LookupTable } from '../names/base'
-import { expressionToString } from '../IRprinting'
-import { IRVisitor, walkDefinition } from '../IRVisitor'
+import { expressionToString } from '../ir/IRprinting'
+import { IRVisitor, walkDefinition } from '../ir/IRVisitor'
 import {
   QuintApp,
   QuintBool,
@@ -30,7 +30,7 @@ import {
   QuintOpDef,
   QuintStr,
   QuintVar,
-} from '../quintIr'
+} from '../ir/quintIr'
 import { Effect, EffectScheme, Signature, effectNames, toScheme, unify } from './base'
 import { Substitutions, applySubstitution, compose } from './substitutions'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } from '../errorTree'

quint/src/effects/modeChecker.ts

@@ -14,10 +14,10 @@
  */
 
 import isEqual from 'lodash.isequal'
-import { qualifierToString } from '../IRprinting'
-import { IRVisitor, walkDefinition } from '../IRVisitor'
+import { qualifierToString } from '../ir/IRprinting'
+import { IRVisitor, walkDefinition } from '../ir/IRVisitor'
 import { QuintError } from '../quintError'
-import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../quintIr'
+import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../ir/quintIr'
 import { unreachable } from '../util'
 import { ArrowEffect, ComponentKind, EffectScheme, Entity, entityNames, stateVariables } from './base'
 import { effectToString, entityToString } from './printing'

quint/src/flattening.ts

@@ -18,21 +18,19 @@ import {
   FlatDef,
   FlatModule,
   QuintDef,
-  QuintEx,
   QuintExport,
   QuintImport,
   QuintInstance,
   QuintModule,
-  QuintOpDef,
-  isAnnotatedDef,
   isFlat,
-} from './quintIr'
-import { definitionToString } from './IRprinting'
-import { ConcreteFixedRow, QuintType, Row } from './quintTypes'
+} from './ir/quintIr'
+import { definitionToString, moduleToString } from './ir/IRprinting'
 import { Loc, parsePhase3importAndNameResolution } from './parsing/quintParserFrontend'
 import { compact, uniqBy } from 'lodash'
 import { AnalysisOutput } from './quintAnalyzer'
 import { inlineAliasesInDef, inlineAnalysisOutput, inlineTypeAliases } from './types/aliasInliner'
+import { addNamespaceToDefinition } from './ir/namespacer'
+import { generateFreshIds } from './ir/idRefresher'
 
 /**
  * Flatten an array of modules, replacing instances, imports and exports with
@@ -146,14 +144,15 @@ export function addDefToFlatModule(
 }
 
 class Flatenner {
-  private idGenerator: IdGenerator
   private table: LookupTable
   private currentModuleNames: Set<string>
-  private sourceMap: Map<bigint, Loc>
-  private analysisOutput: AnalysisOutput
   private importedModules: Map<string, QuintModule>
   private module: QuintModule
 
+  private idGenerator: IdGenerator
+  private sourceMap: Map<bigint, Loc>
+  private analysisOutput: AnalysisOutput
+
   constructor(
     idGenerator: IdGenerator,
     table: LookupTable,
@@ -162,7 +161,6 @@ class Flatenner {
     importedModules: Map<string, QuintModule>,
     module: QuintModule
   ) {
-    this.idGenerator = idGenerator
     this.table = table
     this.currentModuleNames = new Set([
       // builtin names
@@ -171,10 +169,11 @@ class Flatenner {
       ...compact(module.defs.map(d => (isFlat(d) ? d.name : undefined))),
     ])
 
-    this.sourceMap = sourceMap
-    this.analysisOutput = analysisOutput
     this.importedModules = importedModules
     this.module = module
+    this.idGenerator = idGenerator
+    this.sourceMap = sourceMap
+    this.analysisOutput = analysisOutput
   }
 
   flattenDef(def: QuintDef): FlatDef[] {
@@ -260,233 +259,15 @@ class Flatenner {
       throw new Error(`Impossible: ${definitionToString(def)} should have been flattened already`)
     }
 
-    if (!isAnnotatedDef(def)) {
-      return this.addNamespaceToDef(qualifier, def)
-    }
-
-    const type = this.addNamespaceToType(qualifier, def.typeAnnotation)
-    const newDef = this.addNamespaceToDef(qualifier, def)
-    if (!isAnnotatedDef(newDef)) {
-      throw new Error(`Impossible: transformation should preserve kind`)
-    }
-
-    return { ...newDef, typeAnnotation: type }
-  }
-
-  private addNamespaceToDef(name: string | undefined, def: QuintDef): FlatDef {
-    switch (def.kind) {
-      case 'def':
-        return this.addNamespaceToOpDef(name, def)
-      case 'assume':
-        return {
-          ...def,
-          name: this.namespacedName(name, def.name),
-          assumption: this.addNamespaceToExpr(name, def.assumption),
-          id: this.getNewIdWithSameData(def.id),
-        }
-      case 'const':
-      case 'var':
-        return { ...def, name: this.namespacedName(name, def.name), id: this.getNewIdWithSameData(def.id) }
-      case 'typedef':
-        return {
-          ...def,
-          name: this.namespacedName(name, def.name),
-          type: def.type ? this.addNamespaceToType(name, def.type) : undefined,
-          id: this.getNewIdWithSameData(def.id),
-        }
-      case 'instance':
-        throw new Error(`Instance in ${definitionToString(def)} should have been flatenned already`)
-      case 'import':
-        throw new Error(`Import in ${definitionToString(def)} should have been flatenned already`)
-      case 'export':
-        throw new Error(`Export in ${definitionToString(def)} should have been flatenned already`)
-    }
-  }
-
-  private addNamespaceToOpDef(name: string | undefined, opdef: QuintOpDef): QuintOpDef {
-    return {
-      ...opdef,
-      name: this.namespacedName(name, opdef.name),
-      expr: this.addNamespaceToExpr(name, opdef.expr),
-      id: this.getNewIdWithSameData(opdef.id),
-    }
-  }
-
-  private addNamespaceToExpr(name: string | undefined, expr: QuintEx): QuintEx {
-    const id = this.getNewIdWithSameData(expr.id)
-
-    switch (expr.kind) {
-      case 'name':
-        if (this.shouldAddNamespace(expr.name)) {
-          return { ...expr, name: this.namespacedName(name, expr.name), id }
-        }
-
-        return { ...expr, id }
-      case 'bool':
-      case 'int':
-      case 'str':
-        return { ...expr, id }
-      case 'app': {
-        if (this.shouldAddNamespace(expr.opcode)) {
-          return {
-            ...expr,
-            opcode: this.namespacedName(name, expr.opcode),
-            args: expr.args.map(arg => this.addNamespaceToExpr(name, arg)),
-            id,
-          }
-        }
-
-        return {
-          ...expr,
-          args: expr.args.map(arg => this.addNamespaceToExpr(name, arg)),
-          id,
-        }
-      }
-      case 'lambda':
-        return {
-          ...expr,
-          params: expr.params.map(param => ({
-            name: this.namespacedName(name, param.name),
-            id: this.getNewIdWithSameData(param.id),
-          })),
-          expr: this.addNamespaceToExpr(name, expr.expr),
-          id,
-        }
-
-      case 'let':
-        return {
-          ...expr,
-          opdef: this.addNamespaceToOpDef(name, expr.opdef),
-          expr: this.addNamespaceToExpr(name, expr.expr),
-          id,
-        }
-    }
-  }
-
-  private addNamespaceToType(name: string | undefined, type: QuintType): QuintType {
-    const id = type.id ? this.getNewIdWithSameData(type.id) : undefined
-
-    switch (type.kind) {
-      case 'bool':
-      case 'int':
-      case 'str':
-      case 'var':
-        return { ...type, id }
-      case 'const':
-        return { ...type, name: this.namespacedName(name, type.name), id }
-      case 'set':
-      case 'list':
-        return { ...type, elem: this.addNamespaceToType(name, type.elem), id }
-      case 'fun':
-        return {
-          ...type,
-          arg: this.addNamespaceToType(name, type.arg),
-          res: this.addNamespaceToType(name, type.res),
-          id,
-        }
-      case 'oper':
-        return {
-          ...type,
-          args: type.args.map(arg => this.addNamespaceToType(name, arg)),
-          res: this.addNamespaceToType(name, type.res),
-          id,
-        }
-      case 'tup':
-      case 'rec':
-        return {
-          ...type,
-          fields: this.addNamespaceToRow(name, type.fields),
-          id,
-        }
-      case 'sum':
-        return {
-          ...type,
-          fields: this.addNamespaceToSumRow(name, type.fields),
-          id,
-        }
-      case 'union':
-        return {
-          ...type,
-          records: type.records.map(record => {
-            return {
-              ...record,
-              fields: this.addNamespaceToRow(name, record.fields),
-            }
-          }),
-          id,
-        }
-    }
-  }
+    const defWithQualifier = qualifier ? addNamespaceToDefinition(def, qualifier, this.currentModuleNames) : def
+    const defWithNewId = generateFreshIds(defWithQualifier, this.idGenerator, this.sourceMap, this.analysisOutput)
 
-  private addNamespaceToRow(name: string | undefined, row: Row): Row {
-    if (row.kind !== 'row') {
-      return row
-    }
-
-    return {
-      ...row,
-      fields: row.fields.map(field => {
-        return {
-          ...field,
-          fieldType: this.addNamespaceToType(name, field.fieldType),
-        }
-      }),
-    }
-  }
-
-  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
-  }
-
-  /**
-   * Whether a name should be prefixed with the namespace.
-   *
-   * @param name the name to be prefixed
-   *
-   * @returns false if the name is on the curentModulesName list, true otherwise
-   */
-  private shouldAddNamespace(name: string): boolean {
-    if (this.currentModuleNames.has(name)) {
-      return false
-    }
-
-    return true
-  }
-
-  private getNewIdWithSameData(id: bigint): bigint {
-    const newId = this.idGenerator.nextId()
-
-    const type = this.analysisOutput.types.get(id)
-    const effect = this.analysisOutput.effects.get(id)
-    const mode = this.analysisOutput.modes.get(id)
-    const source = this.sourceMap.get(id)
-
-    if (type) {
-      this.analysisOutput.types.set(newId, type)
-    }
-    if (effect) {
-      this.analysisOutput.effects.set(newId, effect)
-    }
-    if (mode) {
-      this.analysisOutput.modes.set(newId, mode)
-    }
-    if (source) {
-      this.sourceMap.set(newId, source)
+    if (!isFlat(defWithNewId)) {
+      // safe cast
+      throw new Error(`Impossible: updating definitions cannot unflatten a def: ${definitionToString(defWithNewId)}`)
     }
 
-    return newId
+    return defWithNewId
   }
 }
 
@@ -504,6 +285,7 @@ function resolveNamesOrThrow(currentTable: LookupTable, sourceMap: Map<bigint, L
       // This should not happen, as the flattening should not introduce any
       // errors, since parsePhase3 analysis of the original modules has already
       // assured all names are correct.
+      console.log(moduleToString(module))
       throw new Error(`Error on resolving names for flattened modules: ${errors.map(e => e.explanation)}`)
     })
     .unwrap().table

quint/src/graphics.ts

@@ -26,13 +26,13 @@ import {
   textify,
 } from './prettierimp'
 
-import { QuintDef, QuintEx, isAnnotatedDef } from './quintIr'
+import { QuintDef, QuintEx, isAnnotatedDef } from './ir/quintIr'
 import { ExecutionFrame } from './runtime/trace'
 import { zerog } from './idGenerator'
-import { ConcreteFixedRow, QuintType, Row } from './quintTypes'
+import { ConcreteFixedRow, QuintType, Row } from './ir/quintTypes'
 import { TypeScheme } from './types/base'
 import { canonicalTypeScheme } from './types/printing'
-import { definitionToString, flattenRow, qualifierToString, rowToString } from './IRprinting'
+import { definitionToString, flattenRow, qualifierToString, rowToString } from './ir/IRprinting'
 
 /**
  * An abstraction of a Console of bounded text width.