Disallow empty PVL enums in PVLToCol transform

An enum that does not define any enumeration constants is now a parse error.

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -37,10 +37,10 @@ case class PVLToCol[G](
 
   def convert(implicit enum: EnumDeclContext): Enum[G] =
     enum match {
-      case EnumDecl0(_, name, _, constants, _, _) =>
-        new vct.col.ast.Enum[G](constants.map(convertConstants(_)).getOrElse(
-          Nil
-        ))(origin(enum).sourceName(convert(name)))
+      case EnumDecl0(_, name, _, Some(constants), _, _) =>
+        new vct.col.ast.Enum[G](convertConstants(constants))(origin(enum).sourceName(convert(name)))
+      case _ =>
+        fail(enum, "This enumeration must specify at least one constant")
     }
 
   def convertConstants(

test/main/vct/test/integration/examples/TechnicalEnumSpec.scala

@@ -45,6 +45,14 @@ class Test {
     enum AB { A, B }
   """
 
+  vercors should error withCode "parseError" in "pvl/empty enum" pvl """
+    enum E { }
+  """
+
+  vercors should error withCode "parseError" in "pvl/empty enum with added comma" pvl """
+    enum E { , }
+  """
+
   vercors should verify using silicon in "pvl/enum return" pvl """
     enum AB { A, B }