Merge branch 'master' into highprecision

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

@@ -34,8 +34,6 @@
 import com.fujitsu.vdmj.pog.RecursiveObligation;
 import com.fujitsu.vdmj.pog.SeqApplyObligation;
 import com.fujitsu.vdmj.pog.SubTypeObligation;
-import com.fujitsu.vdmj.tc.definitions.TCDefinition;
-import com.fujitsu.vdmj.tc.definitions.TCExplicitFunctionDefinition;
 import com.fujitsu.vdmj.tc.types.TCMapType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCTypeList;
@@ -105,36 +103,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		if (!type.isUnknown(location) &&
 			(type.isFunction(location) || type.isOperation(location)))
 		{
-			TCTypeList paramTypes = type.isFunction(location) ?
-				type.getFunction().parameters : type.getOperation().parameters;
-
 			String prename = root.getPreName();
 
-			if (type.isFunction(location) && prename != null && !prename.equals(""))
+			if (type.isFunction(location) && prename != null && !prename.isEmpty())
 			{
-				boolean needed = true;
-
-				if (type.definitions != null)
-				{
-					TCDefinition def = type.definitions.firstElement();
-
-					// If the apply is of an explicit curried function, we don't want to
-					// generate a precondition obligation, because we haven't collected
-					// all the curried parameters yet.
-
-					if (def instanceof TCExplicitFunctionDefinition)
-					{
-						TCExplicitFunctionDefinition edef = (TCExplicitFunctionDefinition)def;
-						needed =!edef.isCurried;
-					}
-				}
-
-				if (needed)
-				{
-					obligations.add(new FunctionApplyObligation(root, args, prename, ctxt));
-				}
+				obligations.add(new FunctionApplyObligation(root, args, prename, ctxt));
 			}
 
+			TCTypeList paramTypes = type.isFunction(location) ?
+					type.getFunction().parameters : type.getOperation().parameters;
+
 			int i=0;
 
 			for (TCType at: argtypes)
@@ -227,6 +205,21 @@ else if (root instanceof POFuncInstantiationExpression)
 		sb.append(")");
 		return sb.toString();
 	}
+
+	/**
+	 * This is used in apply chains or curried calls, where the precondition is needed
+	 * at the end of the chain.
+	 */
+	@Override
+	public String getPreName()
+	{
+		if (root.getPreName() == null)
+		{
+			return null;
+		}
+
+		return FunctionApplyObligation.UNKNOWN;		// Use pre_(root, args) form
+	}
 
 	@Override
 	public <R, S> R apply(POExpressionVisitor<R, S> visitor, S arg)

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

@@ -30,6 +30,7 @@
 import com.fujitsu.vdmj.pog.CasesExhaustiveObligation;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.tc.lex.TCNameList;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.typechecker.Environment;
 import com.fujitsu.vdmj.util.Utils;
@@ -67,22 +68,26 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		int count = 0;
 		boolean hasIgnore = false;
+		TCNameList hidden = new TCNameList();
+		ProofObligationList _obligations = new ProofObligationList();
 
 		for (POCaseAlternative alt: cases)
 		{
 			if (alt.pattern instanceof POIgnorePattern)
 			{
 				hasIgnore = true;
 			}
-
+
+			hidden.addAll(alt.pattern.getHiddenVariables());	// cumulative
+
 			// PONotCaseContext pushed by the POCaseAlternative...
-			obligations.addAll(alt.getProofObligations(ctxt, expType, env));
+			_obligations.addAll(alt.getProofObligations(ctxt, expType, env));
 			count++;
 		}
-
+		
 		if (others != null)
 		{
-			obligations.addAll(others.getProofObligations(ctxt, env));
+			_obligations.addAll(others.getProofObligations(ctxt, env));
 		}
 
 		for (int i=0; i<count; i++)
@@ -92,9 +97,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		if (others == null && !hasIgnore)
 		{
-			obligations.add(new CasesExhaustiveObligation(this, ctxt));
+			_obligations.add(new CasesExhaustiveObligation(this, ctxt));
+		}
+
+
+		if (!hidden.isEmpty())
+		{
+			_obligations.markUnchecked("Obligation patterns contain hidden variables: " + hidden);
 		}
 
+		obligations.addAll(_obligations);
 		return obligations;
 	}
 

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

@@ -55,8 +55,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 			if (pref1 == null || !pref1.equals(""))
 			{
-				obligations.add(new FuncComposeObligation(
-					this, pref1, pref2, ctxt));
+				obligations.add(new FuncComposeObligation(this, pref1, pref2, ctxt));
 			}
 		}
 

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

@@ -27,6 +27,7 @@
 import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
 import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
 import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor;
+import com.fujitsu.vdmj.pog.FunctionApplyObligation;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.types.TCFunctionType;
@@ -89,7 +90,7 @@ public String getPreName()
 	{
 		String prename = function.getPreName();
 
-		if (prename == null || prename.isEmpty())
+		if (prename == null || prename.isEmpty() || prename == FunctionApplyObligation.UNKNOWN)
 		{
 			return prename;
 		}

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

@@ -55,8 +55,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 			if (prename == null || !prename.equals(""))
 			{
-				obligations.add(
-					new FuncIterationObligation(this, prename, ctxt));
+				obligations.add(new FuncIterationObligation(this, prename, ctxt));
 			}
 		}
 

vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java

