quint/grammar: add support for optional leading hashbang line

CHANGELOG.md

@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 
 - `quint verify` has the option `--apalache-version` to pull a custom version (#1521)
+- Grammar updated with support for an optional leading hashbang (`#!`) line (#1522)
 
 ### Changed
 ### Deprecated

quint/cli-tests.md

@@ -381,3 +381,15 @@ Regression test for [#1108](https://github.com/informalsystems/quint/issues/1108
 
 <!-- !test check 1108 -->
     quint parse testFixture/_1052one.qnt
+
+### OK on typecheck SuperSpec via Unix hashbang
+
+See [#1500](https://github.com/informalsystems/quint/issues/1500).
+
+<!-- !test exit 0 -->
+<!-- !test check typecheck SuperSpec via Unix hashbang -->
+```
+if [ `uname -s` == 'Linux' -o `uname -s` == 'Darwin' ]; then
+    ./testFixture/SuperSpec.qnt
+fi
+```

quint/src/generated/Quint.g4

@@ -16,8 +16,9 @@ grammar Quint;
 import { quintErrorToString } from '../quintError'
 
 }
+
 // entry point for the parser
-modules : module+ EOF;
+modules : HASHBANG_LINE? module+ EOF;
 
 module : DOCCOMMENT* 'module' qualId '{' documentedDeclaration* '}';
 documentedDeclaration : DOCCOMMENT* declaration;
@@ -310,7 +311,9 @@ LOW_ID : ([a-z][a-zA-Z0-9_]*|[_][a-zA-Z0-9_]+) ;
 // An identifier starting with uppercase
 CAP_ID : ([A-Z][a-zA-Z0-9_]*|[_][a-zA-Z0-9_]+) ;
 
-DOCCOMMENT : '///' .*? '\n';
+// Unix script prefix, only valid as the first line of a file
+HASHBANG_LINE : '#!' .*? '\n';
+DOCCOMMENT    : '///' .*? '\n';
 
 // comments and whitespaces
 LINE_COMMENT    :   '//' .*? '\n'   -> skip ;