Update language server with new interfaces

informalsystems · Oct 9, 2023 · 2340955 · 2340955
1 parent 7108cca
commit 2340955
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 15 deletions.
diff --git a/quint/src/index.ts b/quint/src/index.ts
@@ -24,3 +24,4 @@ export { newIdGenerator, IdGenerator } from './idGenerator'
 export { fileSourceResolver, stringSourceResolver } from './parsing/sourceResolver'
 export { format } from './prettierimp'
 export { prettyQuintEx, prettyTypeScheme, prettyQuintDeclaration } from './graphics'
+export { Loc } from './ErrorMessage'
diff --git a/vscode/quint-vscode/server/src/parsing.ts b/vscode/quint-vscode/server/src/parsing.ts
@@ -1,7 +1,6 @@
 import {
   IdGenerator,
   ParserPhase3,
-  QuintError,
   fileSourceResolver,
   parsePhase1fromText,
   parsePhase2sourceResolution,
@@ -10,7 +9,7 @@ import {
 } from '@informalsystems/quint'
 import { basename, dirname } from 'path'
 import { URI } from 'vscode-uri'
-import { assembleDiagnostic } from './reporting'
+import { diagnosticsFromErrors } from './reporting'
 import { TextDocument } from 'vscode-languageserver-textdocument'
 
 export async function parseDocument(idGenerator: IdGenerator, textDocument: TextDocument): Promise<ParserPhase3> {
@@ -32,13 +31,7 @@ export async function parseDocument(idGenerator: IdGenerator, textDocument: Text
       })
       .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data))
       .chain(phase3Data => parsePhase4toposort(phase3Data))
-      .mapLeft(messages =>
-        messages.flatMap(msg => {
-          // TODO: Parse errors should be QuintErrors
-          const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} }
-          return msg.locs.map(loc => assembleDiagnostic(error, loc))
-        })
-      )
+      .mapLeft(({ errors, sourceMap }) => diagnosticsFromErrors(errors, sourceMap))
 
     if (result.isRight()) {
       return new Promise((resolve, _reject) => resolve(result.value))

diff --git a/vscode/quint-vscode/server/src/reporting.ts b/vscode/quint-vscode/server/src/reporting.ts
@@ -12,7 +12,7 @@
  * @module
  */
 
-import { Loc, QuintError, QuintModule, findExpressionWithId, findTypeWithId } from '@informalsystems/quint'
+import { Loc, QuintError, QuintModule, SourceMap, findExpressionWithId, findTypeWithId } from '@informalsystems/quint'
 import { Diagnostic, DiagnosticSeverity, Position, Range } from 'vscode-languageserver'
 import { compact } from 'lodash'
 
@@ -25,11 +25,11 @@ import { compact } from 'lodash'
  *
  * @returns a list of diagnostics with the proper error messages and locations
  */
-export function diagnosticsFromErrors(errors: [bigint, QuintError][], sourceMap: Map<bigint, Loc>): Diagnostic[] {
-  const diagnostics = errors.map(([id, error]) => {
-    const loc = sourceMap.get(id)!
+export function diagnosticsFromErrors(errors: QuintError[], sourceMap: SourceMap): Diagnostic[] {
+  const diagnostics = errors.map(error => {
+    const loc = sourceMap.get(error.reference!)!
     if (!loc) {
-      console.log(`loc for ${id} not found in source map`)
+      console.log(`loc for ${error} not found in source map`)
     } else {
       return assembleDiagnostic(error, loc)
     }

diff --git a/vscode/quint-vscode/server/test/reporting.test.ts b/vscode/quint-vscode/server/test/reporting.test.ts
@@ -12,7 +12,7 @@ import { Position } from 'vscode-languageserver'
 import { parseOrThrow } from './util'
 
 describe('diagnosticsFromErrorMap', () => {
-  const errors: [bigint, QuintError][] = [[1n, { code: 'QNT000', message: 'Message', reference: 0n, data: {} }]]
+  const errors: QuintError[] = [{ code: 'QNT000', message: 'Message', reference: 1n, data: {} }]
 
   const sourceMap = new Map<bigint, Loc>([
     [1n, { start: { col: 1, index: 1, line: 1 }, end: { col: 1, index: 1, line: 1 }, source: 'mocked_path' }],