Merge branch 'master' into highprecision

lsp/src/main/java/dap/ExpressionExecutor.java

@@ -27,25 +27,30 @@
 import java.io.IOException;
 
 import com.fujitsu.vdmj.config.Properties;
+import com.fujitsu.vdmj.runtime.Interpreter;
+import com.fujitsu.vdmj.typechecker.Environment;
 
 import json.JSONObject;
 
 public class ExpressionExecutor extends AsyncExecutor
 {
 	private final String expression;
 	private final boolean maximal;
+
+	private Environment env = null;
 	private String answer;
 
-	public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal)
+	public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal, Environment env)
 	{
 		super(id, request);
 		this.expression = expression;
 		this.maximal = maximal;
+		this.env = env;
 	}
 
 	public ExpressionExecutor(String id, DAPRequest request, String expression)
 	{
-		this(id, request, expression, false);
+		this(id, request, expression, false, null);
 	}
 
 	@Override
@@ -58,11 +63,14 @@ protected void head()
 	protected void exec() throws Exception
 	{
 		boolean saved = Properties.parser_maximal_types;	// Used by qcrun
+		Interpreter interpreter = manager.getInterpreter();
+
+		if (env == null) env = interpreter.getGlobalEnvironment();
 
 		try
 		{
 			Properties.parser_maximal_types = maximal;
-			answer = manager.getInterpreter().execute(expression).toString();
+			answer = interpreter.execute(expression, env).toString();
 		}
 		finally
 		{

lsp/src/main/java/json/JSONArray.java

@@ -41,16 +41,7 @@ public JSONArray(Object... args)
 	@Override
 	public boolean add(Object value)
 	{
-		if (value instanceof Integer)
-		{
-			value = ((Integer)value).longValue();
-		}
-		else if (value instanceof Short)
-		{
-			value = ((Short)value).longValue();
-		}
-
-		return super.add(value);
+		return super.add(JSONValue.validate(value));
 	}
 
 	@SuppressWarnings("unchecked")

lsp/src/main/java/json/JSONObject.java

@@ -51,16 +51,7 @@ public JSONObject(Object... args)
 	@Override
 	public Object put(String name, Object value)
 	{
-		if (value instanceof Integer)
-		{
-			value = ((Integer)value).longValue();
-		}
-		else if (value instanceof Short)
-		{
-			value = ((Short)value).longValue();
-		}
-
-		return super.put(name, value);
+		return super.put(name, JSONValue.validate(value));
 	}
 
 	@SuppressWarnings("unchecked")

lsp/src/main/java/json/JSONValue.java

@@ -0,0 +1,61 @@
+/*******************************************************************************
+ *
+ *	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 json;
+
+/**
+ * A class to create valid JSON values. These can be added to JSONObject or JSONArray.
+ */
+public class JSONValue
+{
+	public static Object validate(Object value)
+	{
+		if (value == null)
+		{
+			// fine
+		}
+		else if (value instanceof Double ||
+				 value instanceof Float)
+		{
+			value = ((Number)value).doubleValue();
+		}
+		else if (value instanceof Number)
+		{
+			value = ((Number)value).longValue();
+		}
+		else if (value instanceof String ||
+				 value instanceof Boolean ||
+				 value instanceof JSONArray ||
+				 value instanceof JSONObject)
+		{
+			// fine
+		}
+		else
+		{
+			throw new IllegalArgumentException("Unexpected JSON value: " + value.getClass().getSimpleName());
+		}
+
+		return value;
+	}
+}

lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java

@@ -92,12 +92,24 @@ public JSONArray getDefinitionLenses(ASTDefinition def, ASTClassDefinition cls)
 					}
 
 					ASTFunctionType ftype = (ASTFunctionType) exdef.type;
-					ASTTypeList ptypes = ftype.parameters;
-					int i = 0;
 
-					for (ASTPattern p: exdef.paramPatternList.get(0))	// Curried?
+					for (ASTPatternList pl: exdef.paramPatternList)
 					{
-						applyArgs.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++))));
+						JSONArray params = new JSONArray();
+						ASTTypeList ptypes = ftype.parameters;
+						int i = 0;
+
+						for (ASTPattern p: pl)
+						{
+							params.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++))));
+						}
+
+						applyArgs.add(params);
+
+						if (ftype.result instanceof ASTFunctionType)
+						{
+							ftype = (ASTFunctionType)ftype.result;
+						}
 					}
 				}
 			}
