From 3bdeeebf2ee248746667bf5043f5e224ec789892 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 28 Aug 2015 15:16:11 +0200
Subject: [PATCH] Identifiers stored in Trees in decoded form
---
src/main/scala/leon/codegen/CodeGeneration.scala | 4 +++-
src/main/scala/leon/purescala/Common.scala | 15 ++++++++++++---
src/main/scala/leon/purescala/Expressions.scala | 1 +
.../scala/leon/purescala/PrettyPrinter.scala | 15 ++-------------
.../verification/case-studies/Robot3po.scala | 16 +++++++---------
5 files changed, 25 insertions(+), 26 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index df3c1c78a..77b34d64e 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -77,7 +77,9 @@ trait CodeGeneration {
private[codegen] val GenericValuesClass = "leon/codegen/runtime/GenericValues"
private[codegen] val MonitorClass = "leon/codegen/runtime/LeonCodeGenRuntimeMonitor"
- def idToSafeJVMName(id: Identifier) = id.uniqueName.replaceAll("\\.", "\\$")
+ def idToSafeJVMName(id: Identifier) = {
+ scala.reflect.NameTransformer.encode(id.uniqueName).replaceAll("\\.", "\\$")
+ }
def defToJVMName(d : Definition) : String = "Leon$CodeGen$" + idToSafeJVMName(d.id)
/** Retrieve the name of the underlying lazy field from a lazy field accessor method */
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 6f738e6b3..4399dc2bf 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -28,7 +28,11 @@ object Common {
}
}
- // the type is left blank (Untyped) for Identifiers that are not variables
+ /** Represents a unique symbol in Leon.
+ *
+ * The name is stored in the decoded (source code) form rather than encoded (JVM) form.
+ * The type may be left blank (Untyped) for Identifiers that are not variables.
+ */
class Identifier private[Common](val name: String, val globalId: Int, val id: Int, val tpe: TypeTree, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
self : Serializable =>
@@ -83,19 +87,24 @@ object Common {
}
object FreshIdentifier {
+
+ // Replace $opcode inside a string with the symbolic operator name
+ private def decode(s: String) =
+ scala.reflect.NameTransformer.decode(s)
+
/** Builds a fresh identifier
* @param name The name of the identifier
* @param tpe The type of the identifier
* @param alwaysShowUniqueID If the unique ID should always be shown */
def apply(name: String, tpe: TypeTree = Untyped, alwaysShowUniqueID: Boolean = false) : Identifier =
- new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe, alwaysShowUniqueID)
+ new Identifier(decode(name), UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe, alwaysShowUniqueID)
/** Builds a fresh identifier, whose ID is always shown
* @param name The name of the identifier
* @param forceId The forced ID of the identifier
* @param tpe The type of the identifier */
def apply(name: String, forceId: Int, tpe: TypeTree): Identifier =
- new Identifier(name, UniqueCounter.nextGlobal, forceId, tpe, true)
+ new Identifier(decode(name), UniqueCounter.nextGlobal, forceId, tpe, true)
}
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 96881669c..1e3722565 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -846,6 +846,7 @@ object Expressions {
/* Special trees for synthesis */
/** $encodingof `choose(pred)`, the non-deterministic choice in Leon.
*
+ * The semantics of this expression is some value
* @note [[pred]] should be a of a [[Types.FunctionType]].
*/
case class Choose(pred: Expr) extends Expr {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 16e361928..0014d3876 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -76,15 +76,7 @@ class PrettyPrinter(opts: PrinterOptions,
} else {
id.toString
}
- val alphaNumDollar = "[\\w\\$]"
- // FIXME this does not account for class names with operator symbols
- def isLegalScalaId(id : String) = id.matches(
- s"$alphaNumDollar+|[$alphaNumDollar+_]?[!@#%^&*+-\\|~/?><:]+"
- )
- // Replace $opname with operator symbols
- val candidate = scala.reflect.NameTransformer.decode(name)
-
- if (isLegalScalaId(candidate)) p"$candidate" else p"$name"
+ p"$name"
case Variable(id) =>
p"$id"
@@ -487,10 +479,7 @@ class PrettyPrinter(opts: PrinterOptions,
}
case fd: FunDef =>
- for(a <- fd.annotations) {
- p"""|@$a
- |"""
- }
+ p"${nary(fd.annotations.toSeq, "\n")}"
if (fd.canBeStrictField) {
p"val ${fd.id} : "
diff --git a/testcases/verification/case-studies/Robot3po.scala b/testcases/verification/case-studies/Robot3po.scala
index c78dc15f2..56709fc55 100644
--- a/testcases/verification/case-studies/Robot3po.scala
+++ b/testcases/verification/case-studies/Robot3po.scala
@@ -661,14 +661,12 @@ object Robot {
hsts: List[HeatSensorTransition],
tts: List[TransmitterTransition]): List[RobotTransition] = {
- ets.flatMap { et =>
- nsts.flatMap { nst =>
- hsts.flatMap { hst =>
- tts.map { tt =>
- RobotTransition(et, nst, hst, tt)
- }
- }
- }
- }
+ for {
+ et <- ets
+ nst <- nsts
+ hst <- hsts
+ tt <- tts
+ } yield RobotTransition(et, nst, hst, tt)
+
}
}
--
GitLab