Merge pull request #1371 from informalsystems/1177/via-param-annotations

Constrain operator parameters by their type annotations

Author: Shon Feder

CHANGELOG.md

@@ -39,6 +39,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed type checker to account for type constraints on annotated operator
+  parameters when checking operator bodies (#1177).
+
 ### Security
 
 ## v0.18.1 -- 2024-01-16

quint/src/generated/Quint.g4

@@ -25,7 +25,7 @@ documentedDeclaration : DOCCOMMENT* declaration;
 // a module declaration
 declaration : 'const' qualId ':' type                     # const
             | 'var'   qualId ':' type                     # var
-            | 'assume' identOrHole '=' expr               # assume
+            | 'assume' (assumeName=identOrHole) '=' expr  # assume
             | instanceMod                                 # instance
             | operDef                                     # oper
             | typeDef                                     # typeDefs
@@ -39,17 +39,28 @@ declaration : 'const' qualId ':' type                     # const
             ;
 
 // An operator definition.
-// We embed two kinds of parameters right in this rule.
-// Otherwise, the parser would start recognizing parameters everywhere.
-operDef : qualifier normalCallName
-            ( /* ML-like parameter lists */
-                '(' (parameter (',' parameter)*)? ')' (':' type)?
-                | ':' type
-              /* C-like parameter lists */
-                | '(' (parameter ':' type (',' parameter ':' type)*) ')' ':' type
-            )?
-            ('=' expr)? ';'?
-        ;
+operDef
+    : qualifier normalCallName
+        // Fully-annotated parameter list with at least one parameter
+        '(' (annotOperParam+=annotatedParameter (',' annotOperParam+=annotatedParameter)*) ')'
+        // Mandatory annotation for return type
+        ':' type
+        // We support header declaration with no implementation for documentation genaration
+        ('=' expr)?
+        // Optionally terminated with a semicolon
+        ';'?
+        # annotatedOperDef
+    | qualifier normalCallName // TODO: Remove as per https://github.com/informalsystems/quint/issues/923
+        // Unannotated parameter list
+        ('(' (operParam+=parameter (',' operParam+=parameter)*)? ')')?
+        // Optional type annotation using the deprecated format
+        (':' annotatedRetType=type)?
+        // We support header declaration with no implementation for documentation genaration
+        ('=' expr)?
+        // Optionally terminated with a semicolon
+        ';'?
+        # deprecatedOperDef
+    ;
 
 typeDef
     : 'type' qualId                             # typeAbstractDef
@@ -205,10 +216,12 @@ lambdaUnsugared : parameter '=>' expr
 lambdaTupleSugar : '(' '(' parameter (',' parameter)+ ')' ')' '=>' expr;
 
 // an identifier or a hole '_'
-identOrHole :   '_' | qualId
-        ;
+identOrHole : '_' | qualId;
 
-parameter: identOrHole;
+// TODO: Combine these into a single rule that support optionally annotated parameters
+//       Requires https://github.com/informalsystems/quint/issues/923
+parameter: paramName=identOrHole;
+annotatedParameter: paramName=identOrHole ':' type;
 
 // an identifier or a star '*'
 identOrStar :   '*' | qualId