Resolve type applications at the IR level

Author: bugarela

quint/src/quintAnalyzer.ts

@@ -22,6 +22,7 @@ import { ModeChecker } from './effects/modeChecker'
 import { QuintError } from './quintError'
 import { errorTreeToString } from './errorTree'
 import { MultipleUpdatesChecker } from './effects/MultipleUpdatesChecker'
+import { TypeApplicationResolver } from './types/typeApplicationResolution'
 
 /* Products from static analysis */
 export type AnalysisOutput = {
@@ -42,7 +43,7 @@ export type AnalysisResult = [QuintError[], AnalysisOutput]
  */
 export function analyzeModules(lookupTable: LookupTable, quintModules: QuintModule[]): AnalysisResult {
   const analyzer = new QuintAnalyzer(lookupTable)
-  quintModules.map(m => analyzer.analyzeDeclarations(m.declarations))
+  quintModules.forEach(m => (m.declarations = analyzer.analyzeDeclarations(m.declarations)))
   return analyzer.getResult()
 }
 
@@ -75,6 +76,7 @@ export function analyzeInc(
  * @param previousOutput - The previous analysis output to be used as a starting point.
  */
 class QuintAnalyzer {
+  private typeApplicationResolver: TypeApplicationResolver
   private effectInferrer: EffectInferrer
   private typeInferrer: TypeInferrer
   private modeChecker: ModeChecker
@@ -84,17 +86,20 @@ class QuintAnalyzer {
   private output: AnalysisOutput = { types: new Map(), effects: new Map(), modes: new Map() }
 
   constructor(lookupTable: LookupTable, previousOutput?: AnalysisOutput) {
+    this.typeApplicationResolver = new TypeApplicationResolver(lookupTable)
     this.typeInferrer = new TypeInferrer(lookupTable, previousOutput?.types)
     this.effectInferrer = new EffectInferrer(lookupTable, previousOutput?.effects)
     this.multipleUpdatesChecker = new MultipleUpdatesChecker()
     this.modeChecker = new ModeChecker(previousOutput?.modes)
   }
 
-  analyzeDeclarations(decls: QuintDeclaration[]): void {
-    const [typeErrMap, types] = this.typeInferrer.inferTypes(decls)
-    const [effectErrMap, effects] = this.effectInferrer.inferEffects(decls)
+  analyzeDeclarations(decls: QuintDeclaration[]): QuintDeclaration[] {
+    const resolvedDecls = this.typeApplicationResolver.resolveTypeApplications(decls)
+
+    const [typeErrMap, types] = this.typeInferrer.inferTypes(resolvedDecls)
+    const [effectErrMap, effects] = this.effectInferrer.inferEffects(resolvedDecls)
     const updatesErrMap = this.multipleUpdatesChecker.checkEffects([...effects.values()])
-    const [modeErrMap, modes] = this.modeChecker.checkModes(decls, effects)
+    const [modeErrMap, modes] = this.modeChecker.checkModes(resolvedDecls, effects)
 
     const errorTrees = [...typeErrMap, ...effectErrMap]
 
@@ -114,6 +119,8 @@ class QuintAnalyzer {
       effects: new Map([...this.output.effects, ...effects]),
       modes: new Map([...this.output.modes, ...modes]),
     }
+
+    return resolvedDecls
   }
 
   getResult(): AnalysisResult {

quint/src/types/inferrer.ts

@@ -16,21 +16,17 @@
 import { ErrorTree } from '../errorTree'
 import { walkDeclaration } from '../ir/IRVisitor'
 import { LookupTable } from '../names/base'
-import { QuintDeclaration } from '../ir/quintIr'
+import { QuintDeclaration, isDef } from '../ir/quintIr'
 import { TypeScheme } from './base'
 import { ConstraintGeneratorVisitor } from './constraintGenerator'
 import { solveConstraint } from './constraintSolver'
 import { simplify } from './simplification'
-import { TypeApplicationResolver } from './typeApplicationResolution'
-import { transformDeclaration, transformLookupDefinition } from '../ir/IRTransformer'
 
 export type TypeInferenceResult = [Map<bigint, ErrorTree>, Map<bigint, TypeScheme>]
 
 export class TypeInferrer extends ConstraintGeneratorVisitor {
-  private resolver: TypeApplicationResolver
   constructor(table: LookupTable, types?: Map<bigint, TypeScheme>) {
     super(solveConstraint, table, types)
-    this.resolver = new TypeApplicationResolver(this.table, this.freshVarGenerator)
   }
 
   /**
@@ -43,17 +39,8 @@ export class TypeInferrer extends ConstraintGeneratorVisitor {
    */
   inferTypes(declarations: QuintDeclaration[]): TypeInferenceResult {
     // Resolve all type applications used in expressions in the lookup table
-    this.table.forEach((def, id) => {
-      // Don't resolve type definitions, since those should keep their original type variable names
-      // They are our source of truth for all resolutions
-      if (def.kind !== 'typedef') {
-        const resolvedLookupDef = transformLookupDefinition(this.resolver, def)
-        this.table.set(id, resolvedLookupDef)
-      }
-    })
     declarations.forEach(decl => {
-      const resolvedDecl = transformDeclaration(this.resolver, decl)
-      walkDeclaration(this, resolvedDecl)
+      walkDeclaration(this, decl)
     })
     const simplifiedTypes = new Map([...this.types.entries()].map(([id, t]) => [id, simplify(t)]))
     return [this.errors, simplifiedTypes]

quint/src/types/typeApplicationResolution.ts

@@ -14,9 +14,10 @@
 
 import { fail } from 'assert'
 import { FreshVarGenerator } from '../FreshVarGenerator'
+
 import { typeToString } from '../ir/IRprinting'
-import { IRTransformer, transformType } from '../ir/IRTransformer'
-import { QuintTypeAlias } from '../ir/quintIr'
+import { IRTransformer, transformDeclaration, transformLookupDefinition, transformType } from '../ir/IRTransformer'
+import { QuintDeclaration, QuintTypeAlias } from '../ir/quintIr'
 import { QuintAppType, QuintType, QuintVarType, Row } from '../ir/quintTypes'
 import { LookupTable } from '../names/base'
 import { zip } from '../util'
@@ -29,13 +30,22 @@ export class TypeApplicationResolver implements IRTransformer {
   // Lookup table from the parser
   private table: LookupTable
 
-  constructor(table: LookupTable, freshVarGenerator: FreshVarGenerator) {
+  constructor(table: LookupTable) {
     this.table = table
-    this.freshVarGenerator = freshVarGenerator
+    this.freshVarGenerator = new FreshVarGenerator()
+
+    this.table.forEach((def, id) => {
+      const resolvedLookupDef = transformLookupDefinition(this, def)
+      this.table.set(id, resolvedLookupDef)
+    })
+  }
+
+  resolveTypeApplications(decls: QuintDeclaration[]): QuintDeclaration[] {
+    return decls.map(decl => transformDeclaration(this, decl))
   }
 
   exitType(t: QuintType): QuintType {
-    return this.resolveTypeApplications(t)
+    return this.resolveTypeApplicationsForType(t)
   }
 
   // Transforms `t` by resolving all the type applications in all its sub-terms
@@ -46,8 +56,8 @@ export class TypeApplicationResolver implements IRTransformer {
   //   type Bar[x, y] = {i: x, j: y}
   //
   //
-  // resolveTypeApplications(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
-  resolveTypeApplications(t: QuintType): QuintType {
+  // resolveTypeApplicationsForType(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
+  private resolveTypeApplicationsForType(t: QuintType): QuintType {
     const f: (_: QuintType) => QuintType = x => (x.kind !== 'app' ? x : this.resolveTypeApp(x))
     return mapType(f, t)
   }