From 553db4f435037ccb841eb714dc51160a2e7a9744 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 28 Oct 2024 13:07:53 +0000 Subject: [PATCH] Add better isOpaque method --- .../fujitsu/vdmj/pog/SubTypeObligation.java | 2 ++ .../tc/definitions/TCValueDefinition.java | 4 +-- .../tc/expressions/TCFieldExpression.java | 2 +- .../tc/expressions/TCMkTypeExpression.java | 2 +- .../vdmj/tc/patterns/TCRecordPattern.java | 2 +- .../vdmj/tc/types/TCInvariantType.java | 18 ++++++++++- .../fujitsu/vdmj/tc/types/TCNamedType.java | 32 +++++++++---------- .../fujitsu/vdmj/tc/types/TCRecordType.java | 4 +-- .../vdmj/typechecker/TypeComparator.java | 6 ++-- 9 files changed, 44 insertions(+), 28 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 index dda333f78..b9beb05c9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java @@ -211,6 +211,8 @@ public SubTypeObligation( private String oneType(boolean rec, POExpression exp, TCType etype, TCType atype) { + TypeComparator.setCurrentModule(exp.location.module); + if (atype != null && rec) { if (TypeComparator.isSubType(atype, etype)) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCValueDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCValueDefinition.java index efe473c6c..d5dca4443 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCValueDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCValueDefinition.java @@ -227,7 +227,7 @@ private TCType explicitFix(TCType tofix) if (!nt.typename.getLex().module.equals(location.module)) { TCNamedType fixed = new TCNamedType(nt.typename.getExplicit(true), nt.type); - fixed.setOpaque(nt.opaque); + fixed.setOpaque(nt.isOpaque()); return fixed; } } @@ -238,7 +238,7 @@ else if (tofix instanceof TCRecordType) if (!rt.name.getLex().module.equals(location.module)) { TCRecordType fixed = new TCRecordType(rt.name.getExplicit(true), rt.fields, rt.composed); - fixed.setOpaque(rt.opaque); + fixed.setOpaque(rt.isOpaque()); return fixed; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCFieldExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCFieldExpression.java index a7c5b55f5..e677e117b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCFieldExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCFieldExpression.java @@ -222,7 +222,7 @@ else if (env.isFunctional()) { if (!recOrClass) { - if (root instanceof TCRecordType && ((TCRecordType)root).opaque) + if (root instanceof TCRecordType && ((TCRecordType)root).isOpaque(location)) { object.report(3093, "Field '" + field.getName() + "' applied to non-struct export"); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCMkTypeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCMkTypeExpression.java index 578bf17a6..bd96bb2a6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCMkTypeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/TCMkTypeExpression.java @@ -84,7 +84,7 @@ public TCType typeCheck(Environment env, TCTypeList qualifiers, NameScope scope, recordType = (TCRecordType)rec; - if (recordType.opaque && !location.module.equals(recordType.location.module)) + if (recordType.isOpaque(location)) { report(3127, "Type '" + typename + "' has no struct export"); return setType(rec); 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 index 8b289f18a..27ed44753 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java @@ -98,7 +98,7 @@ public void typeResolve(Environment env) { TCRecordType recordType = (TCRecordType)type; - if (recordType.opaque && !location.module.equals(recordType.location.module)) + if (recordType.isOpaque(location)) { report(3127, "Type '" + typename + "' has no struct export"); } 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 index 6a57c7744..1bd526a8e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCInvariantType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCInvariantType.java @@ -38,7 +38,7 @@ public abstract class TCInvariantType extends TCType public TCExplicitFunctionDefinition eqdef = null; public TCExplicitFunctionDefinition orddef = null; - public boolean opaque = false; + private boolean opaque = false; protected boolean inNarrower = false; protected boolean maximal = false; @@ -69,6 +69,22 @@ public boolean isOpaque(LexLocation from) { return opaque && !from.module.equals(location.module); } + + /** + * Is this opaque from here? + */ + public boolean isOpaque(String from) + { + return opaque && !from.equals(location.module); + } + + /** + * Is opaque from anywhere? + */ + public boolean isOpaque() + { + return opaque; + } public void setInvariant(TCExplicitFunctionDefinition invdef) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCNamedType.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCNamedType.java index 7b6fd92ea..c75fc914f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCNamedType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCNamedType.java @@ -62,21 +62,21 @@ public TCNamedType copy(boolean maximal) @Override public boolean isType(Class typeclass, LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isType(typeclass, location); } @Override public boolean isAlways(Class typeclass, LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isAlways(typeclass, location); } @Override public boolean isUnion(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isUnion(location); } @@ -107,28 +107,28 @@ public TCType typeResolve(Environment env) @Override public boolean isSeq(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isSeq(location); } @Override public boolean isSet(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isSet(location); } @Override public boolean isMap(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isMap(location); } @Override public boolean isRecord(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isRecord(from); } @@ -141,21 +141,21 @@ public boolean isTag() @Override public boolean isClass(Environment env) { - if (opaque) return false; + if (isOpaque()) return false; return type.isClass(env); } @Override public boolean isNumeric(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isNumeric(location); } @Override public boolean isOrdered(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; if (orddef != null && !maximal) { @@ -170,7 +170,7 @@ public boolean isOrdered(LexLocation from) @Override public boolean isEq(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; if (eqdef != null && !maximal) { @@ -185,28 +185,28 @@ public boolean isEq(LexLocation from) @Override public boolean isProduct(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isProduct(location); } @Override public boolean isProduct(int n, LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isProduct(n, location); } @Override public boolean isFunction(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isFunction(location); } @Override public boolean isOperation(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return type.isOperation(location); } @@ -353,7 +353,7 @@ public String toDetailedString() @Override public String toDisplay() { - return typename.toString() + (maximal ? "!" : "") + (opaque ? " /* opaque */" : ""); + return typename.toString() + (maximal ? "!" : "") + (isOpaque() ? " /* opaque */" : ""); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCRecordType.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCRecordType.java index d48c31916..a7b0116c2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCRecordType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCRecordType.java @@ -83,7 +83,7 @@ public TCField findField(String tag) @Override public boolean isRecord(LexLocation from) { - if (opaque && !from.module.equals(location.module)) return false; + if (isOpaque(from)) return false; return true; } @@ -150,7 +150,7 @@ public TCType typeResolve(Environment env) @Override public String toDisplay() { - return name.toString() + (maximal ? "!" : "") + (opaque ? " /* opaque */" : ""); + return name.toString() + (maximal ? "!" : "") + (isOpaque() ? " /* opaque */" : ""); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java index a02dfa7fd..06e5868fa 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java @@ -309,8 +309,7 @@ private static Result comptest(TCType to, TCType from, boolean paramOnly) { TCInvariantType ito =(TCInvariantType)to; - if (to instanceof TCNamedType && - (!ito.opaque || ito.location.module.equals(currentModule))) + if (to instanceof TCNamedType && !ito.isOpaque(currentModule)) { to = ((TCNamedType)to).type; continue; @@ -321,8 +320,7 @@ private static Result comptest(TCType to, TCType from, boolean paramOnly) { TCInvariantType ifrom =(TCInvariantType)from; - if (from instanceof TCNamedType && - (!ifrom.opaque || ifrom.location.module.equals(currentModule))) + if (from instanceof TCNamedType && !ifrom.isOpaque(currentModule)) { from = ((TCNamedType)from).type; continue;