diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
new file mode 100644
index 000000000..b49836e07
--- /dev/null
+++ b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
@@ -0,0 +1,158 @@
+/*******************************************************************************
+ *
+ * Copyright (c) 2024 Nick Battle.
+ *
+ * Author: Nick Battle
+ *
+ * This file is part of VDMJ.
+ *
+ * VDMJ is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * VDMJ is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with VDMJ. If not, see .
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ ******************************************************************************/
+package workspace.lenses;
+
+import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition;
+import com.fujitsu.vdmj.po.patterns.POPattern;
+import com.fujitsu.vdmj.po.patterns.POPatternList;
+import com.fujitsu.vdmj.po.types.POPatternListTypePair;
+import com.fujitsu.vdmj.po.types.POPatternListTypePairList;
+import com.fujitsu.vdmj.pog.ProofObligation;
+import com.fujitsu.vdmj.tc.types.TCFunctionType;
+import com.fujitsu.vdmj.tc.types.TCOperationType;
+import com.fujitsu.vdmj.tc.types.TCType;
+import com.fujitsu.vdmj.tc.types.TCTypeList;
+
+import json.JSONArray;
+import json.JSONObject;
+
+/**
+ * A class to generate launch lenses for PO counterexamples.
+ */
+public class POLaunchDebugLens extends AbstractLaunchDebugLens
+{
+ private final ProofObligation po;
+
+ public POLaunchDebugLens(ProofObligation po)
+ {
+ this.po = po;
+ }
+
+ public JSONArray getLaunchLens()
+ {
+ JSONArray results = new JSONArray();
+ PODefinition def = po.definition;
+
+ if (isClientType("vscode") && def != null)
+ {
+ String launchName = null;
+ String defaultName = null;
+ String applyName = null;
+ JSONArray applyTypes = null;
+ JSONArray applyArgs = null;
+
+ if (def instanceof POExplicitFunctionDefinition)
+ {
+ POExplicitFunctionDefinition exdef = (POExplicitFunctionDefinition) def;
+
+ applyName = exdef.name.getName();
+ launchName = applyName;
+ defaultName = exdef.name.getModule();
+
+ if (exdef.typeParams != null)
+ {
+ applyTypes = new JSONArray();
+
+ for (TCType ptype: exdef.typeParams)
+ {
+ applyTypes.add(ptype.toString());
+ }
+ }
+
+ TCFunctionType ftype = (TCFunctionType) exdef.type;
+ applyArgs = getParams(exdef.paramPatternList.get(0), ftype.parameters);
+ }
+ else if (def instanceof POImplicitFunctionDefinition)
+ {
+ POImplicitFunctionDefinition imdef = (POImplicitFunctionDefinition) def;
+
+ applyName = imdef.name.getName();
+ launchName = applyName;
+ defaultName = imdef.name.getModule();
+ applyArgs = getParams(imdef.parameterPatterns);
+ }
+ else if (def instanceof POExplicitOperationDefinition)
+ {
+ POExplicitOperationDefinition exop = (POExplicitOperationDefinition) def;
+
+ applyName = exop.name.getName();
+ launchName = applyName;
+ defaultName = exop.name.getModule();
+ TCOperationType ftype = (TCOperationType) exop.type;
+ applyArgs = getParams(exop.parameterPatterns, ftype.parameters);
+ }
+ else if (def instanceof POImplicitOperationDefinition)
+ {
+ POImplicitOperationDefinition imop = (POImplicitOperationDefinition) def;
+
+ applyName = imop.name.getName();
+ launchName = applyName;
+ defaultName = imop.name.getModule();
+ applyArgs = getParams(imop.parameterPatterns);
+ }
+
+ if (launchName != null)
+ {
+ JSONArray constructors = null;
+
+ results.add(makeLens(po.location, "Counterexample", CODE_LENS_COMMAND,
+ launchArgs(launchName, defaultName, true, constructors, applyName, applyTypes, applyArgs)));
+ }
+ }
+
+ return results;
+ }
+
+ private JSONArray getParams(POPatternList patterns, TCTypeList types)
+ {
+ JSONArray params = new JSONArray();
+ int i = 0;
+
+ for (POPattern p: patterns)
+ {
+ params.add(new JSONObject("name", p.toString(), "type", types.get(i++).toString()));
+ }
+
+ return params;
+ }
+
+ private JSONArray getParams(POPatternListTypePairList ptList)
+ {
+ JSONArray params = new JSONArray();
+
+ for (POPatternListTypePair param: ptList)
+ {
+ for (POPattern p: param.patterns)
+ {
+ params.add(new JSONObject("name", p.toString(), "type", param.type.toString()));
+ }
+ }
+
+ return params;
+ }
+}
diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java
index 7760d16df..b02bc88e5 100644
--- a/lsp/src/main/java/workspace/plugins/POPlugin.java
+++ b/lsp/src/main/java/workspace/plugins/POPlugin.java
@@ -25,6 +25,10 @@
package workspace.plugins;
import java.io.File;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Vector;
import com.fujitsu.vdmj.lex.Dialect;
import com.fujitsu.vdmj.mapper.Mappable;
@@ -43,7 +47,9 @@
import workspace.MessageHub;
import workspace.events.CheckCompleteEvent;
import workspace.events.CheckPrepareEvent;
+import workspace.events.CodeLensEvent;
import workspace.events.LSPEvent;
+import workspace.lenses.POLaunchDebugLens;
abstract public class POPlugin extends AnalysisPlugin implements EventListener
{
@@ -64,9 +70,13 @@ public static POPlugin factory(Dialect dialect)
}
}
+ private final Map> codeLenses;
+
protected POPlugin()
{
super();
+
+ codeLenses = new HashMap>();
}
@Override
@@ -88,6 +98,7 @@ public void init()
eventhub.register(CheckPrepareEvent.class, this);
eventhub.register(CheckCompleteEvent.class, this);
+ eventhub.register(CodeLensEvent.class, this);
}
@Override
@@ -118,6 +129,11 @@ else if (event instanceof CheckCompleteEvent)
new JSONObject("successful", !messagehub.hasErrors())));
return results;
}
+ else if (event instanceof CodeLensEvent)
+ {
+ CodeLensEvent le = (CodeLensEvent)event;
+ return new RPCMessageList(le.request, getCodeLenses(le.file));
+ }
else
{
Diag.error("Unhandled %s event %s", getName(), event);
@@ -225,4 +241,37 @@ else if (file.isDirectory())
return response;
}
+
+ public void clearLenses()
+ {
+ codeLenses.clear();
+ }
+
+ public void addCodeLens(ProofObligation po)
+ {
+ List array = codeLenses.get(po.location.file);
+
+ if (array == null)
+ {
+ array = new Vector();
+ codeLenses.put(po.location.file, array);
+ }
+
+ array.add(new POLaunchDebugLens(po));
+ }
+
+ private JSONArray getCodeLenses(File file)
+ {
+ JSONArray results = new JSONArray();
+
+ if (codeLenses.containsKey(file))
+ {
+ for (POLaunchDebugLens lens: codeLenses.get(file))
+ {
+ results.add(lens.getLaunchLens());
+ }
+ }
+
+ return results;
+ }
}
diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java
index b05aeed0c..a7885e2cf 100644
--- a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java
+++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java
@@ -80,6 +80,8 @@ protected void body()
LSPServer server = LSPServer.getInstance();
MessageHub.getInstance().clearPluginMessages(pog);
+ pog.clearLenses();
+
List messages = new Vector();
JSONArray list = new JSONArray();
long percentDone = -1;
@@ -141,6 +143,7 @@ protected void body()
{
MessageHub.getInstance().addPluginMessages(pog, messages);
responses.addAll(MessageHub.getInstance().getDiagnosticResponses());
+ responses.add(RPCRequest.create("workspace/codeLens/refresh", null));
}
for (JSONObject message: responses)
@@ -189,6 +192,7 @@ private JSONObject getQCResponse(ProofObligation po, List messages)
if (launch != null)
{
cexample.put("launch", launch);
+ pog.addCodeLens(po);
}
json.put("counterexample", cexample);