From 73321ddd42567f0bce25ad31d420a770e8da88f6 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 26 Oct 2016 16:36:07 +0200
Subject: [PATCH] More flexible transformers
---
src/main/scala/inox/ast/SymbolOps.scala | 18 ++++++++-----
.../inox/transformers/CollectorWithPC.scala | 26 +++++++++++--------
.../inox/transformers/SimplifierWithPC.scala | 8 ++++--
.../inox/transformers/TransformerWithPC.scala | 5 ++--
4 files changed, 35 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 8cbbaf280..239f0cc62 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -642,12 +642,18 @@ trait SymbolOps { self: TypeOps =>
fold[String]{ (e, se) =>
e match {
case FunctionInvocation(id, tps, args) =>
- val tfd = getFunction(id, tps)
- s"${e.asString} is of type ${e.getType.asString}" +
- se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString +
- s" because ${tfd.fd.id.name} was instantiated with " +
- s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
- s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
+ lookupFunction(id, tps) match {
+ case Some(tfd) =>
+ s"${e.asString} is of type ${e.getType.asString}" +
+ se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString +
+ s" because ${tfd.fd.id.name} was instantiated with " +
+ s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
+ s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
+ case None =>
+ s"${e.asString} is of type ${e.getType.asString}" +
+ se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString +
+ s" but couldn't find function $id"
+ }
case e =>
s"${e.asString} is of type ${e.getType.asString}" +
se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 0bad6300d..dbacecd00 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -5,28 +5,32 @@ package transformers
/** A [[Collector]] that collects path conditions */
trait CollectorWithPC extends TransformerWithPC with Collector {
- import program.trees._
- import program.symbols._
-
- lazy val initEnv: Path = Path.empty
+ lazy val initEnv = symbols.Path.empty
}
object CollectorWithPC {
- def apply[T](p: Program)
- (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
- CollectorWithPC { type Result = T; val program: p.type } = {
+ def apply[T](t: ast.Trees)
+ (s: t.Symbols)
+ (f: PartialFunction[(t.Expr, s.Path), T]):
+ CollectorWithPC { type Result = T; val trees: t.type; val symbols: s.type } = {
new CollectorWithPC {
type Result = T
- val program: p.type = p
- import program.trees._
- import program.symbols._
+ val trees: t.type = t
+ val symbols: s.type = s
private val fLifted = f.lift
- protected def step(e: Expr, env: Path): List[T] = {
+ protected def step(e: t.Expr, env: s.Path): List[T] = {
fLifted((e, env)).toList
}
}
}
+ def apply[T](p: Program)
+ (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
+ CollectorWithPC { type Result = T; val trees: p.trees.type; val symbols: p.symbols.type } = {
+ apply(p.trees)(p.symbols)(f)
+ }
+
+
}
diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 0bdbfddad..0cf5581d3 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -8,9 +8,13 @@ import inox.solvers.{SimpleSolverAPI, SolverFactory}
/** Uses solvers to perform PC-aware simplifications */
trait SimplifierWithPC extends TransformerWithPC { self =>
+ val program: Program
+ lazy val trees: program.trees.type = program.trees
+ lazy val symbols: program.symbols.type = program.symbols
+
import program._
- import trees._
- import symbols._
+ import program.trees._
+ import program.symbols._
protected val sf: SolverFactory { val program: self.program.type }
protected lazy val s = SimpleSolverAPI(sf)
diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala
index 1714f9d9d..20698ee34 100644
--- a/src/main/scala/inox/transformers/TransformerWithPC.scala
+++ b/src/main/scala/inox/transformers/TransformerWithPC.scala
@@ -5,11 +5,10 @@ package transformers
/** A [[Transformer]] which uses path conditions as environment */
trait TransformerWithPC extends Transformer {
- val program: Program
- import program._
- final lazy val trees: program.trees.type = program.trees
+ val symbols: trees.Symbols
import trees._
import symbols._
+
type Env = Path
protected def rec(e: Expr, path: Path): Expr = e match {
--
GitLab