Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@gebner
gebner committed Apr 29, 2024
1 parent f6e99fc commit c14b59b
Show file tree
Hide file tree
Showing 3 changed files with 77 additions and 119 deletions.
92 changes: 22 additions & 70 deletions client/src/extension.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ import {
Range,
Position
} from 'vscode-languageclient/node';
import { StatusNotificationParams, statusNotification } from './fstarExtensions';
import { StatusNotificationParams, killAllNotification, killAndRestartSolverNotification, restartNotification, statusNotification, verifyToPositionNotification } from './fstarExtensions';

let client: LanguageClient;

Expand Down Expand Up @@ -76,12 +76,6 @@ const inProgressBackground = vscode.window.createTextEditorDecorationType({
backgroundColor: 'rgba(100, 0, 255, 0.5)'
});


interface AlertMessage {
uri: string;
message: string;
}

function posToCode(range: Position): vscode.Position {
return new vscode.Position(range.line, range.character);
}
Expand Down Expand Up @@ -137,11 +131,6 @@ function updateDecorations() {
}
}

// This function is called by the server in case F* crashed or was killed
async function handleAlert(msg: AlertMessage) {
await vscode.window.showErrorMessage(msg.message + "\n On document: " + msg.uri);
}

export async function activate(context: ExtensionContext) {
// The server is implemented in node
const serverModule = context.asAbsolutePath(
Expand Down Expand Up @@ -174,66 +163,32 @@ export async function activate(context: ExtensionContext) {
);

client.onNotification(statusNotification, status => handleStatus(status));
client.onNotification('fstar-vscode-assistant/alert', handleAlert);
vscode.window.onDidChangeVisibleTextEditors(() => updateDecorations());

// register a command for Ctrl+.
const verifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', async (textEditor, edit) => {
// console.log('Client: Command <verify-to-position> executed with uri: ' + textEditor.document.uri + " at positon " + textEditor.selection.active.line + ", " + textEditor.selection.active.character);
await client.sendRequest('fstar-vscode-assistant/verify-to-position', [textEditor.document.uri.toString(), textEditor.selection.active]);
});
context.subscriptions.push(verifyCommand);
context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', textEditor =>
client.sendNotification(verifyToPositionNotification, {
uri: textEditor.document.uri.toString(),
lax: false,
position: textEditor.selection.active,
})));

// register a command for Ctrl+;,Ctrl+.
const reloadAndVerifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/restart', async (textEditor, edit) => {
// console.log('Client: Command <restart> executed with uri: ' + textEditor.document.uri);
await client.sendRequest('fstar-vscode-assistant/restart', textEditor.document.uri.toString());
});
context.subscriptions.push(reloadAndVerifyCommand);
context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/restart', textEditor =>
client.sendNotification(restartNotification, { uri: textEditor.document.uri.toString() })));

// register a command for Ctrl+Shift+.
const laxVerifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/lax-to-position', async (textEditor, edit) => {
// console.log('Client: Command <lax-to-position> executed with uri: ' + textEditor.document.uri + " at positon " + textEditor.selection.active.line + ", " + textEditor.selection.active.character);
await client.sendRequest('fstar-vscode-assistant/lax-to-position', [textEditor.document.uri.toString(), textEditor.selection.active]);
});
context.subscriptions.push(laxVerifyCommand);

const killAndRestartSolverCommand =
vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-and-restart-solver', async (textEditor, edit) => {
await client.sendRequest('fstar-vscode-assistant/kill-and-restart-solver', [textEditor.document.uri.toString()]);
});
context.subscriptions.push(killAndRestartSolverCommand);
context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/lax-to-position', textEditor =>
client.sendNotification(verifyToPositionNotification, {
uri: textEditor.document.uri.toString(),
lax: true,
position: textEditor.selection.active,
})));

context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-and-restart-solver', textEditor =>
client.sendNotification(killAndRestartSolverNotification, { uri: textEditor.document.uri.toString() })));

const killAllCommand =
vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-all', async (textEditor, edit) => {
await client.sendRequest('fstar-vscode-assistant/kill-all', []);
});
context.subscriptions.push(killAllCommand);

// console.log("Activate called on " + context.asAbsolutePath("/"));

