feat: type-checking with LEO-III-STC

README.md

@@ -167,7 +167,11 @@ Added error handling for "Format TPTP File": display error message and jump to p
 
 ### 0.1.11
 
-Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.
+Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer.
+
+### 0.1.12
+
+Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter.
 
 ---
 

tptplus/CHANGELOG.md

@@ -23,4 +23,5 @@
 - v0.1.8 Fixed issue where some greater-than-signs are not handled correctly by command "Format TPTP File".
 - v0.1.9 Added local pretty-printer so that "Format TPTP File" works without Internet connection. The original remote pretty-printer is kept as a fallback.
 - v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error.
-- v0.1.11 Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.
+- v0.1.11 Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer.
+- v0.1.12 Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter.

tptplus/README.md

@@ -166,7 +166,11 @@ Added error handling for "Format TPTP File": display error message and jump to p
 
 ### 0.1.11
 
-Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.
+Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer.
+
+### 0.1.12
+
+Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter.
 
 ---
 

tptplus/client/src/extension.ts

@@ -14,6 +14,7 @@ import {
 import { errorMessage } from './errorMessage';
 import { createSystemB4TptpForm } from './systemTptpForms';
 import { registerPrettyPrintCommand } from './prettyPrint/command';
+import { registerTypeCheckCommand } from './typeCheck/command';
 
 let client: LanguageClient;
 
@@ -319,6 +320,9 @@ export function activate(context: ExtensionContext) {
   //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK
   context.subscriptions.push(registerPrettyPrintCommand(context));
 
+  //@ CHECK TYPES WITH LEO-III-STC THROUGH SYSTEMONTPTP
+  context.subscriptions.push(registerTypeCheckCommand());
+
   //@ RUN A THEOREM THROUGH SYSTEMONTPTP                                              
   const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => {
 

tptplus/client/src/prettyPrint/remote.ts

@@ -1,6 +1,6 @@
 import { errorMessage } from '../errorMessage';
 import {
-  extractSystemB4TptpOutput,
+  extractSystemB4TptpHtmlOutput,
   lastNonemptyLine
 } from '../systemB4TptpOutput';
 import { createSystemB4TptpForm } from '../systemTptpForms';
@@ -25,7 +25,7 @@ export async function formatTptpRemotely(
       };
     }
 
-    const output = extractSystemB4TptpOutput(await response.text());
+    const output = extractSystemB4TptpHtmlOutput(await response.text());
     if (output === undefined) {
       return { kind: 'failure', message: 'unrecognized response' };
     }

tptplus/client/src/systemB4TptpOutput.ts

@@ -3,7 +3,7 @@ import { JSDOM } from 'jsdom';
 /**
  * Extract the text between `<PRE>` and `</PRE>` from the HTML response of System B4 TPTP.
  */
-export function extractSystemB4TptpOutput(html: string): string | undefined {
+export function extractSystemB4TptpHtmlOutput(html: string): string | undefined {
   const dom = new JSDOM(html);
   const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined;
   if (preText === undefined) {
@@ -40,3 +40,43 @@ export function lastNonemptyLine(text: string): string | undefined {
 
   return undefined;
 }
+
+/** Finds an SZS status line before an SZS output block. */
+function getSzsStatusLine(output: string): string | undefined {
+  for (const line of output.split(/\r?\n/)) {
+    if (/^% SZS output start \S+/.test(line)) {
+      return undefined;
+    }
+    if (/^% SZS status \S+/.test(line)) {
+      return line;
+    }
+  }
+
+  return undefined;
+}
+
+/** Extracts the status name from an SZS status line before an SZS output block. */
+export function getSzsStatus(output: string): string | undefined {
+  return getSzsStatusLine(output)?.match(/^% SZS status (\S+)/)?.[1];
+}
+
+/** Extracts the message after the first colon in an SZS status line. */
+export function getSzsStatusMessage(output: string): string | undefined {
+  const statusLine = getSzsStatusLine(output);
+  const colonIndex = statusLine?.indexOf(':') ?? -1;
+  if (!statusLine || colonIndex < 0) {
+    return undefined;
+  }
+
+  return statusLine.slice(colonIndex + 1).trim() || undefined;
+}
+
+/** Extracts the content between the outermost SZS output markers. */
+export function getSzsOutput(output: string): string | undefined {
+  const szsOutput = output.match(
+    /^% SZS output start \S+[^\r\n]*\r?\n([\s\S]*)\r?\n% SZS output end \S+[^\r\n]*$/m
+  )?.[1];
+
+  // A greedy capture can consume the `\r` from the final CRLF delimiter.
+  return szsOutput?.replace(/\r$/, '');
+}

tptplus/client/src/typeCheck/command.ts

@@ -0,0 +1,191 @@
+import * as path from 'path';
+import * as vscode from 'vscode';
+
+import { errorMessage } from '../errorMessage';
+import {
+  getSzsOutput,
+  getSzsStatus,
+  getSzsStatusMessage
+} from '../systemB4TptpOutput';
+import {
+  formatTypeCheckStatusMessage,
+  getLeoIIITypeErrors
+} from './errors';
+import {
+  createLeoIIITypeErrorDiagnostics,
+  revealFirstTypeError
+} from './diagnostics';
+
+const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply';
+const LEO_III_STC = 'Leo-III-STC---'; // SystemB4TPTP will automatically run the latest version of LEO-III-STC it has available
+const TYPE_CHECK_RUNNING_CONTEXT_KEY = 'tptp.typeCheckRunning';
+const TYPE_CHECK_TIMEOUT_SEC = 60; // TODO: make this configurable
+const TYPE_CHECK_REQUEST_TIMEOUT_MS = 75000; // TODO: make this configurable
+
+function createLeoIIITypeCheckForm(document: vscode.TextDocument): FormData {
+  const form = new FormData();
+
+  // These are the fields used by RemoteSoT.py for one selected system.
+  form.append('NoHTML', '1');
+  form.append('QuietFlag', '-q1');
+  form.append('SubmitButton', 'RunSelectedSystems');
+  form.append('X2TPTP', '');
+  form.append('ProblemSource', 'UPLOAD');
+  form.append(`System___${LEO_III_STC}`, LEO_III_STC);
+  form.append(`TimeLimit___${LEO_III_STC}`, String(TYPE_CHECK_TIMEOUT_SEC));
+  form.append(
+    'UPLOADProblem',
+    new Blob([document.getText()], { type: 'text/plain' }),
+    path.basename(document.fileName) || 'problem.p'
+  );
+
+  return form;
+}
+
+/**
+ * Runs the complete remote request with visible progress, cancellation, and a timeout.
+ *
+ * @returns The response body for a successful request, or `undefined` when the user
+ * cancels the operation. User cancellation is therefore an expected outcome rather
+ * than an error.
+ * @throws An error when the request times out, returns a non-successful HTTP status,
+ * encounters a network failure, or fails while reading the response body.
+ */
+async function requestLeoIIITypeCheck(
+  document: vscode.TextDocument
+): Promise<string | undefined> {
+  return vscode.window.withProgress(
+    {
+      location: vscode.ProgressLocation.Notification,
+      title: 'Type-checking with LEO-III-STC',
+      cancellable: true
+    },
+    async (progress, token) => {
+      const controller = new AbortController();
+      let timedOut = false;
+
+      progress.report({ message: 'Waiting for tptp.org...' });
+      const cancellation = token.onCancellationRequested(() => {
+        controller.abort();
+      });
+      const timeout = setTimeout(() => {
+        timedOut = true;
+        controller.abort();
+      }, TYPE_CHECK_REQUEST_TIMEOUT_MS);
+
+      try {
+        const response = await fetch(SYSTEM_ON_TPTP_URL, {
+          method: 'POST',
+          body: createLeoIIITypeCheckForm(document),
+          signal: controller.signal
+        });
+
+        if (token.isCancellationRequested) {
+          return undefined;
+        }
+        if (!response.ok) {
+          throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`);
+        }
+
+        const output = await response.text();
+        return token.isCancellationRequested ? undefined : output;
+      } catch (error: unknown) {
+        if (token.isCancellationRequested) {
+          return undefined;
+        }
+        if (timedOut) {
+          throw new Error(
+            `LEO-III-STC type check timed out after ${TYPE_CHECK_REQUEST_TIMEOUT_MS / 1000} seconds.`
+          );
+        }
+        throw error;
+      } finally {
+        clearTimeout(timeout);
+        cancellation.dispose();
+      }
+    }
+  );
+}
+
+/** Registers the command that asks LEO-III-STC on SystemB4TPTP to type-check a TPTP document. */
+export function registerTypeCheckCommand(): vscode.Disposable {
+  let typeCheckRunning = false;
+
+  const diagnostics = vscode.languages.createDiagnosticCollection('tptpTypeCheck');
+  const command = vscode.commands.registerCommand('tptp.typeCheck', async (uri?: vscode.Uri) => {
+    if (typeCheckRunning) {
+      vscode.window.showInformationMessage('LEO-III-STC is already checking types.');
+      return;
+    }
+
+    if (!uri) {
+      const activeEditor = vscode.window.activeTextEditor;
+      if (!activeEditor) {
+        vscode.window.showErrorMessage('No TPTP file is currently open.');
+        return;
+      }
+      uri = activeEditor.document.uri;
+    }
+
+    typeCheckRunning = true;
+    try {
+      await vscode.commands.executeCommand('setContext', TYPE_CHECK_RUNNING_CONTEXT_KEY, true);
+
+      const document = await vscode.workspace.openTextDocument(uri);
+      const checkedDocumentVersion = document.version;
+      diagnostics.delete(document.uri);
+      const output = await requestLeoIIITypeCheck(document);
+      if (output === undefined) {
+        vscode.window.showInformationMessage('LEO-III-STC type check cancelled.');
+        return;
+      }
+      if (document.version !== checkedDocumentVersion) {
+        vscode.window.showErrorMessage(
+          'TPTP file changed while type-checking. Please run the type-checker again.'
+        );
+        return;
+      }
+
+      const status = getSzsStatus(output);
+      const statusMessage = formatTypeCheckStatusMessage(
+        status,
+        getSzsStatusMessage(output)
+      );
+      const szsOutput = getSzsOutput(output);
+      const outputSuffix = [statusMessage, szsOutput]
+        .filter((message): message is string => Boolean(message)) // discard '' or undefined
+        .map(message => `\n${message}`)
+        .join('');
+      if (status === 'Success') {
+        vscode.window.showInformationMessage(`LEO-III-STC type check succeeded.`);
+      } else if (status === 'TypeError') {
+        const typeErrors = getLeoIIITypeErrors(szsOutput ?? output);
+        const typeErrorDiagnostics = createLeoIIITypeErrorDiagnostics(document, typeErrors);
+        diagnostics.set(document.uri, typeErrorDiagnostics);
+        await revealFirstTypeError(document, typeErrorDiagnostics);
+        vscode.window.showErrorMessage(
+          `LEO-III-STC found type error(s).${outputSuffix}`
+        );
+      } else if (status) {
+        vscode.window.showErrorMessage(`LEO-III-STC reported ${status}.${outputSuffix}`);
+      } else {
+        vscode.window.showErrorMessage(`LEO-III-STC returned an unrecognized response: ${output}`);
+      }
+    } catch (error: unknown) {
+      vscode.window.showErrorMessage(
+        `Failed to check types with LEO-III-STC: ${errorMessage(error)}`
+      );
+    } finally {
+      typeCheckRunning = false;
+      await vscode.commands.executeCommand('setContext', TYPE_CHECK_RUNNING_CONTEXT_KEY, false);
+    }
+  });
+
+  return vscode.Disposable.from(
+    diagnostics,
+    command,
+    vscode.workspace.onDidChangeTextDocument(event => {
+      diagnostics.delete(event.document.uri);
+    })
+  );
+}

tptplus/client/src/typeCheck/diagnostics.ts

@@ -0,0 +1,52 @@
+import * as vscode from 'vscode';
+
+import type { LeoIIITypeError } from './errors';
+
+const TYPE_CHECK_DIAGNOSTIC_SOURCE = 'LEO-III-STC type checker';
+
+/** Creates warning diagnostic from each LEO-III-STC type error. */
+export function createLeoIIITypeErrorDiagnostics(
+  document: vscode.TextDocument,
+  typeErrors: LeoIIITypeError[]
+): vscode.Diagnostic[] {
+  const diagnostics: vscode.Diagnostic[] = [];
+
+  for (const typeError of typeErrors) {
+    const lineIndex = typeError.line - 1;
+    if (lineIndex < 0 || lineIndex >= document.lineCount) {
+      continue;
+    }
+
+    const line = document.lineAt(lineIndex);
+    const characterIndex = Math.min(typeError.character - 1, line.text.length);
+    const startPosition = line.range.start.with(undefined, characterIndex);
+    diagnostics.push({
+      range: line.range.with(startPosition, line.range.end),
+      message: typeError.message,
+      severity: vscode.DiagnosticSeverity.Warning,
+      source: TYPE_CHECK_DIAGNOSTIC_SOURCE
+    });
+  }
+
+  return diagnostics;
+}
+
+/** Moves the editor cursor to the first source-located type error. */
+export async function revealFirstTypeError(
+  document: vscode.TextDocument,
+  typeErrorDiagnostics: readonly vscode.Diagnostic[]
+): Promise<void> {
+  const firstTypeError = typeErrorDiagnostics[0];
+  if (!firstTypeError) {
+    return;
+  }
+
+  const position = firstTypeError.range.start;
+  const range = new vscode.Range(position, position);
+  const editor = await vscode.window.showTextDocument(document, {
+    preview: false,
+    selection: range
+  });
+  editor.selection = new vscode.Selection(position, position);
+  editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport);
+}