Merge pull request #1105 from informalsystems/gabriela/new-definition…

…s-and-declarations

Store the whole def in `Defintion` and introduce `QuintDeclaration`

quint/io-cli-tests.md

@@ -76,7 +76,7 @@ error: parsing failed
 <!-- !test in module AST is output -->
 ```
 quint parse --out parse-out-example.json ../examples/language-features/tuples.qnt
-jq '.modules[0].name, .table."7".reference' < parse-out-example.json
+jq '.modules[0].name, .table."7".id' < parse-out-example.json
 rm parse-out-example.json
 ```
 

quint/src/docs.ts

@@ -13,9 +13,8 @@
  * @module
  */
 
-import { compact } from 'lodash'
-import { definitionToString } from './ir/IRprinting'
-import { QuintModule } from './ir/quintIr'
+import { declarationToString } from './ir/IRprinting'
+import { QuintModule, isDef } from './ir/quintIr'
 
 /**
  * A documentation entry for a definition, compatible with LSP responses for signature help
@@ -34,23 +33,19 @@ export interface DocumentationEntry {
  * @returns a map of definition names to their documentation
  */
 export function produceDocs(quintModule: QuintModule): Map<string, DocumentationEntry> {
-  const entries = quintModule.defs.map(def => {
-    if (def.kind === 'instance' || def.kind === 'import' || def.kind === 'export') {
-      return undefined
-    }
-
+  const entries = quintModule.declarations.filter(isDef).map(def => {
     const entry: [string, DocumentationEntry] = [
       def.name,
       {
-        label: definitionToString(def, false),
+        label: declarationToString(def, false),
         documentation: def.doc,
       },
     ]
 
     return entry
   })
 
-  return new Map<string, DocumentationEntry>(compact(entries))
+  return new Map<string, DocumentationEntry>(entries)
 }
 
 /**
@@ -60,23 +55,19 @@ export function produceDocs(quintModule: QuintModule): Map<string, Documentation
  * @returns a map of definition ids to their documentation
  */
 export function produceDocsById(quintModule: QuintModule): Map<bigint, DocumentationEntry> {
-  const entries = quintModule.defs.map(def => {
-    if (def.kind === 'instance' || def.kind === 'import' || def.kind === 'export') {
-      return undefined
-    }
-
+  const entries = quintModule.declarations.filter(isDef).map(def => {
     const entry: [bigint, DocumentationEntry] = [
       def.id,
       {
-        label: definitionToString(def, false),
+        label: declarationToString(def, false),
         documentation: def.doc,
       },
     ]
 
     return entry
   })
 
-  return new Map(compact(entries))
+  return new Map(entries)
 }
 
 /**

quint/src/effects/inferrer.ts

@@ -16,12 +16,12 @@
 import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { LookupTable } from '../names/base'
 import { expressionToString } from '../ir/IRprinting'
-import { IRVisitor, walkDefinition } from '../ir/IRVisitor'
+import { IRVisitor, walkDeclaration } from '../ir/IRVisitor'
 import {
   QuintApp,
   QuintBool,
   QuintConst,
-  QuintDef,
+  QuintDeclaration,
   QuintEx,
   QuintInt,
   QuintLambda,
@@ -58,14 +58,14 @@ export class EffectInferrer implements IRVisitor {
    * Infers an effect for every expression in a module based on
    * the definitions table for that module
    *
-   * @param defs: the list of Quint definitions to infer effects for
+   * @param declarations: the list of QuintDeclarations to infer effects for
    *
    * @returns a map from expression ids to their effects and a map from expression
    *          ids to the corresponding error for any problematic expressions.
    */
-  inferEffects(defs: QuintDef[]): EffectInferenceResult {
-    defs.forEach(def => {
-      walkDefinition(this, def)
+  inferEffects(declarations: QuintDeclaration[]): EffectInferenceResult {
+    declarations.forEach(decl => {
+      walkDeclaration(this, decl)
     })
     return [this.errors, this.effects]
   }
@@ -346,7 +346,7 @@ export class EffectInferrer implements IRVisitor {
       return right(this.newInstance(signature))
     } else {
       const def = this.lookupTable.get(nameId)
-      const id = def?.reference
+      const id = def?.id
       if (!def || !id) {
         return left(buildErrorLeaf(this.location, `Signature not found for name: ${name}`))
       }

quint/src/effects/modeChecker.ts

@@ -15,9 +15,9 @@
 
 import isEqual from 'lodash.isequal'
 import { qualifierToString } from '../ir/IRprinting'
-import { IRVisitor, walkDefinition } from '../ir/IRVisitor'
+import { IRVisitor, walkDeclaration } from '../ir/IRVisitor'
 import { QuintError } from '../quintError'
-import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../ir/quintIr'
+import { OpQualifier, QuintDeclaration, QuintInstance, QuintOpDef } from '../ir/quintIr'
 import { unreachable } from '../util'
 import { ArrowEffect, ComponentKind, EffectScheme, Entity, entityNames, stateVariables } from './base'
 import { effectToString, entityToString } from './printing'
@@ -39,18 +39,18 @@ export class ModeChecker implements IRVisitor {
   }
 
   /**
-   * Matches annotated modes for each definition with its inferred effect. Returns
+   * Matches annotated modes for each declaration with its inferred effect. Returns
    * errors for incorrect annotations and suggestions for annotations that could
    * be more strict.
    *
-   * @param defs: the list of definitions to be checked
+   * @param decls: the list of declarations to be checked
    * @param effects: the map from expression ids to their inferred effects
    *
    * @returns The mode errors, if any is found. Otherwise, a map with potential suggestions.
    */
-  checkModes(defs: QuintDef[], effects: Map<bigint, EffectScheme>): ModeCheckingResult {
+  checkModes(decls: QuintDeclaration[], effects: Map<bigint, EffectScheme>): ModeCheckingResult {
     this.effects = effects
-    defs.forEach(def => walkDefinition(this, def))
+    decls.forEach(decl => walkDeclaration(this, decl))
     return [this.errors, this.suggestions]
   }
 

quint/src/flattening.ts

@@ -15,18 +15,18 @@
 import { IdGenerator } from './idGenerator'
 import { LookupTable, builtinNames } from './names/base'
 import {
-  FlatDef,
   FlatModule,
+  QuintDeclaration,
   QuintDef,
   QuintExport,
   QuintImport,
   QuintInstance,
   QuintModule,
-  isFlat,
+  isDef,
 } from './ir/quintIr'
-import { definitionToString, moduleToString } from './ir/IRprinting'
+import { moduleToString } from './ir/IRprinting'
 import { Loc, parsePhase3importAndNameResolution } from './parsing/quintParserFrontend'
-import { compact, uniqBy } from 'lodash'
+import { uniqBy } from 'lodash'
 import { AnalysisOutput } from './quintAnalyzer'
 import { inlineAliasesInDef, inlineAnalysisOutput, inlineTypeAliases } from './types/aliasInliner'
 import { addNamespaceToDefinition } from './ir/namespacer'
@@ -119,10 +119,10 @@ export function addDefToFlatModule(
   sourceMap: Map<bigint, Loc>,
   analysisOutput: AnalysisOutput,
   module: FlatModule,
-  def: QuintDef
+  def: QuintDeclaration
 ): {
   flattenedModule: FlatModule
-  flattenedDefs: FlatDef[]
+  flattenedDefs: QuintDef[]
   flattenedTable: LookupTable
   flattenedAnalysis: AnalysisOutput
 } {
@@ -132,8 +132,8 @@ export function addDefToFlatModule(
   const flattenedDefs = flattener
     .flattenDef(def)
     // Inline type aliases in new defs
-    .map(d => inlineAliasesInDef(d, table) as FlatDef)
-  const flattenedModule: FlatModule = { ...module, defs: [...module.defs, ...flattenedDefs] }
+    .map(d => inlineAliasesInDef(d, table))
+  const flattenedModule: FlatModule = { ...module, declarations: [...module.declarations, ...flattenedDefs] }
 
   return {
     flattenedModule,
@@ -166,7 +166,7 @@ class Flatenner {
       // builtin names
       ...builtinNames,
       // names from the current module
-      ...compact(module.defs.map(d => (isFlat(d) ? d.name : undefined))),
+      ...module.declarations.filter(isDef).map(d => d.name),
     ])
 
     this.importedModules = importedModules
@@ -176,8 +176,8 @@ class Flatenner {
     this.analysisOutput = analysisOutput
   }
 
-  flattenDef(def: QuintDef): FlatDef[] {
-    if (isFlat(def)) {
+  flattenDef(def: QuintDeclaration): QuintDef[] {
+    if (isDef(def)) {
       // Not an instance, import or export, keep the same def
       return [def]
     }
@@ -190,17 +190,20 @@ class Flatenner {
   }
 
   flattenModule(): FlatModule {
-    const newDefs = this.module.defs.flatMap(def => this.flattenDef(def))
+    const newDefs = this.module.declarations.flatMap(def => this.flattenDef(def))
 
-    return { ...this.module, defs: uniqBy(newDefs, 'name') }
+    return { ...this.module, declarations: uniqBy(newDefs, 'name') }
   }
 
-  private flattenInstance(def: QuintInstance): FlatDef[] {
+  private flattenInstance(def: QuintInstance): QuintDef[] {
     // Build pure val definitions from overrides to replace the constants in the
     // instance. Index them by name to make it easier to replace the corresponding constants.
-    const overrides: Map<string, FlatDef> = new Map(
+    const overrides: Map<string, QuintDef> = new Map(
       def.overrides.map(([param, expr]) => {
         const constDef = this.table.get(param.id)!
+        if (constDef.kind !== 'const') {
+          throw new Error(`Impossible: ${constDef} should be a const`)
+        }
 
         return [
           param.name,
@@ -219,8 +222,8 @@ class Flatenner {
     const protoModule = this.importedModules.get(def.protoName)!
 
     // Overrides replace the original constant definitions, in the same position as they appear originally
-    const newProtoDefs = protoModule.defs.map(d => {
-      if (isFlat(d) && overrides.has(d.name)) {
+    const newProtoDefs = protoModule.declarations.filter(isDef).map(d => {
+      if (overrides.has(d.name)) {
         return overrides.get(d.name)!
       }
 
@@ -229,13 +232,13 @@ class Flatenner {
 
     // Add the new defs to the modules table under the instance name
     if (def.qualifiedName) {
-      this.importedModules.set(def.qualifiedName, { ...protoModule, defs: newProtoDefs })
+      this.importedModules.set(def.qualifiedName, { ...protoModule, declarations: newProtoDefs })
     }
 
     return newProtoDefs.map(protoDef => this.copyDef(protoDef, def.qualifiedName))
   }
 
-  private flattenImportOrExport(def: QuintImport | QuintExport): FlatDef[] {
+  private flattenImportOrExport(def: QuintImport | QuintExport): QuintDef[] {
     const qualifiedName = def.defName ? undefined : def.qualifiedName ?? def.protoName
 
     const protoModule = this.importedModules.get(def.protoName)
@@ -249,24 +252,15 @@ class Flatenner {
       this.importedModules.set(qualifiedName, { ...protoModule, name: qualifiedName })
     }
 
-    const defsToFlatten = filterDefs(protoModule.defs, def.defName)
+    const defsToFlatten = filterDefs(protoModule.declarations.filter(isDef), def.defName)
 
     return defsToFlatten.map(protoDef => this.copyDef(protoDef, qualifiedName))
   }
 
-  private copyDef(def: QuintDef, qualifier: string | undefined): FlatDef {
-    if (!isFlat(def)) {
-      throw new Error(`Impossible: ${definitionToString(def)} should have been flattened already`)
-    }
-
+  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)
 
-    if (!isFlat(defWithNewId)) {
-      // safe cast
-      throw new Error(`Impossible: updating definitions cannot unflatten a def: ${definitionToString(defWithNewId)}`)
-    }
-
     return defWithNewId
   }
 }
@@ -276,7 +270,7 @@ function filterDefs(defs: QuintDef[], name: string | undefined): QuintDef[] {
     return defs
   }
 
-  return defs.filter(def => isFlat(def) && def.name === name)
+  return defs.filter(def => def.name === name)
 }
 
 function resolveNamesOrThrow(currentTable: LookupTable, sourceMap: Map<bigint, Loc>, module: QuintModule): LookupTable {