From 823c2b4ef43f966f51dbed51572488df516cbb51 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 16:10:42 +0200
Subject: [PATCH] Remove unneeded files
---
Notes-on-laziness | 140 ---
libtest/build.sbt | 17 -
libtest/project/Build.scala | 35 -
.../main/scala/leon/annotation/isabelle.scala | 31 -
.../main/scala/leon/annotation/package.scala | 43 -
.../src/main/scala/leon/collection/List.scala | 897 ------------------
.../main/scala/leon/collection/package.scala | 25 -
.../scala/leon/instrumentation/package.scala | 24 -
.../main/scala/leon/invariant/package.scala | 26 -
libtest/src/main/scala/leon/lang/Dummy.scala | 3 -
libtest/src/main/scala/leon/lang/Either.scala | 27 -
libtest/src/main/scala/leon/lang/Map.scala | 33 -
libtest/src/main/scala/leon/lang/Option.scala | 84 --
.../src/main/scala/leon/lang/Rational.scala | 85 --
libtest/src/main/scala/leon/lang/Real.scala | 25 -
libtest/src/main/scala/leon/lang/Set.scala | 26 -
libtest/src/main/scala/leon/lang/StrOps.scala | 23 -
.../src/main/scala/leon/lang/package.scala | 85 --
.../scala/leon/lang/synthesis/Oracle.scala | 33 -
.../scala/leon/lang/synthesis/package.scala | 41 -
.../main/scala/leon/lang/xlang/package.scala | 13 -
.../src/main/scala/leon/lazy/package.scala | 90 --
.../src/main/scala/leon/math/package.scala | 18 -
libtest/src/main/scala/leon/mem/package.scala | 56 --
.../main/scala/leon/monads/state/State.scala | 215 -----
libtest/src/main/scala/leon/package.scala | 23 -
libtest/src/main/scala/leon/par/package.scala | 24 -
.../src/main/scala/leon/proof/Internal.scala | 63 --
.../src/main/scala/leon/proof/package.scala | 66 --
.../src/main/scala/leon/stats/package.scala | 28 -
synthesis-collective.txt | 36 -
31 files changed, 2335 deletions(-)
delete mode 100644 Notes-on-laziness
delete mode 100644 libtest/build.sbt
delete mode 100644 libtest/project/Build.scala
delete mode 100644 libtest/src/main/scala/leon/annotation/isabelle.scala
delete mode 100644 libtest/src/main/scala/leon/annotation/package.scala
delete mode 100644 libtest/src/main/scala/leon/collection/List.scala
delete mode 100644 libtest/src/main/scala/leon/collection/package.scala
delete mode 100644 libtest/src/main/scala/leon/instrumentation/package.scala
delete mode 100644 libtest/src/main/scala/leon/invariant/package.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Dummy.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Either.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Map.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Option.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Rational.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Real.scala
delete mode 100644 libtest/src/main/scala/leon/lang/Set.scala
delete mode 100644 libtest/src/main/scala/leon/lang/StrOps.scala
delete mode 100644 libtest/src/main/scala/leon/lang/package.scala
delete mode 100644 libtest/src/main/scala/leon/lang/synthesis/Oracle.scala
delete mode 100644 libtest/src/main/scala/leon/lang/synthesis/package.scala
delete mode 100644 libtest/src/main/scala/leon/lang/xlang/package.scala
delete mode 100644 libtest/src/main/scala/leon/lazy/package.scala
delete mode 100644 libtest/src/main/scala/leon/math/package.scala
delete mode 100644 libtest/src/main/scala/leon/mem/package.scala
delete mode 100644 libtest/src/main/scala/leon/monads/state/State.scala
delete mode 100644 libtest/src/main/scala/leon/package.scala
delete mode 100644 libtest/src/main/scala/leon/par/package.scala
delete mode 100644 libtest/src/main/scala/leon/proof/Internal.scala
delete mode 100644 libtest/src/main/scala/leon/proof/package.scala
delete mode 100644 libtest/src/main/scala/leon/stats/package.scala
delete mode 100644 synthesis-collective.txt
diff --git a/Notes-on-laziness b/Notes-on-laziness
deleted file mode 100644
index e4e094589..000000000
--- a/Notes-on-laziness
+++ /dev/null
@@ -1,140 +0,0 @@
-Some notes:
-------------
-
-A fundamental assumption:
---------------------------
-All functions in the programs must terminate when lazy invocations are treated as eager invocation.
-Otherwise, we report that there could be infinite streams.
-
-Need to Prove
--------------
-How will this enforce the termination of all functions after the translation ?
-This will also ensure that all streams in the program are finite.
-
-Claim 1:
---------
-Since all closures are created by the functions in the program, we have a global
-invariant that whenever we force a value the resulting value cannot be the same
-as the original value.
-Proof:
-(a) since the value is forced it must be a closure with some arguments
-(b) if we get back an identical closure with the same arguments then it means
-we have a recursion the function that corresponds to the the lazy closure,
-and the recursive calls happens with the same set of arguments.
-Which means it is non-terminating when lazy is treated as eager
-
-Claim 2:
---------
-When we force a value it creates some more closures, one of which could again be forced
-returning another closure and so on. Let R(C, n) denote a predicate that
-is true if after forcing closure C, and a closure resulting from C and so on 'n'
-times, we still have a closure.
-We have a invaraint that: \exists n \in nat s.t. ~R(C, n).
-
-Alternatively, we can show that every cycle in the transformed program corresponds to a cycle in the
-input program, but this may also be hard. Since cycle could be offesetted as the recursive
-calls are invoked at different points in the program.
-
-
-Important regarding termination
---------------------------------
-Despite this, in the translation the functions may not terminate on all inputs since there is global
-invariants are not enforced. So how do we make sure that all functions after
-translation do terminate.
-
-One way to handle this would be to change the model and create a new free variable for the result and
-then relate the result and the function in eval, which is like an assumption on the input (a precondition).
-(We know that the precondition is satisfiable because it is for the data-structures created in the program.)
-
-However, we somehow need unlimited supply of free variable of a type.
-To do that we can have a free-list of free-variables as arguments
-(similar to the oracle strategy for non-determinism).
-For eg. sealed abstract class FreeList
- case class Nil() FreeList
- case class Data(fl: FreeList) extends FreeList // returns the data component
- case class Next(fl: FreeList) extends FreeList
-
-define a function 'nextFree' : FreeList -> FreeList.
-var count = 0
-nextFree(l) =
- count += 1
- Data(l :/ (1 to count - 1){ (acc, _) => Next(l) })
-
-Everytime we call a function within the body we case use nextFree(l), where l is the input free-list,
- to get a new free-list.
-We can now add uninterpreted functions that would map the free-list to a desired value,
-for instance, to an ui result of a required type, or to a fresh-integer that denotes
-fresh-ids.
-
-
-Important: Reasons for unsoundness
---------------------------------------
-
-a) the assertion on the newC function that the new closure is unevaluated may result in unsoundness
- - fix: create new identifiers at the time of creating functions. We can also try and use epsilons.
-
-b) Normal data-types can help ensure acyclicity and finiteness of stream but that means we need to create
- free variables at the time of creation
- currently, we are creating axioms that state acyclicity.
-
-Benchmarks to think about
---------------------------
-
-1. Lazy constraint solving
- We can get demand driven pointer-analysis. Can we prove its running time ?
-
-2. Packrat parsers uses memoization
- Can we prove its running time ?
-
-3. ConcTrees full version ?
-
-4. Binomial heaps ?
-
-5. Futures: How about redex algorithms or map-reduce algorithms ?
-
-Things to implement:
-----------------------
-
-a) A way to check monotonicity of preconditions
-b) Use monotonicity while checking proofs
-c) Automatically synthesize the invariant that the state is preserved
-d) We can always assume that state is monotonic which proving the specs
-c) Extensions for futures
-d) Extensions for memoization
-e) Extending Orb for type parameters
-*f) Try to separate the instrumentation for state and value, if not add a postcondition
- that the value part of the state-instrumented program is same as some function that does not use state.
- But, how can we do that ?
-
-Integration
-
-Try to fix bugs in CVC4 proof and also try to integerate it with the system
-Try to integrate the tool with Orb
-
-Some Notes
-----------
-
-a) It is very essential to make the separation between value and state component explicit
- we can use something like: "foo(x, uiState())" and "foo(x, st)" where st is the actual input state.
-
-b) We need to treat Lazyarg's as not closures. That is, they don't change state and are not considered as Unevaluated. They
- are never added to the set.
- We can have an implicit type conversion from normal values to lazyargs.
- Since normal values are eagerly computed. This lets us specify lazyargs succinctly in the code.
- We need to change isEvaluated and value function call modelling
-
-c) Futures when modelled as closures can be stored and then later joined.
-e.g. a function 'spawn' that will spawn tasks and a function 'join' that will join
-the spawned threads.
-However, we need to explicitly mark the functions that can be executed in parallel from the
-point of creation of a Future to the point of joining the Future.
-Eg. as
-spawn()
-spawn()
-parallel(op(), join(), join())
-//this means op() and the two futures will execute in parallel.
-
-d) Memoization: They are evaluated at the time of creation unlike lazy closures.
- We need to track whether a closure belongs to a state or not.
-
-
diff --git a/libtest/build.sbt b/libtest/build.sbt
deleted file mode 100644
index 9e8ce202f..000000000
--- a/libtest/build.sbt
+++ /dev/null
@@ -1,17 +0,0 @@
-name := "LazyBenchmarkExecution"
-
-version := "1.0"
-
-organization := "ch.epfl.lara"
-
-scalaVersion := "2.11.7"
-
-fork in run := true
-
-unmanagedJars in Compile += file("lib/macmemo.jar")
-
-javaOptions in run ++= Seq("-Xmx5G", "-Xms3G", "-Xss500M")
-
-scalacOptions ++= Seq("-optimise")
-
-libraryDependencies += "org.scala-lang" % "scala-reflect" % "2.11.5"
diff --git a/libtest/project/Build.scala b/libtest/project/Build.scala
deleted file mode 100644
index 19f93de52..000000000
--- a/libtest/project/Build.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-import sbt._
-import Keys._
-
-object BuildSettings {
- val paradiseVersion = "2.1.0-M5"
- val buildSettings = Defaults.defaultSettings ++ Seq(
- resolvers += Resolver.sonatypeRepo("snapshots"),
- resolvers += Resolver.sonatypeRepo("releases"),
- addCompilerPlugin("org.scalamacros" % "paradise" % paradiseVersion cross CrossVersion.full)
- )
-}
-
-object MyBuild extends Build {
- import BuildSettings._
-
- lazy val root = Project(
- "root",
- file("."),
- settings = buildSettings
- )
-
-// aggregate (macros, benchmarks)
-//
-// lazy val macros = Project(
-// "leon",
-// file("src/main/scala/leon"),
-// settings = buildSettings
-// )
-//
-// lazy val benchmarks = Project(
-// "benchmark",
-// file("src/main/scala/benchmarks"),
-// settings = buildSettings
-// ) dependsOn macros
-}
diff --git a/libtest/src/main/scala/leon/annotation/isabelle.scala b/libtest/src/main/scala/leon/annotation/isabelle.scala
deleted file mode 100644
index bfb4b39ec..000000000
--- a/libtest/src/main/scala/leon/annotation/isabelle.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-package leon.annotation
-
-import scala.annotation.StaticAnnotation
-
-object isabelle {
-
- @ignore
- class typ(name: String) extends StaticAnnotation
-
- @ignore
- class constructor(name: String) extends StaticAnnotation
-
- @ignore
- class function(term: String) extends StaticAnnotation
-
- @ignore
- class script(name: String, source: String) extends StaticAnnotation
-
- @ignore
- class proof(method: String, kind: String = "") extends StaticAnnotation
-
- @ignore
- class fullBody() extends StaticAnnotation
-
- @ignore
- class noBody() extends StaticAnnotation
-
- @ignore
- class lemma(about: String) extends StaticAnnotation
-
-}
diff --git a/libtest/src/main/scala/leon/annotation/package.scala b/libtest/src/main/scala/leon/annotation/package.scala
deleted file mode 100644
index a355a8557..000000000
--- a/libtest/src/main/scala/leon/annotation/package.scala
+++ /dev/null
@@ -1,43 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import scala.annotation.StaticAnnotation
-import scala.language.experimental.macros
-
-package object annotation {
- @ignore
- class library extends StaticAnnotation
- @ignore
- class induct extends StaticAnnotation
- @ignore
- class traceInduct(name: String = "") extends StaticAnnotation
- @ignore
- class ignore extends StaticAnnotation
- @ignore
- class extern extends StaticAnnotation
- @ignore
- class inline extends StaticAnnotation
- @ignore
- class internal extends StaticAnnotation
-
- // Orb annotations
- @ignore
- class monotonic extends StaticAnnotation
- @ignore
- class compose extends StaticAnnotation
- @ignore
- class axiom extends StaticAnnotation
- @ignore
- class invstate extends StaticAnnotation
- @ignore
- class memoize extends StaticAnnotation {
- def macroTransform(annottees: Any*): Any = macro com.softwaremill.macmemo.memoizeMacro.impl
- }
- @ignore
- class invisibleBody extends StaticAnnotation // do not unfold the body of the function
- @ignore
- class usePost extends StaticAnnotation // assume the post-condition while proving time bounds
- @ignore
- class unfoldFactor(f: Int=0) extends StaticAnnotation // 0 implies no bound on unfolding
-}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/collection/List.scala b/libtest/src/main/scala/leon/collection/List.scala
deleted file mode 100644
index 74a0f0c66..000000000
--- a/libtest/src/main/scala/leon/collection/List.scala
+++ /dev/null
@@ -1,897 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.collection
-
-import leon._
-import leon.lang._
-import leon.annotation._
-import leon.math._
-import leon.proof._
-
-@library
-@isabelle.typ(name = "List.list")
-sealed abstract class List[T] {
-
- @isabelle.function(term = "Int.int o List.length")
- def size: BigInt = (this match {
- case Nil() => BigInt(0)
- case Cons(h, t) => 1 + t.size
- }) ensuring (_ >= 0)
-
- def length = size
-
- @isabelle.function(term = "List.list.set")
- def content: Set[T] = this match {
- case Nil() => Set()
- case Cons(h, t) => Set(h) ++ t.content
- }
-
- @isabelle.function(term = "List.member")
- def contains(v: T): Boolean = (this match {
- case Cons(h, t) => h == v || t.contains(v)
- case Nil() => false
- }) ensuring { _ == (content contains v) }
-
- @isabelle.function(term = "List.append")
- def ++(that: List[T]): List[T] = (this match {
- case Nil() => that
- case Cons(x, xs) => Cons(x, xs ++ that)
- }) ensuring { res =>
- (res.content == this.content ++ that.content) &&
- (res.size == this.size + that.size) &&
- (that != Nil[T]() || res == this)
- }
-
- def head: T = {
- require(this != Nil[T]())
- val Cons(h, _) = this
- h
- }
-
- def tail: List[T] = {
- require(this != Nil[T]())
- val Cons(_, t) = this
- t
- }
-
- @isabelle.fullBody
- def apply(index: BigInt): T = {
- require(0 <= index && index < size)
- if (index == BigInt(0)) {
- head
- } else {
- tail(index-1)
- }
- }
-
- @isabelle.function(term = "%xs x. x # xs")
- def ::(t:T): List[T] = Cons(t, this)
-
- @isabelle.function(term = "%xs x. xs @ [x]")
- def :+(t:T): List[T] = {
- this match {
- case Nil() => Cons(t, this)
- case Cons(x, xs) => Cons(x, xs :+ (t))
- }
- } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
-
- @isabelle.function(term = "List.rev")
- def reverse: List[T] = {
- this match {
- case Nil() => this
- case Cons(x,xs) => xs.reverse :+ x
- }
- } ensuring (res => (res.size == size) && (res.content == content))
-
- def take(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil[T]()
- case (Cons(h, t), i) =>
- if (i <= BigInt(0)) {
- Nil[T]()
- } else {
- Cons(h, t.take(i-1))
- }
- }} ensuring { res =>
- res.content.subsetOf(this.content) && (res.size == (
- if (i <= 0) BigInt(0)
- else if (i >= this.size) this.size
- else i
- ))
- }
-
- def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil[T]()
- case (Cons(h, t), i) =>
- if (i <= BigInt(0)) {
- Cons[T](h, t)
- } else {
- t.drop(i-1)
- }
- }} ensuring { res =>
- res.content.subsetOf(this.content) && (res.size == (
- if (i <= 0) this.size
- else if (i >= this.size) BigInt(0)
- else this.size - i
- ))
- }
-
- def slice(from: BigInt, to: BigInt): List[T] = {
- require(0 <= from && from <= to && to <= size)
- drop(from).take(to-from)
- }
-
- def replace(from: T, to: T): List[T] = { this match {
- case Nil() => Nil[T]()
- case Cons(h, t) =>
- val r = t.replace(from, to)
- if (h == from) {
- Cons(to, r)
- } else {
- Cons(h, r)
- }
- }} ensuring { (res: List[T]) =>
- res.size == this.size &&
- res.content == (
- (this.content -- Set(from)) ++
- (if (this.content contains from) Set(to) else Set[T]())
- )
- }
-
- private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = {
- require(s > 0 && s0 >= 0)
- l match {
- case Nil() =>
- if (acc.size > 0) {
- res :+ acc
- } else {
- res
- }
- case Cons(h, t) =>
- if (s0 == BigInt(0)) {
- chunk0(s, t, Cons(h, Nil()), res :+ acc, s-1)
- } else {
- chunk0(s, t, acc :+ h, res, s0-1)
- }
- }
- }
-
- def chunks(s: BigInt): List[List[T]] = {
- require(s > 0)
-
- chunk0(s, this, Nil(), Nil(), s)
- }
-
- @isabelle.function(term = "List.zip")
- def zip[B](that: List[B]): List[(T, B)] = { (this, that) match {
- case (Cons(h1, t1), Cons(h2, t2)) =>
- Cons((h1, h2), t1.zip(t2))
- case _ =>
- Nil[(T, B)]()
- }} ensuring { _.size == (
- if (this.size <= that.size) this.size else that.size
- )}
-
- @isabelle.function(term = "%xs x. removeAll x xs")
- def -(e: T): List[T] = { this match {
- case Cons(h, t) =>
- if (e == h) {
- t - e
- } else {
- Cons(h, t - e)
- }
- case Nil() =>
- Nil[T]()
- }} ensuring { res =>
- res.size <= this.size &&
- res.content == this.content -- Set(e)
- }
-
- def --(that: List[T]): List[T] = { this match {
- case Cons(h, t) =>
- if (that.contains(h)) {
- t -- that
- } else {
- Cons(h, t -- that)
- }
- case Nil() =>
- Nil[T]()
- }} ensuring { res =>
- res.size <= this.size &&
- res.content == this.content -- that.content
- }
-
- def &(that: List[T]): List[T] = { this match {
- case Cons(h, t) =>
- if (that.contains(h)) {
- Cons(h, t & that)
- } else {
- t & that
- }
- case Nil() =>
- Nil[T]()
- }} ensuring { res =>
- res.size <= this.size &&
- res.content == (this.content & that.content)
- }
-
- def padTo(s: BigInt, e: T): List[T] = { (this, s) match {
- case (_, s) if s <= 0 =>
- this
- case (Nil(), s) =>
- Cons(e, Nil().padTo(s-1, e))
- case (Cons(h, t), s) =>
- Cons(h, t.padTo(s-1, e))
- }} ensuring { res =>
- if (s <= this.size)
- res == this
- else
- res.size == s &&
- res.content == this.content ++ Set(e)
- }
-
- def find(e: T): Option[BigInt] = { this match {
- case Nil() => None[BigInt]()
- case Cons(h, t) =>
- if (h == e) {
- Some[BigInt](0)
- } else {
- t.find(e) match {
- case None() => None[BigInt]()
- case Some(i) => Some(i+1)
- }
- }
- }} ensuring { res => !res.isDefined || (this.content contains e) }
-
- def init: List[T] = {
- require(!isEmpty)
- ((this : @unchecked) match {
- case Cons(h, Nil()) =>
- Nil[T]()
- case Cons(h, t) =>
- Cons[T](h, t.init)
- })
- } ensuring ( (r: List[T]) =>
- r.size == this.size - 1 &&
- r.content.subsetOf(this.content)
- )
-
- def last: T = {
- require(!isEmpty)
- (this : @unchecked) match {
- case Cons(h, Nil()) => h
- case Cons(_, t) => t.last
- }
- } ensuring { this.contains _ }
-
- def lastOption: Option[T] = { this match {
- case Cons(h, t) =>
- t.lastOption.orElse(Some(h))
- case Nil() =>
- None[T]()
- }} ensuring { _.isDefined != this.isEmpty }
-
- def headOption: Option[T] = { this match {
- case Cons(h, t) =>
- Some(h)
- case Nil() =>
- None[T]()
- }} ensuring { _.isDefined != this.isEmpty }
-
- def tailOption: Option[List[T]] = { this match {
- case Cons(h, t) =>
- Some(t)
- case Nil() =>
- None[List[T]]()
- }} ensuring { _.isDefined != this.isEmpty }
-
-
- def unique: List[T] = this match {
- case Nil() => Nil()
- case Cons(h, t) =>
- Cons(h, t.unique - h)
- }
-
- def splitAt(e: T): List[List[T]] = split(Cons(e, Nil()))
-
- def split(seps: List[T]): List[List[T]] = this match {
- case Cons(h, t) =>
- if (seps.contains(h)) {
- Cons(Nil(), t.split(seps))
- } else {
- val r = t.split(seps)
- Cons(Cons(h, r.head), r.tail)
- }
- case Nil() =>
- Cons(Nil(), Nil())
- }
-
- def evenSplit: (List[T], List[T]) = {
- val c = size/2
- (take(c), drop(c))
- }
-
- def splitAtIndex(index: BigInt) : (List[T], List[T]) = { this match {
- case Nil() => (Nil[T](), Nil[T]())
- case Cons(h, rest) => {
- if (index <= BigInt(0)) {
- (Nil[T](), this)
- } else {
- val (left,right) = rest.splitAtIndex(index - 1)
- (Cons[T](h,left), right)
- }
- }
- }} ensuring { (res:(List[T],List[T])) =>
- res._1 ++ res._2 == this &&
- res._1 == take(index) && res._2 == drop(index)
- }
-
- def updated(i: BigInt, y: T): List[T] = {
- require(0 <= i && i < this.size)
- this match {
- case Cons(x, tail) if i == 0 =>
- Cons[T](y, tail)
- case Cons(x, tail) =>
- Cons[T](x, tail.updated(i - 1, y))
- }
- }
-
- private def insertAtImpl(pos: BigInt, l: List[T]): List[T] = {
- require(0 <= pos && pos <= size)
- if(pos == BigInt(0)) {
- l ++ this
- } else {
- this match {
- case Cons(h, t) =>
- Cons(h, t.insertAtImpl(pos-1, l))
- case Nil() =>
- l
- }
- }
- } ensuring { res =>
- res.size == this.size + l.size &&
- res.content == this.content ++ l.content
- }
-
- def insertAt(pos: BigInt, l: List[T]): List[T] = {
- require(-pos <= size && pos <= size)
- if(pos < 0) {
- insertAtImpl(size + pos, l)
- } else {
- insertAtImpl(pos, l)
- }
- } ensuring { res =>
- res.size == this.size + l.size &&
- res.content == this.content ++ l.content
- }
-
- def insertAt(pos: BigInt, e: T): List[T] = {
- require(-pos <= size && pos <= size)
- insertAt(pos, Cons[T](e, Nil()))
- } ensuring { res =>
- res.size == this.size + 1 &&
- res.content == this.content ++ Set(e)
- }
-
- private def replaceAtImpl(pos: BigInt, l: List[T]): List[T] = {
- require(0 <= pos && pos <= size)
- if (pos == BigInt(0)) {
- l ++ this.drop(l.size)
- } else {
- this match {
- case Cons(h, t) =>
- Cons(h, t.replaceAtImpl(pos-1, l))
- case Nil() =>
- l
- }
- }
- } ensuring { res =>
- res.content.subsetOf(l.content ++ this.content)
- }
-
- def replaceAt(pos: BigInt, l: List[T]): List[T] = {
- require(-pos <= size && pos <= size)
- if(pos < 0) {
- replaceAtImpl(size + pos, l)
- } else {
- replaceAtImpl(pos, l)
- }
- } ensuring { res =>
- res.content.subsetOf(l.content ++ this.content)
- }
-
- def rotate(s: BigInt): List[T] = {
- if (isEmpty) {
- Nil[T]()
- } else {
- drop(s mod size) ++ take(s mod size)
- }
- } ensuring { res =>
- res.size == this.size
- }
-
- @isabelle.function(term = "List.null")
- def isEmpty = this match {
- case Nil() => true
- case _ => false
- }
-
- def nonEmpty = !isEmpty
-
- // Higher-order API
- @isabelle.function(term = "%xs f. List.list.map f xs")
- def map[R](f: T => R): List[R] = { this match {
- case Nil() => Nil[R]()
- case Cons(h, t) => f(h) :: t.map(f)
- }} ensuring { _.size == this.size }
-
- @isabelle.function(term = "%bs a f. List.foldl f a bs")
- def foldLeft[R](z: R)(f: (R,T) => R): R = this match {
- case Nil() => z
- case Cons(h,t) => t.foldLeft(f(z,h))(f)
- }
-
- @isabelle.function(term = "%as b f. List.foldr f as b")
- def foldRight[R](z: R)(f: (T,R) => R): R = this match {
- case Nil() => z
- case Cons(h, t) => f(h, t.foldRight(z)(f))
- }
-
- def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
- case Nil() => z :: Nil()
- case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
- }} ensuring { !_.isEmpty }
-
- def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
- case Nil() => z :: Nil[R]()
- case Cons(h, t) =>
- val rest@Cons(h1,_) = t.scanRight(z)(f)
- f(h, h1) :: rest
- }} ensuring { !_.isEmpty }
-
- @isabelle.function(term = "List.bind")
- def flatMap[R](f: T => List[R]): List[R] =
- ListOps.flatten(this map f)
-
- def filter(p: T => Boolean): List[T] = { this match {
- case Nil() => Nil[T]()
- case Cons(h, t) if p(h) => Cons(h, t.filter(p))
- case Cons(_, t) => t.filter(p)
- }} ensuring { res =>
- res.size <= this.size &&
- res.content.subsetOf(this.content) &&
- res.forall(p)
- }
-
- def filterNot(p: T => Boolean): List[T] =
- filter(!p(_)) ensuring { res =>
- res.size <= this.size &&
- res.content.subsetOf(this.content) &&
- res.forall(!p(_))
- }
-
- def partition(p: T => Boolean): (List[T], List[T]) = { this match {
- case Nil() => (Nil[T](), Nil[T]())
- case Cons(h, t) =>
- val (l1, l2) = t.partition(p)
- if (p(h)) (h :: l1, l2)
- else (l1, h :: l2)
- }} ensuring { res =>
- res._1 == filter(p) &&
- res._2 == filterNot(p)
- }
-
- // In case we implement for-comprehensions
- def withFilter(p: T => Boolean) = filter(p)
-
- @isabelle.function(term = "%xs P. List.list_all P xs")
- def forall(p: T => Boolean): Boolean = this match {
- case Nil() => true
- case Cons(h, t) => p(h) && t.forall(p)
- }
-
- @isabelle.function(term = "%xs P. List.list_ex P xs")
- def exists(p: T => Boolean) = !forall(!p(_))
-
- @isabelle.function(term = "%xs P. List.find P xs")
- def find(p: T => Boolean): Option[T] = { this match {
- case Nil() => None[T]()
- case Cons(h, t) => if (p(h)) Some(h) else t.find(p)
- }} ensuring { res => res match {
- case Some(r) => (content contains r) && p(r)
- case None() => true
- }}
-
- def groupBy[R](f: T => R): Map[R, List[T]] = this match {
- case Nil() => Map.empty[R, List[T]]
- case Cons(h, t) =>
- val key: R = f(h)
- val rest: Map[R, List[T]] = t.groupBy(f)
- val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
- (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
- }
-
- def takeWhile(p: T => Boolean): List[T] = { this match {
- case Cons(h,t) if p(h) => Cons(h, t.takeWhile(p))
- case _ => Nil[T]()
- }} ensuring { res =>
- (res forall p) &&
- (res.size <= this.size) &&
- (res.content subsetOf this.content)
- }
-
- def dropWhile(p: T => Boolean): List[T] = { this match {
- case Cons(h,t) if p(h) => t.dropWhile(p)
- case _ => this
- }} ensuring { res =>
- (res.size <= this.size) &&
- (res.content subsetOf this.content) &&
- (res.isEmpty || !p(res.head))
- }
-
- def count(p: T => Boolean): BigInt = { this match {
- case Nil() => BigInt(0)
- case Cons(h, t) =>
- (if (p(h)) BigInt(1) else BigInt(0)) + t.count(p)
- }} ensuring {
- _ == this.filter(p).size
- }
-
- def indexWhere(p: T => Boolean): BigInt = { this match {
- case Nil() => BigInt(-1)
- case Cons(h, _) if p(h) => BigInt(0)
- case Cons(_, t) =>
- val rec = t.indexWhere(p)
- if (rec >= 0) rec + BigInt(1)
- else BigInt(-1)
- }} ensuring {
- _ >= BigInt(0) == (this exists p)
- }
-
-
- // Translation to other collections
- def toSet: Set[T] = foldLeft(Set[T]()){
- case (current, next) => current ++ Set(next)
- }
-
-}
-
-@isabelle.constructor(name = "List.list.Cons")
-case class Cons[T](h: T, t: List[T]) extends List[T]
-
-@isabelle.constructor(name = "List.list.Nil")
-case class Nil[T]() extends List[T]
-
-object List {
- @ignore
- def apply[T](elems: T*): List[T] = {
- var l: List[T] = Nil[T]()
- for (e <- elems) {
- l = Cons(e, l)
- }
- l.reverse
- }
-
- @library
- def fill[T](n: BigInt)(x: T) : List[T] = {
- if (n <= 0) Nil[T]
- else Cons[T](x, fill[T](n-1)(x))
- } ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
- res.size == (if (n <= BigInt(0)) BigInt(0) else n))
-}
-
-@library
-object ListOps {
- @isabelle.function(term = "List.concat")
- def flatten[T](ls: List[List[T]]): List[T] = ls match {
- case Cons(h, t) => h ++ flatten(t)
- case Nil() => Nil()
- }
-
- def isSorted(ls: List[BigInt]): Boolean = ls match {
- case Nil() => true
- case Cons(_, Nil()) => true
- case Cons(h1, Cons(h2, _)) if(h1 > h2) => false
- case Cons(_, t) => isSorted(t)
- }
-
- def sorted(ls: List[BigInt]): List[BigInt] = { ls match {
- case Cons(h, t) => sortedIns(sorted(t), h)
- case Nil() => Nil[BigInt]()
- }} ensuring { isSorted _ }
-
- private def sortedIns(ls: List[BigInt], v: BigInt): List[BigInt] = {
- require(isSorted(ls))
- ls match {
- case Nil() => Cons(v, Nil())
- case Cons(h, t) =>
- if (v <= h) {
- Cons(v, t)
- } else {
- Cons(h, sortedIns(t, v))
- }
- }
- } ensuring { isSorted _ }
-
- def toMap[K, V](l: List[(K, V)]): Map[K, V] = l.foldLeft(Map[K, V]()){
- case (current, (k, v)) => current ++ Map(k -> v)
- }
-}
-
-// 'Cons' Extractor
-object :: {
- @library
- def unapply[A](l: List[A]): Option[(A, List[A])] = l match {
- case Nil() => None()
- case Cons(x, xs) => Some((x, xs))
- }
-}
-
-
-import ListOps._
-
-@library
-object ListSpecs {
- def snocIndex[T](l: List[T], t: T, i: BigInt): Boolean = {
- require(0 <= i && i < l.size + 1)
- ((l :+ t).apply(i) == (if (i < l.size) l(i) else t)) because
- (l match {
- case Nil() => true
- case Cons(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
- })
- }.holds
-
- @induct
- @isabelle.lemma(about = "leon.collection.List.apply")
- def consIndex[T](h: T, t: List[T], i: BigInt): Boolean = {
- require(0 <= i && i < t.size + 1)
- (h :: t).apply(i) == (if (i == 0) h else t.apply(i - 1))
- }.holds
-
- def reverseIndex[T](l: List[T], i: BigInt): Boolean = {
- require(0 <= i && i < l.size)
- (l.reverse.apply(i) == l.apply(l.size - 1 - i)) because
- (l match {
- case Nil() => true
- case Cons(x,xs) => snocIndex(xs.reverse, x, i) && (if (i < xs.size) consIndex(x, xs, l.size - 1 - i) && reverseIndex[T](xs, i) else true)
- })
- }.holds
-
- def snocLast[T](l: List[T], x: T): Boolean = {
- ((l :+ x).last == x) because {
- l match {
- case Nil() => true
- case Cons(y, ys) => {
- ((y :: ys) :+ x).last ==| trivial |
- (y :: (ys :+ x)).last ==| trivial |
- (ys :+ x).last ==| snocLast(ys, x) |
- x
- }.qed
- }
- }
- }.holds
-
- def headReverseLast[T](l: List[T]): Boolean = {
- require (!l.isEmpty)
- (l.head == l.reverse.last) because {
- val Cons(x, xs) = l;
- {
- (x :: xs).head ==| trivial |
- x ==| snocLast(xs.reverse, x) |
- (xs.reverse :+ x).last ==| trivial |
- (x :: xs).reverse.last
- }.qed
- }
- }.holds
-
- def appendIndex[T](l1: List[T], l2: List[T], i: BigInt): Boolean = {
- require(0 <= i && i < l1.size + l2.size)
- ( (l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)) ) because {
- l1 match {
- case Nil() => true
- case Cons(x,xs) =>
- (i != BigInt(0)) ==> appendIndex[T](xs, l2, i - 1)
- }
- }
- }.holds
-
- @induct
- def appendAssoc[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
- (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
- }.holds
-
- @induct
- def rightUnitAppend[T](l1: List[T]): Boolean = {
- l1 ++ Nil() == l1
- }.holds
-
- // This follows immediately from the definition of `++` but we
- // include it here anyway for completeness.
- def leftUnitAppend[T](l1: List[T]): Boolean = {
- Nil() ++ l1 == l1
- }.holds
-
- def snocIsAppend[T](l: List[T], t: T): Boolean = {
- ( (l :+ t) == l ++ Cons[T](t, Nil()) ) because {
- l match {
- case Nil() => true
- case Cons(x,xs) => snocIsAppend(xs,t)
- }
- }
- }.holds
-
- def snocAfterAppend[T](l1: List[T], l2: List[T], t: T): Boolean = {
- ( (l1 ++ l2) :+ t == l1 ++ (l2 :+ t) ) because {
- l1 match {
- case Nil() => true
- case Cons(x,xs) => snocAfterAppend(xs,l2,t)
- }
- }
- }.holds
-
- def snocReverse[T](l: List[T], t: T): Boolean = {
- ( (l :+ t).reverse == Cons(t, l.reverse) ) because {
- l match {
- case Nil() => true
- case Cons(x,xs) => snocReverse(xs,t)
- }
- }
- }.holds
-
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l because {
- l match {
- case Nil() => trivial
- case Cons(x, xs) => {
- (xs.reverse :+ x).reverse ==| snocReverse[T](xs.reverse, x) |
- x :: xs.reverse.reverse ==| reverseReverse[T](xs) |
- (x :: xs)
- }.qed
- }
- }
- }.holds
-
- def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
- ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
- l1 match {
- case Nil() => {
- (Nil() ++ l2).reverse ==| trivial |
- l2.reverse ==| rightUnitAppend(l2.reverse) |
- l2.reverse ++ Nil() ==| trivial |
- l2.reverse ++ Nil().reverse
- }.qed
- case Cons(x, xs) => {
- ((x :: xs) ++ l2).reverse ==| trivial |
- (x :: (xs ++ l2)).reverse ==| trivial |
- (xs ++ l2).reverse :+ x ==| reverseAppend(xs, l2) |
- (l2.reverse ++ xs.reverse) :+ x ==|
- snocAfterAppend(l2.reverse, xs.reverse, x) |
- l2.reverse ++ (xs.reverse :+ x) ==| trivial |
- l2.reverse ++ (x :: xs).reverse
- }.qed
- }
- }
- }.holds
-
- def snocFoldRight[A, B](xs: List[A], y: A, z: B, f: (A, B) => B): Boolean = {
- ( (xs :+ y).foldRight(z)(f) == xs.foldRight(f(y, z))(f) ) because {
- xs match {
- case Nil() => true
- case Cons(x, xs) => snocFoldRight(xs, y, z, f)
- }
- }
- }.holds
-
- def folds[A, B](xs: List[A], z: B, f: (B, A) => B): Boolean = {
- val f2 = (x: A, z: B) => f(z, x)
- ( xs.foldLeft(z)(f) == xs.reverse.foldRight(z)(f2) ) because {
- xs match {
- case Nil() => true
- case Cons(x, xs) => {
- (x :: xs).foldLeft(z)(f) ==| trivial |
- xs.foldLeft(f(z, x))(f) ==| folds(xs, f(z, x), f) |
- xs.reverse.foldRight(f(z, x))(f2) ==| trivial |
- xs.reverse.foldRight(f2(x, z))(f2) ==|
- snocFoldRight(xs.reverse, x, z, f2) |
- (xs.reverse :+ x).foldRight(z)(f2) ==| trivial |
- (x :: xs).reverse.foldRight(z)(f2)
- }.qed
- }
- }
- }.holds
-
- def scanVsFoldLeft[A, B](l: List[A], z: B, f: (B, A) => B): Boolean = {
- ( l.scanLeft(z)(f).last == l.foldLeft(z)(f) ) because {
- l match {
- case Nil() => true
- case Cons(x, xs) => scanVsFoldLeft(xs, f(z, x), f)
- }
- }
- }.holds
-
- //// my hand calculation shows this should work, but it does not seem to be found
- //def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
- // f(l1 ++ l2) == op(f(l1), f(l2))
- //}
- //
- //def existsAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
- // associative[T, Boolean](l1, l2, _.exists(p), _ || _ )
- //}.holds
- //
- //def forallAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
- // associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
- //}.holds
-
- @induct
- def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
- l.scanRight(z)(f).head == l.foldRight(z)(f)
- }.holds
-
- def appendContent[A](l1: List[A], l2: List[A]) = {
- l1.content ++ l2.content == (l1 ++ l2).content
- }.holds
-
- def flattenPreservesContent[T](ls: List[List[T]]): Boolean = {
- val f: (List[T], Set[T]) => Set[T] = _.content ++ _
- ( flatten(ls).content == ls.foldRight(Set[T]())(f) ) because {
- ls match {
- case Nil() => true
- case Cons(h, t) => {
- flatten(h :: t).content ==| trivial |
- (h ++ flatten(t)).content ==| appendContent(h, flatten(t)) |
- h.content ++ flatten(t).content ==| flattenPreservesContent(t) |
- h.content ++ t.foldRight(Set[T]())(f) ==| trivial |
- f(h, Set[T]()) ++ t.foldRight(Set[T]())(f) ==| trivial |
- (h :: t).foldRight(Set[T]())(f)
- }.qed
- }
- }
- }.holds
-
- // A lemma about `append` and `updated`
- def appendUpdate[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
- require(0 <= i && i < l1.size + l2.size)
- // induction scheme
- (l1 match {
- case Nil() => true
- case Cons(x, xs) => if (i == 0) true else appendUpdate[T](xs, l2, i - 1, y)
- }) &&
- // lemma
- ((l1 ++ l2).updated(i, y) == (
- if (i < l1.size)
- l1.updated(i, y) ++ l2
- else
- l1 ++ l2.updated(i - l1.size, y)))
- }.holds
-
- // a lemma about `append`, `take` and `drop`
- def appendTakeDrop[T](l1: List[T], l2: List[T], n: BigInt): Boolean = {
- //induction scheme
- (l1 match {
- case Nil() => true
- case Cons(x, xs) => if (n <= 0) true else appendTakeDrop[T](xs, l2, n - 1)
- }) &&
- // lemma
- ((l1 ++ l2).take(n) == (
- if (n < l1.size) l1.take(n)
- else if (n > l1.size) l1 ++ l2.take(n - l1.size)
- else l1)) &&
- ((l1 ++ l2).drop(n) == (
- if (n < l1.size) l1.drop(n) ++ l2
- else if (n > l1.size) l2.drop(n - l1.size)
- else l2))
- }.holds
-
- // A lemma about `append` and `insertAt`
- def appendInsert[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
- require(0 <= i && i <= l1.size + l2.size)
- (l1 match {
- case Nil() => true
- case Cons(x, xs) => if (i == 0) true else appendInsert[T](xs, l2, i - 1, y)
- }) &&
- // lemma
- ((l1 ++ l2).insertAt(i, y) == (
- if (i < l1.size) l1.insertAt(i, y) ++ l2
- else l1 ++ l2.insertAt((i - l1.size), y)))
- }.holds
-
-}
diff --git a/libtest/src/main/scala/leon/collection/package.scala b/libtest/src/main/scala/leon/collection/package.scala
deleted file mode 100644
index 8a5ae1707..000000000
--- a/libtest/src/main/scala/leon/collection/package.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import leon.collection.List
-import leon.lang._
-import leon.lang.synthesis.choose
-
-package object collection {
-
- @internal @library
- def setToList[A](set: Set[A]): List[A] = choose {
- (x: List[A]) => x.content == set
- }
-
- @library
- def setForall[A](set: Set[A], p: A => Boolean): Boolean =
- setToList(set).forall(p)
-
- @library
- def setExists[A](set: Set[A], p: A => Boolean): Boolean =
- setToList(set).exists(p)
-
-}
diff --git a/libtest/src/main/scala/leon/instrumentation/package.scala b/libtest/src/main/scala/leon/instrumentation/package.scala
deleted file mode 100644
index a6e7545c0..000000000
--- a/libtest/src/main/scala/leon/instrumentation/package.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import leon.lang._
-import scala.language.implicitConversions
-
-package object instrumentation {
- @library
- def time: BigInt = 0
-
- @library
- def stack: BigInt = 0
-
- @library
- def rec: BigInt = 0
-
- @library
- def depth: BigInt = 0
-
- @library
- def tpr: BigInt = 0
-}
diff --git a/libtest/src/main/scala/leon/invariant/package.scala b/libtest/src/main/scala/leon/invariant/package.scala
deleted file mode 100644
index 0cc7919d0..000000000
--- a/libtest/src/main/scala/leon/invariant/package.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import leon.lang._
-import scala.language.implicitConversions
-
-package object invariant {
- @library
- def tmpl(templateFunc: BigInt => Boolean): Boolean = true
- @library
- def tmpl(templateFunc: (BigInt, BigInt) => Boolean): Boolean = true
- @library
- def tmpl(templateFunc: (BigInt, BigInt, BigInt) => Boolean): Boolean = true
- @library
- def tmpl(templateFunc: (BigInt, BigInt, BigInt, BigInt) => Boolean): Boolean = true
- @library
- def tmpl(templateFunc: (BigInt, BigInt, BigInt, BigInt, BigInt) => Boolean): Boolean = true
-
- @library
- def ? : BigInt = 0
-
- @library
- def ?(id: BigInt) = id
-}
diff --git a/libtest/src/main/scala/leon/lang/Dummy.scala b/libtest/src/main/scala/leon/lang/Dummy.scala
deleted file mode 100644
index 41dbe4f90..000000000
--- a/libtest/src/main/scala/leon/lang/Dummy.scala
+++ /dev/null
@@ -1,3 +0,0 @@
-package leon.lang
-
-case class Dummy[T]()
diff --git a/libtest/src/main/scala/leon/lang/Either.scala b/libtest/src/main/scala/leon/lang/Either.scala
deleted file mode 100644
index 9cc2ea4e9..000000000
--- a/libtest/src/main/scala/leon/lang/Either.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-
-/**
- * @author Viktor
- */
-@library
-sealed abstract class Either[A,B] {
- def isLeft : Boolean
- def isRight : Boolean
- def swap : Either[B,A]
-}
-@library
-case class Left[A,B](content: A) extends Either[A,B] {
- def isLeft = true
- def isRight = false
- def swap = Right[B,A](content)
-}
-@library
-case class Right[A,B](content: B) extends Either[A,B] {
- def isLeft = false
- def isRight = true
- def swap = Left[B,A](content)
-}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/lang/Map.scala b/libtest/src/main/scala/leon/lang/Map.scala
deleted file mode 100644
index aff6f26f8..000000000
--- a/libtest/src/main/scala/leon/lang/Map.scala
+++ /dev/null
@@ -1,33 +0,0 @@
-package leon.lang
-import leon.annotation._
-
-object Map {
- @library
- @isabelle.function(term = "Map.empty")
- def empty[A,B] = Map[A,B]()
-
- @ignore
- def apply[A,B](elems: (A,B)*) = {
- new Map[A,B](scala.collection.immutable.Map[A,B](elems : _*))
- }
-}
-
-@ignore
-case class Map[A, B] (theMap: scala.collection.immutable.Map[A,B]) {
- def apply(k: A): B = theMap.apply(k)
- def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap)
- def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v))
- def contains(a: A): Boolean = theMap.contains(a)
- def isDefinedAt(a: A): Boolean = contains(a)
-
- def +(kv: (A, B)): Map[A,B] = updated(kv._1, kv._2)
- def +(k: A, v: B): Map[A,B] = updated(k, v)
-
- def getOrElse(k: A, default: B): B = get(k).getOrElse(default)
-
- def get(k: A): Option[B] = if (contains(k)) {
- Some[B](apply(k))
- } else {
- None[B]()
- }
-}
diff --git a/libtest/src/main/scala/leon/lang/Option.scala b/libtest/src/main/scala/leon/lang/Option.scala
deleted file mode 100644
index a6f09db68..000000000
--- a/libtest/src/main/scala/leon/lang/Option.scala
+++ /dev/null
@@ -1,84 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-import leon.collection._
-
-@library
-@isabelle.typ(name = "Option.option")
-sealed abstract class Option[T] {
-
- def get : T = {
- require(this.isDefined)
- (this : @unchecked) match {
- case Some(x) => x
- }
- }
-
- def getOrElse(default: T) = this match {
- case Some(v) => v
- case None() => default
- }
-
- def orElse(or: Option[T]) = { this match {
- case Some(v) => this
- case None() => or
- }} ensuring {
- _.isDefined == this.isDefined || or.isDefined
- }
-
- def isEmpty = this match {
- case Some(v) => false
- case None() => true
- }
-
- def nonEmpty = !isEmpty
-
- def isDefined = !isEmpty
-
-
- // Higher-order API
- @isabelle.function(term = "%x f. Option.map_option f x")
- def map[R](f: T => R) = { this match {
- case None() => None[R]()
- case Some(x) => Some(f(x))
- }} ensuring { _.isDefined == this.isDefined }
-
- @isabelle.function(term = "Option.bind")
- def flatMap[R](f: T => Option[R]) = this match {
- case None() => None[R]()
- case Some(x) => f(x)
- }
-
- def filter(p: T => Boolean) = this match {
- case Some(x) if p(x) => Some(x)
- case _ => None[T]()
- }
-
- def withFilter(p: T => Boolean) = filter(p)
-
- def forall(p: T => Boolean) = this match {
- case Some(x) if !p(x) => false
- case _ => true
- }
-
- def exists(p: T => Boolean) = !forall(!p(_))
-
- // Transformation to other collections
- def toList: List[T] = this match {
- case None() => Nil[T]()
- case Some(x) => List(x)
- }
-
- def toSet: Set[T] = this match {
- case None() => Set[T]()
- case Some(x) => Set(x)
- }
-}
-
-@isabelle.constructor(name = "Option.option.Some")
-case class Some[T](v: T) extends Option[T]
-
-@isabelle.constructor(name = "Option.option.None")
-case class None[T]() extends Option[T]
diff --git a/libtest/src/main/scala/leon/lang/Rational.scala b/libtest/src/main/scala/leon/lang/Rational.scala
deleted file mode 100644
index 1bcb679a0..000000000
--- a/libtest/src/main/scala/leon/lang/Rational.scala
+++ /dev/null
@@ -1,85 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-
-import scala.language.implicitConversions
-
-@library
-case class Rational(numerator: BigInt, denominator: BigInt) {
-
- require(this.isRational)
-
- def +(that: Rational): Rational = {
- Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
-
- def -(that: Rational): Rational = {
- Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
-
- def unary_- : Rational = {
- Rational(-this.numerator, this.denominator)
- } ensuring(res => res.isRational)
-
- def *(that: Rational): Rational = {
- Rational(this.numerator*that.numerator, this.denominator*that.denominator)
- } ensuring(res => res.isRational)
-
- def /(that: Rational): Rational = {
- require(that.nonZero)
- val newNumerator = this.numerator*that.denominator
- val newDenominator = this.denominator*that.numerator
- normalize(newNumerator, newDenominator)
- } ensuring(res => res.isRational)
-
- def reciprocal: Rational = {
- require(this.nonZero)
- normalize(this.denominator, this.numerator)
- } ensuring(res => res.isRational)
-
-
- def ~(that: Rational): Boolean = {
- this.numerator*that.denominator == that.numerator*this.denominator
- }
-
- def <(that: Rational): Boolean = {
- this.numerator*that.denominator < that.numerator*this.denominator
- }
-
- def <=(that: Rational): Boolean = {
- this.numerator*that.denominator <= that.numerator*this.denominator
- }
-
- def >(that: Rational): Boolean = {
- this.numerator*that.denominator > that.numerator*this.denominator
- }
-
- def >=(that: Rational): Boolean = {
- this.numerator*that.denominator >= that.numerator*this.denominator
- }
-
- def nonZero: Boolean = {
- numerator != 0
- }
-
- private def isRational: Boolean = denominator > 0
-
- private def normalize(num: BigInt, den: BigInt): Rational = {
- require(den != 0)
- if(den < 0)
- Rational(-num, -den)
- else
- Rational(num, den)
- }
-}
-
-@library
-object Rational {
-
- implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)
-
- def apply(n: BigInt): Rational = Rational(n, 1)
-
-}
diff --git a/libtest/src/main/scala/leon/lang/Real.scala b/libtest/src/main/scala/leon/lang/Real.scala
deleted file mode 100644
index 9d600b3b6..000000000
--- a/libtest/src/main/scala/leon/lang/Real.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-package leon.lang
-import leon.annotation._
-
-@ignore
-class Real {
-
- def +(a: Real): Real = ???
- def -(a: Real): Real = ???
- def *(a: Real): Real = ???
- def /(a: Real): Real = ???
-
- def unary_- : Real = ???
-
- def > (a: Real): Boolean = ???
- def >=(a: Real): Boolean = ???
- def < (a: Real): Boolean = ???
- def <=(a: Real): Boolean = ???
-
-}
-
-@ignore
-object Real {
- def apply(n: BigInt, d: BigInt): Real = ???
- def apply(n: BigInt): Real = ???
-}
diff --git a/libtest/src/main/scala/leon/lang/Set.scala b/libtest/src/main/scala/leon/lang/Set.scala
deleted file mode 100644
index 8f4595d33..000000000
--- a/libtest/src/main/scala/leon/lang/Set.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-package leon.lang
-import leon.annotation._
-
-object Set {
- @library
- def empty[T] = Set[T]()
-
- @ignore
- def apply[T](elems: T*) = {
- new Set[T](scala.collection.immutable.Set[T](elems : _*))
- }
-}
-
-@ignore
-case class Set[T](val theSet: scala.collection.immutable.Set[T]) {
- def +(a: T): Set[T] = new Set[T](theSet + a)
- def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
- def -(a: T): Set[T] = new Set[T](theSet - a)
- def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
- def size: BigInt = theSet.size
- def contains(a: T): Boolean = theSet.contains(a)
- def isEmpty: Boolean = theSet.isEmpty
- def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
- def &(a: Set[T]): Set[T] = new Set[T](theSet & a.theSet)
-}
-
diff --git a/libtest/src/main/scala/leon/lang/StrOps.scala b/libtest/src/main/scala/leon/lang/StrOps.scala
deleted file mode 100644
index 723ce5be8..000000000
--- a/libtest/src/main/scala/leon/lang/StrOps.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-package leon.lang
-
-import leon.annotation._
-
-/**
- * @author Mikael
- */
-object StrOps {
- @ignore
- def concat(a: String, b: String): String = {
- a + b
- }
- @ignore
- def length(a: String): BigInt = {
- BigInt(a.length)
- }
- @ignore
- def substring(a: String, start: BigInt, end: BigInt): String = {
- if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
- }
- @internal @library
- def escape(s: String): String = s // Wrong definition, but it will eventually use StringEscapeUtils.escapeJava(s) at parsing and compile time.
-}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/lang/package.scala b/libtest/src/main/scala/leon/lang/package.scala
deleted file mode 100644
index ab713a588..000000000
--- a/libtest/src/main/scala/leon/lang/package.scala
+++ /dev/null
@@ -1,85 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import scala.language.implicitConversions
-
-package object lang {
-
- implicit class BooleanDecorations(val underlying: Boolean) {
- @inline
- def holds : Boolean = {
- underlying
- } ensuring {
- _ == true
- }
-
- @inline
- def ==>(that: => Boolean): Boolean = {
- if (underlying) that else true
- }
- }
-
- @ignore def forall[A](p: A => Boolean): Boolean = sys.error("Can't execute quantified proposition")
- @ignore def forall[A,B](p: (A,B) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
- @ignore def forall[A,B,C](p: (A,B,C) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
- @ignore def forall[A,B,C,D](p: (A,B,C,D) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
- @ignore def forall[A,B,C,D,E](p: (A,B,C,D,E) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
-
- @ignore
- object InvariantFunction {
- def invariant(x: Boolean): Unit = ()
- }
-
- @ignore
- implicit def while2Invariant(u: Unit) = InvariantFunction
-
- @ignore
- def error[T](reason: java.lang.String): T = sys.error(reason)
-
- @ignore
- def old[T](value: T): T = value
-
- @ignore
- implicit class Passes[A,B](io : (A,B)) {
- val (in, out) = io
- def passes(tests : A => B ) : Boolean =
- try { tests(in) == out } catch { case _ : MatchError => true }
- }
-
- @ignore
- def byExample[A, B](in: A, out: B): Boolean = {
- sys.error("Can't execute by example proposition")
- }
-
- implicit class SpecsDecorations[A](val underlying: A) {
- @ignore
- def computes(target: A) = {
- underlying
- } ensuring {
- res => res == target
- }
-
- @ignore // Programming by example: ???[String] ask input
- def ask[I](input : I) = {
- underlying
- } ensuring {
- (res: A) => byExample(input, res)
- }
- }
-
- @ignore
- object BigInt {
- def apply(b: Int): scala.math.BigInt = scala.math.BigInt(b)
- def apply(b: String): scala.math.BigInt = scala.math.BigInt(b)
-
- def unapply(b: scala.math.BigInt): scala.Option[Int] = {
- if(b >= Integer.MIN_VALUE && b <= Integer.MAX_VALUE) {
- scala.Some(b.intValue())
- } else {
- scala.None
- }
- }
- }
-}
diff --git a/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala b/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala
deleted file mode 100644
index 7af697638..000000000
--- a/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala
+++ /dev/null
@@ -1,33 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang.synthesis
-
-import leon.annotation._
-import leon.lang._
-
-import scala.annotation._
-
-@implicitNotFound("No Oracle available for this source of non-determinism, please provide an implicit arg <: Oracle[T]")
-@ignore
-@library
-abstract class Oracle[T] {
- def head: T = this match {
- case Node(_, h, _) => h
- case Leaf(h) => h
- }
-
- def left: Oracle[T] = this match {
- case Node(l, _, _) => l
- case Leaf(_) => this
- }
-
- def right: Oracle[T] = this match {
- case Node(_, _, r) => r
- case Leaf(_) => this
- }
-}
-
-@ignore
-case class Node[T](l: Oracle[T], v: T, r: Oracle[T]) extends Oracle[T];
-@ignore
-case class Leaf[T](v: T) extends Oracle[T];
diff --git a/libtest/src/main/scala/leon/lang/synthesis/package.scala b/libtest/src/main/scala/leon/lang/synthesis/package.scala
deleted file mode 100644
index cb5699279..000000000
--- a/libtest/src/main/scala/leon/lang/synthesis/package.scala
+++ /dev/null
@@ -1,41 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-
-import scala.language.implicitConversions
-import scala.annotation.implicitNotFound
-
-package object synthesis {
- @ignore
- private def noImpl = throw new RuntimeException("Synthesis construct implementation not supported")
-
- @ignore
- def choose[A](predicate: A => Boolean): A = noImpl
- @ignore
- def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noImpl
- @ignore
- def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noImpl
- @ignore
- def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noImpl
- @ignore
- def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noImpl
-
- @ignore
- def ???[T]: T = noImpl
-
- @ignore
- def ?[T](e1: T): T = if(???[Boolean]) e1 else ???[T]
-
- @ignore
- def ?[T](e1: T, es: T*): T = noImpl
-
- // Repair with Holes
- @ignore
- def ?: T = noImpl
-
- @ignore
- def withOracle[A, R](body: Oracle[A] => R): R = noImpl
-
-}
diff --git a/libtest/src/main/scala/leon/lang/xlang/package.scala b/libtest/src/main/scala/leon/lang/xlang/package.scala
deleted file mode 100644
index 6f29c5d33..000000000
--- a/libtest/src/main/scala/leon/lang/xlang/package.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-
-package object xlang {
- @ignore
- def waypoint[A](i: Int, expr: A): A = expr
-
- @ignore
- def epsilon[A](pred: (A) => Boolean): A = throw new RuntimeException("Implementation not supported")
-}
diff --git a/libtest/src/main/scala/leon/lazy/package.scala b/libtest/src/main/scala/leon/lazy/package.scala
deleted file mode 100644
index 7c0f57582..000000000
--- a/libtest/src/main/scala/leon/lazy/package.scala
+++ /dev/null
@@ -1,90 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-
-import annotation._
-import lang._
-import scala.language.implicitConversions
-import scala.annotation.StaticAnnotation
-
-package object lazyeval {
-
- @library
- def $[T](f: => T) = Lazy(Unit => f)
- //def apply[T](f: => T) = new $(Unit => f)
-
- @library
- def eager[T](x: => T) = Lazy(Unit => x)
-
- /**
- * implicit conversion from eager evaluation to lazy evaluation
- */
- @library
- @inline
- implicit def eagerToLazy[T](x: T) = eager(x)
-
- /**
- * For accessing in and out states.
- * Should be used only in ensuring.
- */
- @library
- @extern
- def inState[T]: Set[Lazy[T]] = sys.error("inState method is not executable!")
-
- @library
- @extern
- def outState[T]: Set[Lazy[T]] = sys.error("outState method is not executable")
-
- /**
- * Helper class for invoking with a given state instead of the implicit state
- */
- @library
- case class WithState[T](v: T) {
- @extern
- def withState[U](u: Set[Lazy[U]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V](u: Set[Lazy[U]], v: Set[Lazy[V]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V, W](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V, W, X](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]], x: Set[Lazy[X]]): T = sys.error("withState method is not executable!")
- // extend this to more arguments if needed
- }
-
- @library
- @inline
- implicit def toWithState[T](x: T) = new WithState(x)
-
- /**
- * annotations for monotonicity proofs.
- * Note implemented as of now.
- * Let foo be the method that has the annotation.
- * The given name `methodname` should have the following form:
- * m(arg1, ..., argn, substate-Set1,..., substate-Setn, superstate-Set1, ..., superstate-Setn)
- */
- @ignore
- class monoproof(methodname: String) extends StaticAnnotation
-
- @library
- case class Lazy[T](f: Unit => T) {
- @extern
- lazy val value = {
- val x = f(())
- eval = true
- x
- }
- def * = f(())
-
- @ignore
- var eval = false // is this thread safe ?
-
- @extern
- def isEvaluated = eval
-
- @extern
- def isSuspension[T](f: T): Boolean = sys.error("isSuspensionOf method is not executable")
- }
-}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/math/package.scala b/libtest/src/main/scala/leon/math/package.scala
deleted file mode 100644
index 8eb5f3479..000000000
--- a/libtest/src/main/scala/leon/math/package.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-package leon
-import leon.annotation._
-
-package object math {
-
- @library
- def min(i1: Int, i2: Int) = if (i1 <= i2) i1 else i2
-
- @library
- def max(i1: Int, i2: Int) = if (i1 >= i2) i1 else i2
-
- @library
- def min(i1: BigInt, i2: BigInt) = if (i1 <= i2) i1 else i2
-
- @library
- def max(i1: BigInt, i2: BigInt) = if (i1 >= i2) i1 else i2
-
-}
diff --git a/libtest/src/main/scala/leon/mem/package.scala b/libtest/src/main/scala/leon/mem/package.scala
deleted file mode 100644
index 416b737ac..000000000
--- a/libtest/src/main/scala/leon/mem/package.scala
+++ /dev/null
@@ -1,56 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-
-import annotation._
-import lang._
-import scala.language.implicitConversions
-import scala.annotation.StaticAnnotation
-
-package object mem {
-
- @library
- @inline
- implicit def toMem[T](x: T) = new Mem(x)
-
- /**
- * accessing in and out states of mems
- * Should be used only in ensuring.
- */
- @library
- @extern
- def inState[T]: Set[Mem[T]] = sys.error("inState method is not executable!")
-
- @library
- @extern
- def outState[T]: Set[Mem[T]] = sys.error("outState method is not executable")
-
- /**
- * Helper class for invoking with a given state instead of the implicit state
- */
- @library
- case class memWithState[T](v: T) {
- @extern
- def withState[U](u: Set[Mem[U]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V](u: Set[Mem[U]], v: Set[Mem[V]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V, W](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]]): T = sys.error("withState method is not executable!")
-
- @extern
- def withState[U, V, W, X](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]], x: Set[Mem[X]]): T = sys.error("withState method is not executable!")
- // extend this to more arguments if needed
- }
-
- @library
- @inline
- implicit def toWithState[T](x: T) = new memWithState(x)
-
- @library
- case class Mem[T](v: T) {
- @extern
- def isCached: Boolean = sys.error("not implemented!")
- }
-}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/monads/state/State.scala b/libtest/src/main/scala/leon/monads/state/State.scala
deleted file mode 100644
index ad47c2464..000000000
--- a/libtest/src/main/scala/leon/monads/state/State.scala
+++ /dev/null
@@ -1,215 +0,0 @@
-package leon.monads.state
-
-import leon.collection._
-import leon.lang._
-import leon.annotation._
-import State._
-
-
-@library
-case class State[S, A](runState: S => (A, S)) {
-
- /** Basic monadic methods */
-
- // Monadic bind
- @inline
- def flatMap[B](f: A => State[S, B]): State[S, B] = {
- State { s =>
- val (a, newS) = runState(s)
- f(a).runState(newS)
- }
- }
-
- // All monads are also functors, and they define the map function
- @inline
- def map[B](f: A => B): State[S, B] = {
- State { s =>
- val (a, newS) = runState(s)
- (f(a), newS)
- }
- }
-
- @inline
- def >>=[B](f: A => State[S, B]): State[S, B] = flatMap(f)
-
- @inline
- def >>[B](that: State[S, B]) = >>= ( _ => that )
-
- @inline
- // This is unfortunate, but implementing properly would just lead to an error
- def withFilter(f: A => Boolean): State[S, A] = this
-
- @inline
- def eval(s: S) = runState(s)._1
- @inline
- def exec(s: S) = runState(s)._2
-
- // eval with arguments flipped
- @inline
- def >:: (s: S) = eval(s)
-
- def apply(s: S) = runState(s)
-
-}
-
-@library
-object State {
-
- @inline
- def get[A]: State[A, A] = State( a => (a, a) )
-
- @inline
- def gets[S, A](f: S => A): State[S, A] = for {
- s <- get[S]
- } yield f(s)
-
- @inline
- def put[S](s: S): State[S, Unit] = State { _ => ((), s) }
-
- @inline
- def modify[S](f: S => S): State[S, Unit] = for {
- s <- get[S]
- s2 <- put(f(s))
- } yield s2
-
- // Monadic unit
- @inline
- def unit[S, A](a: A): State[S, A] = State { s => (a, s) }
-
- @inline
- def state[S]: State[S, S] = State(s => (s, s))
-
- @inline
- // Left-to-right Kleisli composition of monads
- def >=>[S, A, B, C](f: A => State[S, B], g: B => State[S, C], a: A): State[S, C] = {
- for {
- b <- f(a)
- c <- g(b)
- } yield c
- }
-
- /* Monadic-List functions */
-
- def mapM[A, B, S](f: A => State[S, B], l: List[A]): State[S, List[B]] = {
- l match {
- case Nil() => unit(Nil[B]())
- case Cons(x, xs) => for {
- mx <- f(x)
- mxs <- mapM(f,xs)
- } yield mx :: mxs
- }
- }
-
- def mapM_ [A, B, S] (f: A => State[S, B], l: List[A]): State[S, Unit] = {
- l match {
- case Nil() => unit(())
- case Cons(x, xs) => for {
- mx <- f(x)
- mxs <- mapM_ (f, xs)
- } yield ()
- }
- }
-
- def sequence[S, A](l: List[State[S, A]]): State[S, List[A]] = {
- l.foldRight[State[S, List[A]]](unit(Nil[A]())){
- case (x, xs) => for {
- v <- x
- vs <- xs
- } yield v :: vs
- }
- }
-
- def filterM[S, A](f: A => State[S, Boolean], l: List[A]): State[S, List[A]] = {
- l match {
- case Nil() => unit(Nil[A]())
- case Cons(x, xs) => for {
- flg <- f(x)
- rest <- filterM(f, xs)
- } yield (if (flg) x :: rest else rest)
- }
- }
-
- //(b -> a -> m b) -> b -> t a -> m b
- def foldLeftM[S, A, B](f: (B, A) => State[S, B], z: B, l: List[A]): State[S, B] = {
- l match {
- case Nil() => unit(z)
- case Cons(x, xs) =>
- f(z, x) >>= ( z0 => foldLeftM(f,z0,xs) )
- }
- }
-
- //(b -> a -> m b) -> b -> t a -> m ()
- def foldLeftM_ [S, A](f: A => State[S, Unit], l: List[A]): State[S, Unit] = {
- l match {
- case Nil() => unit(())
- case Cons(x, xs) =>
- f(x) >> foldLeftM_ (f, xs)
- }
- }
-
-}
-
-@library
-object MonadStateLaws {
- /* Monadic laws:
- *
- * return a >>= k = k a
- * m >>= return = m
- * m >>= (x -> k x >>= h) = (m >>= k) >>= h
- *
- * Note: We cannot compare State's directly because State contains an anonymous function.
- * So we have to run them on an initial state.
- */
-
- def unitLeftId[A, B, S](a: A, k: A => State[S, B])(s: S): Boolean = {
- (unit(a) >>= (k))(s) == k(a)(s)
- }.holds
-
- def unitRightId[S, A](m: State[S,A])(s:S): Boolean = {
- (m >>= unit).runState(s) == m.runState(s)
- }.holds
-
- def assoc[S, A, B, C](m: State[S,A], k: A => State[S, B], h: B => State[S, C])(s: S) = {
- (m >>= (x => k(x) >>= h)).runState(s) == (m >>= k >>= h).runState(s)
- }.holds
-
- /* This is the same as assoc, but proves in 42sec instead of 50ms!
- def assoc2[S, A, B, C](m: State[S,A], k: A => State[S, B], h: B => State[S, C])(s: S) = {
- val lhs = for {
- x <- m
- y <- for {
- z <- k(x)
- w <- h(z)
- } yield w
- } yield y
-
- val rhs = for {
- x <- m
- y <- k(x)
- z <- h(y)
- } yield z
-
- lhs.runState(s) == rhs.runState(s)
- }.holds
- */
-
-
- /* The law connecting monad and functor instances:
- *
- * m >>= (return . f) = m map f
- */
-
- def mapToFlatMap[S, A, B](m: State[S, A], f: A => B)(s: S): Boolean = {
- (m >>= (x => unit(f(x)))).runState(s) == (m map f).runState(s)
- }.holds
-
-
- /* Different theorems */
-
- //@induct
- //def mapMVsSequenceM[S, A, B](f: A => State[S, B], l: List[A])(s: S) = {
- // mapM(f, l).runState(s) == sequence(l map f).runState(s)
- //}.holds
-
-
-}
diff --git a/libtest/src/main/scala/leon/package.scala b/libtest/src/main/scala/leon/package.scala
deleted file mode 100644
index 357010d11..000000000
--- a/libtest/src/main/scala/leon/package.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-import leon.annotation._
-import scala.annotation.elidable
-import scala.annotation.elidable._
-
-/**
- * A collection of methods that can be used to collect run-time statistics about Leon programs.
- * This is mostly used to test the resources properties of Leon programs
- */
-package object leon {
-
- /**
- * Stubs of ensuring and require that do not check contracts.
- * Enable this if you want running time statistics without executing contracts.
- */
- @ignore
- implicit class Ensuring[A](private val self: A) extends AnyVal {
- @inline
- def ensuring(cond: A => Boolean): A = { self }
- }
-
- @ignore
- def require(arg: => Boolean) {}
-}
diff --git a/libtest/src/main/scala/leon/par/package.scala b/libtest/src/main/scala/leon/par/package.scala
deleted file mode 100644
index 5842210fc..000000000
--- a/libtest/src/main/scala/leon/par/package.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import leon.lang._
-import leon.lang.synthesis.choose
-
-package object par {
-
- @library
- @inline
- def parallel[A,B](x: => A, y: => B) : (A,B) = {
- (x,y)
- }
-
- @library
- case class Task[A](c: A) {
- def join: A = c
- }
-
- @library
- def task[A](c: A) = Task(c)
-}
diff --git a/libtest/src/main/scala/leon/proof/Internal.scala b/libtest/src/main/scala/leon/proof/Internal.scala
deleted file mode 100644
index 0962c371c..000000000
--- a/libtest/src/main/scala/leon/proof/Internal.scala
+++ /dev/null
@@ -1,63 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-package leon.proof
-
-import leon.lang._
-import leon.annotation._
-
-/** Internal helper classes and methods for the 'proof' package. */
-object Internal {
-
- /*** Helper classes for relational reasoning ***/
- @library
- case class WithRel[A, B](x: A, r: (A, B) => Boolean, prop: Boolean) {
-
- /** Continue with the next relation. */
- def ^^(y: B): RelReasoning[B] = {
- require(prop ==> r(x, y))
- RelReasoning(y, prop && r(x, y))
- }
-
- /** Add a proof. */
- def ^^|(proof: Boolean): WithProof[A, B] = {
- require(proof)
- WithProof(x, r, proof, prop)
- }
-
- /** Short-hand for equational reasoning. */
- def ==|(proof: Boolean): WithProof[A, A] = {
- require(proof)
- WithProof(x, _ == _, proof, prop)
- }
-
- def qed: Boolean = prop
- }
-
- @library
- case class WithProof[A, B](
- x: A, r: (A, B) => Boolean, proof: Boolean, prop: Boolean) {
-
- /** Close a proof. */
- def |[C](that: WithProof[B, C]): WithProof[B, C] = {
- require(this.prop && this.proof ==> this.r(this.x, that.x))
- WithProof(
- that.x, that.r, that.proof,
- this.prop && this.proof && this.r(this.x, that.x))
- }
-
- /** Close a proof. */
- def |[C](that: WithRel[B, C]): WithRel[B, C] = {
- require(this.prop && this.proof ==> this.r(this.x, that.x))
- WithRel(
- that.x, that.r,
- this.prop && this.proof && this.r(this.x, that.x))
- }
-
- /** Close a proof. */
- def |(that: RelReasoning[B]): RelReasoning[B] = {
- require(this.prop && this.proof ==> this.r(this.x, that.x))
- RelReasoning(
- that.x,
- this.prop && this.proof && this.r(this.x, that.x))
- }
- }
-}
diff --git a/libtest/src/main/scala/leon/proof/package.scala b/libtest/src/main/scala/leon/proof/package.scala
deleted file mode 100644
index 3f0978649..000000000
--- a/libtest/src/main/scala/leon/proof/package.scala
+++ /dev/null
@@ -1,66 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-package leon
-
-import leon.annotation._
-import leon.lang._
-import scala.language.implicitConversions
-
-import leon.proof.Internal._
-
-package object proof {
-
- @library
- case class ProofOps(prop: Boolean) {
- def because(proof: Boolean): Boolean = proof && prop
- def neverHolds: Boolean = {
- require(!prop)
- !prop
- }
- }
-
- @library
- implicit def boolean2ProofOps(prop: Boolean): ProofOps = ProofOps(prop)
-
- @library
- def trivial: Boolean = true
-
- @library
- def by(proof: Boolean)(prop: Boolean): Boolean =
- proof && prop
-
- @library
- def check(prop: Boolean): Boolean = {
- require(prop)
- prop
- }
-
- /**
- * Relational reasoning.
- *
- * {
- * ((y :: ys) :+ x).last ^^ _ == _ ^^| trivial |
- * (y :: (ys :+ x)).last ==| trivial |
- * (ys :+ x).last ==| snocLast(ys, x) |
- * x
- * }.qed
- */
- @library
- case class RelReasoning[A](x: A, prop: Boolean) {
-
- def ^^[B](r: (A, B) => Boolean): WithRel[A, B] = WithRel(x, r, prop)
-
- /** Short-hand for equational reasoning. */
- def ==|(proof: Boolean): WithProof[A, A] = {
- require(proof)
- WithProof(x, _ == _, proof, prop)
- }
-
- def qed: Boolean = prop
- }
-
- @library
- implicit def any2RelReasoning[A](x: A): RelReasoning[A] =
- RelReasoning(x, true)
-
-}
-
diff --git a/libtest/src/main/scala/leon/stats/package.scala b/libtest/src/main/scala/leon/stats/package.scala
deleted file mode 100644
index 17d6286b6..000000000
--- a/libtest/src/main/scala/leon/stats/package.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import leon.annotation._
-import java.lang.management._
-import scala.collection.JavaConversions._
-
-/**
- * A collection of methods that can be used to collect run-time statistics about Leon programs.
- * This is mostly used to test the resources properties of Leon programs
- */
-package object stats {
- @ignore
- def timed[T](code: => T)(cont: Long => Unit): T = {
- var t1 = System.currentTimeMillis()
- val r = code
- cont((System.currentTimeMillis() - t1))
- r
- }
-
- @ignore
- def withTime[T](code: => T): (T, Long) = {
- var t1 = System.currentTimeMillis()
- val r = code
- (r, (System.currentTimeMillis() - t1))
- }
-}
diff --git a/synthesis-collective.txt b/synthesis-collective.txt
deleted file mode 100644
index 84d508e24..000000000
--- a/synthesis-collective.txt
+++ /dev/null
@@ -1,36 +0,0 @@
-Versions: X-X-N for CEGIS(o/n), grammar(o/n), max. size
-✓ = Proof
-? = no proof
-x = invalid solution
-F = Timeout/failed to synth.
-
-
-==============================================================================================================================================
-Name | FDefs| Size | O-O-5 | O-O-7 | 0515ff9 | 75d4219 | 5a22c2f | 4cdcc91 | de6a3a0 | 4fd7f51 | 4b10561 |
-==============================================================================================================================================
-List.insert | 59 | 3 | ✓ | 0.8 | ✓ | 1.0 | ✓ | 0.7 | ✓ | 0.5 | ✓ | 0.5 | ✓ | 0.6 | ✓ | 0.6 | ✓ | 0.5 | ✓ | 0.6 |
-List.delete | 61 | 0 | ✓ | 4.5 | F | 30.1 | ✓ | 3.2 | ✓ | 5.4 | ✓ | 5.4 | ✓ | 6.3 | ✓ | 6.8 | ✓ | 7.0 | ✓ | 9.6 |
-List.union | 75 | 11 | ✓ | 7.1 | ✓ | 12.5 | ✓ | 3.5 | ✓ | 1.7 | ✓ | 1.9 | ✓ | 1.9 | ✓ | 1.9 | ✓ | 1.7 | ✓ | 2.3 |
-List.diff | 106 | 0 | ✓ | 6.1 | F | 31.8 | ✓ | 11.2 | ✓ | 9.1 | ✓ | 10.1 | ✓ | 10.8 | ✓ | 10.8 | ✓ | 10.1 | ✓ | 13.0 |
-List.split*(easier for O-O) | 96 | 24 | ✓ | 3.6 | ✓ | 5.3 | ✓ | 2.6 | ✓ | 2.2 | ✓ | 2.3 | ✓ | 2.6 | ✓ | 2.6 | ✓ | 3.5 | ✓ | 15.7 |
-List.listOfSize | 54 | 11 | | | | | | | | | | | | | ✓ | 1.5 | ✓ | 1.1 | ✓ | 1.7 |
-SortedList.insert | 91 | 0 | ? | 16.5 | F | 30.0 | ? | 23.6 | ? | 11.8 | ? | 11.8 | ? | 10.6 | ? | 11.0 | ? | 11.5 | ? | 16.9 |
-SortedList.insertAlways | 105 | 0 | ✓ | 20.5 | F | 30.0 | ✓ | 40.8 | ✓ | 22.2 | ✓ | 23.2 | ✓ | 21.9 | ✓ | 21.2 | ✓ | 23.7 | ✓ | 25.9 |
-SortedList.delete | 91 | 0 | ? | 7.9 | F | 30.0 | ? | 5.7 | ? | 9.5 | ? | 9.6 | ? | 10.2 | ? | 9.5 | ? | 10.4 | ? | 16.4 |
-SortedList.union | 138 | 11 | ✓ | 6.9 | ✓ | 15.1 | ✓ | 4.0 | ✓ | 2.1 | ✓ | 2.5 | ✓ | 3.6 | ✓ | 2.1 | ✓ | 3.2 | ✓ | 2.8 |
-SortedList.diff | 136 | 0 | ✓ | 5.9 | F | 51.7 | ✓ | 7.7 | ✓ | 7.0 | ✓ | 5.2 | ✓ | 8.0 | ✓ | 5.2 | ✓ | 5.8 | ✓ | 7.1 |
-SortedList.insertionSort | 125 | 10 | ✓ | 1.9 | ✓ | 3.5 | ✓ | 1.7 | ✓ | 1.3 | ✓ | 4.6 | ✓ | 3.2 | ✓ | 1.6 | ✓ | 4.3 | ✓ | 2.4 |
-StrictSortedList.insert | 91 | 0 | ✓ | 13.1 | F | 30.0 | ✓ | 23.4 | ✓ | 9.5 | ✓ | 9.9 | ✓ | 9.5 | ✓ | 10.2 | ✓ | 10.0 | ✓ | 14.3 |
-StrictSortedList.delete | 91 | 0 | ? | 10.2 | F | 30.0 | ✓ | 5.6 | ✓ | 12.7 | ✓ | 12.8 | ✓ | 12.4 | ✓ | 12.9 | ✓ | 12.9 | ✓ | 16.5 |
-StrictSortedList.union | 138 | 11 | ✓ | 7.6 | ✓ | 13.6 | ✓ | 4.7 | ✓ | 2.9 | ✓ | 2.1 | ✓ | 2.0 | ✓ | 2.1 | ✓ | 2.1 | ✓ | 3.4 |
-UnaryNumerals.add | 42 | 9 | ✓ | 4.3 | ✓ | 4.1 | ✓ | 2.2 | ✓ | 1.8 | ✓ | 1.7 | ✓ | 1.6 | ✓ | 1.8 | ✓ | 1.7 | ✓ | 2.1 |
-UnaryNumerals.distinct | 66 | 4 | ✓ | 2.4 | ✓ | 2.3 | ✓ | 1.1 | ✓ | 0.8 | ✓ | 0.9 | ✓ | 1.8 | ✓ | 1.9 | ✓ | 2.1 | ✓ | 2.3 |
-UnaryNumerals.mult | 64 | 10 | ✓ | 4.5 | ✓ | 10.5 | ✓ | 4.4 | ✓ | 3.5 | ✓ | 4.0 | ✓ | 4.3 | ✓ | 4.5 | ✓ | 4.4 | ✓ | 5.1 |
-BatchedQueue.enqueue | 89 | 20 | F | 30.0 | ? | 19.7 | ? | 10.0 | ? | 10.9 | ? | 10.6 | ? | 11.2 | ? | 11.1 | ? | 11.6 | ? | 12.4 |
-BatchedQueue.dequeue | 65 | 9 | ? | 14.3 | ? | 11.4 | ? | 13.3 | ? | 17.0 | ? | 17.3 | ? | 18.2 | ? | 18.2 | ? | 19.2 | ? | 19.5 |
-AddressBook.makeAddressBook | 42 | 0 | F | 14.3 | F | 30.0 | ✓ | 6.7 | ✓ | 6.3 | ✓ | 5.5 | ✓ | 3.9 | ✓ | 4.0 | ✓ | 4.3 | ✓ | 4.4 |
-AddressBook.merge | 99 | 11 | ? | 6.9 | ? | 9.5 | ? | 9.9 | ? | 13.4 | ? | 13.5 | ? | 13.5 | ? | 13.6 | ? | 13.4 | ? | 19.8 |
-RunLength.encode | 110 | 38 | | | | | ✓ | 54.0 | ✓ | 59.1 | ✓ | 42.9 | ✓ | 36.1 | ✓ | 24.7 | ✓ | 44.8 | ✓ | 17.8 |
-Diffs.diffs | 63 | 22 | | | | | ✓ | 20.0 | ✓ | 17.9 | ✓ | 16.5 | ✓ | 11.5 | ✓ | 11.8 | ✓ | 13.4 | ✓ | 29.9 |
-==============================================================================================================================================
-
--
GitLab