From 2b27915b4e523cfd6aae90b629a95706a795ace7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 26 Oct 2012 19:25:39 +0200
Subject: [PATCH] Define choose as an extractable
---
src/main/scala/leon/purescala/TreeOps.scala | 14 ++++++++++----
src/main/scala/leon/purescala/Trees.scala | 5 ++++-
2 files changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2938be18e..0e63a4a27 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -960,24 +960,30 @@ object TreeOps {
val (expr, ctx) = pre(eIn, cIn)
val (newExpr, newC) = expr match {
+ case t: Terminal =>
+ (expr, ctx)
+
case UnaryOperator(e, builder) =>
val (e1, c) = rec(e, ctx)
-
val newE = builder(e1)
+
(newE, combiner(newE, ctx, Seq(c)))
+
case BinaryOperator(e1, e2, builder) =>
val (ne1, c1) = rec(e1, ctx)
val (ne2, c2) = rec(e2, ctx)
-
val newE = builder(ne1, ne2)
+
(newE, combiner(newE, ctx, Seq(c1, c2)))
+
case NAryOperator(es, builder) =>
val (nes, cs) = es.map(e => rec(e, ctx)).unzip
-
val newE = builder(nes)
+
(newE, combiner(newE, ctx, cs))
+
case e =>
- sys.error("Expression "+e+" ["+e.getClass+"] has no defined extractor")
+ sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
}
post(newExpr, newC)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 246f335ad..4ba80bdc8 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -6,6 +6,7 @@ object Trees {
import Common._
import TypeTrees._
import Definitions._
+ import Extractors._
/* EXPRESSIONS */
@@ -42,7 +43,9 @@ object Trees {
case class Epsilon(pred: Expr) extends Expr with ScalacPositional
- case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional
+ case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional with UnaryExtractable {
+ def extract = Some((pred, (e: Expr) => Choose(vars, e)))
+ }
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
--
GitLab