Merge pull request #1493 from informalsystems/romac/qualified-type

Relax uppercase check for types qualified with a namespace

CHANGELOG.md

@@ -31,6 +31,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - Bumped GRPC message sizes to 1G (#1480)
 - Fix format of ITF trace emitted by `verify` command (#1448)
+- Relax uppercase check for types qualified with a namespace (#1494)
 
 ### Security
 
@@ -148,7 +149,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - The latest supported node version is now bounded at <= 20, which covers the
   latest LTS. (#1380)
-- Shadowing names are now supported, which means that the same name can be redefined 
+- Shadowing names are now supported, which means that the same name can be redefined
   in nested scopes. (#1394)
 - The canonical unit type is now the empty tuple, `()`, rather than the empty
   record, `{}`. This should only affect invisible things to do with sum type

quint/src/parsing/ToIrListener.ts

@@ -294,9 +294,7 @@ export class ToIrListener implements QuintListener {
     const name = ctx.qualId()!.text
     const id = this.getId(ctx)
 
-    if (name[0].match('[a-z]')) {
-      this.errors.push(lowercaseTypeError(id, name))
-    }
+    this.checkForUppercaseTypeName(id, name)
 
     const def: QuintTypeDef = {
       id,
@@ -319,9 +317,8 @@ export class ToIrListener implements QuintListener {
     const type = this.popType().unwrap(() =>
       fail('internal error: type alias declaration parsed with no right hand side')
     )
-    if (name[0].match('[a-z]')) {
-      this.errors.push(lowercaseTypeError(id, name))
-    }
+
+    this.checkForUppercaseTypeName(id, name)
 
     let defWithoutParams: QuintTypeDef = { id: id, kind: 'typedef', name, type }
     const def: QuintTypeDef =
@@ -1297,6 +1294,15 @@ export class ToIrListener implements QuintListener {
       }
     }
   }
+
+  private checkForUppercaseTypeName(id: bigint, qualifiedName: string) {
+    const parts = qualifiedName.split('::')
+    const unqualifiedName = parts.pop()!
+
+    if (unqualifiedName[0].match('[a-z]')) {
+      this.errors.push(lowercaseTypeError(id, unqualifiedName, parts))
+    }
+  }
 }
 
 function popMany<T>(stack: T[], n: number, defaultGen: () => T): T[] {

quint/src/parsing/parseErrors.ts

@@ -1,19 +1,21 @@
 import { QuintError } from '../quintError'
 
-export function lowercaseTypeError(id: bigint, name: string): QuintError {
+export function lowercaseTypeError(id: bigint, name: string, prefix: string[]): QuintError {
+  const original = [...prefix, name].join('::')
+  const newName = name[0].toUpperCase() + name.slice(1)
+  const replacement = [...prefix, newName].join('::')
+
   return {
     code: 'QNT007',
     message: 'type names must start with an uppercase letter',
     reference: id,
-    data: name[0].match('[a-z]')
-      ? {
-          fix: {
-            kind: 'replace',
-            original: `type ${name[0]}`,
-            replacement: `type ${name[0].toUpperCase()}`,
-          },
-        }
-      : {},
+    data: {
+      fix: {
+        kind: 'replace',
+        original: `type ${original}`,
+        replacement: `type ${replacement}`,
+      },
+    },
   }
 }
 

quint/testFixture/SuperSpec.qnt

@@ -29,6 +29,9 @@ module withConsts {
   const MyRecord: { i: int, b: bool, s: str }
   const MyRecordWithComma: { i: int, b: bool, s: str, }
 
+  // A type prefixed with a namespace
+  type some::namespace::MyType = int
+
   // a disjoint union is a common pattern in TLA+
   type MyUnionType =
       | Circle(int)