Enable maximal type parsing for qcrun expressions

nickbattle · Nov 27, 2023 · 4fa1315 · 4fa1315
1 parent e1484b9
commit 4fa1315
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 5 deletions.
diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java
@@ -26,6 +26,7 @@
 
 import static com.fujitsu.vdmj.plugins.PluginConsole.println;
 
+import com.fujitsu.vdmj.config.Properties;
 import com.fujitsu.vdmj.plugins.AnalysisCommand;
 import com.fujitsu.vdmj.plugins.analyses.POPlugin;
 import com.fujitsu.vdmj.plugins.commands.PrintCommand;
@@ -102,8 +103,20 @@ else if (!obligation.witness.isEmpty())
 					{
 						String pline = "print " + launch;
 						println("=> " + pline);
-						PrintCommand cmd = new PrintCommand(pline);
-						return cmd.run(pline);
+
+						// Temporarily allow maximal parsing, for invariant POs
+						boolean saved = Properties.parser_maximal_types;
+
+						try
+						{
+							Properties.parser_maximal_types = true;
+							PrintCommand cmd = new PrintCommand(pline);
+							return cmd.run(pline);
+						}
+						finally
+						{
+							Properties.parser_maximal_types = saved;
+						}
 					}
 					else
 					{

diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java
@@ -104,7 +104,8 @@ else if (!obligation.witness.isEmpty())
 				if (launch != null)
 				{
 					println("=> print " + launch);
-					ExpressionExecutor executor = new ExpressionExecutor("print", request, launch);
+					// This allows maximal types to parse, for invariant POs
+					ExpressionExecutor executor = new ExpressionExecutor("print", request, launch, true);
 					executor.start();
 					return null;
 				}

diff --git a/lsp/src/main/java/dap/ExpressionExecutor.java b/lsp/src/main/java/dap/ExpressionExecutor.java
@@ -26,17 +26,26 @@
 
 import java.io.IOException;
 
+import com.fujitsu.vdmj.config.Properties;
+
 import json.JSONObject;
 
 public class ExpressionExecutor extends AsyncExecutor
 {
 	private final String expression;
+	private final boolean maximal;
 	private String answer;
 
-	public ExpressionExecutor(String id, DAPRequest request, String expression)
+	public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal)
 	{
 		super(id, request);
 		this.expression = expression;
+		this.maximal = maximal;
+	}
+
+	public ExpressionExecutor(String id, DAPRequest request, String expression)
+	{
+		this(id, request, expression, false);
 	}
 
 	@Override
@@ -48,7 +57,17 @@ protected void head()
 	@Override
 	protected void exec() throws Exception
 	{
-		answer = manager.getInterpreter().execute(expression).toString();
+		boolean saved = Properties.parser_maximal_types;	// Used by qcrun
+
+		try
+		{
+			Properties.parser_maximal_types = maximal;
+			answer = manager.getInterpreter().execute(expression).toString();
+		}
+		finally
+		{
+			Properties.parser_maximal_types = saved;
+		}
 	}
 
 	@Override