Treat values of type InternalSingleMulti(t, ms) as t for nested dictionaries

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -305,49 +305,53 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
         val baseType = exprType(base)
         val idxType  = exprType(index)
         (underlyingType(baseType), underlyingType(idxType)) match {
-          case (ArrayT(l, _), IntT(_)) =>
-            val idxOpt = intConstantEval(index)
-            error(n, s"index $index is out of bounds", !idxOpt.forall(i => i >= 0 && i < l))
-
-          case (PointerT(ArrayT(l, _)), IntT(_)) =>
-            val idxOpt = intConstantEval(index)
-            error(n, s"index $index is out of bounds", !idxOpt.forall(i => i >= 0 && i < l))
-
-          case (SequenceT(_), IntT(_)) =>
-            noMessages
-
-          case (_: SliceT | _: GhostSliceT, IntT(_)) =>
-            noMessages
-
-          case (VariadicT(_), IntT(_)) =>
-            noMessages
+          case (Single(base), Single(idx)) => (base, idx) match {
+            case (ArrayT(l, _), IntT(_)) =>
+              val idxOpt = intConstantEval(index)
+              error(n, s"index $index is out of bounds", !idxOpt.forall(i => i >= 0 && i < l))
+
+            case (PointerT(ArrayT(l, _)), IntT(_)) =>
+              val idxOpt = intConstantEval(index)
+              error(n, s"index $index is out of bounds", !idxOpt.forall(i => i >= 0 && i < l))
+
+            case (SequenceT(_), IntT(_)) =>
+              noMessages
+
+            case (_: SliceT | _: GhostSliceT, IntT(_)) =>
+              noMessages
+
+            case (VariadicT(_), IntT(_)) =>
+              noMessages
+
+            case (StringT, IntT(_)) =>
+              error(n, "Indexing a string is currently not supported")
+
+            case (MapT(key, _), underlyingIdxType) =>
+              // Assignability in Go is a property between a value and and a type. In Gobra, we model this as a relation
+              // between two types, which is less precise. Because of this limitation, and with the goal of handling
+              // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go
+              // expressions that are not accepted by the compiler.
+              val assignableToIdxType = error(n, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key))
+              if (assignableToIdxType.nonEmpty) {
+                error(n, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key))
+              } else {
+                assignableToIdxType
+              }
 
-          case (StringT, IntT(_)) =>
-            error(n, "Indexing a string is currently not supported")
-
-          case (MapT(key, _), underlyingIdxType) =>
-            // Assignability in Go is a property between a value and and a type. In Gobra, we model this as a relation
-            // between two types, which is less precise. Because of this limitation, and with the goal of handling
-            // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go
-            // expressions that are not accepted by the compiler.
-            val assignableToIdxType = error(n, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key))
-            if (assignableToIdxType.nonEmpty) {
-              error(n, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key))
-            } else {
-              assignableToIdxType
-            }
+            case (MathMapT(key, _), underlyingIdxType) =>
+              // Assignability in Go is a property between a value and and a type. In Gobra, we model this as a relation
+              // between two types, which is less precise. Because of this limitation, and with the goal of handling
+              // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go
+              // expressions that are not accepted by the compiler.
+              val assignableToIdxType = error(n, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key))
+              if (assignableToIdxType.nonEmpty) {
+                error(n, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key))
+              } else {
+                assignableToIdxType
+              }
 
-          case (MathMapT(key, _), underlyingIdxType) =>
-            // Assignability in Go is a property between a value and and a type. In Gobra, we model this as a relation
-            // between two types, which is less precise. Because of this limitation, and with the goal of handling
-            // untyped literals, we introduce an extra condition here. This makes the type checker of Gobra accept Go
-            // expressions that are not accepted by the compiler.
-            val assignableToIdxType = error(n, s"$idxType is not assignable to map key of $key", !assignableTo(idxType, key))
-            if (assignableToIdxType.nonEmpty) {
-              error(n, s"$underlyingIdxType is not assignable to map key of $key", !assignableTo(underlyingIdxType, key))
-            } else {
-              assignableToIdxType
-            }
+            case (bt, it) => error(n, s"$it index is not a proper index of $bt")
+          }
 
           case (bt, it) => error(n, s"$it index is not a proper index of $bt")
         }
