Merge pull request #1444 from informalsystems/gabriela/soft-unshadowing

Relax unshadowing for let defs

CHANGELOG.md

@@ -13,6 +13,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   Model-Based Testing (#1441).
 
 ### Changed
+
+- Shadowing is a bit less agressive. This should improve readability of variable
+  names after compilation, i.e. in Apalache and some simulation errors, and in
+  TLA+ produced from the `compile` command (#1444).
+
 ### Deprecated
 ### Removed
 ### Fixed

quint/io-cli-tests.md

@@ -811,43 +811,37 @@ rm out-itf-mbt-example.itf.json
   },
   "minter": "bob",
   "nondet_picks": {
-    "amount_189": {
+    "amount": {
       "tag": "Some",
       "value": {
         "#bigint": "111009104957917492842738448433884729279015865072041681905260877596484059410831"
       }
     },
-    "eveToBob_295": {
+    "eveToBob": {
       "tag": "None",
       "value": {
         "#tup": []
       }
     },
-    "mintBob_296": {
+    "mintBob": {
       "tag": "None",
       "value": {
         "#tup": []
       }
     },
-    "mintEve_297": {
+    "mintEve": {
       "tag": "None",
       "value": {
         "#tup": []
       }
     },
-    "receiver_190": {
+    "receiver": {
       "tag": "Some",
       "value": "bob"
     },
-    "sender_191": {
+    "sender": {
       "tag": "Some",
       "value": "bob"
-    },
-    "sender_75": {
-      "tag": "None",
-      "value": {
-        "#tup": []
-      }
     }
   }
 }

quint/src/ir/IRVisitor.ts

@@ -465,6 +465,9 @@ export function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {
       }
       break
     case 'let':
+      if (visitor.definitionDepth !== undefined) {
+        visitor.definitionDepth++
+      }
       if (visitor.enterLet) {
         visitor.enterLet(expr)
       }
@@ -475,6 +478,9 @@ export function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void {
       if (visitor.exitLet) {
         visitor.exitLet(expr)
       }
+      if (visitor.definitionDepth !== undefined) {
+        visitor.definitionDepth--
+      }
       break
     default:
       unreachable(expr)

quint/src/names/base.ts

@@ -43,8 +43,10 @@ export type LookupDefinition = (QuintDef | ({ kind: 'param' } & QuintLambdaParam
    * Some types in `QuintDef` already have a `typeAnnotation` field. This
    * ensures that this field is always accessible */
   typeAnnotation?: QuintType
-  /** optional depth of the definition, 0 if top-level. Only for `QuintOpDef`. */
+  /* optional depth of the definition, 0 if top-level. Only for `QuintOpDef`. */
   depth?: number
+  /* optional flag to tell if this is shadowing another def, therefore needing to be unshadowed during compilation */
+  shadowing?: boolean
 }
 
 /**

quint/src/names/collector.ts

@@ -245,19 +245,21 @@ export class NameCollector implements IRVisitor {
    * than `def.name` (i.e. in import-like statements).
    * @param source - An optional source identifier for the definition, if the
    * source is different than `def.id` (i.e. in import-like statements).
+   *
+   * @returns The definition object that was collected.
    */
-  collectDefinition(def: LookupDefinition, importedFrom?: QuintImport | QuintExport | QuintInstance): void {
+  collectDefinition(def: LookupDefinition, importedFrom?: QuintImport | QuintExport | QuintInstance): LookupDefinition {
     const identifier = (importedFrom as QuintImport)?.defName ?? def.name
     const source = importedFrom?.id ?? def.id
     if (identifier === '_') {
       // Don't collect underscores, as they are special identifiers that allow no usage
-      return
+      return def
     }
 
     if (builtinNames.includes(identifier)) {
       // Conflict with a built-in name
       this.recordConflict(identifier, undefined, source)
-      return
+      return def
     }
 
     def.depth ??= 0
@@ -266,7 +268,7 @@ export class NameCollector implements IRVisitor {
     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
+      return def
     }
 
     // Else: There are exiting defs. We need to check for conflicts
@@ -284,12 +286,10 @@ export class NameCollector implements IRVisitor {
     // 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 }])
-    )
+    const newDef = { ...addNamespacesToDef(def, namespaces), importedFrom, shadowing: existingEntries.length > 0 }
+    this.definitionsByName.set(identifier, existingEntries.filter(entry => entry.id !== def.id).concat([newDef]))
+
+    return newDef
   }
 
   /**

quint/src/names/resolver.ts

@@ -75,11 +75,12 @@ class NameResolver implements IRVisitor {
     // Top-level definitions were already collected, so we only need to collect
     // scoped definitions.
     if (this.definitionDepth > 0) {
-      this.collector.collectDefinition({ ...def, depth: this.definitionDepth })
+      const newDef = this.collector.collectDefinition({ ...def, depth: this.definitionDepth })
+      this.table.set(def.id, { ...newDef, depth: this.definitionDepth })
+    } else {
+      // Map the definition to itself so we can recover depth information from the table
+      this.table.set(def.id, { ...def, depth: this.definitionDepth })
     }
-
-    // Map the definition to itself so we can recover depth information from the table
-    this.table.set(def.id, { ...def, depth: this.definitionDepth })
   }
 
   exitLet(expr: QuintLet): void {

quint/src/names/unshadower.ts

@@ -19,7 +19,7 @@ import { QuintApp, QuintLambda, QuintLambdaParameter, QuintLet, QuintModule, Qui
 /**
  * Replace all names with unique names, to avoid shadowing.
  * - Lambda parameters are renamed to `<name>_<lambda-id>`
- * - Nested definitions (from let expressions) are renamed to `<name>_<let-id>`
+ * - Nested definitions (from let expressions) are renamed to `<name>_<let-id>` only if they shadow another name
  *
  * @param module The module to unshadow
  * @param lookupTable The lookup table with the module's name references
@@ -41,6 +41,9 @@ class Unshadower implements IRTransformer {
 
   enterLambda(lambda: QuintLambda): QuintLambda {
     const newParams: QuintLambdaParameter[] = lambda.params.map(p => {
+      // Ideally, we should only rename if `this.lookupTable.get(p.id)?.shadowing` is true, as we do in let.
+      // However, this currently is a problem with Apalache, see issue #1443.
+
       const newName = `${p.name}_${lambda.id}`
       this.nestedNames.set(p.id, newName)
 
@@ -50,6 +53,11 @@ class Unshadower implements IRTransformer {
   }
 
   enterLet(expr: QuintLet): QuintLet {
+    if (!this.lookupTable.get(expr.opdef.id)?.shadowing) {
+      // nothing to do
+      return expr
+    }
+
     const newName = `${expr.opdef.name}_${expr.id}`
     this.nestedNames.set(expr.opdef.id, newName)
 

quint/test/names/resolver.test.ts

@@ -103,8 +103,22 @@ describe('resolveNames', () => {
       )
 
       assert.isEmpty(result.errors)
-      assert.isTrue([...result.table.values()].some(def => def.name === 'shadowing' || def.kind === 'def'))
-      assert.isTrue([...result.table.values()].some(def => def.name === 'shadowing' || def.kind === 'param'))
+      assert.isTrue([...result.table.values()].some(def => def.name === 'shadowing' && def.kind === 'def'))
+      assert.isTrue([...result.table.values()].some(def => def.name === 'shadowing' && def.kind === 'param'))
+    })
+
+    it('collects depth and shadowing information properly', () => {
+      const result = resolveNamesForDefs(['val shadowing = val a = 1 { val a = 2 { a } }'], newIdGenerator())
+
+      assert.isEmpty(result.errors)
+      assert.isTrue(
+        [...result.table.values()].some(def => def.name === 'a' && def.depth === 2),
+        'Could not find first a'
+      )
+      assert.isTrue(
+        [...result.table.values()].some(def => def.name === 'a' && def.depth === 3 && def.shadowing === true),
+        'Could not find second a'
+      )
     })
   })
 

quint/test/names/unshadower.test.ts

@@ -21,8 +21,11 @@ describe('unshadowNames', () => {
   it('returns a module with no shadowed names', () => {
     const { modules, table } = parseModules(`
       module A {
-        def f(a) = a > 0
         val b = val a = 1 { a }
+        val c = val a = { val a = 1 { a } } { a }
+        val d = val a = 1 { val a = 2 { a } }
+        def f(a) = a > 0
+        def g(a) = a.map(a => a + 1)
       }
 
       module B {
@@ -34,8 +37,11 @@ describe('unshadowNames', () => {
 
     assert.sameDeepMembers(unshadowedModules.map(moduleToString), [
       dedent(`module A {
-             |  val b = val a_10 = 1 { a_10 }
-             |  def f = ((a_5) => igt(a_5, 0))
+             |  val d = val a = 1 { val a_19 = 2 { a_19 } }
+             |  def f = ((a_26) => igt(a_26, 0))
+             |  def g = ((a_36) => map(a_36, ((a_34) => iadd(a_34, 1))))
+             |  val b = val a = 1 { a }
+             |  val c = val a = val a_9 = 1 { a_9 } { a }
              |}`),
       dedent(`module B {
               |  var a: int

quint/testFixture/_0099unorderedDefs.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":14,"name":"unorderedDefs","declarations":[{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}}},{"id":6,"kind":"def","name":"double","qualifier":"puredef","expr":{"id":5,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":4,"kind":"app","opcode":"plus","args":[{"id":2,"kind":"name","name":"x"},{"id":3,"kind":"name","name":"x"}]}}}]}],"table":{"2":{"id":1,"name":"x","kind":"param","depth":1},"3":{"id":1,"name":"x","kind":"param","depth":1},"4":{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}},"depth":0},"6":{"id":6,"kind":"def","name":"double","qualifier":"puredef","expr":{"id":5,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":4,"kind":"app","opcode":"plus","args":[{"id":2,"kind":"name","name":"x"},{"id":3,"kind":"name","name":"x"}]}},"depth":0},"9":{"id":7,"name":"x","kind":"param","depth":1},"10":{"id":8,"name":"y","kind":"param","depth":1},"13":{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}},"depth":0}},"errors":[]}
+{"stage":"parsing","warnings":[],"modules":[{"id":14,"name":"unorderedDefs","declarations":[{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}}},{"id":6,"kind":"def","name":"double","qualifier":"puredef","expr":{"id":5,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":4,"kind":"app","opcode":"plus","args":[{"id":2,"kind":"name","name":"x"},{"id":3,"kind":"name","name":"x"}]}}}]}],"table":{"2":{"id":1,"name":"x","kind":"param","depth":1},"3":{"id":1,"name":"x","kind":"param","depth":1},"4":{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}},"depth":0},"6":{"id":6,"kind":"def","name":"double","qualifier":"puredef","expr":{"id":5,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":4,"kind":"app","opcode":"plus","args":[{"id":2,"kind":"name","name":"x"},{"id":3,"kind":"name","name":"x"}]}},"depth":0},"9":{"id":7,"name":"x","kind":"param","depth":1,"shadowing":false},"10":{"id":8,"name":"y","kind":"param","depth":1},"13":{"id":13,"kind":"def","name":"plus","qualifier":"puredef","expr":{"id":12,"kind":"lambda","params":[{"id":7,"name":"x"},{"id":8,"name":"y"}],"qualifier":"puredef","expr":{"id":11,"kind":"app","opcode":"iadd","args":[{"id":9,"kind":"name","name":"x"},{"id":10,"kind":"name","name":"y"}]}},"depth":0}},"errors":[]}

quint/testFixture/_0100cyclicDefs.json

@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"modules":[{"id":16,"name":"cyclicDefs","declarations":[]}],"table":{"2":{"id":1,"name":"x","kind":"param","depth":1},"3":{"id":10,"kind":"def","name":"bar","qualifier":"puredef","expr":{"id":9,"kind":"lambda","params":[{"id":6,"name":"x"}],"qualifier":"puredef","expr":{"id":8,"kind":"app","opcode":"baz","args":[{"id":7,"kind":"name","name":"x"}]}},"depth":0},"5":{"id":5,"kind":"def","name":"foo","qualifier":"puredef","expr":{"id":4,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":3,"kind":"app","opcode":"bar","args":[{"id":2,"kind":"name","name":"x"}]}},"depth":0},"7":{"id":6,"name":"x","kind":"param","depth":1},"8":{"id":15,"kind":"def","name":"baz","qualifier":"puredef","expr":{"id":14,"kind":"lambda","params":[{"id":11,"name":"x"}],"qualifier":"puredef","expr":{"id":13,"kind":"app","opcode":"foo","args":[{"id":12,"kind":"name","name":"x"}]}},"depth":0},"10":{"id":10,"kind":"def","name":"bar","qualifier":"puredef","expr":{"id":9,"kind":"lambda","params":[{"id":6,"name":"x"}],"qualifier":"puredef","expr":{"id":8,"kind":"app","opcode":"baz","args":[{"id":7,"kind":"name","name":"x"}]}},"depth":0},"12":{"id":11,"name":"x","kind":"param","depth":1},"13":{"id":5,"kind":"def","name":"foo","qualifier":"puredef","expr":{"id":4,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":3,"kind":"app","opcode":"bar","args":[{"id":2,"kind":"name","name":"x"}]}},"depth":0},"15":{"id":15,"kind":"def","name":"baz","qualifier":"puredef","expr":{"id":14,"kind":"lambda","params":[{"id":11,"name":"x"}],"qualifier":"puredef","expr":{"id":13,"kind":"app","opcode":"foo","args":[{"id":12,"kind":"name","name":"x"}]}},"depth":0}},"errors":[{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":2,"col":2,"index":70},"end":{"line":2,"col":25,"index":93}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":3,"col":2,"index":97},"end":{"line":3,"col":25,"index":120}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":4,"col":2,"index":124},"end":{"line":4,"col":25,"index":147}}]}]}
+{"stage":"parsing","warnings":[],"modules":[{"id":16,"name":"cyclicDefs","declarations":[]}],"table":{"2":{"id":1,"name":"x","kind":"param","depth":1},"3":{"id":10,"kind":"def","name":"bar","qualifier":"puredef","expr":{"id":9,"kind":"lambda","params":[{"id":6,"name":"x"}],"qualifier":"puredef","expr":{"id":8,"kind":"app","opcode":"baz","args":[{"id":7,"kind":"name","name":"x"}]}},"depth":0},"5":{"id":5,"kind":"def","name":"foo","qualifier":"puredef","expr":{"id":4,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":3,"kind":"app","opcode":"bar","args":[{"id":2,"kind":"name","name":"x"}]}},"depth":0},"7":{"id":6,"name":"x","kind":"param","depth":1,"shadowing":false},"8":{"id":15,"kind":"def","name":"baz","qualifier":"puredef","expr":{"id":14,"kind":"lambda","params":[{"id":11,"name":"x"}],"qualifier":"puredef","expr":{"id":13,"kind":"app","opcode":"foo","args":[{"id":12,"kind":"name","name":"x"}]}},"depth":0},"10":{"id":10,"kind":"def","name":"bar","qualifier":"puredef","expr":{"id":9,"kind":"lambda","params":[{"id":6,"name":"x"}],"qualifier":"puredef","expr":{"id":8,"kind":"app","opcode":"baz","args":[{"id":7,"kind":"name","name":"x"}]}},"depth":0},"12":{"id":11,"name":"x","kind":"param","depth":1,"shadowing":false},"13":{"id":5,"kind":"def","name":"foo","qualifier":"puredef","expr":{"id":4,"kind":"lambda","params":[{"id":1,"name":"x"}],"qualifier":"puredef","expr":{"id":3,"kind":"app","opcode":"bar","args":[{"id":2,"kind":"name","name":"x"}]}},"depth":0},"15":{"id":15,"kind":"def","name":"baz","qualifier":"puredef","expr":{"id":14,"kind":"lambda","params":[{"id":11,"name":"x"}],"qualifier":"puredef","expr":{"id":13,"kind":"app","opcode":"foo","args":[{"id":12,"kind":"name","name":"x"}]}},"depth":0}},"errors":[{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":2,"col":2,"index":70},"end":{"line":2,"col":25,"index":93}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":3,"col":2,"index":97},"end":{"line":3,"col":25,"index":120}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":4,"col":2,"index":124},"end":{"line":4,"col":25,"index":147}}]}]}