From ce3c5dfdf093800b3a162455f140186ab8b02ef7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 25 Feb 2016 18:24:25 +0100
Subject: [PATCH] Remove Waypoint
---
library/lang/xlang/package.scala | 3 --
.../leon/frontends/scalac/ASTExtractors.scala | 10 ------
.../frontends/scalac/CodeExtraction.scala | 5 ---
.../leon/solvers/z3/AbstractZ3Solver.scala | 35 ++++++-------------
src/main/scala/leon/xlang/Expressions.scala | 12 -------
.../leon/xlang/NoXLangFeaturesChecking.scala | 2 --
6 files changed, 10 insertions(+), 57 deletions(-)
diff --git a/library/lang/xlang/package.scala b/library/lang/xlang/package.scala
index 6f29c5d33..75efd0103 100644
--- a/library/lang/xlang/package.scala
+++ b/library/lang/xlang/package.scala
@@ -5,9 +5,6 @@ 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/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index f8509be9c..b0885825c 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -602,16 +602,6 @@ trait ASTExtractors {
}
}
- object ExWaypointExpression {
- def unapply(tree: Apply) : Option[(Tree, Tree, Tree)] = tree match {
- case Apply(
- TypeApply(ExSymbol("leon", "lang", "xlang", "waypoint"), typeTree :: Nil),
- List(i, expr)) =>
- Some((typeTree, i, expr))
- case _ => None
- }
- }
-
object ExErrorExpression {
def unapply(tree: Apply) : Option[(String, Tree)] = tree match {
case a @ Apply(TypeApply(ExSymbol("leon", "lang", "error"), List(tpe)), List(lit : Literal)) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0451b4c08..4b3c577ad 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1267,11 +1267,6 @@ trait CodeExtraction extends ASTExtractors {
}
Epsilon(c1, pstpe)
- case ExWaypointExpression(tpt, i, tree) =>
- val pstpe = extractType(tpt)
- val IntLiteral(ri) = extractTree(i)
- Waypoint(ri, extractTree(tree), pstpe)
-
case update @ ExUpdate(lhs, index, newValue) =>
val lhsRec = extractTree(lhs)
lhsRec match {
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7ad5c222b..84715bb73 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -13,7 +13,6 @@ import purescala.Constructors._
import purescala.Extractors._
import purescala.Expressions._
import purescala.TypeOps._
-import xlang.Expressions._
import purescala.ExprOps._
import purescala.Types._
@@ -271,7 +270,7 @@ trait AbstractZ3Solver extends Solver {
def rec(ex: Expr): Z3AST = ex match {
// TODO: Leave that as a specialization?
- case LetTuple(ids, e, b) => {
+ case LetTuple(ids, e, b) =>
z3Vars = z3Vars ++ ids.zipWithIndex.map { case (id, ix) =>
val entry = id -> rec(tupleSelect(e, ix + 1, ids.size))
entry
@@ -279,7 +278,6 @@ trait AbstractZ3Solver extends Solver {
val rb = rec(b)
z3Vars = z3Vars -- ids
rb
- }
case p @ Passes(_, _, _) =>
rec(p.asConstraint)
@@ -287,40 +285,30 @@ trait AbstractZ3Solver extends Solver {
case me @ MatchExpr(s, cs) =>
rec(matchToIfThenElse(me))
- case Let(i, e, b) => {
+ case Let(i, e, b) =>
val re = rec(e)
z3Vars = z3Vars + (i -> re)
val rb = rec(b)
z3Vars = z3Vars - i
rb
- }
- case Waypoint(_, e, _) => rec(e)
case a @ Assert(cond, err, body) =>
rec(IfExpr(cond, body, Error(a.getType, err.getOrElse("Assertion failed")).setPos(a.getPos)).setPos(a.getPos))
- case e @ Error(tpe, _) => {
+ case e @ Error(tpe, _) =>
val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
// Might introduce dupplicates (e), but no worries here
variables += (e -> newAST)
newAST
- }
- case v @ Variable(id) => z3Vars.get(id) match {
- case Some(ast) =>
- ast
- case None => {
- variables.getB(v) match {
- case Some(ast) =>
- ast
-
- case None =>
+
+ case v @ Variable(id) => z3Vars.getOrElse(id,
+ variables.getB(v).getOrElse {
val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
z3Vars = z3Vars + (id -> newAST)
variables += (v -> newAST)
newAST
}
- }
- }
+ )
case ite @ IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e))
case And(exs) => z3.mkAnd(exs.map(rec): _*)
@@ -337,7 +325,7 @@ trait AbstractZ3Solver extends Solver {
case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
case Minus(l, r) => z3.mkSub(rec(l), rec(r))
case Times(l, r) => z3.mkMul(rec(l), rec(r))
- case Division(l, r) => {
+ case Division(l, r) =>
val rl = rec(l)
val rr = rec(r)
z3.mkITE(
@@ -345,14 +333,11 @@ trait AbstractZ3Solver extends Solver {
z3.mkDiv(rl, rr),
z3.mkUnaryMinus(z3.mkDiv(z3.mkUnaryMinus(rl), rr))
)
- }
- case Remainder(l, r) => {
+ case Remainder(l, r) =>
val q = rec(Division(l, r))
z3.mkSub(rec(l), z3.mkMul(rec(r), q))
- }
- case Modulo(l, r) => {
+ case Modulo(l, r) =>
z3.mkMod(rec(l), rec(r))
- }
case UMinus(e) => z3.mkUnaryMinus(rec(e))
case RealPlus(l, r) => z3.mkAdd(rec(l), rec(r))
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index 98214ee64..0f1dd6b98 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -119,18 +119,6 @@ object Expressions {
override def isSimpleExpr = false
}
- case class Waypoint(i: Int, expr: Expr, tpe: TypeTree) extends XLangExpr with Extractable with PrettyPrintable{
- def extract: Option[(Seq[Expr], Seq[Expr]=>Expr)] = {
- Some((Seq(expr), (es: Seq[Expr]) => Waypoint(i, es.head, tpe)))
- }
-
- def printWith(implicit pctx: PrinterContext) {
- p"waypoint_$i($expr)"
- }
-
- val getType = tpe
- }
-
case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends XLangExpr with Extractable with PrettyPrintable {
val getType = UnitType
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index d054887e9..9c4330ca7 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -29,8 +29,6 @@ object NoXLangFeaturesChecking extends UnitPhase[Program] {
Set((e.getPos, "Usage of epsilons requires xlang desugaring"))
case (e: LetVar) =>
Set((e.getPos, "Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring"))
- case (e: Waypoint) =>
- Set((e.getPos, "Usage of waypoints requires xlang desugaring"))
case (e: ArrayUpdate) =>
Set((e.getPos, "In-place updates of arrays require xlang desugaring"))
case _ =>
--
GitLab