Merge branch 'master' into highprecision

nickbattle · Dec 1, 2023 · 894d834 · 894d834
2 parents bf27f29 + 52d2b87
commit 894d834
Show file tree

Hide file tree

Showing 6 changed files with 75 additions and 10 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java
@@ -87,7 +87,26 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 	@Override
 	public String getPreName()
 	{
-		return function.getPreName();
+		String prename = function.getPreName();
+
+		if (prename == null || prename.isEmpty())
+		{
+			return prename;
+		}
+
+		StringBuilder sb = new StringBuilder(prename);
+		sb.append("[");
+		String sep = "";
+
+		for (TCType p: actualTypes)
+		{
+			sb.append(sep);
+			sb.append(p.toExplicitString(location));
+			sep = ", ";
+		}
+
+		sb.append("]");
+		return sb.toString();
 	}
 
 	@Override

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POGetMatchingExpressionVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POGetMatchingExpressionVisitor.java
@@ -202,7 +202,9 @@ public POExpression caseRecordPattern(PORecordPattern node, Object arg)
 			list.add(p.apply(this, arg));
 		}
 
-		return new POMkTypeExpression(node.typename, list, null, null);
+		// If the type is not within the pattern's module, be explicit
+		boolean explicit = !node.location.module.equals(node.typename.getModule());
+		return new POMkTypeExpression(node.typename.getExplicit(explicit), list, null, null);
 	}
 
 	@Override

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java
@@ -61,11 +61,14 @@ private String getLHS(PODefinition def)
 
 			if (edef.typeParams != null)
 			{
+				String sep = "";
 				sb.append("[");
 
 				for (TCType type: edef.typeParams)
 				{
+					sb.append(sep);
 					sb.append(type);
+					sep = ", ";
 				}
 
 				sb.append("]");

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java
@@ -446,10 +446,9 @@ else if (etype instanceof TCMapType)
 					}
 				}
 			}
-			else
-			{
-				addIs(sb, exp, etype);
-			}
+
+			sb.append(prefix);
+			addIs(sb, exp, etype);	// eg. is injective as well as the above
 		}
 		else if (etype instanceof TCSetType)
 		{

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/ModuleReader.java
@@ -57,6 +57,7 @@
 import com.fujitsu.vdmj.ast.modules.ASTModuleList;
 import com.fujitsu.vdmj.ast.types.ASTType;
 import com.fujitsu.vdmj.ast.types.ASTTypeList;
+import com.fujitsu.vdmj.config.Properties;
 import com.fujitsu.vdmj.lex.LexException;
 import com.fujitsu.vdmj.lex.LexLocation;
 import com.fujitsu.vdmj.lex.LexTokenReader;
@@ -382,8 +383,20 @@ private ASTExportedFunction readExportedFunction()
 		LexNameList nameList = readIdList(true);
 		ASTTypeList typeParams = ignoreTypeParams();
 		checkFor(Token.COLON, 2176, "Expecting ':' after export name");
-		ASTType type = getTypeReader().readType();
-		return new ASTExportedFunction(token.location, nameList, type, typeParams);
+
+		// Allow maximal types for inv_T exports
+		boolean saved = Properties.parser_maximal_types;
+
+		try
+		{
+			Properties.parser_maximal_types = true;
+			ASTType type = getTypeReader().readType();
+			return new ASTExportedFunction(token.location, nameList, type, typeParams);
+		}
+		finally
+		{
+			Properties.parser_maximal_types = saved;
+		}
 	}
 
 	private ASTExportList readExportedOperations()
@@ -642,7 +655,19 @@ private ASTImportedFunction readImportedFunction(LexIdentifierToken from)
 		if (lastToken().is(Token.COLON))
 		{
 			nextToken();
-			type = getTypeReader().readType();
+
+			// Allow maximal ! for inv_T functions
+			boolean saved = Properties.parser_maximal_types;
+
+			try
+			{
+				Properties.parser_maximal_types = true;
+				type = getTypeReader().readType();
+			}
+			finally
+			{
+				Properties.parser_maximal_types = saved;
+			}
 		}
 
 		LexNameToken renamed = null;

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java
@@ -56,7 +56,24 @@ public String toString()
 	@Override
 	public String toSource()
 	{
-		return "mk_" + typename + "(" + Utils.listToString(plist) + ")";
+		StringBuilder sb = new StringBuilder();
+
+		sb.append("mk_");
+		sb.append(typename);
+		sb.append("(");
+
+		String sep = "";
+
+		for (TCPattern p: plist)
+		{
+			sb.append(sep);
+			sb.append(p.toSource());
+			sep =", ";
+		}
+
+		sb.append(")");
+
+		return sb.toString();
 	}
 
 	@Override