diff --git a/library/lang/string/String.scala b/library/lang/string/String.scala deleted file mode 100644 index 0a3e72bd1a6f234a79eba234a646b2c0844ecfaf..0000000000000000000000000000000000000000 --- a/library/lang/string/String.scala +++ /dev/null @@ -1,28 +0,0 @@ -/* Copyright 2009-2015 EPFL, Lausanne */ - -package leon.lang.string - -import leon.annotation._ -import leon.collection._ - -@library -case class String(chars: List[Char]) { - def +(that: String): String = { - String(this.chars ++ that.chars) - } - - def size = chars.size - - def length = size - - @ignore - override def toString = { - - "\""+charsToString(chars)+"\"" - } - @ignore - def charsToString(chars: List[Char]): java.lang.String = chars match { - case Cons(h, t) => h + charsToString(t) - case Nil() => "" - } -} diff --git a/library/lang/string/package.scala b/library/lang/string/package.scala deleted file mode 100644 index d931debe7c587f966aadd30b2860b1793c6ad431..0000000000000000000000000000000000000000 --- a/library/lang/string/package.scala +++ /dev/null @@ -1,24 +0,0 @@ -/* Copyright 2009-2015 EPFL, Lausanne */ - -package leon.lang - -import leon.annotation._ -import leon.collection._ -import scala.language.implicitConversions - -import scala.collection.immutable.{List => ScalaList} - -package object string { - /*@ignore - implicit def strToStr(s: java.lang.String): leon.lang.string.String = { - String(listToList(s.toList)) - }*/ - - @ignore - def listToList[A](s: ScalaList[A]): List[A] = s match { - case scala.::(h, t) => - Cons(h, listToList(t)) - case _ => - Nil[A]() - } -} diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala index 4d100210911734504a96bd005d0299ae0f1b8906..0ddd21078ffe772986bd5487d964d352184cd2e6 100644 --- a/src/main/scala/leon/utils/Library.scala +++ b/src/main/scala/leon/utils/Library.scala @@ -16,7 +16,6 @@ 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 StrOps = lookup("leon.lang.StrOps").collectFirst { case md: ModuleDef => md } lazy val Dummy = lookup("leon.lang.Dummy").collectFirst { case ccd : CaseClassDef => ccd } diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala index d64df7f8c43b1f5f77bb93bce85d8a69cbf230ed..7c0d3e13c044f4cd2491041cf28319986a6df42b 100644 --- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala +++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala @@ -199,7 +199,6 @@ class StringSolverSuite extends FunSuite with Matchers with ScalaFutures { val solution = solve(problem) solution should not be 'empty val firstSolution = solution(0) - println("First solution " + firstSolution) firstSolution(idMap("const8")) should equal("List(") firstSolution(idMap("const4")) should equal("") } @@ -216,7 +215,6 @@ T2: internal T2: ret Pop() -> 5""" val problem: Problem = List(lhs === expected) - println("Problem to solve:" + StringSolver.renderProblem(problem)) solve(problem) should not be 'empty } diff --git a/testcases/verification/case-studies/LambdaSound.scala b/testcases/verification/case-studies/LambdaSound.scala index 6208d2039eaf16ba1dbeae614bf6432e2309ee1e..fa59efbc001614acbd338b83883248d07a736a2d 100644 --- a/testcases/verification/case-studies/LambdaSound.scala +++ b/testcases/verification/case-studies/LambdaSound.scala @@ -3,7 +3,6 @@ import leon.annotation._ import leon.collection._ import leon.lang.synthesis._ import leon._ -import leon.lang.string._ object Lambda { case class Id(v: BigInt) diff --git a/testcases/verification/editor/AsciiToPos.scala b/testcases/verification/editor/AsciiToPos.scala index 4ec536ce71c8f684dc1a2329c51de19cf575269f..9035ab5a00dc303c5318cd8147da9fa73f241c51 100644 --- a/testcases/verification/editor/AsciiToPos.scala +++ b/testcases/verification/editor/AsciiToPos.scala @@ -1,6 +1,5 @@ import leon.lang._ import leon.lang.synthesis._ -import leon.lang.string._ import leon.collection._ object Justify { diff --git a/testcases/verification/higher-order/valid/MonadsException.scala b/testcases/verification/higher-order/valid/MonadsException.scala index 2c80332435b1fb65653932fb93906d6540685e13..27c87d26177ef8c0d42f49766ab56a2c1e68b13c 100644 --- a/testcases/verification/higher-order/valid/MonadsException.scala +++ b/testcases/verification/higher-order/valid/MonadsException.scala @@ -1,5 +1,4 @@ import leon.lang._ -import leon.lang.string._ object TryMonad { diff --git a/testcases/verification/monads/Freshen.scala b/testcases/verification/monads/Freshen.scala index de8c7eda592ba211a948c4beb5f2925d6a53974f..6fe0ef38f7e673f4e0f9ffbee8bbf0e7e7a5eafa 100644 --- a/testcases/verification/monads/Freshen.scala +++ b/testcases/verification/monads/Freshen.scala @@ -6,7 +6,6 @@ import leon.lang._ object Freshen { import State._ - import leon.lang.string._ case class Id(name: String, id: BigInt) diff --git a/testcases/web/demos/005_Tutorial-Monad.scala b/testcases/web/demos/005_Tutorial-Monad.scala index 093e4a2d805a9e8e3ee07dc79eb1adfecc81acdb..ba08a0e1f3f18af7c954c2a06b7c06cc26522369 100644 --- a/testcases/web/demos/005_Tutorial-Monad.scala +++ b/testcases/web/demos/005_Tutorial-Monad.scala @@ -1,4 +1,3 @@ -import leon.lang.string._ import leon.annotation._ sealed abstract class Outcome[T] {