diff --git a/CHANGELOG.md b/CHANGELOG.md index 256f2e1..f7a0d9b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ ### 1.5.1 - Add support for PO code lenses. +- Subsequent launches of polymorphic code lenses now prefill type arguments. +- Fix "Debug example" in QuickCheck panel of PO view in workspaces with multiple modules. ### 1.5.0 - Update VDMJ JARs to stable 4.6.0 release. diff --git a/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar index 86bc0b8..6761e4c 100644 Binary files a/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar and b/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar differ diff --git a/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar index cb618ca..5a6c94c 100644 Binary files a/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar and b/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar differ diff --git a/resources/jars/vdmj/lsp-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/lsp-4.7.0-SNAPSHOT.jar index 54f60c6..c92f70b 100644 Binary files a/resources/jars/vdmj/lsp-4.7.0-SNAPSHOT.jar and b/resources/jars/vdmj/lsp-4.7.0-SNAPSHOT.jar differ diff --git a/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar index 229c7b4..8d9adf1 100644 Binary files a/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar and b/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar differ diff --git a/src/handlers/AddRunConfigurationHandler.ts b/src/handlers/AddRunConfigurationHandler.ts index 0febdc2..2f4d4be 100644 --- a/src/handlers/AddRunConfigurationHandler.ts +++ b/src/handlers/AddRunConfigurationHandler.ts @@ -6,7 +6,7 @@ import { VdmDebugConfiguration } from "../dap/VdmDapSupport"; import { guessDialect, VdmDialect } from "../util/DialectUtil"; import AutoDisposable from "../helper/AutoDisposable"; -type VdmType = string; +type VdmTypeParameter = string; interface VdmArgument { name: string; @@ -32,7 +32,10 @@ interface VdmLaunchLensConfiguration { constructors?: [VdmArgument[]]; applyName: string; applyArgs: VdmArgument[][]; - applyTypes?: VdmType[]; + applyTypes?: VdmTypeParameter[]; + settings: any; + properties: any; + params: any; } export class AddRunConfigurationHandler extends AutoDisposable { @@ -42,6 +45,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Argument storage, map from workspacefolder name to arguments private lastConfigCtorArgs: Map = new Map(); private lastConfigApplyArgs: Map = new Map(); + private lastConfigApplyTypes: Map> = new Map(); constructor() { super(); @@ -142,6 +146,18 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Add remote control if (input.remoteControl) runConfig.remoteControl = input.remoteControl; + if (input.settings) { + runConfig.settings = input.settings; + } + + if (input.properties) { + runConfig.properties = input.properties; + } + + if (input.params) { + runConfig.params = input.params; + } + // Add command if (input.applyName) { // Warn user that types might be unresolved for projects with unsaved files @@ -181,7 +197,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Add class initialisation // A constructor cannot be polymorphic, so no type params are ever available - await this.requestArguments([input.constructors[cIndex]], [], input.defaultName, "constructor").then( + await this.requestArguments([input.constructors[cIndex]], [], input.defaultName, wsFolder.name).then( () => { command += `new ${this.getCommandString(input.defaultName, [input.constructors[cIndex]], [])}.`; this.lastConfigCtorArgs.set(wsFolder.name, input.constructors[cIndex]); @@ -193,10 +209,17 @@ export class AddRunConfigurationHandler extends AutoDisposable { } // Add function/operation call to command - await this.requestArguments(input.applyArgs, input.applyTypes ?? [], input.applyName, "operation/function").then( + await this.requestArguments(input.applyArgs, input.applyTypes ?? [], input.applyName, wsFolder.name).then( (types) => { command += this.getCommandString(input.applyName, input.applyArgs, Array.from(types.values())); this.lastConfigApplyArgs.set(wsFolder.name, input.applyArgs); + + const lastWsConfigApplyTypes = + this.lastConfigApplyTypes.get(wsFolder.name) ?? new Map(); + Array.from(types.entries()).forEach(([typeParam, resolvedType]) => + lastWsConfigApplyTypes.set(typeParam, resolvedType) + ); + this.lastConfigApplyTypes.set(wsFolder.name, lastWsConfigApplyTypes); }, () => { throw new Error("Operation/function arguments missing"); @@ -249,19 +272,25 @@ export class AddRunConfigurationHandler extends AutoDisposable { return runConf.name.startsWith(AddRunConfigurationHandler.lensNameBegin); } - private async requestConcreteTypes(types: VdmType[], outlineString: string, requestType: string): Promise> { - const concreteTypes: Map = new Map(); + private async requestConcreteTypes( + types: VdmTypeParameter[], + outlineString: string, + wsName: string + ): Promise> { + const concreteTypes: Map = new Map(); for (const [idx, t] of types.entries()) { // concrete types don't need to be resolved if (!t.startsWith("@")) { concreteTypes.set(idx.toString(), t); continue; } + const concreteType = await window.showInputBox({ - prompt: `Input type for ${requestType}`, + prompt: `Enter type for ${t}`, title: outlineString, ignoreFocusOut: true, placeHolder: t, + value: this.lastConfigApplyTypes.get(wsName)?.get(t), }); if (concreteType === undefined) { @@ -274,12 +303,12 @@ export class AddRunConfigurationHandler extends AutoDisposable { return Promise.resolve(concreteTypes); } - private async requestArgumentValues(args: VdmArgument[][], outlineString: string, requestType: string): Promise { + private async requestArgumentValues(args: VdmArgument[][], outlineString: string): Promise { const flattenedArgs = args.flat(); for await (let a of flattenedArgs) { let value = await window.showInputBox({ - prompt: `Input argument for ${requestType}`, + prompt: `Enter value for [${a.name}: ${a.type}]`, title: outlineString, ignoreFocusOut: true, placeHolder: `${a.name}: ${a.type}`, @@ -294,7 +323,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { } } - private applyTypesToArgs(argLists: VdmArgument[][], types: Map): VdmArgument[][] { + private applyTypesToArgs(argLists: VdmArgument[][], types: Map): VdmArgument[][] { return argLists.map((args) => { return args.map((a) => { const concreteType = types.get(a.type); @@ -307,17 +336,22 @@ export class AddRunConfigurationHandler extends AutoDisposable { }); } - private async requestArguments(args: VdmArgument[][], types: VdmType[], name: string, type: string): Promise> { + private async requestArguments( + args: VdmArgument[][], + types: VdmTypeParameter[], + name: string, + wsName: string + ): Promise> { const commandString = this.getCommandOutlineString(name, args, types); // Request type arguments from user - const concreteTypes = await this.requestConcreteTypes(types, commandString, type); + const concreteTypes = await this.requestConcreteTypes(types, commandString, wsName); // Request argument values from user - requestArgumentValues modifies args, changing the .value property. const typedArgs = this.applyTypesToArgs(args, concreteTypes); const commandStringConcrete = this.getCommandOutlineString(name, typedArgs); - await this.requestArgumentValues(typedArgs, commandStringConcrete, type); + await this.requestArgumentValues(typedArgs, commandStringConcrete); return Promise.resolve(concreteTypes); } @@ -365,14 +399,14 @@ export class AddRunConfigurationHandler extends AutoDisposable { }); } - private getCommandOutlineString(name: string, args: VdmArgument[][], typeParameters: VdmType[] = []): string { + private getCommandOutlineString(name: string, args: VdmArgument[][], typeParameters: VdmTypeParameter[] = []): string { const typeParametersOutline = typeParameters.length === 0 ? "" : `[${typeParameters.join(", ")}]`; const argumentLists = args.map((a) => `(${a.map((x) => `${x.name}: ${x.type}`).join(", ")})`).join(""); let command = `${name}${typeParametersOutline}${argumentLists}`; return command; } - private getCommandString(name: string, args: VdmArgument[][], types: VdmType[]): string { + private getCommandString(name: string, args: VdmArgument[][], types: VdmTypeParameter[]): string { const typeArguments = types.length === 0 ? "" : `[${types.join(", ")}]`; const argumentLists = args.map((a) => `(${a.map((x) => x.value).join(", ")})`).join(""); let command = `${name}${typeArguments}${argumentLists}`; diff --git a/src/slsp/views/ProofObligationPanel.ts b/src/slsp/views/ProofObligationPanel.ts index 6527c35..0f7a89c 100644 --- a/src/slsp/views/ProofObligationPanel.ts +++ b/src/slsp/views/ProofObligationPanel.ts @@ -14,15 +14,15 @@ import { ExtensionContext, commands, DocumentSelector, - debug, ProgressLocation, Progress, TabInputWebview, + debug, } from "vscode"; import { ClientManager } from "../../ClientManager"; import * as util from "../../util/Util"; import { isSameUri, isSameWorkspaceFolder } from "../../util/WorkspaceFoldersUtil"; -import { VdmDapSupport } from "../../dap/VdmDapSupport"; +// import { VdmDapSupport } from "../../dap/VdmDapSupport"; import { ProofObligationCounterExample, ProofObligationWitness, QuickCheckInfo } from "../protocol/ProofObligationGeneration"; import { CancellationToken } from "vscode-languageclient"; @@ -343,14 +343,19 @@ export class ProofObligationPanel implements Disposable { window.showTextDocument(doc.uri, { selection: po.location.range, viewColumn: 1 }); break; case "debugQCRun": - const requestBody = { - expression: message.data, - context: "repl", - }; - - VdmDapSupport.getAdHocVdmDebugger(this._lastWsFolder, false).then((ds) => { - setTimeout(() => ds.customRequest("evaluate", requestBody).then(() => debug.stopDebugging(ds)), 100); - }); + // const requestBody = { + // expression: message.data, + // context: "repl", + // }; + + console.log("debugging with", message.data, message); + // VdmDapSupport.startDebuggerWithCommand(message.data, this._lastWsFolder, true, false); + debug.startDebugging(this._lastWsFolder, message.data); + + // VdmDapSupport.getAdHocVdmDebugger(this._lastWsFolder, false).then((ds) => { + // ds.customRequest("evaluate", requestBody); + // // setTimeout(() => ds.customRequest("evaluate", requestBody).then(() => debug.stopDebugging(ds)), 100); + // }); break; case "runQC": window.withProgress( diff --git a/src/webviews/proof_obligations/QuickCheckPanel.tsx b/src/webviews/proof_obligations/QuickCheckPanel.tsx index f812a06..0ca1943 100644 --- a/src/webviews/proof_obligations/QuickCheckPanel.tsx +++ b/src/webviews/proof_obligations/QuickCheckPanel.tsx @@ -3,6 +3,7 @@ import { TableHeader } from "./ProofObligationsTableHeader"; import { FormattedProofObligation } from "./ProofObligationsView"; import { VSCodeAPI } from "../shared.types"; import { MouseEvent } from "react"; +import { VdmLaunchConfiguration } from "../../handlers/AddRunConfigurationHandler"; interface QuickCheckExampleTableProps { variables: Array<[string, string]>; @@ -48,12 +49,12 @@ export const QuickCheckPanel = ({ proofObligation, vscodeApi, onClose }: QuickCh // There will never be both a counterexample and a witness, so the following array is either equal to counterExampleVariables or witnessVariables or [] const allVariables = [...counterExampleVariables, ...witnessVariables]; - let launchCommand: string | null = null; + let launchCommand: VdmLaunchConfiguration | null = null; if (proofObligation.counterexample) { - launchCommand = proofObligation.counterexample.launch?.command ?? null; + launchCommand = proofObligation.counterexample.launch ?? null; } else if (proofObligation.witness) { - launchCommand = proofObligation.witness.launch?.command ?? null; + launchCommand = proofObligation.witness.launch ?? null; } return (