feat: integrate ANTLR parser

tptplus/client/src/antlrParser/command.ts

@@ -0,0 +1,107 @@
+import * as vscode from 'vscode';
+import type { LanguageClient } from 'vscode-languageclient/node';
+
+import { toVsCodeDiagnostic } from './diagnostics';
+import type { ExperimentalParseWithAntlrResult } from './types';
+
+const ANTLR_PARSE_COMMAND = 'tptp.experimentalParseWithAntlr';
+const ANTLR_PARSE_REQUEST = 'tptp/experimentalParseWithAntlr';
+
+function writeTptpAntlrParseLog(
+  output: vscode.OutputChannel,
+  document: vscode.TextDocument,
+  result: ExperimentalParseWithAntlrResult
+): void {
+  output.appendLine(`[${new Date().toISOString()}] ${document.uri.fsPath}`);
+  output.appendLine(`Elapsed: ${result.summary.elapsedMs}ms`);
+  output.appendLine(`Syntax errors: ${result.summary.syntaxErrorCount}`);
+
+  if (result.diagnostics.length === 0) {
+    output.appendLine('No ANTLR diagnostics.');
+  } else {
+    result.diagnostics.forEach(diagnostic => {
+      output.appendLine(
+        `${diagnostic.range.start.line + 1}:${diagnostic.range.start.character + 1} ${diagnostic.message}`
+      );
+    });
+  }
+
+  output.appendLine('');
+}
+
+function createAntlrParserCommandHandler(
+  client: LanguageClient,
+  clientReady: Promise<void>,
+  diagnostics: vscode.DiagnosticCollection,
+  output: vscode.OutputChannel
+): () => Promise<void> {
+  return async (): Promise<void> => {
+    const editor = vscode.window.activeTextEditor;
+    if (!editor || editor.document.languageId !== 'tptp') {
+      vscode.window.showErrorMessage('No active TPTP file open');
+      return;
+    }
+
+    if (editor.document.uri.scheme !== 'file') {
+      vscode.window.showErrorMessage(
+        'The experimental TPTP ANTLR parser currently supports file-backed TPTP documents only.'
+      );
+      return;
+    }
+
+    try {
+      await clientReady;
+      const result = await client.sendRequest<ExperimentalParseWithAntlrResult>(
+        ANTLR_PARSE_REQUEST,
+        { uri: editor.document.uri.toString() }
+      );
+
+      diagnostics.set(
+        editor.document.uri,
+        result.diagnostics.map(toVsCodeDiagnostic)
+      );
+      writeTptpAntlrParseLog(output, editor.document, result);
+
+      if (result.ok) {
+        vscode.window.showInformationMessage(
+          `ANTLR parse succeeded in ${result.summary.elapsedMs}ms.`
+        );
+      } else {
+        vscode.window.showWarningMessage(
+          `ANTLR parse found ${result.summary.syntaxErrorCount} error(s).`
+        );
+        output.show(true);
+      }
+    } catch (error: unknown) {
+      const message = error instanceof Error ? error.message : String(error);
+      output.appendLine(`[${new Date().toISOString()}] TPTP ANTLR parser request failed`);
+      output.appendLine(message);
+      output.show(true);
+      vscode.window.showErrorMessage(`TPTP ANTLR parser request failed: ${message}`);
+    }
+  };
+}
+
+/** Registers the experimental ANTLR parser command and its diagnostic lifecycle. */
+export function registerAntlrParserCommand(
+  client: LanguageClient,
+  clientReady: Promise<void>
+): vscode.Disposable {
+  const diagnostics = vscode.languages.createDiagnosticCollection('tptpAntlrExperimental');
+  const output = vscode.window.createOutputChannel('TPTP ANTLR Parser');
+  const commandHandler = createAntlrParserCommandHandler(
+    client,
+    clientReady,
+    diagnostics,
+    output
+  );
+
+  return vscode.Disposable.from(
+    diagnostics,
+    output,
+    vscode.commands.registerCommand(ANTLR_PARSE_COMMAND, commandHandler),
+    vscode.workspace.onDidChangeTextDocument(event => {
+      diagnostics.delete(event.document.uri);
+    })
+  );
+}

tptplus/client/src/antlrParser/diagnostics.ts

