Simplify the composition algorithm

quint/src/effects/substitutions.ts

@@ -14,9 +14,10 @@
 
 import { Either, mergeInMany, right } from '@sweet-monads/either'
 import { ErrorTree, buildErrorTree } from '../errorTree'
-import { Effect, Entity, unify, unifyEntities } from './base'
+import { Effect, Entity } from './base'
 import { effectToString, substitutionsToString } from './printing'
 import { simplify } from './simplification'
+import { isEqual } from 'lodash'
 
 /*
  * Substitutions can be applied to both effects and entities, replacing
@@ -37,7 +38,7 @@ type Substitution = { kind: 'entity'; name: string; value: Entity } | { kind: 'e
  */
 export function compose(s1: Substitutions, s2: Substitutions): Either<ErrorTree, Substitutions> {
   return applySubstitutionsToSubstitutions(s1, s2)
-    .chain(sa => applySubstitutionsToSubstitutions(sa, s1).map((sb: Substitutions) => sb.concat(sa)))
+    .map((sb: Substitutions) => sb.concat(s1))
     .mapLeft(error =>
       buildErrorTree(`Composing substitutions ${substitutionsToString(s1)} and ${substitutionsToString(s2)}`, error)
     )
@@ -86,7 +87,14 @@ export function applySubstitution(subs: Substitutions, e: Effect): Either<ErrorT
     }
   }
 
-  return result.map(simplify)
+  return result.map(simplify).chain(r => {
+    if (!isEqual(r, e)) {
+      // Keep reaplying the substitutions until the effect is unchanged.
+      // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ]
+      return applySubstitution(subs, r)
+    }
+    return right(r)
+  })
 }
 
 /**
@@ -130,23 +138,6 @@ function emptyEntity(entity: Entity): boolean {
 function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions): Either<ErrorTree[], Substitutions> {
   return mergeInMany(
     s2.map((s: Substitution): Either<ErrorTree, Substitutions> => {
-      const sub = s1.find(sub => s.name === sub.name)
-      if (sub) {
-        if (sub.kind === 'effect' && s.kind === 'effect') {
-          return unify(s.value, sub.value).mapLeft(err =>
-            buildErrorTree(`Unifying substitutions with same name: ${s.name}`, err)
-          )
-        } else if (sub.kind === 'entity' && s.kind === 'entity') {
-          return unifyEntities(s.value, sub.value).mapLeft(err =>
-            buildErrorTree(`Unifying substitutions with same name: ${s.name}`, err)
-          )
-        } else {
-          throw new Error(
-            `Substitutions with same name (${s.name}) but incompatible kinds: ${substitutionsToString([sub, s])}`
-          )
-        }
-      }
-
       switch (s.kind) {
         case 'effect':
           return applySubstitution(s1, s.value).map(v => [{ kind: s.kind, name: s.name, value: v }])

quint/test/effects/inferrer.test.ts

@@ -176,6 +176,48 @@ describe('inferEffects', () => {
     assert.deepEqual(effectForDef(defs, effects, 'a'), expectedEffect)
   })
 
+  it('keeps track of substitutions with lambdas and applications', () => {
+    const defs = [
+      `pure def MinBy(__set: Set[a], __f: a => int, __i: a): a = {
+        __set.fold(
+          __i,
+          (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e}
+        )
+      }`,
+    ]
+
+    const [errors, effects] = inferEffectsForDefs(defs)
+
+    const expectedEffect = '∀ v0, v1 . (Read[v0], (Read[v0]) => Read[v1], Read[v0]) => Read[v0, v1]'
+
+    assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
+    assert.deepEqual(effectForDef(defs, effects, 'MinBy'), expectedEffect)
+  })
+
+  it('regression on #1091', () => {
+    const defs = [
+      'var channel: int',
+      `action CoolAction(boolean: bool): bool =
+         any {
+           all {
+             boolean,
+             channel' = channel
+           },
+           all {
+             not(boolean),
+             channel' = channel
+           }
+        }`,
+    ]
+
+    const [errors, effects] = inferEffectsForDefs(defs)
+
+    const expectedEffect = "∀ v0 . (Read[v0]) => Read[v0, 'channel'] & Update['channel']"
+
+    assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
+    assert.deepEqual(effectForDef(defs, effects, 'CoolAction'), expectedEffect)
+  })
+
   it('returns error when operator signature is not unifiable with args', () => {
     const defs = [`def a = S.map(p => x' = p)`]
 
@@ -196,14 +238,15 @@ describe('inferEffects', () => {
                         message: 'Expected [x] and [] to be the same',
                       },
                     ],
-                    location: "Trying to unify Read[v5] & Temporal[v6] and Update['x']",
+                    location: "Trying to unify Read[_v4] & Temporal[_v5] and Update['x']",
                   },
                 ],
-                location: "Trying to unify (Pure) => Read[v5] & Temporal[v6] and (Read[v2]) => Read[v2] & Update['x']",
+                location:
+                  "Trying to unify (Pure) => Read[_v4] & Temporal[_v5] and (Read[_v1]) => Read[_v1] & Update['x']",
               },
             ],
             location:
-              "Trying to unify (Read[v3] & Temporal[v4], (Read[v3] & Temporal[v4]) => Read[v5] & Temporal[v6]) => Read[v3, v5] & Temporal[v4, v6] and (Pure, (Read[v2]) => Read[v2] & Update['x']) => e1",
+              "Trying to unify (Read[_v2] & Temporal[_v3], (Read[_v2] & Temporal[_v3]) => Read[_v4] & Temporal[_v5]) => Read[_v2, _v4] & Temporal[_v3, _v5] and (Pure, (Read[_v1]) => Read[_v1] & Update['x']) => _e1",
           },
         ],
         location: 'Trying to infer effect for operator application in map(S, ((p) => assign(x, p)))',

quint/test/effects/substitutions.test.ts

@@ -33,24 +33,4 @@ describe('compose', () => {
 
     assert.isTrue(result.isRight())
   })
-
-  it('unifies values of substitutions with same name', () => {
-    const s1: Substitutions = [
-      { kind: 'entity', name: 'v1', value: { kind: 'concrete', stateVariables: [{ name: 'x', reference: 2n }] } },
-    ]
-    const s2: Substitutions = [{ kind: 'entity', name: 'v1', value: { kind: 'variable', name: 'q' } }]
-
-    const result = compose(s1, s2)
-
-    result.map(r =>
-      assert.sameDeepMembers(
-        r,
-        s1.concat([
-          { kind: 'entity', name: 'q', value: { kind: 'concrete', stateVariables: [{ name: 'x', reference: 2n }] } },
-        ])
-      )
-    )
-
-    assert.isTrue(result.isRight())
-  })
 })