From dc01ccda4799a67e5bd4d4cb8e08117caba9be1e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 26 Nov 2012 16:04:51 +0100
Subject: [PATCH] Specify ids with per-name counters
---
src/main/scala/leon/purescala/Common.scala | 32 +++++++++-------------
1 file changed, 13 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 6132bd607..172b34ffe 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -6,14 +6,14 @@ object Common {
import TypeTrees.Typed
// the type is left blank (Untyped) for Identifiers that are not variables
- class Identifier private[Common](val name: String, val id: Int, alwaysShowUniqueID: Boolean = false) extends Typed {
+ class Identifier private[Common](val name: String, private val globalId: Int, val id: Int, alwaysShowUniqueID: Boolean = false) extends Typed {
self : Serializable =>
override def equals(other: Any): Boolean = {
if(other == null || !other.isInstanceOf[Identifier])
false
else
- other.asInstanceOf[Identifier].id == this.id
+ other.asInstanceOf[Identifier].globalId == this.globalId
}
override def hashCode: Int = id
@@ -23,7 +23,7 @@ object Common {
// angle brackets: name + "\u3008" + id + "\u3009"
name + "[" + id + "]"
} else if(alwaysShowUniqueID) {
- name + id
+ name + (if(id > 0) id else "")
} else {
name
}
@@ -39,28 +39,22 @@ object Common {
}
private object UniqueCounter {
- private var soFar: Int = -1
+ private var globalId = -1
+ private var nameIds = Map[String, Int]().withDefaultValue(-1)
- def next: Int = {
- soFar = soFar + 1
- soFar
+ def next(name: String): Int = {
+ nameIds += name -> (1+nameIds(name))
+ nameIds(name)
}
-
- def last: Int = {
- soFar
+
+ def nextGlobal = {
+ globalId += 1
+ globalId
}
}
object FreshIdentifier {
- def forceSkip(i : Int) : Unit = {
- while(UniqueCounter.last < i) {
- UniqueCounter.next
- }
- }
-
- def last: Int = UniqueCounter.last
-
- def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.next, alwaysShowUniqueID)
+ def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), alwaysShowUniqueID)
}
trait ScalacPositional {
--
GitLab