@@ -35,6 +35,7 @@
 import com.fujitsu.vdmj.po.patterns.visitors.POGetAllVarNamesVisitor;
 import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor;
 import com.fujitsu.vdmj.po.patterns.visitors.POGetPossibleTypeVisitor;
+import com.fujitsu.vdmj.po.patterns.visitors.POHiddenVariablesVisitor;
 import com.fujitsu.vdmj.po.patterns.visitors.POPatternVisitor;
 import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor;
 import com.fujitsu.vdmj.tc.lex.TCNameList;
@@ -169,6 +170,15 @@ public void setMaximal(boolean maximal)
 	{
 		return;		// Only used in PORecordPattern
 	}
+
+	/**
+	 * Search the pattern for identifiers that hide other definitions. This is
+	 * used during PO generation to avoid TC errors.
+	 */
+	public TCNameList getHiddenVariables()
+	{
+		return apply(new POHiddenVariablesVisitor(), null);
+	}
 
 	/**
 	 * Implemented by all patterns to allow visitor processing.

vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POHiddenVariablesVisitor.java

@@ -0,0 +1,60 @@
+/*******************************************************************************
+ *
+ *	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 com.fujitsu.vdmj.po.patterns.visitors;
+
+import com.fujitsu.vdmj.po.patterns.POIdentifierPattern;
+import com.fujitsu.vdmj.po.patterns.POPattern;
+import com.fujitsu.vdmj.tc.lex.TCNameList;
+import com.fujitsu.vdmj.tc.lex.TCNameToken;
+
+/**
+ * Search a pattern for hidden variables, and return a list.
+ */
+public class POHiddenVariablesVisitor extends POLeafPatternVisitor<TCNameToken, TCNameList, Object>
+{
+	@Override
+	protected TCNameList newCollection()
+	{
+		return new TCNameList();
+	}
+
+	@Override
+	public TCNameList casePattern(POPattern node, Object arg)
+	{
+		return newCollection();
+	}
+
+	@Override
+	public TCNameList caseIdentifierPattern(POIdentifierPattern node, Object arg)
+	{
+		TCNameList result = newCollection();
+
+		if (node.name.getHides() != null)
+		{
+			result.add(node.name);
+		}
+
+		return result;
+	}
+}

vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncComposeObligation.java

@@ -40,7 +40,7 @@ public FuncComposeObligation(
 
 		if (pref2 == null || !pref2.equals(""))
 		{
-    		if (pref2 != null)
+    		if (pref2 != null && pref2 != FunctionApplyObligation.UNKNOWN)
     		{
         		sb.append(pref2);
         		sb.append("(arg) => ");
@@ -53,7 +53,7 @@ public FuncComposeObligation(
     		}
 		}
 
-		if (pref1 != null)
+		if (pref1 != FunctionApplyObligation.UNKNOWN && pref1 != null)
 		{
     		sb.append(pref1);
     		sb.append("(");

vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncIterationObligation.java

@@ -38,7 +38,7 @@ public FuncIterationObligation(
 		sb.append(" > 1 => forall arg:");
 		sb.append(exp.rtype.getNumeric());
 
-		if (prename != null)
+		if (prename != FunctionApplyObligation.UNKNOWN && prename != null)
 		{
     		sb.append(" & ");
     		sb.append(prename);

vdmj/src/main/java/com/fujitsu/vdmj/pog/FunctionApplyObligation.java

@@ -30,12 +30,14 @@
 
 public class FunctionApplyObligation extends ProofObligation
 {
+	public static final String UNKNOWN = "???";		// Use pre_(root, args) form
+
 	public FunctionApplyObligation(POExpression root, POExpressionList args, String prename, POContextStack ctxt)
 	{
 		super(root.location, POType.FUNC_APPLY, ctxt);
 		StringBuilder sb = new StringBuilder();
 
-		if (prename == null)
+		if (prename == UNKNOWN)
 		{
 			sb.append("pre_(");
 			sb.append(root);

vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java

@@ -138,8 +138,10 @@ public PODefinition getDefinition()
 
 	public boolean isExistential()
 	{
-		for (POContext ctxt: this)
+		for (int i = size() - 1; i >= 0; i--)	// NB. reverse order, for tail "exists"
 		{
+			POContext ctxt = get(i);
+
 			if (ctxt instanceof PONameContext ||
 				ctxt instanceof PONoCheckContext ||
 				ctxt instanceof POScopeContext)

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java

@@ -135,6 +135,16 @@ public void setMessage(String message)
 		this.message = message;
 	}
 
+	/**
+	 * This is used to mark obligations as unchecked, with a reason.
+	 */
+	public void markUnchecked(String message)
+	{
+		this.isCheckable = false;
+		this.setStatus(POStatus.UNCHECKED);
+		this.setMessage(message);
+	}
+
 	public boolean isExistential()
 	{
 		return existential;

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java

@@ -227,9 +227,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env
 					{
 						// Probably an implicit missing measure
 						iter.remove();
-						obligation.status = POStatus.UNCHECKED;
-						obligation.isCheckable = false;
-						obligation.message = "PO #" + obligation.number + ": Missing measure function";
+						obligation.markUnchecked("Obligation for missing measure function");
 					}
 					break;
 
@@ -250,4 +248,15 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env
 
 		obligation.setCheckedExpression(tcexp);
 	}
+
+	/**
+	 * This is used by POG to mark obligations as unchecked, with a reason.
+	 */
+	public void markUnchecked(String message)
+	{
+		for (ProofObligation obligation: this)
+		{
+			obligation.markUnchecked(message);
+		}
+	}
 }