First draft of PO codelens to launch counterexamples

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 <http://www.gnu.org/licenses/>.
+ *	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;
+	}
+}

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<File, List<POLaunchDebugLens>> codeLenses;
+
 	protected POPlugin()
 	{
 		super();
+
+		codeLenses = new HashMap<File, List<POLaunchDebugLens>>();
 	}
 
 	@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<POLaunchDebugLens> array = codeLenses.get(po.location.file);
+
+		if (array == null)
+		{
+			array = new Vector<POLaunchDebugLens>();
+			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;
+	}
 }

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<VDMMessage> messages = new Vector<VDMMessage>();
 			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<VDMMessage> messages)
 			if (launch != null)
 			{
 				cexample.put("launch", launch);
+				pog.addCodeLens(po);
 			}
 
 			json.put("counterexample", cexample);