Skip to content

Commit

Permalink
Fix an extraction bug with type synonym definitions (#1595)
Browse files Browse the repository at this point in the history
* fix a bug in the extraction that missed some types hidden behind type synonym definition
  • Loading branch information
samuelchassot authored Oct 27, 2024
1 parent 0010368 commit a4cb53f
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 0 deletions.
18 changes: 18 additions & 0 deletions frontends/benchmarks/extraction/valid/Typedefs3.scala
Original file line number Diff line number Diff line change
@@ -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))

}
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit a4cb53f

Please sign in to comment.