diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala index c7a72fa21fb31d4efb51647806cc0329eb61b179..88cd305ba04572536f9d89c99d761b4ba70ba924 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 bf448e739c3a953e8f32bb78157493b4724e46b5..2cc6591ca6d4ad1dd0cd2b37eceb675d264b69d5 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