diff --git a/library/lang/package.scala b/library/lang/package.scala
index 44351d02ca9328bbbf86063745d233f2db17cd7c..18e1cb6a17861554e221fc781d79a46e5b95f8c2 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -67,5 +67,35 @@ 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/java/leon/codegen/runtime/StrOps.java b/src/main/java/leon/codegen/runtime/StrOps.java
new file mode 100644
index 0000000000000000000000000000000000000000..1e5d7f60d5086dd1a45b4e3e0a52fda11db842a1
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/StrOps.java
@@ -0,0 +1,37 @@
+package leon.codegen.runtime;
+
+public class StrOps {
+ public static String concat(String a, String b) {
+ return a + b;
+ }
+ public static BigInt length(String a) {
+ return new BigInt(String.valueOf(a.length()));
+ }
+ public static String substring (String a, BigInt start, BigInt end) {
+ if(start.greaterEquals(end) || start.greaterEquals(length(a)) || end.lessEquals(new BigInt("0")))
+ return "";
+ else
+ return a.substring(start.underlying().intValue(), end.underlying().intValue());
+ }
+ public static String bigIntToString (BigInt a) {
+ return a.toString();
+ }
+ public static String intToString (int a) {
+ return String.valueOf(a);
+ }
+ public static String doubleToString (double a) {
+ return String.valueOf(a);
+ }
+ public static String booleanToString (boolean a) {
+ if(a)
+ return "true";
+ else
+ return "false";
+ }
+ public static String charToString (char a) {
+ return String.valueOf(a);
+ }
+ public static String realToString (Real a) {
+ return ""; // TODO: Not supported at this moment.
+ }
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 33975a011737d50a45d1511b108d4a2025208eb7..995be0cf939ff2ce5212215513c17a44d1ffcfba 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -61,6 +61,7 @@ trait CodeGeneration {
private[codegen] val JavaListClass = "java/util/List"
private[codegen] val JavaIteratorClass = "java/util/Iterator"
+ private[codegen] val JavaStringClass = "java/lang/String"
private[codegen] val TupleClass = "leon/codegen/runtime/Tuple"
private[codegen] val SetClass = "leon/codegen/runtime/Set"
@@ -77,6 +78,7 @@ trait CodeGeneration {
private[codegen] val GenericValuesClass = "leon/codegen/runtime/GenericValues"
private[codegen] val MonitorClass = "leon/codegen/runtime/LeonCodeGenRuntimeMonitor"
private[codegen] val HenkinClass = "leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor"
+ private[codegen] val StrOpsClass = "leon/codegen/runtime/StrOps"
def idToSafeJVMName(id: Identifier) = {
scala.reflect.NameTransformer.encode(id.uniqueName).replaceAll("\\.", "\\$")
@@ -131,6 +133,9 @@ trait CodeGeneration {
case TypeParameter(_) =>
"L" + ObjectClass + ";"
+
+ case StringType =>
+ "L" + JavaStringClass + ";"
case _ => throw CompilationException("Unsupported type : " + tpe)
}
@@ -564,6 +569,9 @@ trait CodeGeneration {
case UnitLiteral() =>
ch << Ldc(1)
+
+ case StringLiteral(v) =>
+ ch << Ldc(v)
case InfiniteIntegerLiteral(v) =>
ch << New(BigIntClass) << DUP
@@ -888,6 +896,38 @@ trait CodeGeneration {
case f @ Forall(args, body) =>
compileForall(f, ch)
+ // String processing =>
+ case StringConcat(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeStatic(StrOpsClass, "concat", s"(L$JavaStringClass;L$JavaStringClass;)L$JavaStringClass;")
+
+ case StringLength(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "length", s"(L$JavaStringClass;)L$BigIntClass;")
+
+ case Int32ToString(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "intToString", s"(I)L$JavaStringClass;")
+ case BooleanToString(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "booleanToString", s"(z)L$JavaStringClass;")
+ case IntegerToString(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "bigIntToString", s"(L$BigIntClass;)L$JavaStringClass;")
+ case CharToString(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "charToString", s"(C)L$JavaStringClass;")
+ case RealToString(a) =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "realToString", s"(L$RealClass;)L$JavaStringClass;")
+
+ case SubString(a, start, end) =>
+ mkExpr(a, ch)
+ mkExpr(start, ch)
+ mkExpr(end, ch)
+ ch << InvokeStatic(StrOpsClass, "substring", s"(L$JavaStringClass;L$BigIntClass;L$BigIntClass;)L$JavaStringClass;")
+
// Arithmetic
case Plus(l, r) =>
mkExpr(l, ch)
@@ -1217,6 +1257,9 @@ trait CodeGeneration {
case IntegerType =>
ch << CheckCast(BigIntClass)
+ case StringType =>
+ ch << CheckCast(JavaStringClass)
+
case RealType =>
ch << CheckCast(RationalClass)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 69f95f45559737bfd895989aba010dbc0667bb3a..fb060754e55478fe51d275269b1756d849637f6b 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -277,6 +277,9 @@ class CompilationUnit(val ctx: LeonContext,
case (c: java.lang.Character, CharType) =>
CharLiteral(c.toChar)
+ case (c: java.lang.String, StringType) =>
+ StringLiteral(c)
+
case (cc: runtime.CaseClass, ct: ClassType) =>
val fields = cc.productElements()
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 80f71fd87be7f27e1793e13fe38eb09b78f78d62..4471a2eb3047ad1e9dab8ac650fa591886241650 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -279,7 +279,27 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case RealMinus(l,r) =>
e(RealPlus(l, RealUMinus(r)))
-
+
+ case StringConcat(l, r) =>
+ (e(l), e(r)) match {
+ case (StringLiteral(i1), StringLiteral(i2)) => StringLiteral(i1 + i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, StringType))
+ }
+ case StringLength(a) => e(a) match {
+ case StringLiteral(a) => InfiniteIntegerLiteral(a.length)
+ case res => throw EvalError(typeErrorMsg(res, IntegerType))
+ }
+ case SubString(a, start, end) => (e(a), e(start), e(end)) match {
+ case (StringLiteral(a), InfiniteIntegerLiteral(b), InfiniteIntegerLiteral(c)) =>
+ StringLiteral(a.substring(b.toInt, c.toInt))
+ case res => throw EvalError(typeErrorMsg(res._1, StringType))
+ }
+ case Int32ToString(a) => StringLiteral(a.toString)
+ case CharToString(a) => StringLiteral(a.toString)
+ case IntegerToString(a) => StringLiteral(a.toString)
+ case BooleanToString(a) => StringLiteral(a.toString)
+ case RealToString(a) => StringLiteral(a.toString)
+
case BVPlus(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index ea5318e4b96c21bbf2645afd1b791f95a22f9551..1903a0c1f7aab62aee1524078417a5adc1024e2a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1526,14 +1526,14 @@ trait CodeExtraction extends ASTExtractors {
//String methods
case (IsTyped(a1, StringType), "toString", List()) =>
a1
- case (IsTyped(a1, CanHaveStringType(t)), "toString", List()) =>
- ToString(a1)
+ case (IsTyped(a1, WithStringconverter(converter)), "toString", List()) =>
+ converter(a1)
case (IsTyped(a1, StringType), "+", List(IsTyped(a2, StringType))) =>
StringConcat(a1, a2)
- case (IsTyped(a1, StringType), "+", List(IsTyped(a2, CanHaveStringType(t)))) =>
- StringConcat(a1, ToString(a2))
- case (IsTyped(a1, CanHaveStringType(t)), "+", List(IsTyped(a2, StringType))) =>
- StringConcat(ToString(a1), a2)
+ case (IsTyped(a1, StringType), "+", List(IsTyped(a2, WithStringconverter(converter)))) =>
+ StringConcat(a1, converter(a2))
+ case (IsTyped(a1, WithStringconverter(converter)), "+", List(IsTyped(a2, StringType))) =>
+ StringConcat(converter(a1), a2)
case (IsTyped(a1, StringType), "length", List()) =>
StringLength(a1)
case (IsTyped(a1, StringType), "substring", List(IsTyped(start, IntegerType | Int32Type))) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 607f8fe588da87d3cc560f3339432562b1791210..8d6e00ab0271bbbdef497a539ccbce40ac293066 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -547,21 +547,26 @@ object Expressions {
}
}
- /** Returns true if the underlined type can be converted to a String */
- object CanHaveStringType {
- def apply(t: TypeTree): Boolean = t match { case BooleanType | Int32Type | IntegerType | CharType | RealType | StringType => true case _ => false }
- def unapply(t: TypeTree) = if(apply(t)) Some(t) else None
+ abstract class ConverterToString(fromType: TypeTree, toType: TypeTree) extends Expr {
+ def expr: Expr
+ val getType = if(expr.getType == fromType) toType else Untyped
}
/* String Theory */
- /** $encodingof `expr.toString` for strings */
- case class ToString(expr: Expr) extends Expr {
- val getType = if(CanHaveStringType(expr.getType)) StringType else Untyped
- }
+ /** $encodingof `expr.toString` for Int32 to String */
+ case class Int32ToString(expr: Expr) extends ConverterToString(Int32Type, StringType)
+ /** $encodingof `expr.toString` for boolean to String */
+ case class BooleanToString(expr: Expr) extends ConverterToString(BooleanType, StringType)
+ /** $encodingof `expr.toString` for BigInt to String */
+ case class IntegerToString(expr: Expr) extends ConverterToString(IntegerType, StringType)
+ /** $encodingof `expr.toString` for char to String */
+ case class CharToString(expr: Expr) extends ConverterToString(CharType, StringType)
+ /** $encodingof `expr.toString` for real to String */
+ case class RealToString(expr: Expr) extends ConverterToString(RealType, StringType)
/** $encodingof `lhs + rhs` for strings */
case class StringConcat(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
- if (CanHaveStringType(lhs.getType) || CanHaveStringType(rhs.getType)) StringType
+ if (lhs.getType == StringType && rhs.getType == StringType) StringType
else Untyped
}
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 0a6971eb3715aa8e87facf39296c3d73b73630b7..b79602c9ebd65d10e9b5dbda7e157afd915bdbce 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -29,8 +29,16 @@ object Extractors {
Some((Seq(t), (es: Seq[Expr]) => BVNot(es.head)))
case StringLength(t) =>
Some((Seq(t), (es: Seq[Expr]) => StringLength(es.head)))
- case ToString(t) =>
- Some((Seq(t), (es: Seq[Expr]) => ToString(es.head)))
+ case Int32ToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => Int32ToString(es.head)))
+ case BooleanToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => BooleanToString(es.head)))
+ case IntegerToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => IntegerToString(es.head)))
+ case CharToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => CharToString(es.head)))
+ case RealToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => RealToString(es.head)))
case SetCardinality(t) =>
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
@@ -265,6 +273,17 @@ object Extractors {
object IsTyped {
def unapply[T <: Typed](e: T): Option[(T, TypeTree)] = Some((e, e.getType))
}
+
+ object WithStringconverter {
+ def unapply(t: TypeTree): Option[Expr => Expr] = t match {
+ case BooleanType => Some(BooleanToString)
+ case Int32Type => Some(Int32ToString)
+ case IntegerType => Some(IntegerToString)
+ case CharType => Some(CharToString)
+ case RealType => Some(RealToString)
+ case _ => None
+ }
+ }
object FiniteArray {
def unapply(e: Expr): Option[(Map[Int, Expr], Option[Expr], Expr)] = e match {
diff --git a/testcases/stringrender/IntWrapperRender.scala b/testcases/stringrender/IntWrapperRender.scala
index c723e0f5a60172529bf46797ad2f6306c8919010..c760f64e0490d5688f60943e7435d3c04accbfef 100644
--- a/testcases/stringrender/IntWrapperRender.scala
+++ b/testcases/stringrender/IntWrapperRender.scala
@@ -6,7 +6,6 @@
*/
import leon.lang._
-//import string.String
import leon.annotation._
import leon.collection._
import leon.collection.ListOps._