@@ -110,12 +122,14 @@ else if (def instanceof ASTImplicitFunctionDefinition)
 					applyName = imdef.name.getName();
 					launchName = applyName;
 					defaultName = imdef.name.module;
+					JSONArray params = new JSONArray();
+					applyArgs.add(params);
 
 					for (ASTPatternListTypePair param: imdef.parameterPatterns)
 					{
 						for (ASTPattern p: param.patterns)
 						{
-							applyArgs.add(new JSONObject("name", p.toString(), "type", fix(param.type)));
+							params.add(new JSONObject("name", p.toString(), "type", fix(param.type)));
 						}
 					}
 				}
@@ -136,10 +150,12 @@ else if (def instanceof ASTExplicitOperationDefinition)
 						ASTOperationType ftype = (ASTOperationType) exop.type;
 						ASTTypeList ptypes = ftype.parameters;
 						int i = 0;
+						JSONArray params = new JSONArray();
+						applyArgs.add(params);
 
 						for (ASTPattern p: exop.parameterPatterns)
 						{
-							applyArgs.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++))));
+							params.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++))));
 						}
 					}
 				}
@@ -156,12 +172,14 @@ else if (def instanceof ASTImplicitOperationDefinition)
 					if (!applyName.equals(defaultName))	// Not a constructor
 					{
 						launchName = applyName;
+						JSONArray params = new JSONArray();
+						applyArgs.add(params);
 
 						for (ASTPatternListTypePair param: imop.parameterPatterns)
 						{
 							for (ASTPattern p: param.patterns)
 							{
-								applyArgs.add(new JSONObject("name", p.toString(), "type", fix(param.type)));
+								params.add(new JSONObject("name", p.toString(), "type", fix(param.type)));
 							}
 						}
 					}

lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java

@@ -24,11 +24,6 @@
 
 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;
 
@@ -68,45 +63,4 @@ 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();
-
-			for (String atype: apply.applyTypes)
-			{
-				applyTypes.add(atype);
-			}
-
-			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);
-	}
-
 }

lsp/src/main/java/workspace/lenses/CodeLens.java

@@ -66,8 +66,7 @@ protected boolean isClientType(String type)
 	}
 
 	/**
-	 * These helper methods generate the lens response body. The JSONArray returned
-	 * by getDefinitionLenses (above) is an array of these structures, one per lens. 
+	 * These helper methods generate the lens response body.
 	 */
 	protected JSONObject makeLens(LexLocation location, String title, String command)
 	{

lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java

@@ -23,10 +23,16 @@
  ******************************************************************************/
 package workspace.lenses;
 
+import java.util.List;
+
 import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.pog.POLaunchFactory;
 import com.fujitsu.vdmj.pog.ProofObligation;
+import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyArg;
+import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyCall;
 
 import json.JSONArray;
+import json.JSONObject;
 
 /**
  * A class to generate launch lenses for PO counterexamples.
@@ -54,4 +60,51 @@ public JSONArray getLaunchLens()
 
 		return results;
 	}
+
+	private JSONArray launchArgs(ProofObligation po, String defaultName, boolean debug)
+	{
+		JSONObject launchArgs = new JSONObject();
+		POLaunchFactory factory = new POLaunchFactory(po);
+
+		ApplyCall apply = factory.getCexApply();
+
+		launchArgs.put("name", "PO #" + po.number);
+		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();
+
+			for (String atype: apply.applyTypes)
+			{
+				applyTypes.add(atype);
+			}
+
+			launchArgs.put("applyTypes", applyTypes);
+		}
+
+		JSONArray applyArgs = new JSONArray();
+
+		for (List<ApplyArg> arglist: apply.applyArgs)
+		{
+			JSONArray sublist = new JSONArray();
+
+			for (ApplyArg arg: arglist)
+			{
+				sublist.add(new JSONObject("name", arg.name, "type", arg.type, "value", arg.value));
+			}
+
+			applyArgs.add(sublist);
+		}
+
+		launchArgs.put("applyArgs", applyArgs);
+
+    	return new JSONArray(launchArgs);
+	}
 }