diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala index a1fc0c4fe6de2fedacdebe0383fd6985eef6c854..20e41e421ddeff854e809ff194417c478139bcf3 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 9a1c0559fe5529d00b847c0aef4b54f84119bb64..d7533097e4da156889b603e4f69b9e47f6969443 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)