From 7b509ab300321764dcda27178b0ad9cad630e72f Mon Sep 17 00:00:00 2001
From: Nick Battle <nick.battle@gmail.com>
Date: Fri, 1 Dec 2023 10:29:52 +0000
Subject: [PATCH] Allow maximal pling in function exports

---
 .../com/fujitsu/vdmj/syntax/ModuleReader.java   | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 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
index 343b29e93..09fdfa222 100644
--- 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()