From ac3f4b0425aa5597d7f06acbced237e9619cf923 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 1 Sep 2015 15:08:47 +0200
Subject: [PATCH] Remove traces of identifier encoding
---
src/main/scala/leon/LeonOption.scala | 14 ++++----------
src/main/scala/leon/purescala/DefOps.scala | 2 +-
2 files changed, 5 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index ff68b9e36..57a826d70 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -4,7 +4,7 @@ package leon
import OptionParsers._
-import purescala.Definitions.Program
+import purescala.Definitions._
import purescala.DefOps.fullName
abstract class LeonOptionDef[+A] {
@@ -112,19 +112,15 @@ object OptionsHelpers {
val regexPatterns = patterns map { s =>
import java.util.regex.Pattern
- // We encode the user query, reverting the encoding for . as those are
- // not encoded in our fullnames
- val encoded = scala.reflect.NameTransformer.encode(s).replaceAll("\\$u002E", ".")
-
// wildcards become ".*", rest is quoted.
- var p = encoded.split("_").toList.map(Pattern.quote).mkString(".*")
+ var p = s.split("_").toList.map(Pattern.quote).mkString(".*")
// We account for _ at begining and end
- if (encoded.endsWith("_")) {
+ if (s.endsWith("_")) {
p += ".*"
}
- if (encoded.startsWith("_")) {
+ if (s.startsWith("_")) {
p = ".*"+p
}
@@ -136,8 +132,6 @@ object OptionsHelpers {
{ (name: String) => regexPatterns.exists(p => p.matcher(name).matches()) }
}
- import purescala.Definitions.FunDef
-
def fdMatcher(pgm: Program)(patterns: Traversable[String]): FunDef => Boolean = {
{ (fd: FunDef) => fullName(fd)(pgm) } andThen matcher(patterns)
}
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 2ba4f9221..7a7c6b632 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -160,7 +160,7 @@ object DefOps {
}
private def nameToParts(name: String) = {
- name.split("\\.").toList map scala.reflect.NameTransformer.encode
+ name.split("\\.").toList
}
def searchWithin(name: String, within: Definition): Seq[Definition] = {
--
GitLab