From e676355ae26629d272b278fde02409fbcdf331f2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Fri, 6 Feb 2015 19:39:54 +0100
Subject: [PATCH] Yay
---
runTests.sh | 10 +-
src/main/scala/leon/repair/RepairResult.scala | 2 +-
testcases/repair/Compiler/Compiler.scala | 212 +++++++++++++++++
testcases/repair/Compiler/Compiler1.scala | 176 ++++++++++++++
testcases/repair/Compiler/Compiler2.scala | 175 ++++++++++++++
testcases/repair/Compiler/Compiler3.scala | 173 ++++++++++++++
testcases/repair/Compiler/Compiler4.scala | 172 ++++++++++++++
testcases/repair/Compiler/Compiler5.scala | 212 +++++++++++++++++
testcases/repair/Compiler/Compiler6.scala | 214 ++++++++++++++++++
.../repair/evaluation/Desugar/Desugar1.scala | 1 -
.../repair/evaluation/Desugar/Desugar2.scala | 1 -
.../repair/evaluation/Desugar/Desugar3.scala | 1 -
.../repair/evaluation/Desugar/Desugar4.scala | 1 -
.../evaluation/HeapSort/HeapSort3.scala | 1 -
.../evaluation/HeapSort/HeapSort4.scala | 1 -
.../evaluation/HeapSort/HeapSort5.scala | 1 -
.../evaluation/HeapSort/HeapSort6.scala | 1 -
.../evaluation/HeapSort/HeapSort7.scala | 1 -
.../evaluation/HeapSort/HeapSort8.scala | 1 -
.../evaluation/HeapSort/HeapSort9.scala | 1 -
testcases/repair/evaluation/List/List1.scala | 1 -
testcases/repair/evaluation/List/List10.scala | 1 -
testcases/repair/evaluation/List/List11.scala | 1 -
testcases/repair/evaluation/List/List2.scala | 1 -
testcases/repair/evaluation/List/List3.scala | 1 -
testcases/repair/evaluation/List/List5.scala | 1 -
testcases/repair/evaluation/List/List6.scala | 1 -
testcases/repair/evaluation/List/List7.scala | 1 -
testcases/repair/evaluation/List/List8.scala | 1 -
testcases/repair/evaluation/List/List9.scala | 1 -
.../evaluation/PropLogic/PropLogic1.scala | 1 -
.../evaluation/PropLogic/PropLogic2.scala | 1 -
.../evaluation/PropLogic/PropLogic3.scala | 1 -
.../evaluation/PropLogic/PropLogic4.scala | 1 -
.../evaluation/PropLogic/PropLogic5.scala | 1 -
35 files changed, 1341 insertions(+), 31 deletions(-)
create mode 100644 testcases/repair/Compiler/Compiler.scala
create mode 100644 testcases/repair/Compiler/Compiler1.scala
create mode 100644 testcases/repair/Compiler/Compiler2.scala
create mode 100644 testcases/repair/Compiler/Compiler3.scala
create mode 100644 testcases/repair/Compiler/Compiler4.scala
create mode 100644 testcases/repair/Compiler/Compiler5.scala
create mode 100644 testcases/repair/Compiler/Compiler6.scala
delete mode 120000 testcases/repair/evaluation/Desugar/Desugar1.scala
delete mode 120000 testcases/repair/evaluation/Desugar/Desugar2.scala
delete mode 120000 testcases/repair/evaluation/Desugar/Desugar3.scala
delete mode 120000 testcases/repair/evaluation/Desugar/Desugar4.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort3.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort4.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort5.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort6.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort7.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort8.scala
delete mode 120000 testcases/repair/evaluation/HeapSort/HeapSort9.scala
delete mode 120000 testcases/repair/evaluation/List/List1.scala
delete mode 120000 testcases/repair/evaluation/List/List10.scala
delete mode 120000 testcases/repair/evaluation/List/List11.scala
delete mode 120000 testcases/repair/evaluation/List/List2.scala
delete mode 120000 testcases/repair/evaluation/List/List3.scala
delete mode 120000 testcases/repair/evaluation/List/List5.scala
delete mode 120000 testcases/repair/evaluation/List/List6.scala
delete mode 120000 testcases/repair/evaluation/List/List7.scala
delete mode 120000 testcases/repair/evaluation/List/List8.scala
delete mode 120000 testcases/repair/evaluation/List/List9.scala
delete mode 120000 testcases/repair/evaluation/PropLogic/PropLogic1.scala
delete mode 120000 testcases/repair/evaluation/PropLogic/PropLogic2.scala
delete mode 120000 testcases/repair/evaluation/PropLogic/PropLogic3.scala
delete mode 120000 testcases/repair/evaluation/PropLogic/PropLogic4.scala
delete mode 120000 testcases/repair/evaluation/PropLogic/PropLogic5.scala
diff --git a/runTests.sh b/runTests.sh
index edf8d289c..938f44ba3 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -15,10 +15,12 @@ echo "################################" >> $summaryLog
echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala | tee -a $fullLog
diff --git a/src/main/scala/leon/repair/RepairResult.scala b/src/main/scala/leon/repair/RepairResult.scala
index 85dc7a5d5..697434d6f 100644
--- a/src/main/scala/leon/repair/RepairResult.scala
+++ b/src/main/scala/leon/repair/RepairResult.scala
@@ -23,7 +23,7 @@ case class RepairResult(f: File,
}
def toTableLine = {
- val benchCat = f.getParentFile().getName()
+ val benchCat = f.getAbsoluteFile().getParentFile().getName()
val benchName = f.getName()
val benchFun = name
diff --git a/testcases/repair/Compiler/Compiler.scala b/testcases/repair/Compiler/Compiler.scala
new file mode 100644
index 000000000..697f333e0
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler.scala
@@ -0,0 +1,212 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(true)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e)
+ }
+}
diff --git a/testcases/repair/Compiler/Compiler1.scala b/testcases/repair/Compiler/Compiler1.scala
new file mode 100644
index 000000000..2971855c7
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler1.scala
@@ -0,0 +1,176 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it, uses example...
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ ((e, res) passes {
+ case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(42))) =>
+ Plus(Literal(i), Plus(Literal(j), Neg(Literal(42))))
+ }) &&
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler2.scala b/testcases/repair/Compiler/Compiler2.scala
new file mode 100644
index 000000000..a068dadcb
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler2.scala
@@ -0,0 +1,175 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Literal(0)//Plus(desugar(lhs), desugar(rhs)) // FIXME forgot Neg
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e) && ((e,res) passes {
+ case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ })
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler3.scala b/testcases/repair/Compiler/Compiler3.scala
new file mode 100644
index 000000000..ec61a78a5
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler3.scala
@@ -0,0 +1,173 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ // FIXME switched the branches
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(els), desugar(thn))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
new file mode 100644
index 000000000..9f6ac963a
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -0,0 +1,172 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME else should be 0
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler5.scala b/testcases/repair/Compiler/Compiler5.scala
new file mode 100644
index 000000000..95003d1af
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler5.scala
@@ -0,0 +1,212 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(true)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a-b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e)
+ }
+}
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
new file mode 100644
index 000000000..0e6364fc5
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -0,0 +1,214 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(false)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e) && ((e, res) passes {
+ case Or(BoolLiteral(true), e) => BoolLiteral(true)
+ })
+ }
+}
diff --git a/testcases/repair/evaluation/Desugar/Desugar1.scala b/testcases/repair/evaluation/Desugar/Desugar1.scala
deleted file mode 120000
index c97e24b0f..000000000
--- a/testcases/repair/evaluation/Desugar/Desugar1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar2.scala b/testcases/repair/evaluation/Desugar/Desugar2.scala
deleted file mode 120000
index 17e99298c..000000000
--- a/testcases/repair/evaluation/Desugar/Desugar2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar3.scala b/testcases/repair/evaluation/Desugar/Desugar3.scala
deleted file mode 120000
index 4ad63dd72..000000000
--- a/testcases/repair/evaluation/Desugar/Desugar3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar4.scala b/testcases/repair/evaluation/Desugar/Desugar4.scala
deleted file mode 120000
index 2a5a9746e..000000000
--- a/testcases/repair/evaluation/Desugar/Desugar4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort3.scala b/testcases/repair/evaluation/HeapSort/HeapSort3.scala
deleted file mode 120000
index efbc7141e..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort4.scala b/testcases/repair/evaluation/HeapSort/HeapSort4.scala
deleted file mode 120000
index 86163bbc1..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort5.scala b/testcases/repair/evaluation/HeapSort/HeapSort5.scala
deleted file mode 120000
index 3069a2f6a..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort5.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort6.scala b/testcases/repair/evaluation/HeapSort/HeapSort6.scala
deleted file mode 120000
index 0046983b5..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort6.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort6.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort7.scala b/testcases/repair/evaluation/HeapSort/HeapSort7.scala
deleted file mode 120000
index 22dfaedb6..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort7.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort7.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort8.scala b/testcases/repair/evaluation/HeapSort/HeapSort8.scala
deleted file mode 120000
index 2a3343c9a..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort8.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort8.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort9.scala b/testcases/repair/evaluation/HeapSort/HeapSort9.scala
deleted file mode 120000
index 1bb14b50d..000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort9.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort9.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List1.scala b/testcases/repair/evaluation/List/List1.scala
deleted file mode 120000
index 88b9348e0..000000000
--- a/testcases/repair/evaluation/List/List1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List10.scala b/testcases/repair/evaluation/List/List10.scala
deleted file mode 120000
index 6769b7510..000000000
--- a/testcases/repair/evaluation/List/List10.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List10.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List11.scala b/testcases/repair/evaluation/List/List11.scala
deleted file mode 120000
index 2b1bc3b51..000000000
--- a/testcases/repair/evaluation/List/List11.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List11.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List2.scala b/testcases/repair/evaluation/List/List2.scala
deleted file mode 120000
index 5d3bdd5ef..000000000
--- a/testcases/repair/evaluation/List/List2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List3.scala b/testcases/repair/evaluation/List/List3.scala
deleted file mode 120000
index deed1959e..000000000
--- a/testcases/repair/evaluation/List/List3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List5.scala b/testcases/repair/evaluation/List/List5.scala
deleted file mode 120000
index a93655c2f..000000000
--- a/testcases/repair/evaluation/List/List5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List5.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List6.scala b/testcases/repair/evaluation/List/List6.scala
deleted file mode 120000
index bd461d2f6..000000000
--- a/testcases/repair/evaluation/List/List6.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List6.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List7.scala b/testcases/repair/evaluation/List/List7.scala
deleted file mode 120000
index e7120d71a..000000000
--- a/testcases/repair/evaluation/List/List7.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List7.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List8.scala b/testcases/repair/evaluation/List/List8.scala
deleted file mode 120000
index 6b3956d4e..000000000
--- a/testcases/repair/evaluation/List/List8.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List8.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List9.scala b/testcases/repair/evaluation/List/List9.scala
deleted file mode 120000
index 37b271671..000000000
--- a/testcases/repair/evaluation/List/List9.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List9.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic1.scala b/testcases/repair/evaluation/PropLogic/PropLogic1.scala
deleted file mode 120000
index 2b22c7ffd..000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic2.scala b/testcases/repair/evaluation/PropLogic/PropLogic2.scala
deleted file mode 120000
index b77428fee..000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic3.scala b/testcases/repair/evaluation/PropLogic/PropLogic3.scala
deleted file mode 120000
index c7e74b502..000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic4.scala b/testcases/repair/evaluation/PropLogic/PropLogic4.scala
deleted file mode 120000
index fb6548bf1..000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic5.scala b/testcases/repair/evaluation/PropLogic/PropLogic5.scala
deleted file mode 120000
index 2d17e3dc0..000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic5.scala
\ No newline at end of file
--
GitLab