From 5f0ee7d5b02695cb077b46e1ad5d694571eb77f5 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 22 Jan 2015 11:13:09 +0100
Subject: [PATCH] Make sure Generic values get updated according to expected
type in some cases
---
src/main/scala/leon/codegen/CompilationUnit.scala | 5 +++--
src/main/scala/leon/purescala/TypeTreeOps.scala | 8 ++++++++
2 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index a1fc0c4fe..20e41e421 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -213,8 +213,9 @@ class CompilationUnit(val ctx: LeonContext,
}
Tuple(elems)
- case (gv : GenericValue, _: TypeParameter) =>
- gv
+ case (gv @ GenericValue(gtp, id), tp: TypeParameter) =>
+ if (gtp == tp) gv
+ else GenericValue(tp, id).copiedFrom(gv)
case (set : runtime.Set, SetType(b)) =>
FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSet).setType(SetType(b))
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 9a1c0559f..d7533097e 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -302,6 +302,14 @@ object TypeTreeOps {
case Error(tpe, desc) =>
Error(tpeSub(tpe), desc).copiedFrom(e)
+ case g @ GenericValue(tpar, id) =>
+ tpeSub(tpar) match {
+ case newTpar : TypeParameter =>
+ GenericValue(newTpar, id).copiedFrom(g)
+ case other => // FIXME any better ideas?
+ sys.error(s"Tried to substitute $tpar with $other within GenericValue $g")
+ }
+
case ens @ Ensuring(body, id, pred) =>
val newId = freshId(id, tpeSub(id.getType))
Ensuring(srec(body), newId, rec(idsMap + (id -> newId))(pred)).copiedFrom(ens)
--
GitLab