Deal with type definition contexts for counterexample/witnesses

nickbattle · Nov 13, 2023 · d6f7f21 · d6f7f21
1 parent c4c7257
commit d6f7f21
Showing 1 changed file with 50 additions and 35 deletions.
diff --git a/lsp/src/main/java/workspace/plugins/POPluginSL.java b/lsp/src/main/java/workspace/plugins/POPluginSL.java
@@ -31,6 +31,7 @@
 import com.fujitsu.vdmj.po.definitions.PODefinition;
 import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
 import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POTypeDefinition;
 import com.fujitsu.vdmj.po.modules.POModuleList;
 import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
@@ -99,49 +100,17 @@ protected JSONObject getLaunch(ProofObligation po, Context ctxt)
 		if (def instanceof POExplicitFunctionDefinition)
 		{
 			POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)def;
-			StringBuilder callString = new StringBuilder();
-			PORemoveIgnoresVisitor.init();
-
-			for (POPatternList pl: efd.paramPatternList)
-			{
-				callString.append("(");
-				String sep = "";
-
-				for (POPattern p: pl)
-				{
-					String match = paramMatch(p.removeIgnorePatterns(), ctxt);
-
-					if (match == null)
-					{
-						return null;	// Can't match some params
-					}
-
-					callString.append(sep);
-					callString.append(match);
-					sep = ", ";
-				}
-
-				callString.append(")");
-			}
-
-			result = new JSONObject(
-				"name",		"PO #" + po.number + " counterexample",
-				"type",		"vdm",
-				"request",	"launch",
-				"noDebug",	false,
-				"defaultName",	def.name.getModule(),
-				"command",	"print " + def.name.getName() + callString
-			);
+			result = launchExplicitFunction(po, efd, ctxt);
 		}
 		else if (def instanceof POImplicitFunctionDefinition)
 		{
-			POImplicitFunctionDefinition efd = (POImplicitFunctionDefinition)def;
+			POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)def;
 			StringBuilder callString = new StringBuilder();
 			callString.append("(");
 			String sep = "";
 			PORemoveIgnoresVisitor.init();
 
-			for (POPatternListTypePair pl: efd.parameterPatterns)
+			for (POPatternListTypePair pl: ifd.parameterPatterns)
 			{
 				for (POPattern p: pl.patterns)
 				{
@@ -169,9 +138,55 @@ else if (def instanceof POImplicitFunctionDefinition)
 				"command",	"print " + def.name.getName() + callString
 			);
 		}
+		else if (def instanceof POTypeDefinition)
+		{
+			POTypeDefinition td = (POTypeDefinition)def;
+
+			if (td.invdef != null)
+			{
+				result = launchExplicitFunction(po, td.invdef, ctxt);
+			}
+		}
 
 		return result;
 	}
+
+	private JSONObject launchExplicitFunction(ProofObligation po, POExplicitFunctionDefinition efd, Context ctxt)
+	{
+		StringBuilder callString = new StringBuilder();
+		PORemoveIgnoresVisitor.init();
+
+		for (POPatternList pl: efd.paramPatternList)
+		{
+			callString.append("(");
+			String sep = "";
+
+			for (POPattern p: pl)
+			{
+				String match = paramMatch(p.removeIgnorePatterns(), ctxt);
+
+				if (match == null)
+				{
+					return null;	// Can't match some params
+				}
+
+				callString.append(sep);
+				callString.append(match);
+				sep = ", ";
+			}
+
+			callString.append(")");
+		}
+
+		return new JSONObject(
+			"name",		"PO #" + po.number + " counterexample",
+			"type",		"vdm",
+			"request",	"launch",
+			"noDebug",	false,
+			"defaultName",	efd.name.getModule(),
+			"command",	"print " + efd.name.getName() + callString
+		);
+	}
 
 	private String paramMatch(POPattern p, Context ctxt)
 	{