diff --git a/README.md b/README.md index 0019cfe..bfd5baa 100644 --- a/README.md +++ b/README.md @@ -158,8 +158,16 @@ Fixed issue where some greater-than-signs are not handled correctly by command " ### 0.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. +Added local pretty-printer so that "Format TPTP File" works without Internet connection. +The original remote pretty-printer is kept as a fallback. + +### 0.1.10 + +Added error handling for "Format TPTP File": display error message and jump to position of syntax error. + +### 0.1.11 + +Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. --- diff --git a/tptplus/CHANGELOG.md b/tptplus/CHANGELOG.md index b683c06..59c6fc9 100644 --- a/tptplus/CHANGELOG.md +++ b/tptplus/CHANGELOG.md @@ -21,4 +21,6 @@ - v0.1.5 Added dynamic loading of ATP systems from tptp.org by using fetch. - v0.1.7 Automated linting, and standardized releases with GitHub actions. - 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. \ No newline at end of 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. diff --git a/tptplus/README.md b/tptplus/README.md index 248d3c4..20feff2 100644 --- a/tptplus/README.md +++ b/tptplus/README.md @@ -157,8 +157,16 @@ Fixed issue where some greater-than-signs are not handled correctly by command " ### 0.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. +Added local pretty-printer so that "Format TPTP File" works without Internet connection. +The original remote pretty-printer is kept as a fallback. + +### 0.1.10 + +Added error handling for "Format TPTP File": display error message and jump to position of syntax error. + +### 0.1.11 + +Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. --- diff --git a/tptplus/client/package-lock.json b/tptplus/client/package-lock.json index 29a3e0c..ff64661 100644 --- a/tptplus/client/package-lock.json +++ b/tptplus/client/package-lock.json @@ -109,7 +109,6 @@ "url": "https://opencollective.com/csstools" } ], - "peer": true, "engines": { "node": ">=18" }, @@ -131,7 +130,6 @@ "url": "https://opencollective.com/csstools" } ], - "peer": true, "engines": { "node": ">=18" } diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.d.ts b/tptplus/client/resources/wasm/tptp4X_wasm.d.ts index ab716e4..d29901e 100644 --- a/tptplus/client/resources/wasm/tptp4X_wasm.d.ts +++ b/tptplus/client/resources/wasm/tptp4X_wasm.d.ts @@ -1,3 +1,3 @@ -declare const createTPTP4X: import('../../src/localPrettyPrinterProcess').CreateTPTP4X; +declare const createTPTP4X: import('../../src/prettyPrint/localPrettyPrintProcess').CreateTPTP4X; export = createTPTP4X; diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.wasm b/tptplus/client/resources/wasm/tptp4X_wasm.wasm index 4157f2c..915ceef 100755 Binary files a/tptplus/client/resources/wasm/tptp4X_wasm.wasm and b/tptplus/client/resources/wasm/tptp4X_wasm.wasm differ diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 9750727..b2f7c29 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -11,14 +11,19 @@ import { TransportKind } from 'vscode-languageclient/node'; -import { - createSystemB4TptpForm -} from './systemTptpForms'; -import { formatTptpLocally } from './localPrettyPrinter'; +import { createSystemB4TptpForm } from './systemTptpForms'; +import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand'; let client: LanguageClient; export function activate(context: ExtensionContext) { + const prettyPrintDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); + context.subscriptions.push(prettyPrintDiagnostics); + context.subscriptions.push( + vscode.workspace.onDidChangeTextDocument(event => { + prettyPrintDiagnostics.delete(event.document.uri); + }) + ); async function fetchList(url: string, inputType: string = 'radio') { const response = await fetch(url, { @@ -314,61 +319,14 @@ export function activate(context: ExtensionContext) { } }) - }) + }); context.subscriptions.push(prepareProblem); - //@ FORMAT A PROBLEM THROUGH SYSTEMB4TPTP - const formatProblem = vscode.commands.registerCommand('tptp.formatProblem', async (uri: vscode.Uri) => { - if (!uri) { - const activeEditor = vscode.window.activeTextEditor; - if (!activeEditor) { - vscode.window.showErrorMessage('No active TPTP file open'); - return; - } - uri = activeEditor.document.uri; - } - - const document = await vscode.workspace.openTextDocument(uri); - const sourceText = document.getText(); - const fullTextRange = new vscode.Range( - document.positionAt(0), - document.positionAt(sourceText.length) - ); - - // use WorkspaceEdit to edit any URI's document, even if it's invisible - const edit = new vscode.WorkspaceEdit(); - - const localOutput = - !sourceText.trim() ? "" : // a whitespace-only file should become empty - await formatTptpLocally(context, sourceText); - if (localOutput !== undefined) { - edit.replace(uri, fullTextRange, localOutput); - await vscode.workspace.applyEdit(edit); - return; - } - - // fall back to remote pretty-printer if the local pretty-printer fails - const form = createSystemB4TptpForm(sourceText, null); - const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { - method: 'POST', - body: form - }); - const text = await response.text(); - const match = text.match(/]*>([\s\S]*?)<\/pre>/i); - - let output = sourceText; - - if (match) { - output = match[1].split("\n").slice(2, match[1].split("\n").length - 4).join("\n") - } - - edit.replace(uri, fullTextRange, output.replace(/>/g, ">")); - await vscode.workspace.applyEdit(edit); - - }) - - context.subscriptions.push(formatProblem); + //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK + context.subscriptions.push( + registerPrettyPrintCommand(context, prettyPrintDiagnostics) + ); //@ RUN A THEOREM THROUGH SYSTEMONTPTP const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => { @@ -1663,7 +1621,7 @@ export function activate(context: ExtensionContext) { } }); - }) + }); context.subscriptions.push(proveProblemMultiple); @@ -2000,7 +1958,7 @@ export function activate(context: ExtensionContext) { } } }) - }) + }); context.subscriptions.push(processSolution); @@ -2341,7 +2299,7 @@ export function activate(context: ExtensionContext) { } } }) - }) + }); context.subscriptions.push(processSolutionMultiple); @@ -2387,7 +2345,7 @@ export function activate(context: ExtensionContext) { } else { vscode.window.showInformationMessage('No problem selected.'); } - }) + }); context.subscriptions.push(importProblem); @@ -2434,7 +2392,7 @@ export function activate(context: ExtensionContext) { vscode.window.showInformationMessage('No Solution selected.'); } - }) + }); context.subscriptions.push(importSolution); diff --git a/tptplus/client/src/localPrettyPrinter.ts b/tptplus/client/src/localPrettyPrinter.ts deleted file mode 100644 index 818c9d6..0000000 --- a/tptplus/client/src/localPrettyPrinter.ts +++ /dev/null @@ -1,49 +0,0 @@ -import { spawn } from 'child_process'; -import * as path from 'path'; -import * as vscode from 'vscode'; - -const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; - -export async function formatTptpLocally( - context: vscode.ExtensionContext, - input: string -): Promise { - const runnerPath = context.asAbsolutePath(path.join('client', 'out', 'localPrettyPrinterProcess.js')); - - return new Promise(resolve => { - let stdout = ''; - let settled = false; // prevent the promise from resolving twice - const child = spawn(process.execPath, [runnerPath], { - env: { - ...process.env, - ELECTRON_RUN_AS_NODE: '1', - }, - // parent can write to and read from child process; stderr is discarded - stdio: ['pipe', 'pipe', 'ignore'], - }); - - function finish(output: string | undefined): void { - if (settled) return; - settled = true; - clearTimeout(timeout); - resolve(output); - } - - const timeout = setTimeout(() => { - child.kill(); - finish(undefined); - }, LOCAL_PRETTY_PRINT_TIMEOUT_MS); - - child.on('error', () => finish(undefined)); - child.on('close', code => { - finish(code === 0 && stdout.length > 0 ? stdout : undefined); - }); - child.stdout.setEncoding('utf8'); - child.stdout.on('data', chunk => { - stdout += chunk; - }); - - child.stdin.on('error', () => undefined); - child.stdin.end(input, 'utf8'); - }); -} diff --git a/tptplus/client/src/localPrettyPrinterProcess.ts b/tptplus/client/src/localPrettyPrinterProcess.ts deleted file mode 100644 index c3a9cc3..0000000 --- a/tptplus/client/src/localPrettyPrinterProcess.ts +++ /dev/null @@ -1,95 +0,0 @@ -import * as fs from 'fs'; -import * as path from 'path'; -import createTPTP4X from '../resources/wasm/tptp4X_wasm.js'; - -export type TPTP4XModule = { - lengthBytesUTF8(value: string): number; - stringToUTF8(value: string, pointer: number, maxBytesToWrite: number): void; - UTF8ToString(pointer: number): string; - _malloc(size: number): number; - _free(pointer: number): void; - _tptp4x_pretty_print_tptp(inputPointer: number): number; - _tptp4x_free_string(pointer: number): void; -}; - -export type CreateTPTP4X = (options: { - locateFile(file: string): string; - print(): void; - printErr(): void; - quit(status: number, error: unknown): never; - wasmBinary: ArrayBuffer | ArrayBufferView; -}) => Promise; - -function readStdin(): string { - return fs.readFileSync(0, 'utf8'); -} - -/** - * Copies a JavaScript string into WASM memory - * @param value - the string to be copied - * @returns pointer to the copy in WASM memory - */ -function writeString(module: TPTP4XModule, value: string): number { - const length = module.lengthBytesUTF8(value) + 1; - const pointer = module._malloc(length); - - if (!pointer) { - throw new Error('Unable to allocate wasm memory for TPTP input'); - } - - module.stringToUTF8(value, pointer, length); - return pointer; -} - -function statusFromError(error: unknown): number { - if ( - typeof error === 'object' && - error !== null && - 'status' in error && - typeof (error as { status?: unknown }).status === 'number' - ) { - return (error as { status: number }).status || 1; - } - return 1; -} - -async function main(): Promise { - const wasmDirectory = path.join(__dirname, '..', 'resources', 'wasm'); - const module = await createTPTP4X({ - locateFile: (file: string) => path.join(wasmDirectory, file), - // print and printErr are silenced because stdout is reserved for the formatted TPTP output - print: () => undefined, - printErr: () => undefined, - quit: (status: number, error: unknown): never => { - const throwable = error instanceof Error ? error : new Error(`WASM exited with status ${status}`); - (throwable as Error & { status?: number }).status = status; - throw throwable; - }, - wasmBinary: fs.readFileSync(path.join(wasmDirectory, 'tptp4X_wasm.wasm')), - }); - - let inputPointer = 0; - let outputPointer = 0; - - try { - inputPointer = writeString(module, readStdin()); - outputPointer = module._tptp4x_pretty_print_tptp(inputPointer); - - if (!outputPointer) { - process.exit(1); - } - - process.stdout.write(module.UTF8ToString(outputPointer)); - } finally { - if (outputPointer) { - module._tptp4x_free_string(outputPointer); - } - if (inputPointer) { - module._free(inputPointer); - } - } -} - -main().catch((error: unknown) => { - process.exit(statusFromError(error)); -}); diff --git a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts b/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts new file mode 100644 index 0000000..189813b --- /dev/null +++ b/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts @@ -0,0 +1,103 @@ +import * as vscode from "vscode"; + +export interface JJParserErrorLocation { + position: vscode.Position; + range: vscode.Range; + message: string; + reportedText?: string; +} + +/** + * Takes a JJParser error message and turns it into a VS Code location. + * @param message The expected message shape is like + * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' or + * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' + * @returns VS Code location or undefined + */ +export function getJJParserErrorLocation(document: vscode.TextDocument, message: string): + JJParserErrorLocation | undefined +{ + const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/); + if (!match) { + return undefined; + } + + const reportedLine = Number.parseInt(match[1], 10); + const reportedCharacter = Number.parseInt(match[2], 10); + if (Number.isNaN(reportedLine) || Number.isNaN(reportedCharacter)) { + return undefined; + } + + const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); + const lineText = document.lineAt(lineIndex).text; + let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); + const reportedText = match[3]; + + // If the error message reports a token or character, try to move cursor to its beginning. + if (reportedText) { + const reportedTextIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(reportedText); + if (reportedTextIndex >= 0) { + characterIndex = reportedTextIndex; + } + } + + const startPosition = new vscode.Position(lineIndex, characterIndex); + const endCharacterIndex = reportedText + ? Math.min(lineText.length, characterIndex + reportedText.length) + : characterIndex; + const endPosition = new vscode.Position(lineIndex, endCharacterIndex); + + return { + position: startPosition, + range: new vscode.Range(startPosition, endPosition), + message: message, + reportedText: reportedText + }; +} + +/** + * Adds a warning diagnostic for a JJParser-reported token or character. + * The squiggle and diagnostic message are cleared on document edit or before + * each new pretty-printer run. + */ +export function setJJParserErrorDiagnostic( + diagnostics: vscode.DiagnosticCollection, + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +) { + if (!errorLocation?.reportedText) { + return; + } + + const diagnostic = new vscode.Diagnostic( + errorLocation.range, + errorLocation.message, + vscode.DiagnosticSeverity.Warning + ); + diagnostic.source = 'TPTP pretty-printer (JJParser)'; + diagnostics.set(document.uri, [diagnostic]); +} + +/** + * Takes a JJParser error location and, if it points to a specific position in source file, + * highlight the position. + * @param errorLocation The location parsed from a JJParser error message. + */ +export async function revealJJParserErrorLocation( + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +): Promise +{ + const position = errorLocation?.position; + if (!position) { + return; + } + + 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); +} diff --git a/tptplus/client/src/prettyPrint/localPrettyPrint.ts b/tptplus/client/src/prettyPrint/localPrettyPrint.ts new file mode 100644 index 0000000..b40cdeb --- /dev/null +++ b/tptplus/client/src/prettyPrint/localPrettyPrint.ts @@ -0,0 +1,87 @@ +import { spawn } from 'child_process'; +import * as path from 'path'; +import * as vscode from 'vscode'; + +const RUNNER_PATH = path.join('client', 'out', 'prettyPrint', 'localPrettyPrintProcess.js'); +const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; // TODO: make this configurable + +export type LocalPrettyPrintResult = + | { kind: 'success'; output: string } + | { kind: 'parser-error'; message: string } + | { kind: 'unknown-error' }; + +function readParserError(stderr: string): string | undefined { + for (const line of stderr.trim().split(/\r?\n/).reverse()) { + if (!line.trim()) { + continue; + } + + try { + const diagnostic = JSON.parse(line) as { kind?: unknown; message?: unknown }; + if (diagnostic.kind === 'jjparser' && typeof diagnostic.message === 'string') { + return diagnostic.message; + } + } catch { + // Ignore non-JSON stderr from the child process. + } + } + + return undefined; +} + +export async function formatTptpLocally( + context: vscode.ExtensionContext, + input: string +): Promise { + + // // debugging: uncomment this to simulate a failure of the local JJParser + // return { kind: 'parser-error', message: '(This is an error message for debugging that does not point to any specific location in source file.)' }; + // return { kind: 'unknown-error' }; + + return new Promise(resolve => { + let stdout = ''; + let stderr = ''; + let settled = false; // prevent the promise from resolving twice + const child = spawn(process.execPath, [context.asAbsolutePath(RUNNER_PATH)], { + env: { + ...process.env, + ELECTRON_RUN_AS_NODE: '1', + }, + stdio: ['pipe', 'pipe', 'pipe'], // stdin, stdout, stderr + }); + + function finish(result: LocalPrettyPrintResult): void { + if (settled) return; + settled = true; + clearTimeout(timeout); + resolve(result); + } + + const timeout = setTimeout(() => { + child.kill(); + finish({ + kind: 'parser-error', + message: `timeout after ${LOCAL_PRETTY_PRINT_TIMEOUT_MS} ms` + }); + }, LOCAL_PRETTY_PRINT_TIMEOUT_MS); + + child.on('error', () => finish({ kind: 'unknown-error' })); + child.on('close', exitCode => { + if (exitCode === 0) { + finish({ kind: 'success', output: stdout }); + } else { + const parserError = readParserError(stderr); + finish(parserError ? + { kind: 'parser-error', message: parserError } : + { kind: 'unknown-error' } + ); + } + }); + child.stdout.setEncoding('utf8'); + child.stdout.on('data', chunk => { stdout += chunk; }); + child.stderr.setEncoding('utf8'); + child.stderr.on('data', chunk => { stderr += chunk; }); + child.stdin.on('error', () => undefined); + child.stdin.end(input, 'utf8'); + }); +} diff --git a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts new file mode 100644 index 0000000..ca73108 --- /dev/null +++ b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts @@ -0,0 +1,150 @@ +import * as fs from 'fs'; +import * as path from 'path'; +import createTPTP4X from '../../resources/wasm/tptp4X_wasm.js'; +import { isDuplicateFormulaNameError } from './prettyPrintErrors'; + +const WASM_DIR = path.join(__dirname, '..', '..', 'resources', 'wasm'); +const WASM_BIN_PATH = path.join(WASM_DIR, 'tptp4X_wasm.wasm'); + +export type TPTP4XModule = { + lengthBytesUTF8(value: string): number; + stringToUTF8(value: string, pointer: number, maxBytesToWrite: number): void; + UTF8ToString(pointer: number): string; + _malloc(size: number): number; + _free(pointer: number): void; + _tptp4x_pretty_print_tptp(inputPointer: number): number; + _tptp4x_free_string(pointer: number): void; +}; + +export type CreateTPTP4X = (options: { + locateFile(file: string): string; + print(message?: string): void; + printErr(message?: string): void; + quit(status: number, error: unknown): never; + wasmBinary: ArrayBuffer | ArrayBufferView; +}) => Promise; + +const wasmDiagnostics: string[] = []; + +function readStdin(): string { + return fs.readFileSync(0, 'utf8'); +} + +function captureWasmDiagnostic(message?: string): void { + if (message && message.trim()) { + wasmDiagnostics.push(message); + } +} + +function parserDiagnosticMessage(): string | undefined { + const diagnosticStart = wasmDiagnostics.findIndex(message => + /^ERROR:\s/.test(message) || /^%\s*SZS status\s+\S+\s*:/.test(message) + ); + + if (diagnosticStart < 0) { + return undefined; + } + + const message = wasmDiagnostics.slice(diagnosticStart).join('\n'); + if (isDuplicateFormulaNameError(message)) { + return message.trim(); + } + + const errorMatch = message.match(/^ERROR:\s*(.*)$/s); + if (errorMatch) { + return errorMatch[1].trim(); + } + + const szsMatch = message.match(/^%\s*SZS status\s+(\S+)\s*:\s*(.*)$/s); + if (szsMatch) { + return `${szsMatch[1]}: ${szsMatch[2].trim()}`; + } + + return undefined; +} + +function writeParserDiagnostic(): void { + const message = parserDiagnosticMessage(); + + if (!message) { + return; + } + + process.stderr.write(`${JSON.stringify({ + kind: 'jjparser', + message, + })}\n`); +} + +/** + * Copies a JavaScript string into WASM memory. + * @param value - the string to be copied + * @returns pointer to the copy in WASM memory + */ +function writeString(module: TPTP4XModule, value: string): number { + const length = module.lengthBytesUTF8(value) + 1; + const pointer = module._malloc(length); + + if (!pointer) { + throw new Error('Unable to allocate wasm memory for TPTP input'); + } + + module.stringToUTF8(value, pointer, length); + return pointer; +} + +/** + * Returns a non-zero exit code (default = 1) by parsing an error of unknown type. + */ +function statusFromError(error: unknown): number { + if (error !== null && typeof error === 'object' && + 'status' in error && typeof error.status === 'number' + ) { + return error.status || 1; + } + return 1; +} + +async function main(): Promise { + let wasmExited = false; + const module = await createTPTP4X({ + locateFile: (file: string) => path.join(WASM_DIR, file), + print: captureWasmDiagnostic, + printErr: captureWasmDiagnostic, + quit: (status: number, error: unknown): never => { + wasmExited = true; + const throwable = error instanceof Error ? error : new Error(`WASM exited with status ${status}`); + (throwable as Error & { status?: number }).status = status; + throw throwable; + }, + wasmBinary: fs.readFileSync(WASM_BIN_PATH), + }); + + let inputPointer = 0; + let outputPointer = 0; + + try { + inputPointer = writeString(module, readStdin()); + outputPointer = module._tptp4x_pretty_print_tptp(inputPointer); + + if (!outputPointer) { + writeParserDiagnostic(); + process.exitCode = 1; + return; + } + + process.stdout.write(module.UTF8ToString(outputPointer)); + } finally { + if (outputPointer && !wasmExited) { + module._tptp4x_free_string(outputPointer); + } + if (inputPointer && !wasmExited) { + module._free(inputPointer); + } + } +} + +main().catch((error: unknown) => { + writeParserDiagnostic(); + process.exit(statusFromError(error)); +}); diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts new file mode 100644 index 0000000..7d530dc --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -0,0 +1,111 @@ +import * as vscode from "vscode"; + +import { + getJJParserErrorLocation, + revealJJParserErrorLocation, + setJJParserErrorDiagnostic +} from './jjParserDiagnostics'; +import { formatTptpLocally } from './localPrettyPrint'; +import { isDuplicateFormulaNameError } from './prettyPrintErrors'; +import { createSystemB4TptpForm } from '../systemTptpForms'; +import { + extractSystemB4TptpOutput, + lastNonemptyLine +} from '../systemB4TptpOutput'; + +export function registerPrettyPrintCommand( + context: vscode.ExtensionContext, + prettyPrintDiagnostics: vscode.DiagnosticCollection +): vscode.Disposable { + return vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { + if (!uri) { + const activeEditor = vscode.window.activeTextEditor; + if (!activeEditor) { + vscode.window.showErrorMessage('No active TPTP file open'); + return; + } + uri = activeEditor.document.uri; + } + + // Clear stale parser diagnostics before each new pretty-printer run. + prettyPrintDiagnostics.delete(uri); + + const document = await vscode.workspace.openTextDocument(uri); + const sourceText = document.getText(); + const fullTextRange = new vscode.Range( + document.positionAt(0), + document.positionAt(sourceText.length) + ); + + // use WorkspaceEdit to edit any URI's document, even if it's invisible + const edit = new vscode.WorkspaceEdit(); + + // a whitespace-only file should become empty + if (!sourceText.trim()) { + edit.replace(uri, fullTextRange, ''); + await vscode.workspace.applyEdit(edit); + return; + } + + // run the local pretty-printer (JJParser) + const localResult = await formatTptpLocally(context, sourceText); + + if (localResult.kind === 'success') { + edit.replace(uri, fullTextRange, localResult.output); + await vscode.workspace.applyEdit(edit); + return; + } + + if (localResult.kind === 'parser-error') { + if (isDuplicateFormulaNameError(localResult.message)) { + vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + return; + } + + const errorLocation = getJJParserErrorLocation(document, localResult.message); + if (errorLocation !== undefined) { + setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); + vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + return; + } + } + + // Fall back to remote pretty-printer if the local pretty-printer fails on a critical error, + // i.e., either an `unknown-error`, or a `parser-error` that is not a duplicate formula name + // error and does not point to any specific location in `sourceText`. + const localFailMessage = + localResult.kind === 'parser-error' ? localResult.message : 'unknown error'; + vscode.window.showWarningMessage( + `Failed to format TPTP file locally: ${localFailMessage}. ` + + 'Trying the remote formatter provided by SystemB4TPTP...' + ); + + // run the remote pretty-printer (provided by SystemB4TPTP) + const form = createSystemB4TptpForm(sourceText, null); + const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { + method: 'POST', + body: form + }); + const text = await response.text(); + const formattedOutput = extractSystemB4TptpOutput(text); + + if (formattedOutput !== undefined) { + const lastLine = lastNonemptyLine(formattedOutput); + if (lastLine?.startsWith('ERROR: ')) { + const errorLocation = getJJParserErrorLocation(document, lastLine); + setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); + vscode.window.showErrorMessage( + 'Failed to format TPTP file: ' + + `remote formatter provided by SystemB4TPTP exited with ${lastLine}` + ); + } else { + edit.replace(uri, fullTextRange, formattedOutput); + await vscode.workspace.applyEdit(edit); + vscode.window.showInformationMessage('Format TPTP file successful.'); + } + } + + }); +} diff --git a/tptplus/client/src/prettyPrint/prettyPrintErrors.ts b/tptplus/client/src/prettyPrint/prettyPrintErrors.ts new file mode 100644 index 0000000..74ef799 --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintErrors.ts @@ -0,0 +1,6 @@ +export const DUPLICATE_FORMULA_NAME_ERROR_PREFIX = + 'ERROR: Duplicate annotated formula name'; + +export function isDuplicateFormulaNameError(message: string): boolean { + return message.trim().startsWith(DUPLICATE_FORMULA_NAME_ERROR_PREFIX); +} diff --git a/tptplus/client/src/systemB4TptpOutput.ts b/tptplus/client/src/systemB4TptpOutput.ts new file mode 100644 index 0000000..894a727 --- /dev/null +++ b/tptplus/client/src/systemB4TptpOutput.ts @@ -0,0 +1,42 @@ +import { JSDOM } from 'jsdom'; + +/** + * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. + */ +export function extractSystemB4TptpOutput(html: string): string | undefined { + const dom = new JSDOM(html); + const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined; + if (preText === undefined) { + return undefined; + } + + const startMarker = '% START OF SYSTEM OUTPUT'; + const endMarker = '% END OF SYSTEM OUTPUT'; + const lines = preText.split('\n'); + const startLine = lines.findIndex(line => line.trim() === startMarker); + let endLine = -1; // TODO: use `findLastIndex`? + for (let i = lines.length - 1; i >= Math.max(0, startLine); i -= 1) { + if (lines[i].trim() === endMarker) { + endLine = i; + break; + } + } + + if (startLine === -1 || endLine === -1 || startLine >= endLine) { + return undefined; + } + + return lines.slice(startLine + 1, endLine).join('\n'); +} + +export function lastNonemptyLine(text: string): string | undefined { + const lines = text.split('\n'); + for (let i = lines.length - 1; i >= 0; i -= 1) { + const line = lines[i].trim(); + if (line) { + return line; + } + } + + return undefined; +} diff --git a/tptplus/images/icons/Syntax.png b/tptplus/images/icons/Syntax.png new file mode 100644 index 0000000..6b12f2a Binary files /dev/null and b/tptplus/images/icons/Syntax.png differ diff --git a/tptplus/images/TPTPWorld.png b/tptplus/images/icons/TPTPWorld.png similarity index 100% rename from tptplus/images/TPTPWorld.png rename to tptplus/images/icons/TPTPWorld.png diff --git a/tptplus/images/TPTPWorld.svg b/tptplus/images/icons/TPTPWorld.svg similarity index 100% rename from tptplus/images/TPTPWorld.svg rename to tptplus/images/icons/TPTPWorld.svg diff --git a/tptplus/native/tptp-pretty/CMakeLists.txt b/tptplus/native/tptp-pretty/CMakeLists.txt index 6ae4b11..8a49688 100644 --- a/tptplus/native/tptp-pretty/CMakeLists.txt +++ b/tptplus/native/tptp-pretty/CMakeLists.txt @@ -1,6 +1,6 @@ cmake_minimum_required(VERSION 3.18) -project(TPTPPrettyPrinter LANGUAGES C) +project(TPTPPrettyPrint LANGUAGES C) # provide clues to IDE IntelliSense set(CMAKE_EXPORT_COMPILE_COMMANDS ON) diff --git a/tptplus/native/tptp-pretty/src/tptp4X_api.c b/tptplus/native/tptp-pretty/src/tptp4X_api.c index b679573..f62cf3e 100644 --- a/tptplus/native/tptp-pretty/src/tptp4X_api.c +++ b/tptplus/native/tptp-pretty/src/tptp4X_api.c @@ -20,6 +20,8 @@ typedef struct { READFILE InputStream; SIGNATURE Signature; ANNOTATEDFORMULA AnnotatedFormula; + char * NamesBuffer; + int NamesBufferSize; FILE * OutputStream; char * OutputBuffer; size_t OutputLength; @@ -51,6 +53,24 @@ ThisNodeType != blank_line) { return(1); } +// Mirror `CheckOneDuplicateName` in NumberNames.c of TPTP4X +// TODO: improve time complexity? perhaps using ANTLR-based parser? +static int CheckOneDuplicateNameLikeTptp4X(TPTP4XPrettyState * State) { + + char * Name; + + if ((Name = GetName(State->AnnotatedFormula, NULL)) != NULL) { + if (NameInList(Name, State->NamesBuffer)) { + printf("ERROR: Duplicate annotated formula name \"%s\"\n", Name); + fflush(stdout); + return(0); + } + ExtendString(&(State->NamesBuffer), Name, &(State->NamesBufferSize)); + ExtendString(&(State->NamesBuffer), "\n", &(State->NamesBufferSize)); + } + return(1); +} + // This runs on normal returns only. Fatal JJParser errors exit the disposable // child process before control reaches this cleanup path. static void CleanupPrettyState(TPTP4XPrettyState * State) { @@ -70,6 +90,9 @@ static void CleanupPrettyState(TPTP4XPrettyState * State) { if (State->OutputStream != NULL) { fclose(State->OutputStream); } + if (State->NamesBuffer != NULL) { + Free((void **)&(State->NamesBuffer)); + } free(State->OutputBuffer); free(State); } @@ -100,9 +123,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { OldSZSStatusReporting = GetSZSStatusReporting(); SetNeedForNonLogicTokens(1); - SetAllowFreeVariables(0); + SetAllowFreeVariables(0); // no getter for AllowFreeVariables (default value is 0) SetWarnings(0); - SetSZSStatusReporting(0); + SetSZSStatusReporting(1); State->OutputStream = open_memstream(&(State->OutputBuffer), &(State->OutputLength)); if (State->OutputStream == NULL) { @@ -116,6 +139,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { NextToken(State->InputStream); State->Signature = NewSignature(); LastNodeType = nontype; + State->NamesBuffer = (char *)Malloc(sizeof(String)); + State->NamesBuffer[0] = '\0'; + State->NamesBufferSize = sizeof(String); // Reading formulae one-by-one while (!CheckTokenType(State->InputStream, endeof)) { @@ -123,6 +149,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { if (State->AnnotatedFormula == NULL) { goto finish; } + if (!CheckOneDuplicateNameLikeTptp4X(State)) { + goto finish; + } if (!PrintAnnotatedFormulaLikeFtptp(State, &LastNodeType)) { goto finish; } @@ -139,7 +168,7 @@ char * tptp4x_pretty_print_tptp(const char * Input) { finish: SetNeedForNonLogicTokens(OldNeedNonLogicTokens); - SetAllowFreeVariables(0); + SetAllowFreeVariables(0); // no getter for AllowFreeVariables (default value is 0) SetWarnings(OldWarnings); SetSZSStatusReporting(OldSZSStatusReporting); CleanupPrettyState((TPTP4XPrettyState *)State); diff --git a/tptplus/package-lock.json b/tptplus/package-lock.json index c720f7d..e895acd 100644 --- a/tptplus/package-lock.json +++ b/tptplus/package-lock.json @@ -1,12 +1,12 @@ { - "name": "tptpeditor", - "version": "0.1.7", + "name": "tptp", + "version": "0.1.11", "lockfileVersion": 3, "requires": true, "packages": { "": { - "name": "tptpeditor", - "version": "0.1.7", + "name": "tptp", + "version": "0.1.11", "hasInstallScript": true, "devDependencies": { "@types/node": "^16.18.34", diff --git a/tptplus/package.json b/tptplus/package.json index e1d39a9..b429d2d 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -3,8 +3,8 @@ "displayName": "TPTP", "publisher": "TPTPWorld", "description": "Syntax highlighting, error detection, pretty-printing, and proving & processing theorems functions for TPTP language", - "version": "0.1.9", - "icon": "images/TPTPWorld.png", + "version": "0.1.11", + "icon": "images/icons/TPTPWorld.png", "repository": { "type": "git", "url": "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/TPTPWorld/VSCodeExtension" @@ -33,8 +33,8 @@ ], "configuration": "./language-configuration.json", "icon": { - "light": "./images/TPTPWorld.svg", - "dark": "./images/TPTPWorld.svg" + "light": "./images/icons/TPTPWorld.svg", + "dark": "./images/icons/TPTPWorld.svg" } } ], @@ -48,15 +48,19 @@ "commands": [ { "command": "tptp.formatDocument", - "title": "TPTP: Format Document" + "title": "TPTP: Format Document (legacy)" }, { "command": "tptp.prepareProblem", "title": "TPTP: Prepare Problem" }, { - "command": "tptp.formatProblem", - "title": "TPTP: Format TPTP File" + "command": "tptp.prettyPrint", + "title": "TPTP: Check Syntax and Format TPTP File", + "icon": { + "light": "./images/icons/Syntax.png", + "dark": "./images/icons/Syntax.png" + } }, { "command": "tptp.proveProblem", @@ -86,7 +90,7 @@ "menus": { "editor/title": [ { - "command": "tptp.formatDocument", + "command": "tptp.prettyPrint", "when": "editorLangId == tptp", "group": "navigation" } @@ -98,7 +102,7 @@ "group": "navigation" }, { - "command": "tptp.formatProblem", + "command": "tptp.prettyPrint", "when": "editorLangId == tptp", "group": "navigation" },