Merge branch 'master' into highprecision

# Conflicts:
#	examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
#	examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java
#	examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java
#	examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java
#	examples/quickcheck/src/main/java/quickcheck/visitors/SearchQCVisitor.java
#	vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java
#	vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java

annotations/src/main/java/annotations/ast/ASTConjectureAnnotation.java

@@ -43,9 +43,9 @@ public ASTConjectureAnnotation(LexIdentifierToken name)
 	}
 
 	@Override
-	public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserException
+	public void parse(LexTokenReader ltr) throws LexException, ParserException
 	{
-		ASTExpressionList args = new ASTExpressionList();
+		this.args = new ASTExpressionList();
 
 		try
 		{
@@ -75,8 +75,5 @@ public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserEx
 			// cause this annotation to be ignored.
 			args.clear();
 		}
-
-		return args;
 	}
-
 }

annotations2/src/main/java/annotations/ast/ASTGhostAnnotation.java

@@ -52,10 +52,11 @@ public ASTGhostAnnotation(LexIdentifierToken name)
 	 * Override the default parse, and look for @Ghost <name> = <exp>;
 	 */
 	@Override
-	public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserException
+	public void parse(LexTokenReader ltr) throws LexException, ParserException
 	{
+		this.args = new ASTExpressionList();
+
 		ltr.nextToken();
-		ASTExpressionList args = new ASTExpressionList();
 		ExpressionReader er = new ExpressionReader(ltr);
 		ASTExpression exp = er.readExpression();
 
@@ -82,7 +83,5 @@ public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserEx
 		{
 			parseException("missing ;", ltr.getLast().location);
 		}
-
-		return args;
 	}
 }

examples/quickcheck/TODO

@@ -3,5 +3,4 @@ Things still to do with QuickCheck
 1. Make getValues interruptible as well as checkObligations?
 2. Move QC to be part of POPlugin(s)
 3. Separate IO from calculations (and allow LSP control)
-4. Make SearchQCPlugin use the "sense" of forall/exists to choose values.
-6. Add -file and -func PO selection options?
+4. Add -file and -func PO selection options?

examples/quickcheck/src/main/java/annotations/IterableContext.java

@@ -0,0 +1,90 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 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 annotations;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Vector;
+
+import com.fujitsu.vdmj.lex.LexLocation;
+import com.fujitsu.vdmj.runtime.Context;
+import com.fujitsu.vdmj.tc.lex.TCNameToken;
+import com.fujitsu.vdmj.values.Value;
+
+/**
+ * A Context that is backed by a list of maps, which can be iterated through.
+ * This is used in QuickCheck to load a context with one of a selection of
+ * ParameterType settings. 
+ */
+public class IterableContext extends Context
+{
+	private static final long serialVersionUID = 1L;
+	private final List<Map<TCNameToken, Value>> maps;
+	private int nextMap = 0;
+
+	public IterableContext(LexLocation location, String title, Context outer)
+	{
+		super(location, title, outer);
+		maps = new Vector<Map<TCNameToken, Value>>();
+	}
+
+	public Map<TCNameToken, Value> newMap(int index)
+	{
+		if (index < maps.size())
+		{
+			return maps.get(index);
+		}
+		else
+		{
+			Map<TCNameToken, Value> values = new HashMap<TCNameToken, Value>(); 
+			maps.add(values);
+			return values;
+		}
+	}
+
+	public boolean hasNext()
+	{
+		return nextMap < maps.size();
+	}
+
+	public void next()
+	{
+		this.clear();
+		this.putAll(maps.get(nextMap));
+		nextMap++;
+	}
+
+	public void setDefaults(TCNameToken name, Value value)
+	{
+		for (Map<TCNameToken, Value> map: maps)
+		{
+			if (!map.containsKey(name))
+			{
+				map.put(name, value);
+			}
+		}
+	}
+}

examples/quickcheck/src/main/java/annotations/ast/ASTQuickCheckAnnotation.java

@@ -0,0 +1,95 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 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 annotations.ast;
+
+import com.fujitsu.vdmj.ast.annotations.ASTAnnotation;
+import com.fujitsu.vdmj.ast.lex.LexIdentifierToken;
+import com.fujitsu.vdmj.ast.types.ASTParameterType;
+import com.fujitsu.vdmj.ast.types.ASTType;
+import com.fujitsu.vdmj.ast.types.ASTTypeList;
+import com.fujitsu.vdmj.lex.LexException;
+import com.fujitsu.vdmj.lex.LexTokenReader;
+import com.fujitsu.vdmj.lex.Token;
+import com.fujitsu.vdmj.syntax.ParserException;
+import com.fujitsu.vdmj.syntax.TypeReader;
+import com.fujitsu.vdmj.util.Utils;
+
+public class ASTQuickCheckAnnotation extends ASTAnnotation
+{
+	private static final long serialVersionUID = 1L;
+
+	public ASTParameterType qcParam = null;
+	public ASTTypeList qcTypes = null;
+
+	public ASTQuickCheckAnnotation(LexIdentifierToken name)
+	{
+		super(name);
+	}
+
+	@Override
+	public String toString()
+	{
+		return "@" + name + " " + qcParam + " = " + Utils.listToString("", qcTypes, ", ", ";");
+	}
+
+	/**
+	 * Override the default parse, and look for @QuickCheck @T = <type> [,<type>*];
+	 */
+	@Override
+	public void parse(LexTokenReader ltr) throws LexException, ParserException
+	{
+		ltr.nextToken();
+		TypeReader er = new TypeReader(ltr);
+		ASTType start = er.readType();
+
+		if (start instanceof ASTParameterType)
+		{
+			qcParam = (ASTParameterType)start;
+			qcTypes = new ASTTypeList();
+
+			if (!ltr.getLast().is(Token.EQUALS))
+			{
+				parseException("expecting @T = <type>;", qcParam.location);
+			}
+
+			do
+			{
+				ltr.nextToken();
+				ASTType type = er.readType();
+				qcTypes.add(type);
+			}
+			while (ltr.getLast().is(Token.COMMA));
+		}
+		else
+		{
+			parseException("expecting @T = <type> [,<type>*];", start.location);
+		}
+
+		if (ltr.getLast().isNot(Token.SEMICOLON))
+		{
+			parseException("missing ;", ltr.getLast().location);
+		}
+	}
+}

examples/quickcheck/src/main/java/annotations/po/POQuickCheckAnnotation.java

@@ -0,0 +1,52 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2018 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 annotations.po;
+
+import com.fujitsu.vdmj.po.annotations.POAnnotation;
+import com.fujitsu.vdmj.tc.lex.TCIdentifierToken;
+import com.fujitsu.vdmj.tc.types.TCParameterType;
+import com.fujitsu.vdmj.tc.types.TCTypeList;
+import com.fujitsu.vdmj.util.Utils;
+
+public class POQuickCheckAnnotation extends POAnnotation
+{
+	private static final long serialVersionUID = 1L;
+
+	public final TCParameterType qcParam;
+	public final TCTypeList qcTypes;
+
+	public POQuickCheckAnnotation(TCIdentifierToken name, TCParameterType qcParam, TCTypeList qcTypes)
+	{
+		super(name, null);
+		this.qcParam = qcParam;
+		this.qcTypes = qcTypes;
+	}
+
+	@Override
+	public String toString()
+	{
+		return "@" + name + " " + qcParam + " = " + Utils.listToString("", qcTypes, ", ", ";");
+	}
+}