diff --git a/frontends/benchmarks/extraction/valid/Typedefs3.scala b/frontends/benchmarks/extraction/valid/Typedefs3.scala new file mode 100644 index 000000000..cb10b2cbe --- /dev/null +++ b/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)) + +} diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala index 4400873ae..0553d3d7a 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala +++ b/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)