Merge pull request #1355 from informalsystems/1073/poly-types

Add support for parsing polymorphic type declarations

Author: Shon Feder

quint/package.json

@@ -2,13 +2,7 @@
   "name": "@informalsystems/quint",
   "version": "0.18.1",
   "description": "Core tool for the Quint specification language",
-  "keywords": [
-    "temporal",
-    "logic",
-    "formal",
-    "specification",
-    "verification"
-  ],
+  "keywords": ["temporal", "logic", "formal", "specification", "verification"],
   "homepage": "https://github.com/informalsystems/quint",
   "bugs": "https://github.com/informalsystems/quint/issues",
   "license": "Apache 2.0",
@@ -35,11 +29,7 @@
   "bin": {
     "quint": "dist/src/cli.js"
   },
-  "files": [
-    "README.md",
-    "dist/**/*",
-    "test/**/*.ts"
-  ],
+  "files": ["README.md", "dist/**/*", "test/**/*.ts"],
   "engines": {
     "node": ">=18"
   },
@@ -72,6 +62,8 @@
     "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/reflection.proto ./src/builtin.qnt ./dist/src/",
     "prepare": "rm -rf ./dist && npm run compile && chmod +x ./dist/src/cli.js",
     "test": "mocha --reporter-option maxDiffSize=0 -r ts-node/register test/*.test.ts test/**/*.test.ts",
+    "test-w": "while inotifywait -r -e close_write ./ ; do npm run test; done",
+    "test-f": "mocha --reporter-option maxDiffSize=0 -r ts-node/register",
     "coverage": "nyc npm run test",
     "integration": "txm cli-tests.md && txm io-cli-tests.md",
     "apalache-integration": "txm apalache-tests.md",

quint/src/generated/Quint.g4

@@ -52,11 +52,15 @@ operDef : qualifier normalCallName
         ;
 
 typeDef
-    : 'type' qualId                                                         # typeAbstractDef
-    | 'type' qualId '=' type                                                # typeAliasDef
-    | 'type' typeName=qualId '=' '|'? typeSumVariant ('|' typeSumVariant)*  # typeSumDef
+    : 'type' qualId                             # typeAbstractDef
+    | 'type' typeDefHead '=' type               # typeAliasDef
+    | 'type' typeDefHead '=' sumTypeDefinition  # typeSumDef
     ;
 
+typeDefHead : typeName=qualId ('[' typeVars+=typeVar(',' typeVars+=typeVar)* ']')?;
+
+sumTypeDefinition : '|'? typeSumVariant ('|' typeSumVariant)* ;
+
 // A single variant case in a sum type definition or match statement.
 // E.g., `A(t)` or `A`.
 typeSumVariant : sumLabel=simpleId["variant label"] ('(' type ')')? ;
@@ -96,28 +100,32 @@ qualifiedName : qualId;
 fromSource: STRING;
 
 // Types in Type System 1.2 of Apalache
-type :          <assoc=right> type '->' type                    # typeFun
-        |       <assoc=right> type '=>' type                    # typeOper
-        |       '(' (type (',' type)*)? ','? ')' '=>' type      # typeOper
-        |       SET '[' type ']'                                # typeSet
-        |       LIST '[' type ']'                               # typeList
-        |       '(' type ',' type (',' type)* ','? ')'          # typeTuple
-        |       '{' row '}'                                     # typeRec
-        |       'int'                                           # typeInt
-        |       'str'                                           # typeStr
-        |       'bool'                                          # typeBool
-        |       LOW_ID                                          # typeVar
-        |       qualId                                          # typeConst
-        |       '(' type ')'                                    # typeParen
-        ;
+type
+    : <assoc=right> type '->' type                               # typeFun
+    | <assoc=right> type '=>' type                               # typeOper
+    | '(' (type (',' type)*)? ','? ')' '=>' type                 # typeOper
+    // TODO: replace Set with general type application
+    | SET '[' type ']'                                           # typeSet
+    // TODO: replace List with general type application
+    | LIST '[' type ']'                                          # typeList
+    | '(' type ',' type (',' type)* ','? ')'                     # typeTuple
+    | '{' row? '}'                                               # typeRec
+    | 'int'                                                      # typeInt
+    | 'str'                                                      # typeStr
+    | 'bool'                                                     # typeBool
+    | typeVar                                                    # typeVarCase
+    | qualId                                                     # typeConst
+    | '(' type ')'                                               # typeParen
+    | typeCtor=type ('[' typeArg+=type (',' typeArg+=type)* ']') # typeApp
+    ;
 
-row : (rowLabel ':' type ',')* ((rowLabel ':' type) (',' | '|' (rowVar=identifier))?)?
+typeVar: LOW_ID;
+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.,
@@ -269,8 +277,6 @@ AND             :   'and' ;
 OR              :   'or'  ;
 IFF             :   'iff' ;
 IMPLIES         :   'implies' ;
-SET             :   'Set' ;
-LIST            :   'List' ;
 MAP             :   'Map' ;
 MATCH           :   'match' ;
 PLUS            :   '+' ;
@@ -287,6 +293,8 @@ EQ              :   '==' ;
 ASGN            :   '=' ;
 LPAREN          :   '(' ;
 RPAREN          :   ')' ;
+SET             :   'Set';
+LIST            :   'List';
 
 // An identifier starting with lowercase
 LOW_ID : ([a-z][a-zA-Z0-9_]*|[_][a-zA-Z0-9_]+) ;