Merge branch 'master' into highprecision

# Conflicts:
#	examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java
#	examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java

examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java

@@ -48,6 +48,7 @@
 public class QuickCheckCommand extends AnalysisCommand
 {
 	private final static String CMD = "quickcheck [-?|-help][-q][-t <secs>][-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
+	private final static String SHORT = "quickcheck [-help][<options>][<POs>]";
 	private final static String USAGE = "Usage: " + CMD;
 
 	public QuickCheckCommand(String line)
@@ -224,6 +225,6 @@ public String run(String line)
 
 	public static void help()
 	{
-		println("quickcheck [-?|-help][-p <names>]* [<plugin options>] [<PO numbers>] - lightweight PO verification");
+		println(SHORT + " - lightweight PO verification");
 	}
 }

examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java

@@ -44,6 +44,7 @@
 public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable
 {
 	public final static String CMD = "quickcheck [-?|-help][-q][-t <secs>][-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
+	public final static String SHORT = "quickcheck [-help][<options>][<POs>]";
 	private final static String USAGE = "Usage: " + CMD;
 
 	private List<Integer> poList = new Vector<Integer>();

examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java

@@ -55,11 +55,11 @@ public void init()
 	@Override
 	public void setServerCapabilities(JSONObject capabilities)
 	{
-		JSONObject experimental = capabilities.get("experimental");
+		JSONObject provider = capabilities.getPath("experimental.proofObligationProvider");
 
-		if (experimental != null)
+		if (provider != null)
 		{
-			experimental.put("quickCheckProvider", true);
+			provider.put("quickCheckProvider", true);
 		}
 	}
 
@@ -79,6 +79,6 @@ public AnalysisCommand getCommand(String line)
 	@Override
 	public HelpList getCommandHelp()
 	{
-		return new HelpList("quickcheck [-p <names>]* [<plugin options>] [<PO numbers>] - lightweight PO verification");
+		return new HelpList(QuickCheckLSPCommand.SHORT + " - lightweight PO verification");
 	}
 }

examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java

@@ -278,7 +278,7 @@ public Boolean caseExpression(TCExpression node, Stack<TCExpression> truths)
 	{
 		if (truths.contains(node))
 		{
-			evaluated.add(node.toString());		// This truth was used
+			evaluated.add(Utils.deBracketed(node));		// This truth was used
 			return true;
 		}
 		else

lsp/src/main/java/workspace/plugins/POPlugin.java

@@ -34,6 +34,7 @@
 import com.fujitsu.vdmj.messages.VDMWarning;
 import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.runtime.Context;
 
 import json.JSONArray;
 import json.JSONObject;
@@ -96,7 +97,7 @@ public void setServerCapabilities(JSONObject capabilities)
 
 		if (experimental != null)
 		{
-			experimental.put("proofObligationProvider", true);
+			experimental.put("proofObligationProvider", new JSONObject());
 		}
 	}
 
@@ -139,6 +140,8 @@ protected void preCheck(CheckPrepareEvent event)
 
 	abstract public ProofObligationList getProofObligations();
 
+	abstract protected JSONObject getLaunch(ProofObligation po, Context ctxt);
+
 	protected JSONArray splitPO(String value)
 	{
 		String[] parts = value.trim().split("\\n\\s+");
@@ -199,19 +202,42 @@ else if (file.isDirectory())
 
 			if (!po.counterexample.isEmpty())
 			{
-				json.put("counterexample", Utils.contextToJSON(po.counterexample));
+				JSONObject cexample = new JSONObject();
+				cexample.put("variables", Utils.contextToJSON(po.counterexample));
+				JSONObject launch = getLaunch(po, po.counterexample);
+
+				if (launch != null)
+				{
+					cexample.put("launch", launch);
+				}
+
+				json.put("counterexample", cexample);
 
 				StringBuilder sb = new StringBuilder();
 				sb.append("PO #");
 				sb.append(po.number);
 				sb.append(" counterexample: ");
 				sb.append(po.counterexample.toStringLine());
 				messages.add(new VDMWarning(9000, sb.toString(), po.location));
+
+				if (po.message != null)		// Add any message as a warning too
+				{
+					messages.add(new VDMWarning(9000, po.message, po.location));
+				}
 			}
 
 			if (!po.witness.isEmpty())
 			{
-				json.put("witness", Utils.contextToJSON(po.witness));
+				JSONObject witness = new JSONObject();
+				witness.put("variables", Utils.contextToJSON(po.witness));
+				JSONObject launch = getLaunch(po, po.witness);
+
+				if (launch != null)
+				{
+					witness.put("launch", launch);
+				}
+
+				json.put("witness", witness);
 			}
 
 			if (po.provedBy != null)

lsp/src/main/java/workspace/plugins/POPluginPR.java

@@ -29,8 +29,11 @@
 import com.fujitsu.vdmj.po.PONode;
 import com.fujitsu.vdmj.po.annotations.POAnnotation;
 import com.fujitsu.vdmj.po.definitions.POClassList;
+import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.runtime.Context;
 
+import json.JSONObject;
 import workspace.events.CheckPrepareEvent;
 
 public class POPluginPR extends POPlugin
@@ -78,4 +81,11 @@ public ProofObligationList getProofObligations()
 
 		return obligationList;
 	}
+
+	@Override
+	protected JSONObject getLaunch(ProofObligation po, Context ctxt)
+	{
+		// TODO More complex than SL as we have to think about constructors...
+		return null;
+	}
 }

lsp/src/main/java/workspace/plugins/POPluginSL.java

@@ -28,9 +28,21 @@
 import com.fujitsu.vdmj.mapper.Mappable;
 import com.fujitsu.vdmj.po.PONode;
 import com.fujitsu.vdmj.po.annotations.POAnnotation;
+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;
+import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor;
+import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor;
+import com.fujitsu.vdmj.po.types.POPatternListTypePair;
+import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.runtime.Context;
 
+import json.JSONObject;
 import workspace.events.CheckPrepareEvent;
 
 public class POPluginSL extends POPlugin
@@ -78,4 +90,108 @@ public ProofObligationList getProofObligations()
 
 		return obligationList;
 	}
+
+	@Override
+	protected JSONObject getLaunch(ProofObligation po, Context ctxt)
+	{
+		PODefinition def = po.definition;
+		JSONObject result = null;
+
+		if (def instanceof POExplicitFunctionDefinition)
+		{
+			POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)def;
+			result = launchExplicitFunction(po, efd, ctxt);
+		}
+		else if (def instanceof POImplicitFunctionDefinition)
+		{
+			POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)def;
+			StringBuilder callString = new StringBuilder();
+			callString.append("(");
+			String sep = "";
+			PORemoveIgnoresVisitor.init();
+
+			for (POPatternListTypePair pl: ifd.parameterPatterns)
+			{
+				for (POPattern p: pl.patterns)
+				{
+					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
+			);
+		}
+		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)
+	{
+		POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor();
+		String result = p.apply(visitor, ctxt);
+		return visitor.hasFailed() ? null : result;
+	}
 }

vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java

@@ -160,7 +160,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			{
 				for (PODefinitionList loop: recursive)
 				{
-					obligations.add(new RecursiveObligation(loop, this, ctxt));
+					obligations.add(new RecursiveObligation(location, loop, this, ctxt));
 				}
 			}
 		}