Correct POLaunchDebugLens to add "value" presets

nickbattle · Nov 4, 2024 · 1e32396 · 1e32396
1 parent 35bb54d
commit 1e32396
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 106 deletions.
diff --git a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java
@@ -24,6 +24,11 @@
 
 package workspace.lenses;
 
+import com.fujitsu.vdmj.pog.POLaunchFactory;
+import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyArg;
+import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyCall;
+import com.fujitsu.vdmj.pog.ProofObligation;
+
 import json.JSONArray;
 import json.JSONObject;
 
@@ -63,4 +68,39 @@ protected JSONArray launchArgs(String launchName, String defaultName,
 
     	return new JSONArray(launchArgs);	// Array with one object
 	}
+
+	protected JSONArray launchArgs(ProofObligation po, String defaultName, boolean debug)
+	{
+		JSONObject launchArgs = new JSONObject();
+		POLaunchFactory factory = new POLaunchFactory(po);
+
+		ApplyCall apply = factory.getCexApply();
+
+		launchArgs.put("name", (debug ? "Debug " : "Launch ") + apply.applyName);
+		launchArgs.put("defaultName", defaultName);
+		launchArgs.put("type", "vdm");
+		launchArgs.put("request", "launch");
+		launchArgs.put("noDebug", !debug);		// Note: inverted :)
+		launchArgs.put("remoteControl", null);
+
+		launchArgs.put("applyName", apply.applyName);
+
+		if (!apply.applyTypes.isEmpty())
+		{
+			JSONArray applyTypes = new JSONArray(apply.applyTypes);
+			launchArgs.put("applyTypes", applyTypes);
+		}
+
+		JSONArray applyArgs = new JSONArray();
+
+		for (ApplyArg arg: apply.applyArgs)
+		{
+			applyArgs.add(new JSONObject("name", arg.name, "type", arg.type, "value", arg.value));
+		}
+
+		launchArgs.put("applyArgs", applyArgs);
+
+    	return new JSONArray(launchArgs);
+	}
+
 }
diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
@@ -24,22 +24,9 @@
 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.
@@ -60,99 +47,11 @@ public JSONArray getLaunchLens()
 
 		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, "PO #" + po.number, CODE_LENS_COMMAND,
-						launchArgs(launchName, defaultName, true, constructors, applyName, applyTypes, applyArgs)));
-			}
+			results.add(
+				makeLens(po.location, "PO #" + po.number, CODE_LENS_COMMAND,
+					launchArgs(po, def.location.module, true)));
 		}
 
 		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/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java
@@ -51,14 +51,14 @@
  */
 public class POLaunchFactory
 {
-	private static class ApplyCall
+	public static class ApplyCall
 	{
 		public String applyName = null;
 		public List<String> applyTypes = new Vector<String>();
 		public List<ApplyArg> applyArgs = new Vector<ApplyArg>();
 	}
 
-	private static class ApplyArg
+	public static class ApplyArg
 	{
 		public String name;
 		public String type;