workspace.onDidChangeTextDocument(async (event) => {
// console.log("OnDidChangeTextDocument");
const textDoc = event.document;
let minRange : vscode.Range | undefined;
function compareRange (a? : vscode.Range, b? : vscode.Range) : number {
if (!a) { return -1; }
if (!b) { return 1; }
if (a.start.line < b.start.line) return -1;
if (a.start.line > b.start.line) return 1;
if (a.start.character < b.start.character) return -1;
if (a.start.character > b.start.character) return 1;
return 0;
}
event.contentChanges.forEach((change) => {
if (compareRange(minRange, change.range) < 0) {
minRange = change.range;
}
});
if (minRange) {
await client.sendRequest('fstar-vscode-assistant/text-doc-changed', [textDoc.uri.toString(), minRange]);
}
});
context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-all', () =>
client.sendNotification(killAllNotification, {})));

workspace.onDidChangeConfiguration((event) => {
const cfg = workspace.getConfiguration('fstarVSCodeAssistant');
Expand All @@ -249,9 +204,6 @@ export async function activate(context: ExtensionContext) {
await client.start();
}

export function deactivate(): Thenable<void> | undefined {
if (!client) {
return undefined;
}
return client.stop();
export async function deactivate() {
await client?.stop();
}
27 changes: 25 additions & 2 deletions server/src/fstarExtensions.ts
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import { ProtocolNotificationType, Range } from 'vscode-languageserver-protocol';
import { ProtocolNotificationType, Position, Range } from 'vscode-languageserver-protocol';

export type StatusKind
= 'ok'
Expand All @@ -18,8 +18,31 @@ export interface StatusNotificationParams {
uri: string;
fragments: FragmentStatus[];
}

export const statusNotification: ProtocolNotificationType<StatusNotificationParams, RegistrationParams> =
new ProtocolNotificationType('$/fstar/status');

export interface RestartParams {
uri: string;
}
export const restartNotification: ProtocolNotificationType<RestartParams, RegistrationParams> =
new ProtocolNotificationType('$/fstar/restart');

export interface KillAndRestartSolverParams {
uri: string;
}
export const killAndRestartSolverNotification: ProtocolNotificationType<KillAndRestartSolverParams, RegistrationParams> =
new ProtocolNotificationType('$/fstar/killAndRestartSolver');

export interface KillAllParams {}
export const killAllNotification: ProtocolNotificationType<KillAllParams, RegistrationParams> =
new ProtocolNotificationType('$/fstar/killAll');

export interface VerifyToPositionParams {
uri: string;
position: Position;
lax: boolean;
}
export const verifyToPositionNotification: ProtocolNotificationType<VerifyToPositionParams, RegistrationParams> =
new ProtocolNotificationType('$/fstar/verifyToPosition');

interface RegistrationParams {}
77 changes: 30 additions & 47 deletions server/src/server.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ import { FStar, FStarConfig } from './fstar';
import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition } from './fstar_messages';
import * as path from 'path';
import { pathToFileURL } from 'url';
import { statusNotification, FragmentStatus } from './fstarExtensions';
import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification } from './fstarExtensions';

// LSP Server
//
Expand Down Expand Up @@ -105,13 +105,7 @@ export class Server {
this.connection.onInitialize(params => this.onInitialize(params));
this.connection.onInitialized(() => this.onInitializedHandler());
// We don't do anything special when the configuration changes
this.connection.onDidChangeConfiguration(async _change => {
await this.updateConfigurationSettings();
});
this.connection.onDidChangeWatchedFiles(_change => {
// Monitored files have change in VSCode
// connection.console.log('We received an file change event');
});
this.connection.onDidChangeConfiguration(() => this.updateConfigurationSettings());
this.connection.onCompletion(textDocumentPosition =>
this.getDocumentState(textDocumentPosition.textDocument.uri)?.onCompletion(textDocumentPosition));
// This handler resolves additional information for the item selected in
Expand All @@ -125,17 +119,19 @@ export class Server {
this.getDocumentState(formatParams.textDocument.uri)?.onDocumentRangeFormatting(formatParams));

// Custom events
this.connection.onRequest("fstar-vscode-assistant/verify-to-position", params =>
this.getDocumentState(params[0])?.onVerifyToPositionRequest(params));
this.connection.onRequest("fstar-vscode-assistant/lax-to-position", params =>
this.getDocumentState(params[0])?.onLaxToPositionRequest(params));
this.connection.onRequest("fstar-vscode-assistant/restart", uri =>
this.connection.onNotification(verifyToPositionNotification, ({uri, position, lax}) => {
const state = this.getDocumentState(uri);
if (lax) {
state?.laxToPosition(position);
} else {
state?.verifyToPosition(position);
}
});
this.connection.onNotification(restartNotification, ({uri}) =>
this.onRestartRequest(uri));
this.connection.onRequest("fstar-vscode-assistant/text-doc-changed", params =>
this.getDocumentState(params[0])?.onTextDocChanged(params));
this.connection.onRequest("fstar-vscode-assistant/kill-and-restart-solver", uri =>
this.connection.onNotification(killAndRestartSolverNotification, ({uri}) =>
this.getDocumentState(uri)?.killAndRestartSolver());
this.connection.onRequest("fstar-vscode-assistant/kill-all", params =>
this.connection.onNotification(killAllNotification, () =>
this.onKillAllRequest());
}

Expand All @@ -152,10 +148,6 @@ export class Server {
return this.documentStates.get(uri);
}

getDocument(uri: string): TextDocument | undefined {
return this.documents.get(uri);
}

async updateConfigurationSettings() {
const settings = await this.connection.workspace.getConfiguration('fstarVSCodeAssistant');
if (settings.debug) {
Expand Down Expand Up @@ -272,10 +264,8 @@ export class Server {
docState.fstar_lax?.validateFStarDocument('lax');
}

private async onRestartRequest(uri: any) {
// console.log("Received restart request with parameters: " + uri);
const textDocument = this.getDocument(uri);
if (!textDocument) return;
private async onRestartRequest(uri: string) {
if (!this.documents.get(uri)) return;
this.documentStates.get(uri)?.dispose();
this.documentStates.delete(uri);
await this.refreshDocumentState(uri);
Expand Down Expand Up @@ -343,7 +333,7 @@ export class DocumentState {
this.fstar_lax?.dispose();

// Clear all diagnostics for a document when it is closed
this.server.connection.sendDiagnostics({
void this.server.connection.sendDiagnostics({
uri: this.uri,
diagnostics: [],
});
Expand Down Expand Up @@ -397,25 +387,6 @@ export class DocumentState {
return (this.fstar_lax ?? this.fstar).onDocumentRangeFormatting(formatParams);
}

onVerifyToPositionRequest(params: any) {
const position: { line: number, character: number } = params[1];
this.verifyToPosition(position);
}

onLaxToPositionRequest(params: any) {
const position: { line: number, character: number } = params[1];
this.laxToPosition(position);
}

onTextDocChanged(params: any) {
const range: { line: number; character: number }[] = params[1];
// TODO(klinvill): It looks like this function can only be called for
// non-lax checking. Is that correct?
const fstarPos: FStarPosition = [range[0].line + 1, range[0].character];
this.fstar?.fstar?.cancelFBQ(fstarPos);
this.fstar_lax?.fstar?.cancelFBQ(fstarPos);
}

async killAndRestartSolver() {
// TODO(klinvill): It looks like this function only restarts the
// standard F* solver (not the lax one), is this the desired behavior?
Expand All @@ -435,7 +406,7 @@ export class DocumentState {
diags.push(...this.fstar_lax.results.diagnostics.filter(d => posLe(lastPos, d.range.start)));
}

this.server.connection.sendDiagnostics({
void this.server.connection.sendDiagnostics({
uri: this.uri,
diagnostics: diags,
});
Expand All @@ -458,7 +429,7 @@ export class DocumentState {
});
}

this.server.connection.sendNotification(statusNotification, {
void this.server.connection.sendNotification(statusNotification, {
uri: this.uri,
fragments: statusFragments,
});
Expand Down Expand Up @@ -498,6 +469,13 @@ function emptyResults(): DocumentResults {
};
}

function findFirstDiffPos(a: string, b: string): undefined | number {
if (a === b) return undefined;
let i = 0;
while (a[i] === b[i]) i++;
return i;
}

export class DocumentProcess {
uri: string;
filePath: string;
Expand Down Expand Up @@ -543,6 +521,11 @@ export class DocumentProcess {
if (!this.lastPendingChange) return;
this.validateFStarDocument(this.lax ? 'lax' : 'cache');
}, 200);

const diffPos = findFirstDiffPos(this.currentDoc.getText(), this.lastPendingChange.getText());
if (diffPos) {
this.fstar.cancelFBQ(posAsFStarPos(this.currentDoc.positionAt(diffPos)));
}
}

// Lookup the proof state table for the line at the cursor
Expand Down

0 comments on commit c14b59b

Please sign in to comment.