@@ -669,16 +673,19 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       val baseType = exprType(base)
       val idxType  = exprType(index)
       (underlyingType(baseType), underlyingType(idxType)) match {
-        case (ArrayT(_, elem), IntT(_)) => elem
-        case (PointerT(ArrayT(_, elem)), IntT(_)) => elem
-        case (SequenceT(elem), IntT(_)) => elem
-        case (SliceT(elem), IntT(_)) => elem
-        case (GhostSliceT(elem), IntT(_)) => elem
-        case (VariadicT(elem), IntT(_)) => elem
-        case (MapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) =>
-          InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT)))
-        case (MathMapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) =>
-          InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT)))
+        case (Single(base), Single(idx)) => (base, idx) match {
+          case (ArrayT(_, elem), IntT(_)) => elem
+          case (PointerT(ArrayT(_, elem)), IntT(_)) => elem
+          case (SequenceT(elem), IntT(_)) => elem
+          case (SliceT(elem), IntT(_)) => elem
+          case (GhostSliceT(elem), IntT(_)) => elem
+          case (VariadicT(elem), IntT(_)) => elem
+          case (MapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) =>
+            InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT)))
+          case (MathMapT(key, elem), underlyingIdxType) if assignableTo(idxType, key) || assignableTo(underlyingIdxType, key) =>
+            InternalSingleMulti(elem, InternalTupleT(Vector(elem, BooleanT)))
+          case (bt, it) => violation(s"$it is not a valid index for the the base $bt")
+        }
         case (bt, it) => violation(s"$it is not a valid index for the the base $bt")
       }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -205,11 +205,11 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
           case t => error(op, s"expected a sequence, multiset or option type, but got $t")
         }
         case PMapKeys(exp) => underlyingType(exprType(exp)) match {
-          case _: MathMapT | _: MapT => isExpr(exp).out
+          case Single(_: MathMapT | _: MapT) => isExpr(exp).out
           case t => error(expr, s"expected a map, but got $t")
         }
         case PMapValues(exp) => underlyingType(exprType(exp)) match {
-          case _: MathMapT | _: MapT => isExpr(exp).out
+          case Single(_: MathMapT | _: MapT) => isExpr(exp).out
           case t => error(expr, s"expected a map, but got $t")
         }
       }
@@ -260,7 +260,14 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PGhostEquals | _: PGhostUnequals => BooleanT
 
     case POptionNone(t) => OptionT(typeSymbType(t))
-    case POptionSome(e) => OptionT(exprType(e))
+    case POptionSome(e) =>
+      val et = exprType(e)
+      val ut = underlyingType(et)
+      ut match {
+        case Single(t) => OptionT(t)
+        case t => violation(s"expected a single type, but got $t")
+      }
+
     case POptionGet(e) => exprType(e) match {
       case OptionT(t) => t
       case t => violation(s"expected an option type, but got $t")
@@ -308,13 +315,13 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
           case t => violation(s"expected a sequence, set, multiset or option type, but got $t")
         }
         case PMapKeys(exp) => underlyingType(exprType(exp)) match {
-          case t: MathMapT => SetT(t.key)
-          case t: MapT => SetT(t.key)
+          case Single(t: MathMapT) => SetT(t.key)
+          case Single(t: MapT) => SetT(t.key)
           case t => violation(s"expected a map, but got $t")
         }
         case PMapValues(exp) => underlyingType(exprType(exp)) match {
-          case t: MathMapT => SetT(t.elem)
-          case t: MapT => SetT(t.elem)
+          case Single(t: MathMapT) => SetT(t.elem)
+          case Single(t: MapT) => SetT(t.elem)
           case t => violation(s"expected a map, but got $t")
         }
       }

src/main/scala/viper/gobra/translator/Names.scala

@@ -62,6 +62,7 @@ object Names {
     case in.ArrayT(len, elemT, addr) => s"Array$len${serializeType(elemT)}${serializeAddressability(addr)}"
     case in.SliceT(elemT, addr) => s"Slice${serializeType(elemT)}${serializeAddressability(addr)}"
     case in.MapT(keyT, valueT, addr) => s"Map${serializeType(keyT)}_${serializeType(valueT)}_${serializeAddressability(addr)}"
+    case in.MathMapT(keyT, valueT, addr) => s"Dict${serializeType(keyT)}_${serializeType(valueT)}_${serializeAddressability(addr)}"
     case in.SequenceT(elemT, addr) => s"Sequence${serializeType(elemT)}${serializeAddressability(addr)}"
     case in.SetT(elemT, addr) => s"Set${serializeType(elemT)}${serializeAddressability(addr)}"
     case in.MultisetT(elemT, addr) => s"Multiset${serializeType(elemT)}${serializeAddressability(addr)}"

src/test/resources/regressions/features/maps/maps-nested.gobra

@@ -0,0 +1,11 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+ghost
+func foo(){
+    mm := dict[int](dict[int]int){1 : {2:3}}
+    assert mm[1][2] == 3
+    assert 2 in domain(mm[1])
+}

src/test/resources/regressions/features/options/options-nested-maps.gobra

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+ghost
+pure func bar(m dict[int]int, idx int) option[int] {
+    return idx in domain(m) ? some(m[idx]) : none[int]
+}
+
+ghost
+pure func baz(m dict[int]int, idx int) option[int] {
+    return match idx in domain(m){
+        case true:
+            some(m[idx])
+        case false:
+            none[int]
+    }
+}