diff --git a/.gitignore b/.gitignore
index 1005f6f1ecd698c1c1e9ae945b1afd1ad3845c78..bafda3ab2c3d6dea79a0b7cdf7479a1ed0c10195 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,7 @@
-bin
*.swp
+bin
+leon
+project/boot
+project/build
+project/target
+target
diff --git a/PERMISSIONS b/PERMISSIONS
index d64302cc67ed57f9a103cdc5b149fc74d3142a0d..0fe05bfa0d1f347b99a98acfc140782faebba141 100755
--- a/PERMISSIONS
+++ b/PERMISSIONS
@@ -5,12 +5,12 @@
#
# The creator of this repository is psuter.
-thisrepo="projects/leon-kaplan"
+thisrepo="projects/leon-2.0"
tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
exit $_
# **Do not** add new lines after the following two!
-WRITERS kuncak psuter koeksal rblanc
-READERS megard @lara
+WRITERS kuncak psuter rblanc
+READERS @lara
diff --git a/build.sbt b/build.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..908d231bc6bb940904d7a957c2187892f11ac649
--- /dev/null
+++ b/build.sbt
@@ -0,0 +1,16 @@
+name := "Leon"
+
+version := "2.0"
+
+organization := "ch.epfl.lara"
+
+scalaVersion := "2.9.0-1"
+
+scalacOptions += "-deprecation"
+
+scalacOptions += "-unchecked"
+
+libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.0-1"
+
+unmanagedBase <<= baseDirectory { base => base / "unmanaged" }
+
diff --git a/demo/AssociativeList.scala b/demo/AssociativeList.scala
deleted file mode 100644
index dc56e8fd4eb2c28c216e7191990a31084c5ec89a..0000000000000000000000000000000000000000
--- a/demo/AssociativeList.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
-
-object AssociativeList {
- sealed abstract class KeyValuePairAbs
- case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
-
- sealed abstract class List
- case class Cons(head: KeyValuePairAbs, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class OptionInt
- case class Some(i: Int) extends OptionInt
- case class None() extends OptionInt
-
- def domain(l: List): Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
- }
-
- def find(l: List, e: Int): OptionInt = l match {
- case Nil() => None()
- case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
- }
-
- def noDuplicates(l: List): Boolean = l match {
- case Nil() => true
- case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
- }
-
- def update(l1: List, l2: List): List = (l2 match {
- case Nil() => l1
- case Cons(x, xs) => update(updateElem(l1, x), xs)
- }) ensuring(domain(_) == domain(l1) ++ domain(l2))
-
- def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
- case Nil() => Cons(e, Nil())
- case Cons(KeyValuePair(k, v), xs) => e match {
- case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
- }
- }) ensuring(res => e match {
- case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
- })
-
- @induct
- def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
- find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
- } holds
-}
diff --git a/demo/AssociativeListReloaded.scala b/demo/AssociativeListReloaded.scala
deleted file mode 100644
index a8ea94c725fc41f0e5ca375970b56b38b9cede2b..0000000000000000000000000000000000000000
--- a/demo/AssociativeListReloaded.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-import funcheck.Utils._
-import funcheck.Annotations._
-
-object AssociativeList {
- sealed abstract class KeyValuePairAbs
- case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
-
- sealed abstract class List
- case class Cons(head: KeyValuePairAbs, tail: List) extends List
- case class Nil() extends List
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def asMap(l : List) : Map[Int,Int] = (l match {
- case Nil() => Map.empty[Int,Int]
- case Cons(KeyValuePair(k,v), t) => asMap(t).updated(k, v)
- })
-
- sealed abstract class OptionInt
- case class Some(i: Int) extends OptionInt
- case class None() extends OptionInt
-
- def domain(l: List): Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
- }
-
- def find(l: List, k0: Int): OptionInt = (l match {
- case Nil() => None()
- case Cons(KeyValuePair(k, v), xs) => if (k == k0) Some(v) else find(xs, k0)
- }) ensuring(res => res match {
- case None() => !asMap(l).isDefinedAt(k0)
- case Some(v) => asMap(l).isDefinedAt(k0) && asMap(l)(k0) == v
- })
-
- def noDuplicates(l: List): Boolean = l match {
- case Nil() => true
- case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
- }
-
-// @induct
- def updateElem(l: List, k0: Int, v0: Int): List = (l match {
- case Nil() => Cons(KeyValuePair(k0, v0), Nil())
- case Cons(KeyValuePair(k, v), xs) => if(k0 == k) Cons(KeyValuePair(k0, v0), xs) else Cons(KeyValuePair(k, v), updateElem(xs, k0, v0))
- }) ensuring(res => {
- asMap(res).isDefinedAt(k0) && asMap(res)(k0) == v0
- })
-
- @induct
- def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
- find(updateElem(l, k2, e), k1) == (if (k1 == k2) Some(e) else find(l, k1))
- } holds
-
- def prop1(l : List) : Boolean = {
- (l == Nil()) == (asMap(l) == Map.empty[Int,Int])
- } holds
-
- def weird(m : Map[Int,Int], k : Int, v : Int) : Boolean = {
- m(k) == v && !m.isDefinedAt(k)
- // m.isDefinedAt(k) || !(m(k) == v)
- } ensuring(res => !res)
-
- // def prop0(l : List, m : Map[Int,Int]) : Boolean = {
- // size(l) > 4 && asMap(l) == m
- // } ensuring(res => !res)
-}
diff --git a/demo/Functions.scala b/demo/Functions.scala
deleted file mode 100644
index 7c666b772cb56884543b38d924511274e19a8bb5..0000000000000000000000000000000000000000
--- a/demo/Functions.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-import funcheck.Annotations._
-import funcheck.Utils._
-
-object Functions {
- def someFunction(f : Int => Int, a : Int) : Boolean = {
- f(a) != a + 5
- } holds
-
- def conditional(a : Int, f : Int => Int, h : Int => Int) : Boolean = {
- val g = if (a > 5) f else h
- (f(a) == 42 && h(a) == 42) || h(a + 1) == 43
- } holds
-
- def plus42(a : Int) : Int = a + 42
-
- def usesSpecFun(a : Int) : Boolean = {
- someFunction(plus42, a)
- }
-}
diff --git a/demo/InsertionSort.scala b/demo/InsertionSort.scala
deleted file mode 100644
index 8fbeaa447fe506f19f1a8e5d33358a4a062802fa..0000000000000000000000000000000000000000
--- a/demo/InsertionSort.scala
+++ /dev/null
@@ -1,99 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- sealed abstract class OptInt
- case class Some(value: Int) extends OptInt
- case class None() extends OptInt
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def min(l : List) : OptInt = l match {
- case Nil() => None()
- case Cons(x, xs) => min(xs) match {
- case None() => Some(x)
- case Some(x2) => if(x < x2) Some(x) else Some(x2)
- }
- }
-
- // def minProp0(l : List) : Boolean = (l match {
- // case Nil() => true
- // case c @ Cons(x, xs) => min(c) match {
- // case None() => false
- // case Some(m) => x >= m
- // }
- // }) holds
-
- // def minProp1(l : List) : Boolean = {
- // require(isSorted(l) && size(l) <= 5)
- // l match {
- // case Nil() => true
- // case c @ Cons(x, xs) => min(c) match {
- // case None() => false
- // case Some(m) => x == m
- // }
- // }
- // } holds
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def buggySortedIns(e: Int, l: List): List = {
- // require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
- && isSorted(res)
- && size(res) == size(l)
- )
-
- def main(args: Array[String]): Unit = {
- val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
-
- println(ls)
- println(sort(ls))
- }
-}
diff --git a/demo/ListOperations.scala b/demo/ListOperations.scala
deleted file mode 100644
index 2c9b4a3d31bfaeebaaaf5f139e517fc377746b8d..0000000000000000000000000000000000000000
--- a/demo/ListOperations.scala
+++ /dev/null
@@ -1,169 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class IntPairList
- case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
- case class IPNil() extends IntPairList
-
- sealed abstract class IntPair
- case class IP(fst: Int, snd: Int) extends IntPair
-
- def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
-
- def iplSize(l: IntPairList) : Int = (l match {
- case IPNil() => 0
- case IPCons(_, xs) => 1 + iplSize(xs)
- }) ensuring(_ >= 0)
-
- def zip(l1: List, l2: List) : IntPairList = {
- // try to comment this and see how pattern-matching becomes
- // non-exhaustive and post-condition fails
- require(size(l1) == size(l2))
-
- l1 match {
- case Nil() => IPNil()
- case Cons(x, xs) => l2 match {
- case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
- }
- }
- } ensuring(iplSize(_) == size(l1))
-
- def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: Int) : Int = {
- require(acc >= 0)
- l match {
- case Nil() => acc
- case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
- }
- } ensuring(res => res == size(l) + acc)
-
- def sizesAreEquiv(l: List) : Boolean = {
- size(l) == sizeTailRec(l)
- } holds
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- def sizeAndContent(l: List) : Boolean = {
- size(l) == 0 || content(l) != Set.empty[Int]
- } holds
-
- def drunk(l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
- }) ensuring (size(_) == 2 * size(l))
-
- def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
- def reverse0(l1: List, l2: List) : List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverse0(xs, Cons(x, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- def append(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, append(xs, l2))
- }) // ensuring(content(_) == content(l1) ++ content(l2))
-
- def map(f : Int => Int, l : List) : List = l match {
- case Nil() => Nil()
- case Cons(x, xs) => Cons(f(x), map(f, xs))
- }
-
- def definedForAll(m: Map[Int,Int], l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, xs) => m.isDefinedAt(x) && definedForAll(m, xs)
- }
-
- def map2(m : Map[Int,Int], l : List) : List = {
- //require(definedForAll(m, l))
- l match {
- case Nil() => Nil()
- case Cons(x, xs) => Cons(m(x), map2(m, xs))
- }
- }
-
- @induct
- def appendMapCommute(l1 : List, l2 : List, f : Int => Int) : Boolean = {
- map(f, append(l1, l2)) == append(map(f, l1), map(f, l2))
- } holds
-
- @induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
-
- // @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
-
- def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
- (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
- } holds
-
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
-
- @induct
- def concat(l1: List, l2: List) : List =
- concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
- case Nil() => l2 match {
- case Nil() => reverse(l3)
- case Cons(y, ys) => {
- concat0(Nil(), ys, Cons(y, l3))
- }
- }
- case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
- }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
-
- def curiousAndWrongMap(f : Int => Int, l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => Cons(f(x), map(f, xs))
- }) ensuring(res => res == l)
-
- def rev(l: List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => append(rev(xs), Cons(x, Nil()))
- })
-
- // @induct
- // def rev_app(xs: List, ys: List): Boolean = {
- // rev(append(xs, ys)) == append(rev(ys), rev(xs))
- // } ensuring (x => appendAssoc(xs, ys) && nilAppend(xs) && nilAppend(ys) && x)
-
- // def rev_app(xs: List, ys: List) : Boolean {
- //
- // }
- /* TO TRY OUT */
- /*
- lemma app_Nil2 [simp]: "xs @ [] = xs"
- apply(induct_tac xs)
- apply(auto)
- done
- lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
- apply(induct_tac xs)
- apply(auto)
- done
- lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
- apply(induct_tac xs)
- apply(auto)
- done
- theorem rev_rev [simp]: "rev(rev xs) = xs"
- apply(induct_tac xs)
- apply(auto)
- done
- end
- */
-}
diff --git a/demo/Maps.scala b/demo/Maps.scala
deleted file mode 100644
index 437811694f7f569ff01302f99ebf320f799a7a7e..0000000000000000000000000000000000000000
--- a/demo/Maps.scala
+++ /dev/null
@@ -1,41 +0,0 @@
-// import scala.collection.immutable.Set
-// import scala.collection.immutable.Map
-import funcheck.Utils._
-import funcheck.Annotations._
-
-object Maps {
-
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- def applyTest(m : Map[Int,Int], i : Int) : Int = m(i)
-
- def isDefinedAtTest(m : Map[Int,Int], i : Int) : Boolean = m.isDefinedAt(i)
-
- def emptyTest() : Map[Int,Int] = Map.empty[Int,Int]
-
- def updatedTest(m : Map[Int,Int]) : Map[Int,Int] = m.updated(1, 2)
-
- def useCase(map : Map[Int,Int], k : Int, v : Int) : Boolean = {
- val map2 = map.updated(k, v)
- map2.isDefinedAt(k)
- } holds
-
- def useCase2(map : Map[Int,Int], k : Int, v : Int) : Map[Int,Int] = {
- val map2 = map.updated(k, v)
- map2
- } ensuring (res => res.isDefinedAt(k))
-
- def readOverWrite(m : Map[Int,Int], k1 : Int, k2 : Int, e : Int) : Boolean = {
- val newM = m.updated(k2, e)
- if (m.isDefinedAt(k1))
- newM(k1) == (if (k1 == k2) e else m(k1))
- else
- true
- } holds
-
- def findModel(m : Map[Int,List]) : Boolean = {
- m == Map.empty[Int,List].updated(42, Nil()) || m == Map.empty[Int, List]
- } holds
-}
diff --git a/demo/PropositionalLogic.scala b/demo/PropositionalLogic.scala
deleted file mode 100644
index c6928de10d13ebcd7fe6ce4307ae4139d2d63d25..0000000000000000000000000000000000000000
--- a/demo/PropositionalLogic.scala
+++ /dev/null
@@ -1,86 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
-
-object PropositionalLogic {
-
- sealed abstract class Formula
- case class And(lhs: Formula, rhs: Formula) extends Formula
- case class Or(lhs: Formula, rhs: Formula) extends Formula
- case class Implies(lhs: Formula, rhs: Formula) extends Formula
- case class Not(f: Formula) extends Formula
- case class Literal(id: Int) extends Formula
-
- def simplify(f: Formula): Formula = (f match {
- case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
- case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
- case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
- case Not(f) => Not(simplify(f))
- case Literal(_) => f
- }) ensuring(isSimplified(_))
-
- def isSimplified(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Implies(_,_) => false
- case Not(f) => isSimplified(f)
- case Literal(_) => true
- }
-
- def nnf(formula: Formula): Formula = (formula match {
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
- case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
- case Not(Not(f)) => nnf(f)
- case Not(Literal(_)) => formula
- case Literal(_) => formula
- }) ensuring(isNNF(_))
-
- def isNNF(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Not(Literal(_)) => true
- case Not(_) => false
- case Literal(_) => true
- }
-
- def vars(f: Formula): Set[Int] = {
- require(isNNF(f))
- f match {
- case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Not(Literal(i)) => Set[Int](i)
- case Literal(i) => Set[Int](i)
- }
- }
-
- def fv(f : Formula) = { vars(nnf(f)) }
-
- @induct
- def wrongCommutative(f: Formula) : Boolean = {
- nnf(simplify(f)) == simplify(nnf(f))
- } holds
-
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
- require(isNNF(f))
- isNNF(simplify(f))
- } holds
-
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- } holds
-
- @induct
- def simplifyIsStable(f: Formula) : Boolean = {
- require(isSimplified(f))
- simplify(f) == f
- } holds
-}
diff --git a/demo/RBTO.scala b/demo/RBTO.scala
deleted file mode 100644
index c278fe57979a495fbaf92edab3301067dd6388da..0000000000000000000000000000000000000000
--- a/demo/RBTO.scala
+++ /dev/null
@@ -1,129 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
-
-object RedBlackTree {
- sealed abstract class Color
- case class Red() extends Color
- case class Black() extends Color
-
- sealed abstract class Tree
- case class Empty() extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
-
- sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
- case class None() extends OptionInt
-
- def content(t: Tree) : Set[Int] = t match {
- case Empty() => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
-
- def size(t: Tree) : Int = t match {
- case Empty() => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
-
- /* We consider leaves to be black by definition */
- def isBlack(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(),_,_,_) => true
- case _ => false
- }
-
- def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
- case Empty() => true
- }
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty() => 1
- case Node(Black(), l, _, _) => blackHeight(l) + 1
- case Node(Red(), l, _, _) => blackHeight(l)
- }
-
- // <<insert element x into the tree t>>
- def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) && orderedKeys(t))
- t match {
- case Empty() => Node(Red(),Empty(),x,Empty())
- case Node(c,a,y,b) =>
- if (x < y) balance(c, ins(x, a), y, b)
- else if (x == y) Node(c,a,y,b)
- else balance(c,a,y,ins(x, b))
- }
- } ensuring (res => content(res) == content(t) ++ Set(x)
- && size(t) <= size(res) && size(res) <= size(t) + 1
- && redDescHaveBlackChildren(res)
- && blackBalanced(res)
- && orderedKeys(res)
- )
-
- def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) && orderedKeys(n))
- n match {
- case Node(Red(),l,v,r) => Node(Black(),l,v,r)
- case _ => n
- }
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) && orderedKeys(res))
-
- def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) && orderedKeys(t))
- makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) && orderedKeys(res))
-
- def buggyAdd(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t))
- makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
-
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- require(orderedKeys(a, None(), Some(x)) && orderedKeys(b, Some(x), None()))
- Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(c,a,xV,b) => Node(c,a,xV,b)
- }
- } ensuring (res => content(res) == content(Node(c,a,x,b)) && orderedKeys(res))
-
- def orderedKeys(t : Tree) : Boolean = orderedKeys(t, None(), None())
-
- def orderedKeys(t : Tree, min : OptionInt, max : OptionInt) : Boolean = (t match {
- case Empty() => true
- case Node(c,a,v,b) =>
- val minOK =
- min match {
- case Some(minVal) =>
- v > minVal
- case None() => true
- }
- val maxOK =
- max match {
- case Some(maxVal) =>
- v < maxVal
- case None() => true
- }
- minOK && maxOK && orderedKeys(a, min, Some(v)) && orderedKeys(b, Some(v), max)
- }) ensuring(res => if(!res) true else (t match {
- case Node(_, a, v, b) => orderedKeys(a, None(), Some(v)) && orderedKeys(b, Some(v), None())
- case _ => true
- }))
-}
diff --git a/demo/RedBlackTree.scala b/demo/RedBlackTree.scala
deleted file mode 100644
index 3a1d768b013ef495b69acb95582d61581344bfe1..0000000000000000000000000000000000000000
--- a/demo/RedBlackTree.scala
+++ /dev/null
@@ -1,117 +0,0 @@
-import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
-
-object RedBlackTree {
- sealed abstract class Color
- case class Red() extends Color
- case class Black() extends Color
-
- sealed abstract class Tree
- case class Empty() extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
-
- sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
- case class None() extends OptionInt
-
- def content(t: Tree) : Set[Int] = t match {
- case Empty() => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
-
- def size(t: Tree) : Int = t match {
- case Empty() => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
-
- /* We consider leaves to be black by definition */
- def isBlack(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(),_,_,_) => true
- case _ => false
- }
-
- def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
- case Empty() => true
- }
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty() => 1
- case Node(Black(), l, _, _) => blackHeight(l) + 1
- case Node(Red(), l, _, _) => blackHeight(l)
- }
-
- // <<insert element x into the tree t>>
- def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- t match {
- case Empty() => Node(Red(),Empty(),x,Empty())
- case Node(c,a,y,b) =>
- if (x < y) balance(c, ins(x, a), y, b)
- else if (x == y) Node(c,a,y,b)
- else balance(c,a,y,ins(x, b))
- }
- } ensuring (res => content(res) == content(t) ++ Set(x)
- && size(t) <= size(res) && size(res) <= size(t) + 1
- && redDescHaveBlackChildren(res)
- && blackBalanced(res))
-
- def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n))
- n match {
- case Node(Red(),l,v,r) => Node(Black(),l,v,r)
- case _ => n
- }
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def buggyAdd(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t))
- ins(x, t)
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
-
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(c,a,xV,b) => Node(c,a,xV,b)
- }
- } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
-
- def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- // case Node(c,a,xV,b) => Node(c,a,xV,b)
- }
- } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
-}
diff --git a/demo/SoftTypingWithUniversalType.scala b/demo/SoftTypingWithUniversalType.scala
deleted file mode 100644
index 6dca5a0eddce2aaa0c7adca8b312fc2b9b5b6bbb..0000000000000000000000000000000000000000
--- a/demo/SoftTypingWithUniversalType.scala
+++ /dev/null
@@ -1,65 +0,0 @@
-
-import scala.collection.immutable.Set
-
-object Implicit {
- sealed abstract class U
- case class UInt(i : Int) extends U
- case class UIntSet(s : Set[Int]) extends U
- case class UCons(head : U, tail : U) extends U
- case class UNil() extends U
-
- def isIntList(u : U) : Boolean = u match {
- case UNil() => true
- case UCons(h, t) => isInt(h) && isIntList(t)
- case _ => false
- }
-
- def isInt(u : U) : Boolean = u match {
- case UInt(_) => true
- case _ => false
- }
- implicit def fromInt(i : Int) : U = UInt(i)
- implicit def toInt(u : U) : Int = {
- require(isInt(u))
- u match {
- case UInt(i) => i
- //case _ => 0
- }
- }
-
- def isIntSet(u : U) : Boolean = u match {
- case UIntSet(_) => true
- case _ => false
- }
- implicit def fromIntSet(s : Set[Int]) : U = UIntSet(s)
- implicit def toIntSet(u : U) : Set[Int] = {
- require(isIntSet(u))
- u match {
- case UIntSet(s) => s
- //case _ => Set.empty[Int]
- }
- }
-
- def sum(u1 : U, u2 : U) : U = {
- require(isInt(u1) && isInt(u2))
- (u1 : Int) + u2
- }
-
- def listSize(u : U) : U = {
- require(isIntList(u))
-
- (u match {
- case UNil() => 0
- case UCons(_, t) => 1 + listSize(t)
- }) : U // weird type hint... alternatively, build a UInt explicitly.
-
- } ensuring(res => isInt(res) && res >= 0)
-
- def listContent(u : U) : U = {
- require(isIntList(u))
- u match {
- case UNil() => UIntSet(Set.empty)
- case UCons(h, tail) => UIntSet(listContent(tail) ++ Set[Int](h))
- }
- } ensuring(res => isIntSet(res))
-}
diff --git a/lib/ScalaCheck-1.5-src.jar b/lib/ScalaCheck-1.5-src.jar
deleted file mode 100644
index 49771420824b55e95a835af1c76eef4338248f8a..0000000000000000000000000000000000000000
Binary files a/lib/ScalaCheck-1.5-src.jar and /dev/null differ
diff --git a/lib/ScalaCheck-1.5.jar b/lib/ScalaCheck-1.5.jar
deleted file mode 100644
index 629b26c69d150a85e993210ccb903062e98a2514..0000000000000000000000000000000000000000
Binary files a/lib/ScalaCheck-1.5.jar and /dev/null differ
diff --git a/lib/scalacheck_2.8.1-1.8.jar b/lib/scalacheck_2.8.1-1.8.jar
deleted file mode 100644
index 097225991a7b801ea6e8e7f92ae4128cc284d16c..0000000000000000000000000000000000000000
Binary files a/lib/scalacheck_2.8.1-1.8.jar and /dev/null differ
diff --git a/lib/specs-1.5.0.jar b/lib/specs-1.5.0.jar
deleted file mode 100644
index 25439fbabfdd6db2a5f3f3499b2752efefb94544..0000000000000000000000000000000000000000
Binary files a/lib/specs-1.5.0.jar and /dev/null differ
diff --git a/project/Build.scala b/project/Build.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b24af4918454a381aa37bea303ae9898455d6d00
--- /dev/null
+++ b/project/Build.scala
@@ -0,0 +1,64 @@
+import sbt._
+import Process._
+import Keys._
+
+object Leon extends Build {
+ private val scriptName = "leon"
+ def scriptFile = file(".") / scriptName
+ def ldLibraryDir = file(".") / "lib-bin"
+
+ val scriptTask = TaskKey[Unit]("script", "Generate the " + scriptName + " Bash script") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
+ if(!scriptFile.exists) {
+ s.log.info("Generating script...")
+ try {
+ val depsPaths = deps.map(_.data.absolutePath)
+ // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
+ val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
+ case None => throw new Exception("Couldn't guess SCALA_HOME.")
+ case Some(p) => p.substring(0, p.length - 21)
+ }
+ s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
+
+ val nl = System.getProperty("line.separator")
+ val fw = new java.io.FileWriter(scriptFile)
+ fw.write("#!/bin/bash --posix" + nl)
+ fw.write("SCALACLASSPATH=\"")
+ fw.write((out.absolutePath +: depsPaths).mkString(":"))
+ fw.write("\"" + nl + nl)
+
+ // Setting the dynamic lib path
+ fw.write("LD_LIBRARY_PATH=\"" + ldLibraryDir.absolutePath + "\" \\" + nl)
+
+ // the Java command that uses sbt's local Scala to run the whole contraption.
+ fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
+ fw.write(scalaHomeDir)
+ fw.write("\" -Dscala.usejavacp=true ")
+ fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
+ fw.write("funcheck.Main $@" + nl)
+ fw.close
+ scriptFile.setExecutable(true)
+ } catch {
+ case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
+ }
+ }
+ }
+
+ // private val nameKey = SettingKey[String]("name", "Name of the project")
+ // private val scalaVersionKey = SettingKey[String]("scalaVersion", "Scala Version")
+ // private val versionKey = SettingKey[String]("version", "Version")
+
+ object LeonProject {
+ val settings = Seq(
+ scriptTask /*,
+ nameKey := "Scala Readability",
+ scalaVersionKey := "2.9.1",
+ versionKey := "1.0.0" */
+ )
+ }
+
+ lazy val root = Project(
+ id = "leon",
+ base = file("."),
+ settings = Project.defaultSettings ++ LeonProject.settings
+ )
+}
diff --git a/project/build.properties b/project/build.properties
deleted file mode 100644
index 98fd1d35bd981279ca5159a18baf5704cfb16a74..0000000000000000000000000000000000000000
--- a/project/build.properties
+++ /dev/null
@@ -1,9 +0,0 @@
-#Project properties
-#Wed May 25 21:58:40 CEST 2011
-project.scratch=true
-project.name=FunCheck
-sbt.version=0.7.4
-project.version=1.0
-def.scala.version=2.7.7
-build.scala.versions=2.9.0-1
-project.initialize=false
diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala
deleted file mode 100644
index cd55cffde95a5373576dfcb987b91a86c235cd68..0000000000000000000000000000000000000000
--- a/project/build/funcheck.scala
+++ /dev/null
@@ -1,78 +0,0 @@
-import sbt._
-
-class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileTasks {
- override def outputDirectoryName = "bin"
- override def dependencyPath = "lib"
- override def shouldCheckOutputDirectories = false
-
- lazy val purescala = project(".", "PureScala Definitions", new PureScalaProject(_))
- lazy val plugin = project(".", "FunCheck Plugin", new PluginProject(_), purescala)
-
- lazy val extensionJars : List[Path] = Nil
-
- val scriptPath: Path = "." / "funcheck"
-
- lazy val all = task { None } dependsOn(generateScript) describedAs("Compile everything and produce a script file.")
-
- override def cleanAction = super.cleanAction dependsOn(cleanScript)
-
- lazy val generateScript = genScript
- def genScript = fileTask(scriptPath ::Nil)({
- log.info("Generating runner script")
- try {
- val nl = System.getProperty("line.separator")
- val f = scriptPath.asFile
- val fw = new java.io.FileWriter(f)
- fw.write("#!/bin/bash" + nl)
- fw.write("FUNCHECKCLASSPATH=\"")
- fw.write(buildLibraryJar.absolutePath + ":")
- fw.write(buildCompilerJar.absolutePath + ":")
- fw.write(purescala.jarPath.absolutePath + ":")
- fw.write(plugin.jarPath.absolutePath + ":")
- fw.write(("lib" / "z3.jar").absolutePath)
- fw.write("\"" + nl + nl)
- fw.write("for f in " + extensionJars.map(_.absolutePath).map(n => "\"" + n + "\"").mkString(" ") + "; do" + nl)
- fw.write(" if [ -e ${f} ]" + nl)
- fw.write(" then" + nl)
- fw.write(" FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}" + nl)
- fw.write(" fi" + nl)
- fw.write("done" + nl + nl)
- fw.write("SCALACCLASSPATH=\"")
- fw.write(plugin.jarPath.absolutePath + ":")
- fw.write(purescala.jarPath.absolutePath)
- fw.write("\"" + nl + nl)
- fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
- fw.write("scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH}" + " \\" + nl)
- fw.write("funcheck.Main -cp " + plugin.jarPath.absolutePath + " $@" + nl)
- fw.close
- f.setExecutable(true)
- None
- } catch {
- case e => Some("There was an error while generating the script file: " + e.getLocalizedMessage)
- }
- }) dependsOn(plugin.`package`) describedAs("Produce the runner script.")
-
- lazy val cleanScript = clnScript
- def clnScript = task {
- log.info("Deleting runner script")
- scriptPath.asFile.delete
- None
- }
-
- sealed abstract class PersonalizedProject(info: ProjectInfo) extends DefaultProject(info) {
- override def dependencyPath = "lib"
- override def outputDirectoryName = "bin"
- override def compileOptions = super.compileOptions ++ Seq(Unchecked)
- }
- class PureScalaProject(info: ProjectInfo) extends PersonalizedProject(info) {
- override def outputPath = "bin" / "purescala"
- override def mainScalaSourcePath = "src" / "purescala"
-
- }
- class PluginProject(info: ProjectInfo) extends PersonalizedProject(info) {
- override def outputPath = "bin" / "funcheck"
- override def mainScalaSourcePath = "src" / "funcheck"
- override def unmanagedClasspath = super.unmanagedClasspath +++ purescala.jarPath
- override def mainResourcesPath = "resources" / "funcheck"
- }
-}
diff --git a/resources/funcheck/scalac-plugin.xml b/src/main/resources/funcheck/scalac-plugin.xml
similarity index 100%
rename from resources/funcheck/scalac-plugin.xml
rename to src/main/resources/funcheck/scalac-plugin.xml
diff --git a/src/funcheck/AnalysisComponent.scala b/src/main/scala/funcheck/AnalysisComponent.scala
similarity index 100%
rename from src/funcheck/AnalysisComponent.scala
rename to src/main/scala/funcheck/AnalysisComponent.scala
diff --git a/src/funcheck/Annotations.scala b/src/main/scala/funcheck/Annotations.scala
similarity index 100%
rename from src/funcheck/Annotations.scala
rename to src/main/scala/funcheck/Annotations.scala
diff --git a/src/funcheck/CodeExtraction.scala b/src/main/scala/funcheck/CodeExtraction.scala
similarity index 100%
rename from src/funcheck/CodeExtraction.scala
rename to src/main/scala/funcheck/CodeExtraction.scala
diff --git a/src/funcheck/Extractors.scala b/src/main/scala/funcheck/Extractors.scala
similarity index 100%
rename from src/funcheck/Extractors.scala
rename to src/main/scala/funcheck/Extractors.scala
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/main/scala/funcheck/FunCheckPlugin.scala
similarity index 100%
rename from src/funcheck/FunCheckPlugin.scala
rename to src/main/scala/funcheck/FunCheckPlugin.scala
diff --git a/src/funcheck/Main.scala b/src/main/scala/funcheck/Main.scala
similarity index 100%
rename from src/funcheck/Main.scala
rename to src/main/scala/funcheck/Main.scala
diff --git a/src/funcheck/SimpleReporter.scala b/src/main/scala/funcheck/SimpleReporter.scala
similarity index 100%
rename from src/funcheck/SimpleReporter.scala
rename to src/main/scala/funcheck/SimpleReporter.scala
diff --git a/src/funcheck/Utils.scala b/src/main/scala/funcheck/Utils.scala
similarity index 100%
rename from src/funcheck/Utils.scala
rename to src/main/scala/funcheck/Utils.scala
diff --git a/src/purescala/AbstractZ3Solver.scala b/src/main/scala/purescala/AbstractZ3Solver.scala
similarity index 100%
rename from src/purescala/AbstractZ3Solver.scala
rename to src/main/scala/purescala/AbstractZ3Solver.scala
diff --git a/src/purescala/Analysis.scala b/src/main/scala/purescala/Analysis.scala
similarity index 100%
rename from src/purescala/Analysis.scala
rename to src/main/scala/purescala/Analysis.scala
diff --git a/src/purescala/Common.scala b/src/main/scala/purescala/Common.scala
similarity index 100%
rename from src/purescala/Common.scala
rename to src/main/scala/purescala/Common.scala
diff --git a/src/purescala/DefaultTactic.scala b/src/main/scala/purescala/DefaultTactic.scala
similarity index 100%
rename from src/purescala/DefaultTactic.scala
rename to src/main/scala/purescala/DefaultTactic.scala
diff --git a/src/purescala/Definitions.scala b/src/main/scala/purescala/Definitions.scala
similarity index 100%
rename from src/purescala/Definitions.scala
rename to src/main/scala/purescala/Definitions.scala
diff --git a/src/purescala/Evaluator.scala b/src/main/scala/purescala/Evaluator.scala
similarity index 100%
rename from src/purescala/Evaluator.scala
rename to src/main/scala/purescala/Evaluator.scala
diff --git a/src/purescala/Extensions.scala b/src/main/scala/purescala/Extensions.scala
similarity index 100%
rename from src/purescala/Extensions.scala
rename to src/main/scala/purescala/Extensions.scala
diff --git a/src/purescala/FairZ3Solver.scala b/src/main/scala/purescala/FairZ3Solver.scala
similarity index 100%
rename from src/purescala/FairZ3Solver.scala
rename to src/main/scala/purescala/FairZ3Solver.scala
diff --git a/src/purescala/FunctionTemplate.scala b/src/main/scala/purescala/FunctionTemplate.scala
similarity index 100%
rename from src/purescala/FunctionTemplate.scala
rename to src/main/scala/purescala/FunctionTemplate.scala
diff --git a/src/purescala/InductionTactic.scala b/src/main/scala/purescala/InductionTactic.scala
similarity index 100%
rename from src/purescala/InductionTactic.scala
rename to src/main/scala/purescala/InductionTactic.scala
diff --git a/src/purescala/ParallelSolver.scala b/src/main/scala/purescala/ParallelSolver.scala
similarity index 100%
rename from src/purescala/ParallelSolver.scala
rename to src/main/scala/purescala/ParallelSolver.scala
diff --git a/src/purescala/PrettyPrinter.scala b/src/main/scala/purescala/PrettyPrinter.scala
similarity index 100%
rename from src/purescala/PrettyPrinter.scala
rename to src/main/scala/purescala/PrettyPrinter.scala
diff --git a/src/purescala/RandomSolver.scala b/src/main/scala/purescala/RandomSolver.scala
similarity index 100%
rename from src/purescala/RandomSolver.scala
rename to src/main/scala/purescala/RandomSolver.scala
diff --git a/src/purescala/Reporter.scala b/src/main/scala/purescala/Reporter.scala
similarity index 100%
rename from src/purescala/Reporter.scala
rename to src/main/scala/purescala/Reporter.scala
diff --git a/src/purescala/Settings.scala b/src/main/scala/purescala/Settings.scala
similarity index 100%
rename from src/purescala/Settings.scala
rename to src/main/scala/purescala/Settings.scala
diff --git a/src/purescala/Stopwatch.scala b/src/main/scala/purescala/Stopwatch.scala
similarity index 100%
rename from src/purescala/Stopwatch.scala
rename to src/main/scala/purescala/Stopwatch.scala
diff --git a/src/purescala/TestExtension.scala b/src/main/scala/purescala/TestExtension.scala
similarity index 100%
rename from src/purescala/TestExtension.scala
rename to src/main/scala/purescala/TestExtension.scala
diff --git a/src/purescala/TimeoutSolver.scala b/src/main/scala/purescala/TimeoutSolver.scala
similarity index 100%
rename from src/purescala/TimeoutSolver.scala
rename to src/main/scala/purescala/TimeoutSolver.scala
diff --git a/src/purescala/Timer.scala b/src/main/scala/purescala/Timer.scala
similarity index 100%
rename from src/purescala/Timer.scala
rename to src/main/scala/purescala/Timer.scala
diff --git a/src/purescala/Trees.scala b/src/main/scala/purescala/Trees.scala
similarity index 100%
rename from src/purescala/Trees.scala
rename to src/main/scala/purescala/Trees.scala
diff --git a/src/purescala/TrivialSolver.scala b/src/main/scala/purescala/TrivialSolver.scala
similarity index 100%
rename from src/purescala/TrivialSolver.scala
rename to src/main/scala/purescala/TrivialSolver.scala
diff --git a/src/purescala/TypeTrees.scala b/src/main/scala/purescala/TypeTrees.scala
similarity index 100%
rename from src/purescala/TypeTrees.scala
rename to src/main/scala/purescala/TypeTrees.scala
diff --git a/src/purescala/VerificationCondition.scala b/src/main/scala/purescala/VerificationCondition.scala
similarity index 100%
rename from src/purescala/VerificationCondition.scala
rename to src/main/scala/purescala/VerificationCondition.scala
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/main/scala/purescala/Z3ModelReconstruction.scala
similarity index 100%
rename from src/purescala/Z3ModelReconstruction.scala
rename to src/main/scala/purescala/Z3ModelReconstruction.scala
diff --git a/src/purescala/Z3Solver.scala b/src/main/scala/purescala/Z3Solver.scala
similarity index 100%
rename from src/purescala/Z3Solver.scala
rename to src/main/scala/purescala/Z3Solver.scala
diff --git a/src/purescala/isabelle/Main.scala b/src/main/scala/purescala/isabelle/Main.scala
similarity index 100%
rename from src/purescala/isabelle/Main.scala
rename to src/main/scala/purescala/isabelle/Main.scala
diff --git a/src/purescala/isabelle/README b/src/main/scala/purescala/isabelle/README
similarity index 100%
rename from src/purescala/isabelle/README
rename to src/main/scala/purescala/isabelle/README
diff --git a/src/purescala/isabelle/StrongConnectedComponents.scala b/src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
similarity index 100%
rename from src/purescala/isabelle/StrongConnectedComponents.scala
rename to src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
diff --git a/src/purescala/testcases/Main.scala b/src/main/scala/purescala/testcases/Main.scala
similarity index 100%
rename from src/purescala/testcases/Main.scala
rename to src/main/scala/purescala/testcases/Main.scala
diff --git a/src/purescala/z3plugins/bapa/AST.scala b/src/main/scala/purescala/z3plugins/bapa/AST.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/AST.scala
rename to src/main/scala/purescala/z3plugins/bapa/AST.scala
diff --git a/src/purescala/z3plugins/bapa/BAPATheory.scala b/src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/BAPATheory.scala
rename to src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala
diff --git a/src/purescala/z3plugins/bapa/BAPATheoryBubbles.scala b/src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/BAPATheoryBubbles.scala
rename to src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala
diff --git a/src/purescala/z3plugins/bapa/BAPATheoryEqc.scala b/src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/BAPATheoryEqc.scala
rename to src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala
diff --git a/src/purescala/z3plugins/bapa/Bubbles.scala b/src/main/scala/purescala/z3plugins/bapa/Bubbles.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/Bubbles.scala
rename to src/main/scala/purescala/z3plugins/bapa/Bubbles.scala
diff --git a/src/purescala/z3plugins/bapa/NormalForms.scala b/src/main/scala/purescala/z3plugins/bapa/NormalForms.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/NormalForms.scala
rename to src/main/scala/purescala/z3plugins/bapa/NormalForms.scala
diff --git a/src/purescala/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/PrettyPrinter.scala
rename to src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala
diff --git a/src/purescala/z3plugins/bapa/VennRegions.scala b/src/main/scala/purescala/z3plugins/bapa/VennRegions.scala
similarity index 100%
rename from src/purescala/z3plugins/bapa/VennRegions.scala
rename to src/main/scala/purescala/z3plugins/bapa/VennRegions.scala
diff --git a/src/purescala/z3plugins/instantiator/AbstractInstantiator.scala b/src/main/scala/purescala/z3plugins/instantiator/AbstractInstantiator.scala
similarity index 100%
rename from src/purescala/z3plugins/instantiator/AbstractInstantiator.scala
rename to src/main/scala/purescala/z3plugins/instantiator/AbstractInstantiator.scala
diff --git a/src/purescala/z3plugins/instantiator/Instantiator.scala b/src/main/scala/purescala/z3plugins/instantiator/Instantiator.scala
similarity index 100%
rename from src/purescala/z3plugins/instantiator/Instantiator.scala
rename to src/main/scala/purescala/z3plugins/instantiator/Instantiator.scala
diff --git a/lib/z3.jar b/unmanaged/z3.jar
similarity index 100%
rename from lib/z3.jar
rename to unmanaged/z3.jar