From 7a12c40b47e4fc4b26155331e7ec5b5af8ded3f6 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 6 May 2015 17:50:26 +0200
Subject: [PATCH] Remove traces of Gives
---
library/lang/package.scala | 5 -----
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../leon/frontends/scalac/ASTExtractors.scala | 22 -------------------
.../scala/leon/synthesis/ConvertHoles.scala | 2 +-
4 files changed, 2 insertions(+), 29 deletions(-)
diff --git a/library/lang/package.scala b/library/lang/package.scala
index c9755e885..a80e25cba 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -27,11 +27,6 @@ package object lang {
@ignore
def error[T](reason: java.lang.String): T = sys.error(reason)
-
- @ignore
- implicit class Gives[A](v : A) {
- def gives[B](tests : A => B) : B = tests(v)
- }
@ignore
implicit class Passes[A,B](io : (A,B)) {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 8858fbf3b..c8ddeba0a 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -111,7 +111,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Hole(_,_) => true
case _ => false
}(en))
- e(convertHoles(en, ctx, true))
+ e(convertHoles(en, ctx))
else
e(en.toAssert)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index e83f51196..06ab50a2e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -170,28 +170,6 @@ trait ASTExtractors {
case _ => None
}
}
-
- object ExGives {
- def unapply(tree : Apply) : Option[(Tree, List[CaseDef])] = tree match {
- case Apply(
- TypeApply(
- Select(
- Apply(
- TypeApply(
- ExSelected("leon", "lang", "package", "Gives"),
- _ :: Nil
- ),
- body :: Nil
- ),
- ExNamed("gives")
- ),
- _ :: Nil
- ),
- (Function((_ @ ValDef(_, _, _, EmptyTree)) :: Nil, ExpressionExtractors.ExPatternMatching(_,tests))) :: Nil)
- => Some((body, tests))
- case _ => None
- }
- }
object ExPasses {
def unapply(tree : Apply) : Option[(Tree, Tree, List[CaseDef])] = tree match {
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 96c3118b5..3d9183a7b 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -37,7 +37,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
*
*/
- def convertHoles(e : Expr, ctx : LeonContext, treatGives : Boolean = false) : Expr = {
+ def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
val (pre, body, post) = breakDownSpecs(e)
// Ensure that holes are not found in pre and/or post conditions
--
GitLab