diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala new file mode 100644 index 0000000000000000000000000000000000000000..2c04d5dc7fc7cede6018c66e10653eef24b9d43e --- /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 18e1cb6a17861554e221fc781d79a46e5b95f8c2..398ae9e36e53c689b69ae4dbda6788d643c25d42 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 ef386d5de05acb264ad9e5db698e0e626cf63ad0..b2c382fd80d2a2a63157e1fb41cb804bbab870cf 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 }