diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index e9ab87604c5ef9709f1b0eb65f60476c2aeb4fca..3d398cebd409976d07360bee49ee1383b17d69d1 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -253,6 +253,13 @@ trait Definitions { self: Trees =>
require(tps.length == tparams.length)
TypedADTSort(this, tps)
}
+
+ def copy(
+ id: Identifier = this.id,
+ tparams: Seq[TypeParameterDef] = this.tparams,
+ cons: Seq[Identifier] = this.cons,
+ flags: Set[Flag] = this.flags
+ ): ADTSort = new ADTSort(id, tparams, cons, flags)
}
/** Case classes/ ADT constructors. For single-case classes these may coincide
@@ -290,6 +297,14 @@ trait Definitions { self: Trees =>
require(tps.length == tparams.length)
TypedADTConstructor(this, tps)
}
+
+ def copy(
+ id: Identifier = this.id,
+ tparams: Seq[TypeParameterDef] = this.tparams,
+ sort: Option[Identifier] = this.sort,
+ fields: Seq[ValDef] = this.fields,
+ flags: Set[Flag] = this.flags
+ ): ADTConstructor = new ADTConstructor(id, tparams, sort, fields, flags)
}
/** Represents an [[ADTDefinition]] whose type parameters have been instantiated to ''tps'' */
@@ -378,6 +393,15 @@ trait Definitions { self: Trees =>
def applied(args: Seq[Expr])(implicit s: Symbols): FunctionInvocation = s.functionInvocation(this, args)
/** Applies this function on its formal parameters */
def applied = FunctionInvocation(id, typeArgs, params map (_.toVariable))
+
+ def copy(
+ id: Identifier = this.id,
+ tparams: Seq[TypeParameterDef] = this.tparams,
+ params: Seq[ValDef] = this.params,
+ returnType: Type = this.returnType,
+ fullBody: Expr = this.fullBody,
+ flags: Set[Flag] = this.flags
+ ): FunDef = new FunDef(id, tparams, params, returnType, fullBody, flags)
}
@@ -393,15 +417,15 @@ trait Definitions { self: Trees =>
}
}
- private lazy val typesMap: Map[TypeParameter, Type] = {
+ lazy val tpSubst: Map[TypeParameter, Type] = {
(fd.typeArgs zip tps).toMap.filter(tt => tt._1 != tt._2)
}
/** A [[Type]] instantiated with this [[TypedFunDef]]'s type instantiation */
- def instantiate(t: Type): Type = symbols.instantiateType(t, typesMap)
+ def instantiate(t: Type): Type = symbols.instantiateType(t, tpSubst)
/** A [[Expr]] instantiated with this [[TypedFunDef]]'s type instantiation */
- def instantiate(e: Expr): Expr = symbols.instantiateType(e, typesMap)
+ def instantiate(e: Expr): Expr = symbols.instantiateType(e, tpSubst)
/** A mapping from this [[TypedFunDef]]'s formal parameters to real arguments
*
@@ -431,7 +455,7 @@ trait Definitions { self: Trees =>
/** The paremeters of the respective [[FunDef]] instantiated with the real type parameters */
lazy val params: Seq[ValDef] = {
- if (typesMap.isEmpty) {
+ if (tpSubst.isEmpty) {
fd.params
} else {
fd.params.map(vd => vd.copy(tpe = instantiate(vd.getType)))
diff --git a/src/main/scala/inox/ast/Paths.scala b/src/main/scala/inox/ast/Paths.scala
index 9c78d2677efded9efd4010693cfb6b0d6adc0143..6e15804d1ff0dc2f2dee97e9e9f31205fb091001 100644
--- a/src/main/scala/inox/ast/Paths.scala
+++ b/src/main/scala/inox/ast/Paths.scala
@@ -3,7 +3,7 @@
package inox
package ast
-trait Paths { self: TypeOps with Constructors =>
+trait Paths { self: SymbolOps with TypeOps with Constructors =>
import trees._
object Path {
@@ -69,7 +69,19 @@ trait Paths { self: TypeOps with Constructors =>
* Expressions in a path appear both on the right-hand side of let binders
* and in boolean path conditions.
*/
- def map(f: Expr => Expr) = new Path(elements.map(_.left.map { case (id, e) => id -> f(e) }.right.map(f)))
+ def map(f: Expr => Expr) = new Path(elements.map(_.left.map { case (vd, e) => vd -> f(e) }.right.map(f)))
+
+ /** Instantiates type parameters within the path
+ *
+ * Type parameters within a path may appear both inside expressions and in
+ * the type associated to a let binder.
+ */
+ def instantiate(tps: Map[TypeParameter, Type]) = {
+ val t = new TypeInstantiator(tps)
+ new Path(elements.map(_.left.map {
+ case (vd, e) => t.transform(vd) -> t.transform(e)
+ }.right.map(t.transform)))
+ }
/** Splits the path on predicate `p`
*
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index 5b44cc92d9ca408298940293036be4caf68739e1..67de1df3405fcb8f48e5a5235ed4f783d496cc7c 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -19,7 +19,7 @@ trait TreeOps { self: Trees =>
} = self.deconstructor
}
- class TreeIdentity extends SelfTreeTransformer {
+ trait IdentityTreeTransformer extends SelfTreeTransformer {
override def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = (id, tpe)
override def transform(v: s.Variable): t.Variable = v
override def transform(vd: s.ValDef): t.ValDef = vd
@@ -28,17 +28,17 @@ trait TreeOps { self: Trees =>
override def transform(flag: s.Flag): t.Flag = flag
}
- lazy val TreeIdentity: SelfTransformer = new TreeIdentity
+ trait IdentitySymbolTransformer extends SymbolTransformer {
+ /* For some reason, the scala compiler doesn't accept {{{
+ * object transformer extends IdentityTreeTransformer
+ * }}} which would be nicer. */
+ val transformer = new IdentityTreeTransformer {}
- class SymbolIdentity extends SymbolTransformer {
- val transformer = TreeIdentity
override protected final def transformFunction(fd: s.FunDef): t.FunDef = sys.error("unexpected")
override protected final def transformADT(adt: s.ADTDefinition): t.ADTDefinition = sys.error("unexpected")
override def transform(syms: s.Symbols): t.Symbols = syms
}
- lazy val SymbolIdentity: SymbolTransformer { val transformer: SelfTransformer } = new SymbolIdentity
-
trait TreeTraverser {
def traverse(vd: ValDef): Unit = traverse(vd.tpe)
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index d7b17734b2b3b39d30f4ae32a5a49fa82b75edef..3af74feb6e2a68e3ccbfab5e856d082ad3f7f2cc 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -19,6 +19,8 @@ trait SolverFactory {
def reclaim(s: S) {
s.free()
}
+
+ def toAPI = SimpleSolverAPI(this)
}
object SolverFactory {
diff --git a/src/main/scala/inox/solvers/combinators/EncodingSolver.scala b/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
index f32d2bd6da7f30e85a292f1d8c635dd89c501810..726cbe8c61138404c6976ff5fef9083ad952023f 100644
--- a/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/EncodingSolver.scala
@@ -33,8 +33,8 @@ object ProgramEncoder {
val sourceProgram: p.type = p
val t: p.trees.type = p.trees
- val encoder = p.trees.SymbolIdentity
- val decoder = p.trees.SymbolIdentity
+ object encoder extends p.trees.IdentitySymbolTransformer
+ object decoder extends p.trees.IdentitySymbolTransformer
}
}
diff --git a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
index 95ece9fb34adaa78cc1196ec30edd8222e030fac..225aa13a434c61f4c649765e024ab9a6ed183050 100644
--- a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
@@ -46,7 +46,7 @@ trait TheoryEncoder extends ast.TreeBijection {
trait NoEncoder extends TheoryEncoder {
import trees._
- protected val treeEncoder: SelfTransformer = TreeIdentity
- protected val treeDecoder: SelfTransformer = TreeIdentity
+ protected object treeEncoder extends IdentityTreeTransformer
+ protected object treeDecoder extends IdentityTreeTransformer
}
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 8097214e7078a14420770cbb352a8009176e2ac9..0da53d7668477d58d048443fa3ee0ea794f83a4f 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -4,13 +4,11 @@ package inox
package transformers
/** A common trait for objects that collect something from expressions.
- * The [[Transformer]] environment will also be collected along the way.
* This trait is meant to be mixed in with a specific [[Transformer]] to attach collect functionality.
*/
trait Collector extends Transformer {
/** The type of collected objects */
- type R
- final type Result = (R, Env)
+ type Result
private var results: List[Result] = Nil
import trees._
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 823b351960bf3a2945f6e778b19159a146e2e7d4..0bad6300d08814ed56dee880989f9d5833df6865 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -14,19 +14,18 @@ trait CollectorWithPC extends TransformerWithPC with Collector {
object CollectorWithPC {
def apply[T](p: Program)
(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
- CollectorWithPC { type R = T; val program: p.type } = {
+ CollectorWithPC { type Result = T; val program: p.type } = {
new CollectorWithPC {
- type R = T
+ type Result = T
val program: p.type = p
import program.trees._
import program.symbols._
private val fLifted = f.lift
- protected def step(e: Expr, env: Path): List[(T, Path)] = {
- fLifted((e, env)).map((_, env)).toList
+ protected def step(e: Expr, env: Path): List[T] = {
+ fLifted((e, env)).toList
}
-
}
}