refactor: replace lodash.isequal with node:util.isDeepStrictEqual, #1606

CONTRIBUTING.md

@@ -1,6 +1,6 @@
 # Contributing
 
-Welcome to the Quint  repository! We are excited that you  want to contribute to
+Welcome to the Quint repository! We are excited that you want to contribute to
 Quint, whether it is by reporting issues, suggesting features, or writing code.
 
 ## Table of Contents
@@ -78,7 +78,7 @@ This repository hosts all Quint pieces:
 - [ADR002: Error
   codes](./docs/content/docs/development-docs/architecture-decision-records/adr002-errors.md)
 - [ADR003: Interface to visit Internal Representation
-   components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md)
+  components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md)
 - [ADR004: An Effect System for
   Quint](./docs/content/docs/development-docs/architecture-decision-records/adr004-effect-system.md)
 - [ADR005: A Type System for
@@ -280,14 +280,14 @@ ln -s $PWD/vscode/quint-vscode/ $HOME/.vscode/extensions/informal.quint-vscode-X
 
 We use `yalc` to manage unpublished packages. To install it, run
 
-``` sh
+```sh
 npm i yalc -g
 ```
 
 Then use the `local` make target to replace the published version of `quint`
 with the local one and build the extension:
 
-``` sh
+```sh
 make local
 ```
 
@@ -308,13 +308,13 @@ Write unit tests in [quint/test](./quint/test), add test data to
 [quint/testFixture](./quint/testFixture). To run the tests and check code
 coverage, run the following commands (in the [quint](./quint) folder):
 
- 1. Run unit tests:
+1.  Run unit tests:
 
     ```sh
     npm run test
     ```
 
- 1. Check code coverage with tests:
+1.  Check code coverage with tests:
 
     ```sh
     npm run coverage
@@ -326,7 +326,7 @@ When adding a new test fixture or updating an existing one, you might need to
 generate the `.json` and `.map.json` files used in test expectations. For that,
 run:
 
-``` sh
+```sh
 npm run update-fixtures
 ```
 
@@ -365,10 +365,10 @@ The files containing tests for `txm` are:
 
 Run integration tests:
 
-  ```sh
-  npm run compile && npm link && npm run integration
-  ```
-  
+```sh
+npm run compile && npm link && npm run integration
+```
+
 PS: this will not run the Apalache-related tests, as they usually won't break as
 consequences of changes in the Quint codebase. They are run in the CI, and you
 can run them locally by running `npm run apalache-integration` and `npm run
@@ -388,7 +388,7 @@ To [add a new dependency for integration tests or other development
 purposes](https://docs.npmjs.com/specifying-dependencies-and-devdependencies-in-a-package-json-file)
 run:
 
-``` sh
+```sh
 npm install <dep> --save-dev
 ```
 
@@ -402,7 +402,7 @@ To [add a new dependency for integration tests or other development
 purposes](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html)
 run:
 
-``` sh
+```sh
 cargo add <dep> --dev
 ```
 
@@ -436,7 +436,7 @@ lose the advantage of exhaustiveness checking. Here's an example:
 Assume we have a type `T`
 
 ```typescript
-type T = 'a' | 'b' | 'c'
+type T = 'a' | 'b' | 'c';
 ```
 
 We should structure our program such that
@@ -445,7 +445,7 @@ We should structure our program such that
 - whenever a new alternative is added to this type, the type system will warn us
   about all the places we need to account for the new kind of data.
 
-If we use `T` with a `switch` or `if`/`then` statement that *returns values*,
+If we use `T` with a `switch` or `if`/`then` statement that _returns values_,
 this indispensable help is ensured. E.g., if we try to write the following:
 
 ```typescript
@@ -535,15 +535,15 @@ false
 false
 ```
 
-For this reason, we are using `isEqual` provided by the [lodash.isequal][]
+For this reason, we are using `isEqual` provided by the [node:util][]
 package:
 
 ```js
 > import { none, just } from '@sweet-monads/maybe'
-> import isEqual from 'lodash.isequal'
-> isEqual(just(true), just(true))
+> import { isDeepStrictEqual } from 'node:util'
+> isDeepStrictEqual(just(true), just(true))
 true
-> isEqual(none(), none())
+> isDeepStrictEqual(none(), none())
 true
 ```
 
@@ -606,7 +606,7 @@ the Rust evaluator and the VSCode extension + the language server.
 
   This will trigger the release and publication of the package to npm and
   GitHub.
-  
+
 ### Evaluator
 
 The evaluator is the latest addition to the Quint repository, and it's release

quint/package.json

@@ -67,7 +67,6 @@
     "line-column": "^1.0.2",
     "lodash": "^4.17.21",
     "lodash.clonedeep": "4.5.0",
-    "lodash.isequal": "^4.5.0",
     "seedrandom": "^3.0.5",
     "tar": "^6.1.14",
     "yargs": "^17.7.2"

quint/src/effects/base.ts

@@ -17,7 +17,7 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { Substitutions, applySubstitution, applySubstitutionToEntity, compose } from './substitutions'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree'
 import { flattenUnions, simplify } from './simplification'
-import isEqual from 'lodash.isequal'
+import { isDeepStrictEqual } from 'node:util'
 import { differenceWith, intersectionWith } from 'lodash'
 
 /* Kinds for concrete effect components */
@@ -332,7 +332,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
   const location = `Trying to unify entities [${entityToString(v1)}] and [${entityToString(v2)}]`
 
   if (v1.kind === 'concrete' && v2.kind === 'concrete') {
-    if (isEqual(new Set(v1.stateVariables.map(v => v.name)), new Set(v2.stateVariables.map(v => v.name)))) {
+    if (isDeepStrictEqual(new Set(v1.stateVariables.map(v => v.name)), new Set(v2.stateVariables.map(v => v.name)))) {
       return right([])
     } else {
       return left({
@@ -349,7 +349,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
     return right(bindEntity(v1.name, v2))
   } else if (v2.kind === 'variable') {
     return right(bindEntity(v2.name, v1))
-  } else if (isEqual(v1, v2)) {
+  } else if (isDeepStrictEqual(v1, v2)) {
     return right([])
   } else if (v1.kind === 'union' && v2.kind === 'concrete') {
     return mergeInMany(v1.entities.map(v => unifyEntities(v, v2)))
@@ -358,10 +358,10 @@ export function unifyEntities(va: Entity, vb: Entity): Either<ErrorTree, Substit
   } else if (v1.kind === 'concrete' && v2.kind === 'union') {
     return unifyEntities(v2, v1)
   } else if (v1.kind === 'union' && v2.kind === 'union') {
-    const intersection = intersectionWith(v1.entities, v2.entities, isEqual)
+    const intersection = intersectionWith(v1.entities, v2.entities, isDeepStrictEqual)
     if (intersection.length > 0) {
-      const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isEqual) }
-      const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isEqual) }
+      const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isDeepStrictEqual) }
+      const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isDeepStrictEqual) }
 
       // There was an intersection, try to unify the remaining entities
       return unifyEntities(s1, s2)

quint/src/effects/modeChecker.ts

@@ -13,7 +13,7 @@
  * @module
  */
 
-import isEqual from 'lodash.isequal'
+import { isDeepStrictEqual } from 'node:util'
 import { qualifierToString } from '../ir/IRprinting'
 import { IRVisitor, walkDeclaration } from '../ir/IRVisitor'
 import { QuintError } from '../quintError'
@@ -248,15 +248,15 @@ function addedEntities(paramEntities: Entity[], resultEntity: Entity): Entity[]
     case 'union':
       return resultEntity.entities.flatMap(entity => addedEntities(paramEntities, entity))
     case 'concrete': {
-      const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isEqual(p, v)))
+      const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isDeepStrictEqual(p, v)))
       if (vars.length === 0) {
         return []
       }
 
       return [{ kind: 'concrete', stateVariables: vars }]
     }
     case 'variable':
-      return !paramEntities.some(p => isEqual(p, resultEntity)) ? [resultEntity] : []
+      return !paramEntities.some(p => isDeepStrictEqual(p, resultEntity)) ? [resultEntity] : []
   }
 }
 

quint/src/effects/simplification.ts

@@ -12,8 +12,7 @@
  * @module
  */
 
-import isEqual from 'lodash.isequal'
-import { unreachable } from '../util'
+import { isEqual, unreachable } from '../util'
 import { ConcreteEffect, Effect, Entity, StateVariable } from './base'
 
 /**
@@ -100,7 +99,7 @@ function deduplicateEntity(entity: Entity): Entity {
       const nestedEntities = entity.entities.map(v => deduplicateEntity(v))
       const unique: Entity[] = []
       nestedEntities.forEach(entity => {
-        if (!unique.some(v => isEqual(v, entity))) {
+        if (!unique.some(v => isDeepStrictEqual(v, entity))) {
           unique.push(entity)
         }
       })

quint/src/effects/substitutions.ts

@@ -88,7 +88,7 @@ export function applySubstitution(subs: Substitutions, e: Effect): Either<ErrorT
   }
 
   return result.map(simplify).chain(r => {
-    if (!isEqual(r, e)) {
+    if (!isDeepStrictEqual(r, e)) {
       // Keep re-applying the substitutions until the effect is unchanged.
       // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ]
       return applySubstitution(subs, r)

quint/src/runtime/impl/nondet.ts

@@ -92,7 +92,7 @@ export function evalNondet(
         }
 
         // Retry if condition is satisfied and we haven't exhausted all possible positions.
-      } while (shouldRetry && !isEqual(newPositions, originalPositions))
+      } while (shouldRetry && !isDeepStrictEqual(newPositions, originalPositions))
 
       // Reset the cache
       cache.value = undefined

quint/src/types/substitutions.ts

@@ -113,7 +113,7 @@ export function applySubstitution(table: LookupTable, subs: Substitutions, t: Qu
   }
 
   const result = singleApplication()
-  if (isEqual(result, t)) {
+  if (isDeepStrictEqual(result, t)) {
     return t
   } else {
     return applySubstitution(table, subs, result)

quint/src/util.ts

@@ -56,7 +56,7 @@ export function zip<A, B>(a: A[], b: B[]): [A, B][] {
  *
  * ```
  * const result = findMap([1,2,3], (x) => x % 2 === 0 ? just(x) : none<int>())
- * lodash.isEqual(result, just(2))
+ * lodash.isDeepStrictEqual(result, just(2))
  * ```
  * */
 export function findMap<X, Y>(xs: Iterable<X>, f: (x: X) => Maybe<Y>): Maybe<Y> {