Merge pull request #1498 from informalsystems/gabriela/fix-windows-so…

…urces

Fix file source resolution in Windows

CHANGELOG.md

@@ -60,6 +60,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Bumped GRPC message sizes to 1G (#1480)
 - Fix format of ITF trace emitted by `verify` command (#1448)
 - Relax uppercase check for types qualified with a namespace (#1494)
+- Fixed file loading from imports on Windows (#1498)
 
 ### Security
 

examples/cosmos/ics20/bank.qnt

@@ -14,6 +14,7 @@
  */
 
 module bank {
+  import basicSpells.* from "../../spells/basicSpells"
   import base.* from "./base"
 
   /* ***************************************************************************
@@ -48,7 +49,7 @@ module bank {
 
   // Get balances of all denominations in the given account `addr`.
   pure def getBalances(accounts: Accounts, addr: Address) : TokenBalances = {
-    if (accounts.keys().contains(addr)) {
+    if (accounts.has(addr)) {
       accounts.get(addr)
     } else {
       Map()
@@ -57,7 +58,7 @@ module bank {
 
   // Get the amount of tokens of denomination `denom` in `balances`.
   pure def getBalance(balances: TokenBalances, denom: Denomination): Amount = {
-    if (balances.keys().contains(denom)) balances.get(denom) else 0
+    if (balances.has(denom)) balances.get(denom) else 0
   }
 
   /* Return `accounts`, where `address` is updated to hold

examples/cosmos/ics20/base.qnt

@@ -36,18 +36,6 @@ module base {
     { baseDenom: baseDenom, path: [] }
   }
 
-  // TODO(#879): Remove and import ../../spells/basicSpells
-  // The following is only here to work around a failing integration test on Windows.
-
-  /// Test whether a key is present in a map
-  ///
-  /// - @param __map a map to query
-  /// - @param __key the key to look for
-  /// - @returns true if and only __map has an entry associated with __key
-  pure def has(__map: a -> b, __key: a): bool = {
-    __map.keys().contains(__key)
-  }
-
   /// Test whether a set is non-empty
   ///
   /// - @param __set a map to query

examples/cosmos/ics20/ics20.qnt

@@ -191,6 +191,7 @@ module ics20 {
 }
 
 module ics20Test {
+  import basicSpells.* from "../../spells/basicSpells"
   import base.* from "./base"
   import bank.getBalance from "./bank"
   import bank.getBalances from "./bank"

quint/src/index.ts

@@ -21,7 +21,7 @@ export { findExpressionWithId, findTypeWithId, findDefinitionWithId } from './ir
 export * from './quintAnalyzer'
 export * from './quintError'
 export { newIdGenerator, IdGenerator } from './idGenerator'
-export { fileSourceResolver, stringSourceResolver } from './parsing/sourceResolver'
+export { fileSourceResolver } from './parsing/sourceResolver'
 export { format } from './prettierimp'
 export { prettyQuintEx, prettyTypeScheme, prettyQuintDeclaration } from './graphics'
 export { Loc } from './ErrorMessage'

quint/src/parsing/sourceResolver.ts

@@ -13,9 +13,8 @@
  * @module
  */
 import { Either, left, right } from '@sweet-monads/either'
-import { dirname } from 'path'
+import { dirname, join, normalize, posix } from 'path'
 import { readFileSync } from 'fs'
-import { posix } from 'path'
 import { lf } from 'eol'
 
 /**
@@ -90,7 +89,7 @@ export function fileSourceResolver(
   return {
     lookupPath: (basepath: string, importPath: string) => {
       return {
-        normalizedPath: posix.join(basepath, importPath),
+        normalizedPath: normalize(join(basepath, importPath)),
         toSourceName: () => {
           return replacer(posix.join(basepath, importPath))
         },
@@ -112,34 +111,3 @@ export function fileSourceResolver(
     },
   }
 }
-
-/**
- * Read the source code from a map of strings. This resolver is especially
- * useful for tests.
- * @param sources a map of paths mapped to text
- * @returns a static resolver that uses the map to read the contents.
- */
-export const stringSourceResolver = (sources: Map<string, string>): SourceResolver => {
-  return {
-    lookupPath: (stempath: string, importPath: string) => {
-      return {
-        normalizedPath: posix.join(stempath, importPath),
-        toSourceName: () => {
-          return posix.join(stempath, importPath)
-        },
-      }
-    },
-
-    load: (lookupPath: SourceLookupPath): Either<string, string> => {
-      // We are using nodejs path.join here.
-      // If we have to decouple this resolver from nodejs in the future,
-      // we would have to write our own version of join.
-      const contents = sources.get(lookupPath.normalizedPath)
-      return contents ? right(contents) : left(`Source not found: '${lookupPath.normalizedPath}'`)
-    },
-
-    stempath: (lookupPath: SourceLookupPath): string => {
-      return dirname(lookupPath.normalizedPath)
-    },
-  }
-}

quint/test/parsing/sourceResolver.test.ts

@@ -3,7 +3,7 @@ import { assert } from 'chai'
 import { left, right } from '@sweet-monads/either'
 import { resolve } from 'path'
 
-import { fileSourceResolver, stringSourceResolver } from '../../src/parsing/sourceResolver'
+import { fileSourceResolver } from '../../src/parsing/sourceResolver'
 import { readFileSync } from 'fs'
 import { lf } from 'eol'
 
@@ -17,14 +17,14 @@ function readQuint(name: string): string {
 }
 
 describe('resolve sources from files', () => {
-  it('parses empty module', () => {
+  it('resolves relative path on same dir', () => {
     const expected = readQuint('./_0001emptyModule')
     const r = fileSourceResolver()
     const result = r.load(r.lookupPath(basename, './_0001emptyModule.qnt'))
     assert.deepEqual(result, right(expected))
   })
 
-  it('parses via ..', () => {
+  it('resolves relative path on parent dir', () => {
     const expected = readQuint('./_0001emptyModule')
     const r = fileSourceResolver()
     const result = r.load(r.lookupPath(basename, '../testFixture/_0001emptyModule.qnt'))
@@ -34,61 +34,14 @@ describe('resolve sources from files', () => {
   it('errors on non-existant', () => {
     const r = fileSourceResolver()
     const result = r.load(r.lookupPath(basename, 'does-not-exist'))
-    assert.deepEqual(result, left(`ENOENT: no such file or directory, open '${basename}/does-not-exist'`))
+    const filenameInError = resolve(basename, 'does-not-exist')
+    assert.deepEqual(result, left(`ENOENT: no such file or directory, open '${filenameInError}'`))
   })
 
   it('stemname', () => {
     const r = fileSourceResolver()
     const result = r.stempath(r.lookupPath(`${basename}/testFixture`, './_0001emptyModule.qnt'))
-    assert.deepEqual(result, `${basename}/testFixture`)
-  })
-})
-
-// a static table that contains sources in strings
-const staticTable = new Map<string, string>([
-  ['/foo.qnt', 'module foo {}'],
-  ['/bar.qnt', 'module bar {}'],
-  ['/baz/baz.qnt', 'module baz {}'],
-])
-
-describe('resolve sources from strings', () => {
-  it('parses foo', () => {
-    const expected = staticTable.get('/foo.qnt')
-    const r = stringSourceResolver(staticTable)
-    const result = r.load(r.lookupPath('/', './foo.qnt'))
-    assert.deepEqual(result, right(expected))
-  })
-
-  it('parses bar via ..', () => {
-    const expected = staticTable.get('/bar.qnt')
-    const r = stringSourceResolver(staticTable)
-    const result = r.load(r.lookupPath('/', './baz/../bar.qnt'))
-    assert.deepEqual(result, right(expected))
-  })
-
-  it('parses baz via baz/baz.qnt', () => {
-    const expected = staticTable.get('/baz/baz.qnt')
-    const r = stringSourceResolver(staticTable)
-    const result = r.load(r.lookupPath('/', './baz/baz.qnt'))
-    assert.deepEqual(result, right(expected))
-  })
-
-  it('parses baz via baz.qnt', () => {
-    const expected = staticTable.get('/baz/baz.qnt')
-    const r = stringSourceResolver(staticTable)
-    const result = r.load(r.lookupPath('/baz', './baz.qnt'))
-    assert.deepEqual(result, right(expected))
-  })
-
-  it('errors on non-existant', () => {
-    const r = stringSourceResolver(staticTable)
-    const result = r.load(r.lookupPath('/', 'does-not-exist'))
-    assert.deepEqual(result, left(`Source not found: '/does-not-exist'`))
-  })
-
-  it('stemname', () => {
-    const r = stringSourceResolver(staticTable)
-    const result = r.stempath(r.lookupPath('/baz', './baz.qnt'))
-    assert.deepEqual(result, '/baz')
+    const expected = resolve(basename, 'testFixture')
+    assert.deepEqual(result, expected)
   })
 })

quint/test/runtime/compile.test.ts

@@ -5,7 +5,7 @@ import { newTraceRecorder } from '../../src/runtime/trace'
 import { dedent } from '../textUtils'
 import { newIdGenerator } from '../../src/idGenerator'
 import { newRng } from '../../src/rng'
-import { stringSourceResolver } from '../../src/parsing/sourceResolver'
+import { fileSourceResolver } from '../../src/parsing/sourceResolver'
 import { QuintEx, parseExpressionOrDeclaration, quintErrorToString, walkExpression } from '../../src'
 import { parse } from '../../src/parsing/quintParserFrontend'
 import { Evaluator } from '../../src/runtime/impl/evaluator'
@@ -29,7 +29,7 @@ function assertResultAsString(input: string, expected: string | undefined, evalC
 }
 
 function prepareEvaluator(input: string, evalContext: string): [Evaluator, QuintEx] {
-  const mockLookupPath = stringSourceResolver(new Map()).lookupPath('/', './mock')
+  const mockLookupPath = fileSourceResolver(new Map()).lookupPath('/', './mock')
   const { resolver, sourceMap } = parse(idGen, '<test>', mockLookupPath, `module contextM { ${evalContext} }`)
 
   const parseResult = parseExpressionOrDeclaration(input, '<input>', idGen, sourceMap)

vscode/quint-vscode/server/test/util.ts

@@ -16,11 +16,11 @@ import {
   Loc,
   LookupTable,
   QuintModule,
+  fileSourceResolver,
   newIdGenerator,
   parsePhase1fromText,
   parsePhase2sourceResolution,
   parsePhase3importAndNameResolution,
-  stringSourceResolver,
 } from '@informalsystems/quint'
 
 /**
@@ -37,7 +37,7 @@ export function parseOrThrow(moduleText: string): [QuintModule[], Map<bigint, Lo
   const idgen = newIdGenerator()
   const phase1Data = parsePhase1fromText(idgen, moduleText, 'mocked_path')
 
-  const resolver = stringSourceResolver(new Map())
+  const resolver = fileSourceResolver(new Map())
   const mainPath = resolver.lookupPath('mocked_path', './main')
   const phase2Data = parsePhase2sourceResolution(idgen, resolver, mainPath, phase1Data)