Merge branch 'main' into sam/sets

frontends/benchmarks/extraction/valid/Typedefs3.scala

@@ -0,0 +1,18 @@
+import stainless.lang.Set
+import stainless.lang.Bag
+import stainless.collection.List
+import stainless.lang.Map
+import stainless.lang.MutableMap
+
+object Typedefs3 {
+  type TypeSet[A] = Set[List[A]]
+  type TypeBag[A] = Bag[List[A]]
+  type TypeMap[A] = Map[Int, List[A]]
+  type TypeMutableMap[A] = MutableMap[Int, List[A]]
+
+  val t: TypeSet[Int] = Set(List(1, 2, 3), List(4, 5, 6))
+  val b: TypeBag[Int] = Bag((List(1, 2, 3), BigInt(3)), (List(4, 5, 6), BigInt(2)))
+  val m: TypeMap[Int] = Map(1 -> List(1, 2, 3), 2 -> List(4, 5, 6))
+  val mm: TypeMutableMap[Int] = MutableMap.withDefaultValue[Int, List[Int]](() => List(1, 2, 3))
+
+}

frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala

@@ -2362,19 +2362,31 @@ class CodeExtraction(inoxCtx: inox.Context,
       case tpe if isStringSym(tpe.typeSymbol) => xt.StringType()
 
       case AppliedType(tr: TypeRef, Seq(tp)) if isSetSym(tr.symbol) =>
+        // We know the underlying is a set, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, Seq(tp)) = tpt.dealias: @unchecked
         xt.SetType(extractType(tp))
 
       case AppliedType(tr: TypeRef, Seq(tp)) if isBagSym(tr.symbol) =>
+        // We know the underlying is a bag, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, Seq(tp)) = tpt.dealias: @unchecked
         xt.BagType(extractType(tp))
 
       case FrontendBVType(signed, size) =>
         xt.AnnotatedType(xt.BVType(signed, size), Seq(xt.StrictBV))
 
       case AppliedType(tr: TypeRef, tps) if isMapSym(tr.symbol) =>
+        // We know the underlying is a map, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, tps) = tpt.dealias: @unchecked
         val Seq(from, to) = tps map extractType
         xt.MapType(from, xt.ClassType(getIdentifier(optionSymbol), Seq(to)).setPos(pos))
 
       case AppliedType(tr: TypeRef, tps) if isMutableMapSym(tr.symbol) =>
+        // We know the underlying is a map, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, tps) = tpt.dealias: @unchecked
         val Seq(from, to) = tps map extractType
         xt.MutableMapType(from, to)