From d04c3bc006bc30aae67b784b68c13c071d5ae2b1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 12 Feb 2015 15:20:51 +0100
Subject: [PATCH] Remove unused RepairHole
---
src/main/scala/leon/codegen/CodeGeneration.scala | 3 ---
.../scala/leon/evaluators/RecursiveEvaluator.scala | 3 ---
.../scala/leon/frontends/scalac/ASTExtractors.scala | 10 ----------
.../scala/leon/frontends/scalac/CodeExtraction.scala | 5 -----
src/main/scala/leon/purescala/PrettyPrinter.scala | 3 ---
src/main/scala/leon/purescala/TreeOps.scala | 1 -
src/main/scala/leon/purescala/Trees.scala | 8 --------
.../leon/solvers/templates/TemplateGenerator.scala | 6 ------
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 5 -----
9 files changed, 44 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 0540745f1..f83c724db 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -672,9 +672,6 @@ trait CodeGeneration {
ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
ch << ATHROW
- case rh: RepairHole =>
- mkExpr(simplestValue(rh.getType), ch) // It is expected to be invalid, we want to repair it
-
case Choose(_, _, Some(e)) =>
mkExpr(e, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 747a5d52b..6eb4323b4 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -393,9 +393,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case gv: GenericValue =>
gv
- case rh: RepairHole =>
- simplestValue(rh.getType) // It will be wrong, we don't care
-
case g : Gives =>
e(convertHoles(g, ctx, true))
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index a7b5f1e87..0424350cf 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -421,16 +421,6 @@ trait ASTExtractors {
}
}
- object ExRepairHoleExpression {
- def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
- case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$bang"), List(tpt)), args1) =>
- Some((tpt, args1))
- case TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$bang"), List(tpt)) =>
- Some((tpt, Nil))
- case _ => None
- }
- }
-
object ExHoleExpression {
def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b98faa52f..bbfffc373 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1229,11 +1229,6 @@ trait CodeExtraction extends ASTExtractors {
Hole(extractType(tpt), exprs.map(extractTree))
- case hole @ ExRepairHoleExpression(tpt, exprs) =>
- val leonExprs = exprs.map(extractTree)
-
- RepairHole(extractType(tpt), exprs.map(extractTree))
-
case ops @ ExWithOracleExpression(oracles, body) =>
val newOracles = oracles map { case (tpt, sym) =>
val aTpe = extractType(tpt)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fa16449fa..de7052e22 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -240,9 +240,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
| $pred
|}"""
- case h @ RepairHole(tpe, es) =>
- p"""|?"""
-
case h @ Hole(tpe, es) =>
if (es.isEmpty) {
p"""|???[$tpe]"""
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index ebba57547..801469a6b 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1409,7 +1409,6 @@ object TreeOps {
preTraversal{
case Choose(_, _, None) => return false
case Hole(_, _) => return false
- case RepairHole(_, _) => return false
case Gives(_,_) => return false
case _ =>
}(e)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 421d97600..052dd2305 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -477,14 +477,6 @@ object Trees {
}
}
- case class RepairHole(tpe: TypeTree, components: Seq[Expr]) extends Expr with NAryExtractable {
- val getType = tpe
-
- def extract = {
- Some((components, (es: Seq[Expr]) => RepairHole(tpe, es).setPos(this)))
- }
- }
-
/**
* DEPRECATED TREES
* These trees are not guaranteed to be supported by Leon.
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index cdad71b88..a570d9597 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -264,15 +264,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
}
}
- case h @ RepairHole(_, _) =>
- val hid = FreshIdentifier("hole", true).setType(h.getType)
- exprVars += hid
- Variable(hid)
-
case c @ Choose(ids, cond, Some(impl)) =>
rec(pathVar, impl)
-
case c @ Choose(ids, cond, None) =>
val cid = FreshIdentifier("choose", true).setType(c.getType)
storeExpr(cid)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 51dc20d56..02b6683c4 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -676,11 +676,6 @@ trait AbstractZ3Solver
case gv @ GenericValue(tp, id) =>
z3.mkApp(genericValueToDecl(gv))
- case h @ RepairHole(_, _) =>
- val newAST = z3.mkFreshConst("hole", typeToSort(h.getType))
- variables += (h -> newAST)
- newAST
-
case _ => {
reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex)
throw new CantTranslateException
--
GitLab