use unapply

viperproject · May 21, 2024 · 2e825d1 · 2e825d1
1 parent 5dbb6b3
commit 2e825d1
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 16 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/UnderlyingType.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/UnderlyingType.scala
@@ -19,6 +19,10 @@ trait UnderlyingType { this: TypeInfoImpl =>
     def unapply(t: Type): Option[Type] = Some(underlyingType(t))
   }
 
+  object UnderlyingPType {
+    def unapply(t: PType): Option[PType] = underlyingTypeP(t)
+  }
+
   lazy val underlyingType: Type => Type =
     attr[Type, Type] {
       case Single(DeclaredT(t: PTypeDecl, context: ExternalTypeInfo)) => underlyingType(context.symbType(t.right))

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
@@ -467,25 +467,22 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
       case PCompositeLit(typ, _) => typ match {
         case _: PImplicitSizeArrayType => true
-        case t: PType => underlyingTypeP(t) match {
-          case Some(ut: PType with PLiteralType) => ut match {
-            case g: PGhostLiteralType => g match {
-              case _: PGhostSliceType => false
-              case _: PAdtType | _: PDomainType | _: PMathematicalMapType |
-                _: PMultisetType | _: POptionType | _: PSequenceType | _: PSetType => true
-            }
-            case _: PArrayType | _: PStructType => true
-            case _: PMapType | _: PSliceType => false
-            case d@(_: PDot | _: PNamedOperand) =>
-              // underlyingTypeP should never return any of these types
-              violation(s"Unexpected underlying type $d")
+        case UnderlyingPType(t: PLiteralType) => t match {
+          case g: PGhostLiteralType => g match {
+            case _: PGhostSliceType => false
+            case _: PAdtType | _: PDomainType | _: PMathematicalMapType |
+              _: PMultisetType | _: POptionType | _: PSequenceType | _: PSetType => true
           }
-          case Some(d) =>
-            // the type system should already have rejected composite literals whose underlying type is not a valid
-            // literal type.
+          case _: PArrayType | _: PStructType => true
+          case _: PMapType | _: PSliceType => false
+          case d@(_: PDot | _: PNamedOperand) =>
+            // UnderlyingPType should never return any of these types
             violation(s"Unexpected underlying type $d")
-          case None => false
         }
+        case t =>
+          // the type system should already have rejected composite literals whose underlying type is not a valid
+          // literal type.
+          violation(s"Unexpected literal type $t")
       }
 
       case POptionNone(_) => true