diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala index 0eb453a067a0318026839e9af4f4bd1ff569ffcf..4f3bf2a7d390c08b5091093acde71aafbd5c8eee 100644 --- a/src/main/scala/inox/ast/ExprOps.scala +++ b/src/main/scala/inox/ast/ExprOps.scala @@ -32,7 +32,7 @@ trait ExprOps extends GenTreeOps { type Source = Expr type Target = Expr - val Deconstructor = Operator + lazy val Deconstructor = Operator /** Replaces bottom-up variables by looking up for them in a map */ def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = { diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala index d2af32ea89cbebdbb99a9b4c093d398f815a477c..9a235fa844c91600494c554632acdf3fc5bc3d6b 100644 --- a/src/main/scala/inox/ast/Extractors.scala +++ b/src/main/scala/inox/ast/Extractors.scala @@ -239,11 +239,23 @@ trait Extractors { self: Trees => * tools for performing tree transformations that are very predictable, if * one need to simplify the tree, it is easy to write/call a simplification * function that would simply apply the corresponding constructor for each node. + * + * XXX: ideally, we would want [[Operator]] to be defined as + * {{{ + * val Operator: ExprDeconstructor { + * val s: self.type + * val t: self.type + * } + * }}} + * however the Scala compiler seems to have some bug with this and reports + * wrong errors when we define it this way... + * @see https://issues.scala-lang.org/browse/SI-9247 */ - - object Operator extends ExprDeconstructor { - val s: self.type = self - val t: self.type = self + val Operator: TreeExtractor { + val s: self.type + val t: self.type + type Source = self.Expr + type Target = self.Expr } object TopLevelOrs { // expr1 OR (expr2 OR (expr3 OR ..)) => List(expr1, expr2, expr3) diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala index 1de21b0c064010bb268152ad1d6c473dad1ed130..a8767c3ae78274d9c3e4f0f46127cb9c0ccd3670 100644 --- a/src/main/scala/inox/ast/Types.scala +++ b/src/main/scala/inox/ast/Types.scala @@ -85,6 +85,10 @@ trait Types { self: Trees => def tcd(implicit s: Symbols): TypedClassDef = s.getClass(id, tps) } + /** NAryType extractor to extract any Type in a consistent way. + * + * @see [[Extractors.Operator]] about why we can't have nice(r) things + */ val NAryType: TreeExtractor { val s: self.type val t: self.type diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala index 3fec7b2283dfc86888119eda3032d04bc0489aa9..6f67768b00045081c126b54ea4b6c7ca172eae55 100644 --- a/src/main/scala/inox/package.scala +++ b/src/main/scala/inox/package.scala @@ -1,7 +1,5 @@ /* Copyright 2009-2016 EPFL, Lausanne */ -import inox.ast.TypeDeconstructor - /** Core package of the Inox solving interface * * == Structure == @@ -45,10 +43,15 @@ package object inox { object trees extends ast.Trees { + object Operator extends { + protected val s: trees.type = trees + protected val t: trees.type = trees + } with ast.ExprDeconstructor + object NAryType extends { protected val s: trees.type = trees protected val t: trees.type = trees - } with TypeDeconstructor + } with ast.TypeDeconstructor class Symbols( val functions: Map[Identifier, FunDef],