Try to fix subtype obligation for unions

nickbattle · Oct 28, 2024 · 74a37f4 · 74a37f4
1 parent 3051cf0
commit 74a37f4
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 3 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java
@@ -206,6 +206,9 @@ public SubTypeObligation(
 		source = ctxt.getSource(oneType(false, result, def.type.result, actualResult));
 	}
 
+	// NOTE! The atype parameter used to allow null to mean "any type", but this
+	// also caused problems sometimes with POs. Currently atype is not null...
+
 	private String oneType(boolean rec, POExpression exp, TCType etype, TCType atype)
 	{
 		if (atype != null && rec)
@@ -215,7 +218,7 @@ private String oneType(boolean rec, POExpression exp, TCType etype, TCType atype
 				return "";		// A sub comparison is OK without checks
 			}
 		}
-
+		
 		StringBuilder sb = new StringBuilder();
 		String prefix = "";
 		etype = etype.deBracket();
@@ -237,7 +240,7 @@ private String oneType(boolean rec, POExpression exp, TCType etype, TCType atype
 
 			for (TCType poss: possibles)
 			{
-				String s = oneType(true, exp, poss, null);
+				String s = oneType(true, exp, poss, atype);
 
 				sb.append(prefix);
 				sb.append("(");
@@ -287,7 +290,7 @@ else if (etype instanceof TCNamedType)
 				}
 				else
 				{
-					atype = null;
+					// atype = null;
 				}
 
 				String s = oneType(true, exp, nt.type, atype);

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCInvariantType.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCInvariantType.java
@@ -61,6 +61,14 @@ public void setOpaque(boolean opaque)
 	{
 		this.opaque = opaque;
 	}
+
+	/**
+	 * Is this opaque from here?
+	 */
+	public boolean isOpaque(LexLocation from)
+	{
+		return opaque && !from.module.equals(location.module);
+	}
 
 	public void setInvariant(TCExplicitFunctionDefinition invdef)
 	{