From 5b05bf347dbfdd6d996795b3dd37212ee8ad3981 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 2 Mar 2015 18:08:59 +0100
Subject: [PATCH] Variables never need explicit type overriding

---
 .../scala/leon/purescala/Definitions.scala    |  4 +++-
 src/main/scala/leon/purescala/Trees.scala     | 20 ++-----------------
 .../leon/xlang/ArrayTransformation.scala      |  2 +-
 3 files changed, 6 insertions(+), 20 deletions(-)

diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index eee37aa02..2f96aa02c 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -57,7 +57,9 @@ object Definitions {
 
     def subDefinitions = Seq()
 
-    def toVariable : Variable = Variable(id, tpe)
+    // Warning: the variable will not have the same type as the ValDef, but 
+    // the Identifier type is enough for all use cases in Leon
+    def toVariable : Variable = Variable(id)
 
     setSubDefOwners()
   }
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 2792539aa..059f2f00f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -241,24 +241,8 @@ object Trees {
     val getType = BooleanType
   }
 
-  // tpe, if present, overrides the type of the underlying Identifier id.
-  // This is useful for variables that represent class fields with instantiated types.
-  // E.g. list.head when list: List[Int]
-  // @mk: TODO: This breaks symmetry with the rest of the trees and is ugly-ish.
-  //      Feel free to rename the underlying class and define constructor/extractor,
-  //      or do it some other way
-  class Variable(val id: Identifier, val tpe: Option[TypeTree]) extends Expr with Terminal {
-    val getType = tpe getOrElse id.getType
-    override def equals(that: Any) = that match {
-      case Variable(id2) => id == id2
-      case _ => false
-    }
-    override def hashCode: Int = id.hashCode
-  }
-
-  object Variable {
-    def apply(id: Identifier, tpe: Option[TypeTree] = None) = new Variable(id, tpe)
-    def unapply(v: Variable) = Some(v.id)
+  case class Variable(val id: Identifier) extends Expr with Terminal {
+    val getType = id.getType
   }
 
   /* Literals */
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 1d1c7e24d..513052d1e 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -53,7 +53,7 @@ object ArrayTransformation extends TransformationPhase {
     }
     case v@Variable(i) => {
       val freshId = id2FreshId.get(i).getOrElse(i)
-      Variable(freshId, Some(v.getType))
+      Variable(freshId)
     }
 
     case LetVar(id, e, b) => {
-- 
GitLab