From bc1a6fc9cacb44317a20c30400ed459b8ddb33de Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 21 Jan 2015 16:44:59 +0100
Subject: [PATCH] TypeParameterDef.freshen, TypeParameter.freshen
---
src/main/scala/leon/purescala/Definitions.scala | 10 +++++++++-
src/main/scala/leon/purescala/TypeTrees.scala | 4 +++-
2 files changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index c7a72fa21..88cd305ba 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -45,7 +45,10 @@ object Definitions {
}
- /** A ValDef declares a new identifier to be of a certain type. */
+ /**
+ * A ValDef declares a new identifier to be of a certain type.
+ * When creating a new FunDef, its parameters should obey (id.getType == tp)
+ */
case class ValDef(id: Identifier, tpe: TypeTree) extends Definition with Typed {
self: Serializable =>
@@ -103,6 +106,7 @@ object Definitions {
case class TypeParameterDef(tp: TypeParameter) extends Definition {
def subDefinitions = Seq()
+ def freshen = TypeParameterDef(tp.freshen)
val id = tp.id
setSubDefOwners()
}
@@ -460,6 +464,10 @@ object Definitions {
def translated(e: Expr): Expr = instantiateType(e, typesMap, paramsMap)
+ /**
+ * Params will return ValDefs instantiated with the correct types
+ * For such a ValDef(id,tp) it may hold that (id.getType != tp)
+ */
lazy val (params: Seq[ValDef], paramsMap: Map[Identifier, Identifier]) = {
if (typesMap.isEmpty) {
(fd.params, Map())
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index bf448e739..2cc6591ca 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -60,7 +60,9 @@ object TypeTrees {
case object UnitType extends TypeTree
case object CharType extends TypeTree
- case class TypeParameter(id: Identifier) extends TypeTree
+ case class TypeParameter(id: Identifier) extends TypeTree {
+ def freshen = TypeParameter(id.freshen)
+ }
case class TupleType(val bases: Seq[TypeTree]) extends TypeTree {
lazy val dimension: Int = bases.length
--
GitLab