Require record fields to be simple identifiers

CHANGELOG.md

@@ -11,12 +11,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - `quint repl` produces an evaluation trace on errors too (#1056)
 - `S.setOfMaps(Int).oneOf()` is now supported (#1060)
+- `quint run` produces a friendlier message when it meets a `const` (#1050)
 
 ### Changed
 
-- **Breaking**: the behavior of `oneOf` has changed, existing seed values for `quint test`
+- The behavior of `oneOf` has changed, existing seed values for `quint test`
   can exhibit different behavior than before (#1060)
-- `quint run` produces a friendlier message when it meets a `const` (#1050)
+- Record field labels that include `::` are now illegal and raise a syntax error
+  (#1086)
 
 ### Deprecated
 ### Removed

quint/src/generated/Quint.g4

@@ -10,23 +10,27 @@
  */
 grammar Quint;
 
+@header {
+    // Used for forming errors
+    import { quintErrorToString } from '../quintError'
+}
 // entry point for the parser
 modules : module+ EOF;
 
-module : DOCCOMMENT* 'module' IDENTIFIER '{' documentedUnit* '}';
+module : DOCCOMMENT* 'module' qualId '{' documentedUnit* '}';
 documentedUnit : DOCCOMMENT* unit;
 
 // a module unit
-unit :    'const' IDENTIFIER ':' type                     # const
-        | 'var'   IDENTIFIER ':' type                     # var
-        | 'assume' identOrHole '=' expr                   # assume
-        | instanceMod                                     # instance
-        | operDef                                         # oper
-        | typeDef                                         # typeDefs
-        | importMod                                       # importDef
-        | exportMod                                       # exportDef
+unit :    'const' qualId ':' type                     # const
+        | 'var'   qualId ':' type                     # var
+        | 'assume' identOrHole '=' expr               # assume
+        | instanceMod                                 # instance
+        | operDef                                     # oper
+        | typeDef                                     # typeDefs
+        | importMod                                   # importDef
+        | exportMod                                   # exportDef
         // https://github.com/informalsystems/quint/issues/378
-        //| 'nondet' IDENTIFIER (':' type)? '=' expr ';'? expr {
+        //| 'nondet' qualId (':' type)? '=' expr ';'? expr {
         //  const m = "QNT007: 'nondet' is only allowed inside actions"
         //  this.notifyErrorListeners(m)
         //}                                                 # nondetError
@@ -46,11 +50,11 @@ operDef : qualifier normalCallName
         ;
 
 typeDef
-    : 'type' IDENTIFIER          # typeAbstractDef
-    | 'type' IDENTIFIER '=' type # typeAliasDef
+    : 'type' qualId          # typeAbstractDef
+    | 'type' qualId '=' type # typeAliasDef
     ;
 
-nondetOperDef : 'nondet' IDENTIFIER (':' type)? '=' expr ';'?;
+nondetOperDef : 'nondet' qualId (':' type)? '=' expr ';'?;
 
 qualifier : 'val'
           | 'def'
@@ -79,9 +83,9 @@ instanceMod :   // creating an instance and importing all names introduced in th
                   ('from' fromSource)?
         ;
 
-moduleName : IDENTIFIER;
-name: IDENTIFIER;
-qualifiedName : IDENTIFIER;
+moduleName : qualId;
+name: qualId;
+qualifiedName : qualId;
 fromSource: STRING;
 
 // Types in Type System 1.2 of Apalache, which supports discriminated unions
@@ -96,17 +100,20 @@ type :          <assoc=right> type '->' type                    # typeFun
         |       'int'                                           # typeInt
         |       'str'                                           # typeStr
         |       'bool'                                          # typeBool
-        |       IDENTIFIER                                      # typeConstOrVar
+        |       qualId                                          # typeConstOrVar
         |       '(' type ')'                                    # typeParen
         ;
 
-typeUnionRecOne : '|' '{' IDENTIFIER ':' STRING (',' row)? ','? '}'
+typeUnionRecOne : '|' '{' qualId ':' STRING (',' row)? ','? '}'
                 ;
 
-row : | (IDENTIFIER ':' type ',')* ((IDENTIFIER ':' type) (',' | '|' (IDENTIFIER))?)?
-      | '|' (IDENTIFIER)
+row : (rowLabel ':' type ',')* ((rowLabel ':' type) (',' | '|' (rowVar=IDENTIFIER))?)?
+    | '|' (rowVar=IDENTIFIER)
     ;
 
+rowLabel : simpleId["record"] ;
+
+
 // A Quint expression. The order matters, it defines the priority.
 // Wherever possible, we keep the same order of operators as in TLA+.
 // We are also trying to be consistent with mainstream languages, e.g.,
@@ -129,7 +136,7 @@ expr:           // apply a built-in operator via the dot notation
         |       expr op=(PLUS | MINUS) expr                         # plusMinus
                 // standard relations
         |       expr op=(GT | LT | GE | LE | NE | EQ) expr          # relations
-        |       IDENTIFIER '\'' ASGN expr                           # asgn
+        |       qualId '\'' ASGN expr                               # asgn
         |       expr '=' expr {
                   const m = "QNT006: unexpected '=', did you mean '=='?"
                   this.notifyErrorListeners(m)
@@ -146,7 +153,7 @@ expr:           // apply a built-in operator via the dot notation
                     ('|' STRING ':' parameter '=>' expr)+           # match
         |       'all' '{' expr (',' expr)* ','? '}'                 # actionAll
         |       'any' '{' expr (',' expr)* ','? '}'                 # actionAny
-        |       ( IDENTIFIER | INT | BOOL | STRING)                 # literalOrId
+        |       ( qualId | INT | BOOL | STRING)                     # literalOrId
         //      a tuple constructor, the form tup(...) is just an operator call
         |       '(' expr ',' expr (',' expr)* ','? ')'              # tuple
         //      short-hand syntax for pairs, mainly designed for maps
@@ -176,31 +183,31 @@ lambda:         parameter '=>' expr
 
 
 // an identifier or a hole '_'
-identOrHole :   '_' | IDENTIFIER
+identOrHole :   '_' | qualId
         ;
 
 parameter: identOrHole;
 
 // an identifier or a star '*'
-identOrStar :   '*' | IDENTIFIER
+identOrStar :   '*' | qualId
         ;
 
 argList :      expr (',' expr)*
         ;
 
-recElem : IDENTIFIER ':' expr
+recElem : simpleId["record"] ':' expr
         | '...' expr
         ;
 
 // operators in the normal call may use a few reserved names,
 // which are not recognized as identifiers.
-normalCallName :   IDENTIFIER
+normalCallName :   qualId
         |       op=(AND | OR | IFF | IMPLIES | SET | LIST | MAP)
         ;
 
 // A few infix operators may be called via lhs.oper(rhs),
 // without causing any ambiguity.
-nameAfterDot :  IDENTIFIER
+nameAfterDot :  qualId
         |       op=(AND | OR | IFF | IMPLIES)
         ;
 
@@ -214,6 +221,21 @@ operator: (AND | OR | IFF | IMPLIES |
 literal: (STRING | BOOL | INT)
         ;
 
+// A (possibly) qualified identifier, like `Foo` or `Foo::bar`
+qualId : IDENTIFIER ('::' IDENTIFIER)* ;
+// An unqualified identifier that raises an error if a qualId is supplied
+simpleId[context: string]
+    : IDENTIFIER
+    | qualId {
+        const err = quintErrorToString(
+          { code: 'QNT008',
+            message: "Identifiers in a " + $context + " cannot be qualified with '::'. Found " + $qualId.text + "."
+          },
+        )
+        this.notifyErrorListeners(err)
+      }
+    ;
+
 // TOKENS
 
 // literals
@@ -250,8 +272,7 @@ LPAREN          :   '(' ;
 RPAREN          :   ')' ;
 
 // other TLA+ identifiers
-IDENTIFIER             : SIMPLE_IDENTIFIER | SIMPLE_IDENTIFIER '::' IDENTIFIER ;
-SIMPLE_IDENTIFIER      : ([a-zA-Z][a-zA-Z0-9_]*|[_][a-zA-Z0-9_]+) ;
+IDENTIFIER      : ([a-zA-Z][a-zA-Z0-9_]*|[_][a-zA-Z0-9_]+) ;
 
 DOCCOMMENT : '///' .*? '\n';