From 32f3a9a0368e13eede06f8debbc7104a42f7dfec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 11 Nov 2015 22:26:54 -0500
Subject: [PATCH] Moved StrOps to its own file. Made StrOps available from the
library.
---
library/lang/StrOps.scala | 42 +++++++++++++++++++++++++
library/lang/package.scala | 31 ------------------
src/main/scala/leon/utils/Library.scala | 3 +-
3 files changed, 44 insertions(+), 32 deletions(-)
create mode 100644 library/lang/StrOps.scala
diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala
new file mode 100644
index 000000000..2c04d5dc7
--- /dev/null
+++ b/library/lang/StrOps.scala
@@ -0,0 +1,42 @@
+package leon.lang
+
+import leon.annotation._
+
+/**
+ * @author Mikael
+ */
+object StrOps {
+ @ignore
+ def concat(a: String, b: String): String = {
+ a + b
+ }
+ @ignore
+ def length(a: String): BigInt = {
+ BigInt(a.length)
+ }
+ @ignore
+ def substring(a: String, start: BigInt, end: BigInt): String = {
+ if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
+ }
+ @ignore
+ def bigIntToString(a: BigInt): String = {
+ a.toString
+ }
+ @ignore
+ def intToString(a: Int): String = {
+ a.toString
+ }
+ @ignore
+ def doubleToString(a: Double): String = {
+ a.toString
+ }
+ def booleanToString(a: Boolean): String = {
+ if(a) "true" else "false"
+ }
+ @ignore
+ def charToString(a: Char): String = {
+ a.toString
+ }
+ @ignore
+ def realToString(a: Real): String = ???
+}
\ No newline at end of file
diff --git a/library/lang/package.scala b/library/lang/package.scala
index 18e1cb6a1..398ae9e36 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -67,35 +67,4 @@ package object lang {
}
}
}
-
- @ignore
- object StrOps {
- def concat(a: String, b: String): String = {
- a + b
- }
- def length(a: String): BigInt = {
- BigInt(a.length)
- }
- def substring(a: String, start: BigInt, end: BigInt): String = {
- if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
- }
- def bigIntToString(a: BigInt): String = {
- a.toString
- }
- def intToString(a: Int): String = {
- a.toString
- }
- def doubleToString(a: Double): String = {
- a.toString
- }
- def booleanToString(a: Boolean): String = {
- if(a) "true" else "false"
- }
- def charToString(a: Char): String = {
- a.toString
- }
- def realToString(a: Real): String = ???
- }
-
-
}
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index ef386d5de..b2c382fd8 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -16,7 +16,8 @@ case class Library(pgm: Program) {
lazy val Some = lookup("leon.lang.Some").collectFirst { case ccd : CaseClassDef => ccd }
lazy val None = lookup("leon.lang.None").collectFirst { case ccd : CaseClassDef => ccd }
- lazy val String = lookup("leon.lang.string.String").collectFirst { case ccd : CaseClassDef => ccd }
+ //lazy val String = lookup("leon.lang.string.String").collectFirst { case ccd : CaseClassDef => ccd }
+ lazy val StrOps = lookup("leon.lang.StrOps").collectFirst { case md: ModuleDef => md }
lazy val Dummy = lookup("leon.lang.Dummy").collectFirst { case ccd : CaseClassDef => ccd }
--
GitLab