@@ -0,0 +1,34 @@
+import * as vscode from 'vscode';
+
+import type { LspDiagnostic } from './types';
+
+function toVsCodeSeverity(severity: number | undefined): vscode.DiagnosticSeverity {
+  switch (severity) {
+    case 2:
+      return vscode.DiagnosticSeverity.Warning;
+    case 3:
+      return vscode.DiagnosticSeverity.Information;
+    case 4:
+      return vscode.DiagnosticSeverity.Hint;
+    case 1:
+    default:
+      return vscode.DiagnosticSeverity.Error;
+  }
+}
+
+/** Converts a language-server diagnostic into its VS Code client representation. */
+export function toVsCodeDiagnostic(diagnostic: LspDiagnostic): vscode.Diagnostic {
+  const range = new vscode.Range(
+    diagnostic.range.start.line,
+    diagnostic.range.start.character,
+    diagnostic.range.end.line,
+    diagnostic.range.end.character
+  );
+  const result = new vscode.Diagnostic(
+    range,
+    diagnostic.message,
+    toVsCodeSeverity(diagnostic.severity)
+  );
+  result.source = diagnostic.source;
+  return result;
+}

tptplus/client/src/antlrParser/types.ts

@@ -0,0 +1,25 @@
+export interface LspPosition {
+  line: number;
+  character: number;
+}
+
+export interface LspRange {
+  start: LspPosition;
+  end: LspPosition;
+}
+
+export interface LspDiagnostic {
+  range: LspRange;
+  message: string;
+  severity?: number;
+  source?: string;
+}
+
+export interface ExperimentalParseWithAntlrResult {
+  ok: boolean;
+  diagnostics: LspDiagnostic[];
+  summary: {
+    elapsedMs: number;
+    syntaxErrorCount: number;
+  };
+}

tptplus/client/src/extension.ts

@@ -13,6 +13,7 @@ import {
 
 import { errorMessage } from './errorMessage';
 import { createSystemB4TptpForm } from './systemTptpForms';
+import { registerAntlrParserCommand } from './antlrParser/command';
 import { registerPrettyPrintCommand } from './prettyPrint/command';
 import { registerTypeCheckCommand } from './typeCheck/command';
 
@@ -2410,7 +2411,8 @@ export function activate(context: ExtensionContext) {
   );
 
   // Start the client (and server)
-  client.start();
+  const clientReady = client.start();
+  context.subscriptions.push(registerAntlrParserCommand(client, clientReady));
 }
 
 export function deactivate(): Thenable<void> | undefined {

tptplus/package.json

@@ -68,6 +68,14 @@
           "dark": "./images/icons/Type.png"
         }
       },
+      {
+        "command": "tptp.experimentalParseWithAntlr",
+        "title": "TPTP: Experimental Parse with ANTLR",
+        "icon": {
+          "light": "./images/icons/Syntax.png",
+          "dark": "./images/icons/Syntax.png"
+        }
+      },
       {
         "command": "tptp.proveProblem",
         "title": "TPTP: Prove Problem"
@@ -101,9 +109,14 @@
           "group": "navigation@1"
         },
         {
-          "command": "tptp.typeCheck",
+          "command": "tptp.experimentalParseWithAntlr",
           "when": "editorLangId == tptp",
           "group": "navigation@2"
+        },
+        {
+          "command": "tptp.typeCheck",
+          "when": "editorLangId == tptp",
+          "group": "navigation@3"
         }
       ],
       "editor/context": [
@@ -174,6 +187,7 @@
   "scripts": {
     "build:wasm": "emcmake cmake -S native/tptp-pretty -B native/tptp-pretty/build-wasm && cmake --build native/tptp-pretty/build-wasm",
     "vscode:prepublish": "npm run compile",
+    "precompile": "npm install --prefix server --no-audit --no-fund",
     "compile": "tsc -b",
     "watch": "tsc -b -w",
     "postinstall": "cd client && npm install && cd ../server && npm install && cd ..",

tptplus/server/package.json

@@ -3,11 +3,12 @@
   "description": "TPTP language server",
   "version": "1.0.0",
   "dependencies": {
+    "antlr4": "^4.13.2",
     "vscode-languageserver": "^8.1.0",
     "vscode-languageserver-textdocument": "^1.0.8"
   },
   "devDependencies": {
     "@types/node": "^16.18.34",
     "typescript": "^5.1.3"
   }
-}
+}