From 8f743372a4ce430a381c5492fabf3cb3b439c2dc Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 17 Sep 2015 17:05:59 +0200
Subject: [PATCH] Substitute types in synthesis holes
---
src/main/scala/leon/purescala/TypeOps.scala | 3 +++
.../scala/leon/unit/purescala/TypeOpsSuite.scala | 15 +++++++++++++++
2 files changed, 18 insertions(+)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index f64c05219..4b458b5d8 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -319,6 +319,9 @@ object TypeOps {
case Error(tpe, desc) =>
Error(tpeSub(tpe), desc).copiedFrom(e)
+ case Hole(tpe, alts) =>
+ Hole(tpeSub(tpe), alts.map(srec)).copiedFrom(e)
+
case g @ GenericValue(tpar, id) =>
tpeSub(tpar) match {
case newTpar : TypeParameter =>
diff --git a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
index 57f37ed34..c7ce03cf7 100644
--- a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
@@ -61,4 +61,19 @@ class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
assert(isSubtypeOf(listD.typed, listD.typed), "List[T] <: List[T]")
}
+ test("instantiateType Hole") { ctx =>
+ val tp1 = TypeParameter.fresh("a")
+ val tp2 = TypeParameter.fresh("b")
+
+ val tpd = TypeParameterDef(tp1)
+
+ val e1 = Hole(tp1, Nil)
+ val e2 = instantiateType(e1, Map(tpd -> tp2), Map())
+
+ e2 match {
+ case Hole(tp, _) => assert(tp == tp2, "Type should have been substituted")
+ case _ => fail("Incorrect expr shape, should be a Hole")
+ }
+ }
+
}
--
GitLab