diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e1de9e64c26b540869648f849008808ea6dcad0b..8858fbf3b65f67d4fe51cad9fd52ee020e526129 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -109,7 +109,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case en@Ensuring(body, post) =>
if ( exists{
case Hole(_,_) => true
- case Gives(_,_) => true
case _ => false
}(en))
e(convertHoles(en, ctx, true))
@@ -493,8 +492,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case gv: GenericValue =>
gv
- case g : Gives =>
- e(convertHoles(g, ctx, true))
case p : Passes =>
e(p.asConstraint)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 408cdfe167df64eae4f30d0b411b25b57d740dba..03f1d1778f8c2927a2de91f98fd77acdd08a3ac0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1124,11 +1124,6 @@ trait CodeExtraction extends ASTExtractors {
}
passes(ine, oute, rc)
- case ExGives(sel, cses) =>
- val rs = extractTree(sel)
- val rc = cses.map(extractMatchCase)
- gives(rs, rc)
-
case ExArrayLiteral(tpe, args) =>
finiteArray(args.map(extractTree), None, extractType(tpe)(dctx, current.pos))
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 98b46fb1f3eb9c27287b33c516e27b3533fb2129..0bc69cb3b74c4018dbf63f0a055697a2f1d8bf74 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -105,9 +105,6 @@ object Constructors {
}
}
- def gives(scrutinee : Expr, cases : Seq[MatchCase]) : Gives =
- Gives(scrutinee, filterCases(scrutinee.getType, None, cases))
-
def passes(in : Expr, out : Expr, cases : Seq[MatchCase]): Expr = {
val resultingCases = filterCases(in.getType, Some(out.getType), cases)
if (resultingCases.nonEmpty) {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 894a77a855959fb0f245494b12aa9e9e63134617..0d56b84ac940c58fb19e36ef02d6fe0175d8e613 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -355,7 +355,7 @@ object ExprOps {
case Variable(i) => subvs + i
case LetDef(fd,_) => subvs -- fd.params.map(_.id)
case Let(i,_,_) => subvs - i
- case MatchLike(_, cses, _) => subvs -- cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b)
+ case MatchExpr(_, cses) => subvs -- cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b)
case Passes(_, _ , cses) => subvs -- cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b)
case Lambda(args, body) => subvs -- args.map(_.id)
case Forall(args, body) => subvs -- args.map(_.id)
@@ -432,8 +432,8 @@ object ExprOps {
postMap({
- case m @ MatchLike(s, cses, builder) =>
- Some(builder(s, cses.map(freshenCase)).copiedFrom(m))
+ case m @ MatchExpr(s, cses) =>
+ Some(matchExpr(s, cses.map(freshenCase)).copiedFrom(m))
case p @ Passes(in, out, cses) =>
Some(Passes(in, out, cses.map(freshenCase)).copiedFrom(p))
@@ -621,7 +621,7 @@ object ExprOps {
case v @ Variable(id) if s.isDefinedAt(id) => rec(s(id), s)
case l @ Let(i,e,b) => rec(b, s + (i -> rec(e, s)))
case i @ IfExpr(t1,t2,t3) => IfExpr(rec(t1, s),rec(t2, s),rec(t3, s))
- case m @ MatchLike(scrut,cses,builder) => builder(rec(scrut, s), cses.map(inCase(_, s))).setPos(m)
+ case m @ MatchExpr(scrut, cses) => matchExpr(rec(scrut, s), cses.map(inCase(_, s))).setPos(m)
case p @ Passes(in, out, cses) => Passes(rec(in, s), rec(out,s), cses.map(inCase(_, s))).setPos(p)
case n @ NAryOperator(args, recons) => {
var change = false
@@ -852,10 +852,6 @@ object ExprOps {
// This introduces a MatchExpr
Some(p.asConstraint)
- case g: Gives =>
- // This introduces a MatchExpr
- Some(g.asMatch)
-
case _ => None
}
@@ -1236,7 +1232,7 @@ object ExprOps {
case t: Terminal =>
1
- case ml: MatchLike =>
+ case ml: MatchExpr =>
ml.cases.foldLeft(formulaSize(ml.scrutinee)) {
case (s, MatchCase(p, og, rhs)) =>
s + formulaSize(rhs) + og.map(formulaSize).getOrElse(0) + patternSize(p)
@@ -1262,7 +1258,6 @@ object ExprOps {
case Hole(_, _) => return false
//@EK FIXME: do we need it?
//case Error(_, _) => return false
- case Gives(_,_) => return false
case _ =>
}(e)
true
@@ -1496,7 +1491,7 @@ object ExprOps {
fdHomo(fd1, fd2) &&
isHomo(e1, e2)(map + (fd1.id -> fd2.id))
- case Same(MatchLike(s1, cs1, _), MatchLike(s2, cs2, _)) =>
+ case (MatchExpr(s1, cs1), MatchExpr(s2, cs2)) =>
cs1.size == cs2.size && isHomo(s1, s2) && casesMatch(cs1,cs2)
case (Passes(in1, out1, cs1), Passes(in2, out2, cs2)) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 2f793f5b17b2d14f127739308718e2a1d3c40742..596ddc2df4264294c2793a1065bf9a927762f65c 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -155,27 +155,11 @@ object Expressions {
}
}
- abstract sealed class MatchLike extends Expr {
- val scrutinee : Expr
- val cases : Seq[MatchCase]
- val getType = leastUpperBound(cases.map(_.rhs.getType)).getOrElse(Untyped).unveilUntyped
- }
-
- case class MatchExpr(scrutinee: Expr, cases: Seq[MatchCase]) extends MatchLike {
+ case class MatchExpr(scrutinee: Expr, cases: Seq[MatchCase]) extends Expr {
require(cases.nonEmpty)
+ val getType = leastUpperBound(cases.map(_.rhs.getType)).getOrElse(Untyped).unveilUntyped
}
- case class Gives(scrutinee: Expr, cases : Seq[MatchCase]) extends MatchLike {
- def asMatchWithHole = {
- val theHole = SimpleCase(WildcardPattern(None), Hole(this.getType, Seq()))
- MatchExpr(scrutinee, cases :+ theHole)
- }
-
- def asMatch = {
- matchExpr(scrutinee, cases)
- }
- }
-
case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends Expr {
require(cases.nonEmpty)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 1059f1be6015340e03d14050ffc5cd13c9f9339f..d3186cde0176c0e7e24c5e81886879e22b16365f 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -142,7 +142,7 @@ object Extractors {
Seq(cond, thenn, elze),
(as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))
))
- case MatchLike(scrut, cases, builder) => Some((
+ case MatchExpr(scrut, cases) => Some((
scrut +: cases.flatMap {
case SimpleCase(_, e) => Seq(e)
case GuardedCase(_, e1, e2) => Seq(e1, e2)
@@ -154,7 +154,7 @@ object Extractors {
case GuardedCase(b, _, _) => i+=2; GuardedCase(b, es(i-2), es(i-1))
}
- builder(es(0), newcases)
+ matchExpr(es(0), newcases)
}
))
case Passes(in, out, cases) => Some((
@@ -303,17 +303,6 @@ object Extractors {
None
}
}
-
- object MatchLike {
- def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => Expr)] = {
- Option(m) map { m =>
- (m.scrutinee, m.cases, m match {
- case _ : MatchExpr => matchExpr
- case _ : Gives => gives
- })
- }
- }
- }
object SimpleCase {
def apply(p : Pattern, rhs : Expr) = MatchCase(p, None, rhs)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 44d4e90bfc6880d1683ddbcadc90f1e05afe793f..c312ad18fe6000ab5f583ab131ebe26de5ecb5d5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -206,13 +206,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
| $post
|}"""
- case Gives(s, tests) =>
- optP {
- p"""|$s gives {
- | ${nary(tests, "\n")}
- |}"""
- }
-
case p@Passes(in, out, tests) =>
optP {
p"""|($in, $out) passes {
@@ -749,7 +742,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
case (_, Some(_: FunctionInvocation)) => false
case (ie: IfExpr, _) => true
- case (me: MatchLike, _ ) => true
+ case (me: MatchExpr, _ ) => true
case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
case (_, _) => true
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 958fcaac4f909f5e6d37ad43c43b2bf7b04c7587..3781cb3e536928eb3f4a0fc4a3edc3d5dd6d1821 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -202,7 +202,6 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
*/
case m : MatchExpr => sys.error("'MatchExpr's should have been eliminated before generating templates.")
case p : Passes => sys.error("'Passes's should have been eliminated before generating templates.")
- case g : Gives => sys.error("'Gives' should have been eliminated before generating templates.")
case i @ Implies(lhs, rhs) =>
implies(rec(pathVar, lhs), rec(pathVar, rhs))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index d0d02f9faa096f299f64ea59015653278d40ae4d..f2303d6997c26ddd59a6ffac08e1fc07c6fc2fc2 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -514,9 +514,6 @@ trait AbstractZ3Solver
case me @ MatchExpr(s, cs) =>
rec(matchToIfThenElse(me))
-
- case g @ Gives(scrut, tests) =>
- rec(g.asMatch)
case tu @ Tuple(args) =>
typeToSort(tu.getType) // Make sure we generate sort & meta info
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index de1e5d2721041d6883e94ed6632493e243dc7bc2..96c3118b52febb9817e9fd75b9bd83ffd185c225 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -54,8 +54,6 @@ object ConvertHoles extends LeonPhase[Program, Program] {
var holes = List[Identifier]()
val withoutHoles = preMap {
- case p : Gives if treatGives =>
- Some(p.asMatchWithHole)
case h : Hole =>
val (expr, ids) = toExpr(h)