Skip to content

Commit

Permalink
Merge pull request #24 from lorchrob/type-decl-buttons
Browse files Browse the repository at this point in the history 
Update buttons for type decls
  • Loading branch information
@daniel-larraz
daniel-larraz authored Jun 19, 2024
2 parents ea0f8e1 + eb9a4b5 commit 92e7b6b
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 16 deletions.
40 changes: 28 additions & 12 deletions src/Kind2.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
* Licensed under the MIT License. See LICENSE in the project root for license information.
*/

import * as os from "os";
import * as path from "path";
import { CancellationToken, CancellationTokenSource, CodeLens, CodeLensProvider, DecorationOptions, Event, EventEmitter, ExtensionContext, Position, ProviderResult, Range, ShellExecution, Task, tasks, TaskScope, TextDocument, TextEditorDecorationType, TreeDataProvider, TreeItem, TreeItemCollapsibleState, TreeView, Uri, window } from "vscode";
import { LanguageClient } from "vscode-languageclient";
Expand Down Expand Up @@ -41,6 +40,8 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
["unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("unrealizable")) })],
["contract realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("contract realizable")) })],
["contract unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("contract unrealizable")) })],
["type realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("type realizable")) })],
["type unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("type unrealizable")) })],
["inputs realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("inputs realizable")) })],
["inputs unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("inputs unrealizable")) })],
])
Expand All @@ -54,20 +55,25 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
if (file) {
for (const component of file.components) {
let range = new Range(component.line, 0, component.line, 0);

if (component.state.length > 0 && component.state[0] === "running") {
codeLenses.push(new CodeLens(range, { title: "Cancel", command: "kind2/cancel", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
codeLenses.push(new CodeLens(range, { title: "Raw Output", command: "kind2/raw", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
} else if (component.imported) {
codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }))
codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
} else if (component.typeDecl) {
codeLenses. push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
} else {
codeLenses.push(new CodeLens(range, { title: "Check Properties", command: "kind2/check", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }))
}
codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
if (!component.imported) {
codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
codeLenses.push(new CodeLens(range, { title: "Raw Output", command: "kind2/raw", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
}
codeLenses.push(new CodeLens(range, { title: "Show in Explorer", command: "kind2/reveal", arguments: [component] }));
}
}
return codeLenses;
Expand Down Expand Up @@ -140,7 +146,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
public updateDecorations(): void {
let decorations = new Map<string, Map<State, DecorationOptions[]>>();
for (const file of this._files) {
decorations.set(file.uri, new Map<State, DecorationOptions[]>([["pending", []], ["running", []], ["passed", []], ["reachable", []], ["failed", []], ["unreachable", []], ["stopped", []], ["unknown", []], ["errored", []], ["realizable", []], ["inputs realizable", []], ["contract realizable", []], ["unrealizable", []], ["inputs unrealizable", []], ["contract unrealizable", []],]));
decorations.set(file.uri, new Map<State, DecorationOptions[]>([["pending", []], ["running", []], ["passed", []], ["reachable", []], ["failed", []], ["unreachable", []], ["stopped", []], ["unknown", []], ["errored", []], ["realizable", []], ["inputs realizable", []], ["contract realizable", []], ["type realizable", []], ["unrealizable", []], ["inputs unrealizable", []], ["contract unrealizable", []], ["type unrealizable", []]]));
}
for (const file of this._files) {
for (const component of file.components) {
Expand Down Expand Up @@ -170,7 +176,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
}
for (const uri of decorations.keys()) {
let editor = window.visibleTextEditors.find(editor => editor.document.uri.toString() === uri);
for (const state of <State[]>["pending", "running", "passed", "reachable", "failed", "unreachable", "stopped", "unknown", "errored", "realizable", "unrealizable", "inputs realizable", "contract realizable", "inputs unrealizable", "contract unrealizable"]) {
for (const state of <State[]>["pending", "running", "passed", "reachable", "failed", "unreachable", "stopped", "unknown", "errored", "realizable", "unrealizable", "inputs realizable", "contract realizable", "inputs unrealizable", "contract unrealizable", "type realizable", "type unrealizable"]) {
editor?.setDecorations(this._decorationTypeMap.get(state)!, decorations.get(uri)?.get(state)!);
}
}
Expand Down Expand Up @@ -251,7 +257,11 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
if (component.contractStartLine === undefined) {
contractStart = component.startLine - 1;
}
file.components.push(new Component(component.name, component.startLine - 1, contractStart, file, component.imported));
var hasRefType = false;
if (component.containsRefinementType !== undefined) {
hasRefType = component.containsRefinementType === "true";
}
file.components.push(new Component(component.name, component.startLine - 1, contractStart, file, component.imported, component.kind, hasRefType));
}
}
this._files = this._files.concat(newFiles);
Expand Down Expand Up @@ -384,7 +394,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
this.updateDecorations();
let tokenSource = new CancellationTokenSource();
this._runningChecks.set(mainComponent, tokenSource);
await this._client.sendRequest("kind2/realizability", [mainComponent.uri, mainComponent.name], tokenSource.token).then((values: string[]) => {
await this._client.sendRequest("kind2/realizability", [mainComponent.uri, mainComponent.name, mainComponent.typeDecl], tokenSource.token).then((values: string[]) => {
let results: any[] = values.map(s => JSON.parse(s));
for (const nodeResult of results) {
let component = undefined;
Expand All @@ -402,6 +412,9 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
else if (analysisResult.context === "environment") {
analysis.realizabilitySource = "inputs"
}
else if (analysisResult.context === "type") {
analysis.realizabilitySource = "type"
}
else {
analysis.realizabilitySource = "imported node"
}
Expand Down Expand Up @@ -480,6 +493,9 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
else if (analysis.realizabilitySource === "contract") {
context = "contract"
}
else if (analysis.realizabilitySource === "type") {
context = "type"
}
await this._client.sendRequest("kind2/deadlock", [analysis.parent.uri, name, context]).then((dl: string) => {
WebPanel.createOrShow(this._context.extensionPath);
WebPanel.currentPanel?.sendMessage({ uri: analysis.parent.uri, main: analysis.parent.name, json: dl });
Expand Down
31 changes: 27 additions & 4 deletions src/treeNode.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,16 +21,22 @@ export class File implements File {
}

export type RealizabilityResult = "realizable" | "unrealizable"
export type RealizabilitySource = "inputs" | "contract" | "imported node"
export type RealizabilitySource = "inputs" | "contract" | "imported node" | "type"

export class Component {
private _state: State[];
private _analyses: Analysis[];
private _imported: boolean;
private _typeDecl: boolean;
private _hasRefType: boolean;
set analyses(analyses: Analysis[]) { this._analyses = analyses; }
get analyses(): Analysis[] { return this._analyses; }
set imported(imported: boolean) { this._imported = imported; }
get imported(): boolean { return this._imported; }
set typeDecl(typeDecl: boolean) { this._typeDecl = typeDecl; }
get typeDecl(): boolean { return this._typeDecl; }
set hasRefType(hasRefType: boolean) { this._hasRefType = hasRefType; }
get hasRefType(): boolean { return this._hasRefType; }
set state(state: State[]) {
if (this._analyses.length == 0) {
this._state = state;
Expand Down Expand Up @@ -88,18 +94,28 @@ export class Component {
if (property.state === "unknown") { unknownProperties.add(property.name); }
if (property.state === "errored") { erroredProperties.add(property.name); }
}
// "Trivial" type declaration realizability checks give a question mark
if (analysis.realizability === "realizable" && !this.hasRefType) {
return ["unknown"]
}
if (analysis.realizability === "realizable" && analysis.realizabilitySource === "contract") {
ret.push("contract realizable");
}
if (analysis.realizability === "realizable" && analysis.realizabilitySource === "inputs") {
ret.push("inputs realizable");
}
if (analysis.realizability === "realizable" && analysis.realizabilitySource === "type") {
ret.push("type realizable");
}
if (analysis.realizability === "unrealizable" && analysis.realizabilitySource === "contract") {
ret.push("contract unrealizable");
}
if (analysis.realizability === "unrealizable" && analysis.realizabilitySource === "inputs") {
ret.push("inputs unrealizable");
}
if (analysis.realizability === "unrealizable" && analysis.realizabilitySource === "type") {
ret.push("type unrealizable");
}
}
if (ret.length !== 0) {
return ret
Expand All @@ -123,10 +139,12 @@ export class Component {
return this.state.some(str => str.includes("unrealizable"))
}
get uri(): string { return this.parent.uri; }
constructor(readonly name: string, readonly line: number, readonly contractLine: number, readonly parent: File, readonly imported_comp: string) {
constructor(readonly name: string, readonly line: number, readonly contractLine: number, readonly parent: File, readonly importedComp: string, readonly compKind: string, readonly hasRefinementType: boolean) {
this._state = ["pending"];
this._analyses = [];
this._imported = imported_comp === "true";
this._imported = importedComp === "true";
this._typeDecl = compKind === "typeDecl";
this._hasRefType = hasRefinementType;
}
}

Expand Down Expand Up @@ -158,7 +176,8 @@ export class Property {
export type State =
"pending" | "running" | "passed" | "reachable" | "failed" | "unreachable"
| "unknown" | "stopped" | "errored" | "realizable" | "unrealizable" | "inputs realizable"
| "inputs unrealizable" | "contract realizable" | "contract unrealizable";
| "inputs unrealizable" | "contract realizable" | "contract unrealizable"
| "type realizable" | "type unrealizable";

export function statePath(state: State) {
switch (state) {
Expand All @@ -170,13 +189,15 @@ export function statePath(state: State) {
case "reachable":
case "contract realizable":
case "inputs realizable":
case "type realizable":
case "realizable":
return "icons/passed.svg";
case "failed":
case "unreachable":
case "unrealizable":
case "inputs unrealizable":
case "contract unrealizable":
case "type unrealizable":
return "icons/failed.svg";
case "unknown":
return "icons/unknown.svg";
Expand All @@ -197,13 +218,15 @@ export function stateIcon(state: State) {
case "reachable":
case "contract realizable":
case "inputs realizable":
case "type realizable":
case "realizable":
return new ThemeIcon("$(testing-passed-icon)", new ThemeColor("testing.iconPassed"));
case "failed":
case "unreachable":
case "unrealizable":
case "inputs unrealizable":
case "contract unrealizable":
case "type unrealizable":
return new ThemeIcon("$(testing-failed-icon)", new ThemeColor("testing.iconFailed"));
case "unknown":
return new ThemeIcon("$(question)", new ThemeColor("testing.iconQueued"));
Expand Down

0 comments on commit 92e7b6b

Please sign in to comment.