From 5d5d95038b4df33ef652bdb84a14fdf4d67c997d Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 23 Oct 2024 17:53:14 +0200 Subject: [PATCH] fix a bug in the extraction that missed some types hidden behind type definition --- frontends/benchmarks/extraction/valid/Typedefs3.scala | 10 ++++++++-- .../stainless/frontends/dotc/CodeExtraction.scala | 9 +++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/frontends/benchmarks/extraction/valid/Typedefs3.scala b/frontends/benchmarks/extraction/valid/Typedefs3.scala index 6b4a0800c..cb10b2cbe 100644 --- a/frontends/benchmarks/extraction/valid/Typedefs3.scala +++ b/frontends/benchmarks/extraction/valid/Typedefs3.scala @@ -1,12 +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 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), 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 4dc996b02..0553d3d7a 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala @@ -2368,16 +2368,25 @@ class CodeExtraction(inoxCtx: inox.Context, 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)