From db91a8c30a15fbc39a94ab5861af891362a1edcd Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 18 Oct 2016 09:13:00 +0200
Subject: [PATCH] Esthetic changes in transformers + unary minus in DSL
---
src/main/scala/inox/ast/DSL.scala | 1 +
.../scala/inox/transformers/Collector.scala | 8 ++++++--
.../inox/transformers/CollectorWithPC.scala | 18 +++++++++++-------
.../inox/transformers/SimplifierWithPC.scala | 2 +-
4 files changed, 19 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index 46778edff..f8de46db2 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -30,6 +30,7 @@ trait DSL {
def - = Minus(e, _: Expr)
def % = Modulo(e, _: Expr)
def / = Division(e, _: Expr)
+ def unary_- = UMinus(e)
// Comparisons
def < = LessThan(e, _: Expr)
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 5424859c3..8097214e7 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -11,9 +11,10 @@ trait Collector extends Transformer {
/** The type of collected objects */
type R
final type Result = (R, Env)
- import trees.Expr
private var results: List[Result] = Nil
+ import trees._
+
/** Does one step of collection for the current [[Expr]] and [[Env]] */
protected def step(e: Expr, env: Env): List[Result]
@@ -23,9 +24,12 @@ trait Collector extends Transformer {
}
/** Traverses the expression and collects */
- final def collect(e: Expr) = {
+ final def collect(e: Expr): List[Result] = {
results = Nil
transform(e)
results
}
+
+ /** Collect the expressions in a [[FunDef]]'s body */
+ final def collect(fd: FunDef): List[Result] = collect(fd.fullBody)
}
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 0681991d3..823b35196 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -4,18 +4,22 @@ package inox
package transformers
/** A [[Collector]] that collects path conditions */
-trait CollectorWithPC extends TransformerWithPC with Collector
+trait CollectorWithPC extends TransformerWithPC with Collector {
+ import program.trees._
+ import program.symbols._
+
+ lazy val initEnv: Path = Path.empty
+}
object CollectorWithPC {
- def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]): CollectorWithPC { type R = T; val program: p.type } = {
+ def apply[T](p: Program)
+ (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
+ CollectorWithPC { type R = T; val program: p.type } = {
new CollectorWithPC {
-
type R = T
val program: p.type = p
- import program._
- import symbols._
- import trees._
- val initEnv: Path = Path.empty
+ import program.trees._
+ import program.symbols._
private val fLifted = f.lift
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index b0bb42569..0bdbfddad 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -12,7 +12,7 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
import trees._
import symbols._
- protected val sf: SolverFactory{ val program: self.program.type }
+ protected val sf: SolverFactory { val program: self.program.type }
protected lazy val s = SimpleSolverAPI(sf)
private def querie(e: Expr, path: Path, implied: Boolean) = {
--
GitLab