Allow maximal pling in function exports

nickbattle · Dec 1, 2023 · 7b509ab · 7b509ab
1 parent de3f852
commit 7b509ab
Showing 1 changed file with 15 additions and 2 deletions.
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()