From f15d214df2b52dd8436cb02c0f0cf4763d85a13c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 5 Mar 2014 12:24:18 +0100
Subject: [PATCH] Handle Choose and LetTuple correctly in instantiateType
---
src/main/scala/leon/purescala/TypeTreeOps.scala | 14 +++++++++++++-
1 file changed, 13 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index cb0dd2044..2c22a6e97 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -117,7 +117,11 @@ object TypeTreeOps {
def rec(idsMap: Map[Identifier, Identifier])(e: Expr): Expr = {
def freshId(id: Identifier, newTpe: TypeTree) = {
- FreshIdentifier(id.name, true).setType(newTpe).copiedFrom(id)
+ if (id.getType != newTpe) {
+ FreshIdentifier(id.name, true).setType(newTpe).copiedFrom(id)
+ } else {
+ id
+ }
}
// Simple rec without affecting map
@@ -140,6 +144,14 @@ object TypeTreeOps {
val newId = freshId(id, tpeSub(id.getType))
Let(newId, srec(value), rec(idsMap + (id -> newId))(body)).copiedFrom(l)
+ case l @ LetTuple(ids, value, body) =>
+ val newIds = ids.map(id => freshId(id, tpeSub(id.getType)))
+ LetTuple(newIds, srec(value), rec(idsMap ++ (ids zip newIds))(body)).copiedFrom(l)
+
+ case c @ Choose(xs, pred) =>
+ val newXs = xs.map(id => freshId(id, tpeSub(id.getType)))
+ Choose(newXs, rec(idsMap ++ (xs zip newXs))(pred)).copiedFrom(c)
+
case m @ MatchExpr(e, cases) =>
val newTpe = tpeSub(e.getType)
--
GitLab