diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index b4af9cdc1457797e6f59f892e87d15d4a3d4ac69..5013774f76544d2be7ff49d49ade4fb05d66d5ee 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -163,10 +163,18 @@ trait TreeTransformer {
}
}
+ /* Type parameters can't be modified by transformed but they need to be
+ * translated into the new tree definitions given by `t`. */
+ @inline
+ protected[ast] final def transformTypeParams(tparams: Seq[s.TypeParameterDef]): Seq[t.TypeParameterDef] = {
+ if (s eq t) tparams.asInstanceOf[Seq[t.TypeParameterDef]]
+ else tparams.map(tdef => t.TypeParameterDef(t.TypeParameter(tdef.id)))
+ }
+
final def transform(fd: s.FunDef): t.FunDef = {
new t.FunDef(
fd.id,
- fd.tparams.map(tpd => t.TypeParameterDef(transform(tpd.tp).asInstanceOf[t.TypeParameter])),
+ transformTypeParams(fd.tparams),
fd.params.map(transform),
transform(fd.returnType),
transform(fd.fullBody),
@@ -174,6 +182,25 @@ trait TreeTransformer {
)
}
+ final def transform(adt: s.ADTDefinition): t.ADTDefinition = adt match {
+ case sort: s.ADTSort if (s eq t) => sort.asInstanceOf[t.ADTSort]
+
+ case sort: s.ADTSort => new t.ADTSort(
+ sort.id,
+ transformTypeParams(sort.tparams),
+ sort.cons,
+ sort.flags map transform
+ )
+
+ case cons: s.ADTConstructor => new t.ADTConstructor(
+ cons.id,
+ transformTypeParams(cons.tparams),
+ cons.sort,
+ cons.fields map transform,
+ cons.flags map transform
+ )
+ }
+
protected trait TreeTransformerComposition extends TreeTransformer {
protected val t1: TreeTransformer
protected val t2: TreeTransformer { val s: t1.t.type }
@@ -234,36 +261,11 @@ trait SymbolTransformer {
def transform(tpe: s.Type): t.Type = transformer.transform(tpe)
def transform(flag: s.Flag): t.Flag = transformer.transform(flag)
- /* Type parameters can't be modified by transformed but they need to be
- * translated into the new tree definitions given by `t`. */
- protected def transformTypeParams(tparams: Seq[s.TypeParameterDef]): Seq[t.TypeParameterDef] = {
- if (s eq t) tparams.asInstanceOf[Seq[t.TypeParameterDef]]
- else tparams.map(tdef => t.TypeParameterDef(t.TypeParameter(tdef.id)))
- }
+ @inline
+ protected def transformTypeParams(tparams: Seq[s.TypeParameterDef]) = transformer.transformTypeParams(tparams)
- protected def transformFunction(fd: s.FunDef): t.FunDef = new t.FunDef(
- fd.id,
- transformTypeParams(fd.tparams),
- fd.params.map(vd => transformer.transform(vd)),
- transformer.transform(fd.returnType),
- transformer.transform(fd.fullBody),
- fd.flags.map(f => transformer.transform(f))
- )
-
- protected def transformADT(adt: s.ADTDefinition): t.ADTDefinition = adt match {
- case sort: s.ADTSort if (s eq t) => sort.asInstanceOf[t.ADTSort]
- case sort: s.ADTSort => new t.ADTSort(
- sort.id,
- transformTypeParams(sort.tparams),
- sort.cons,
- sort.flags.map(f => transformer.transform(f)))
- case cons: s.ADTConstructor => new t.ADTConstructor(
- cons.id,
- transformTypeParams(cons.tparams),
- cons.sort,
- cons.fields.map(vd => transformer.transform(vd)),
- cons.flags.map(f => transformer.transform(f)))
- }
+ protected def transformFunction(fd: s.FunDef): t.FunDef = transformer.transform(fd)
+ protected def transformADT(adt: s.ADTDefinition): t.ADTDefinition = transformer.transform(adt)
def transform(syms: s.Symbols): t.Symbols = t.NoSymbols
.withFunctions(syms.functions.values.toSeq.map(transformFunction))
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 272ff38c5fb3035874e23dee9f2a8822b10577e0..7b0f89a1aefeecce12ff25b3b959d7c068ef172d 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -15,6 +15,21 @@ trait Trees
with Printers
with TreeOps {
+ /** We provide aliases to [[ast.Identifier]] and [[ast.FreshIdentifier]] here in
+ * order for {{{import trees._}}} to also provide these. Note that this DOES NOT
+ * mean that [[Identifier]] or [[FreshIdentifier]] become dependent types!!
+ *
+ * I (@nv) feel it makes sense for all types necessary for expression/tree
+ * construction to be available from a single import. It would be rather
+ * counter-intuitive for an Inox user to have to go in search of the
+ * [[ast.Identifier]] type in the [[ast]] package when all other expression and
+ * definitions have been imported.
+ */
+ type Identifier = ast.Identifier
+
+ /** @see [[Identifier]] for a discussion about why this is here. */
+ val FreshIdentifier = ast.FreshIdentifier
+
class Unsupported(t: Tree, msg: String)(implicit ctx: Context)
extends Exception(s"${t.asString(PrinterOptions.fromContext(ctx))}@${t.getPos} $msg")
diff --git a/src/main/scala/inox/datagen/ModelEnumerator.scala b/src/main/scala/inox/datagen/ModelEnumerator.scala
index 060168a4a5f42a57d6b5eada097a4c6f97c2bcb6..6cfbc50d884955c874bd29db5eb1190f132b17c8 100644
--- a/src/main/scala/inox/datagen/ModelEnumerator.scala
+++ b/src/main/scala/inox/datagen/ModelEnumerator.scala
@@ -6,7 +6,6 @@ package datagen
import evaluators._
import solvers._
import utils._
-import ast.FreshIdentifier
trait ModelEnumerator {
val program: Program
diff --git a/src/main/scala/inox/datagen/SolverDataGen.scala b/src/main/scala/inox/datagen/SolverDataGen.scala
index 432635247e96ae38327327fddbfb45a5f7f9259f..2576742684986384139a28a7b875d26e79a1d168 100644
--- a/src/main/scala/inox/datagen/SolverDataGen.scala
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -6,7 +6,6 @@ package datagen
import evaluators._
import solvers._
import utils._
-import ast.{FreshIdentifier, Identifier}
trait SolverDataGen extends DataGenerator { self =>
import program._
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 4af6b1d73dea9a1469e690455b8ca67ff9948a69..d3b0e2da23d19456a9333f7c27274f9d17968f40 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -4,7 +4,6 @@ package inox
package evaluators
import scala.collection.BitSet
-import ast.FreshIdentifier
trait RecursiveEvaluator
extends ContextualEvaluator
diff --git a/src/main/scala/inox/grammars/ClosureGrammars.scala b/src/main/scala/inox/grammars/ClosureGrammars.scala
index 2e9ad0ad56a06d7527967e7d65b4f939b01b5e14..cbf304ab5b434009b58c0c8f28cde92229b914c4 100644
--- a/src/main/scala/inox/grammars/ClosureGrammars.scala
+++ b/src/main/scala/inox/grammars/ClosureGrammars.scala
@@ -3,8 +3,6 @@
package inox
package grammars
-import ast.FreshIdentifier
-
trait ClosureGrammars { self: GrammarsUniverse =>
import program._
import trees._
diff --git a/src/main/scala/inox/grammars/ExpressionGrammars.scala b/src/main/scala/inox/grammars/ExpressionGrammars.scala
index 85b15fc40e86763cca02e87424b2cebd44925901..0bc1bf8754e24ff21251876cd9f87c98d50a7094 100644
--- a/src/main/scala/inox/grammars/ExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/ExpressionGrammars.scala
@@ -3,7 +3,6 @@
package inox
package grammars
-import ast.FreshIdentifier
import scala.collection.mutable.{HashMap => MutableMap}
/** Represents a context-free grammar of expressions */
diff --git a/src/main/scala/inox/grammars/ValueGrammars.scala b/src/main/scala/inox/grammars/ValueGrammars.scala
index 7e09acb6476974159bbe9b693533700a8ea518e3..cf3f60cc8aceaf66b607308cfe4f61d3ca3fca1c 100644
--- a/src/main/scala/inox/grammars/ValueGrammars.scala
+++ b/src/main/scala/inox/grammars/ValueGrammars.scala
@@ -3,8 +3,6 @@
package inox
package grammars
-import ast.FreshIdentifier
-
trait ValueGrammars { self: GrammarsUniverse =>
import program._
import trees._
diff --git a/src/main/scala/inox/grammars/utils/Helpers.scala b/src/main/scala/inox/grammars/utils/Helpers.scala
index 2b17c5680324baca8d22ef4d07e7e7bedaee66ae..08e91da1a71434423bfc1fe53c3d9529b79e2ec7 100644
--- a/src/main/scala/inox/grammars/utils/Helpers.scala
+++ b/src/main/scala/inox/grammars/utils/Helpers.scala
@@ -4,8 +4,6 @@ package inox
package grammars
package utils
-import ast.{Identifier, FreshIdentifier}
-
trait Helpers { self: GrammarsUniverse =>
import program._
import trees.{ Minus => EMinus, Plus => EPlus, Variable => EVariable, _ }
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
index 47e401349ed75a69894a0db83620f1f40a07e53a..22d8617d81236126cfdf9e3b04971a7282d17596 100644
--- a/src/main/scala/inox/solvers/ADTManagers.scala
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -4,7 +4,6 @@ package inox
package solvers
import utils._
-import ast.{Identifier, FreshIdentifier}
trait ADTManagers {
val program: Program
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
index 00c319d35ea7cdea4ee6a0066fffc7222cf0f293..b28755ba2f5feb05913bc1b3a23df152a35baa44 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -6,7 +6,6 @@ package smtlib
import org.apache.commons.lang3.StringEscapeUtils
-import ast.{Identifier, FreshIdentifier}
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 598264d90b9c8ec6bbbb55abd2e40e3d27c40b09..890761d963ea4bb37625985d6e34a354bdb2f471 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package smtlib
-import ast.{Identifier, FreshIdentifier}
import utils._
import _root_.smtlib.common._
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
index 9b9825eba0dbbd3c4e79dcb62110f948f6495783..e803c54a3ddfc36ab1ffce0331bb70ff56321bb4 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package smtlib
-import ast.{Identifier, FreshIdentifier}
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.interpreters.Z3Interpreter
diff --git a/src/main/scala/inox/solvers/theories/BagEncoder.scala b/src/main/scala/inox/solvers/theories/BagEncoder.scala
index 4cd485c725298206e0879d6d0fe94549a3ba2a68..b91f3e52df3bcaa58ae1b823e12f71ca8a629ed8 100644
--- a/src/main/scala/inox/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/BagEncoder.scala
@@ -4,8 +4,6 @@ package inox
package solvers
package theories
-import ast.{Identifier, FreshIdentifier}
-
trait BagEncoder extends TheoryEncoder {
import trees._
import trees.dsl._
diff --git a/src/main/scala/inox/solvers/theories/StringEncoder.scala b/src/main/scala/inox/solvers/theories/StringEncoder.scala
index b572373e4651300de50379967e6b35479e325a97..b37b9aaef4c787c74a2fbad026ec3ca14cf546bd 100644
--- a/src/main/scala/inox/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/StringEncoder.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package theories
-import ast.{Identifier, FreshIdentifier}
import utils._
trait StringEncoder extends TheoryEncoder {
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 795a7f7991f9019c54c78a2908f18ca7a411f64e..9a2f915e35a9397d71f1c87b19daf9ca560ef315 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package unrolling
-import ast.{Identifier, FreshIdentifier}
import utils._
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
diff --git a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
index 84e5a31ca1143311d333f69601126ed4f6397277..eada1e7e803c839e8bd49b6ab9c38c3d8ff0f1ac 100644
--- a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
@@ -5,7 +5,6 @@ package solvers
package unrolling
import utils._
-import ast.FreshIdentifier
trait FunctionTemplates { self: Templates =>
import program._
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index ebe84c69c2771721b9ef8c66b09066d89dd8ed6e..8442624baf7886c71dde9e72ffe28554791d0664 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -5,7 +5,6 @@ package solvers
package unrolling
import utils._
-import ast.{Identifier, FreshIdentifier}
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
trait LambdaTemplates { self: Templates =>
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 33f7f2fe5aac99bcd1989da5d4acd20066fe7094..4cd8f09a2ef1ae751702ea8f764539191b491e02 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package unrolling
-import ast.{Identifier, FreshIdentifier}
import utils._
import evaluators._
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 255c25bd176dc2b6fd20130b8e41ff3a9e1c2e3b..62c214b6915791cef732950c83b661999390e5f5 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package unrolling
-import ast.FreshIdentifier
import utils._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index 9bf18c367656a5352df9b0465b447a3fa1153fea..ddf72be387221cc8ee8b439a1c5a1356c70ad474 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package unrolling
-import ast.FreshIdentifier
import utils._
import scala.collection.generic.CanBuildFrom
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index d1601e6512268348143466af0186bd8bbf8709b5..57daddc41e257a3f5f6c4faa88b8e4524ba14fff 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package unrolling
-import ast.FreshIdentifier
import utils._
import theories._
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index 461f33d403251d3b6d2b083942a22eeb28f1f5de..a2fc56cf3898cdc186009173cf0cb0a27b045f16 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -3,7 +3,6 @@
package inox
package solvers.z3
-import ast.FreshIdentifier
import utils._
import z3.scala.{Z3Solver => ScalaZ3Solver, _}
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index bf1e99c779aadf44b4ea24bdbc666b66693e3485..72245aeb8a555a135a69d49e8338f59329a24b87 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -3,7 +3,6 @@
package inox
package tip
-import ast.{Identifier, FreshIdentifier}
import utils._
import smtlib.lexer._
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 324c3c88089ee2d957f422368a84ed7a2c42d573..e33a078f45d11f40b3e9717dca0ce41b77ee7083 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -3,8 +3,6 @@
package inox
package tip
-import ast.Identifier
-
import smtlib.parser.Terms.{Forall => SMTForall, Identifier => SMTIdentifier, _}
import smtlib.parser.Commands.{Constructor => SMTConstructor, _}
import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTApplication, _}
diff --git a/src/main/scala/inox/transformers/ScopeSimplifier.scala b/src/main/scala/inox/transformers/ScopeSimplifier.scala
index 1836232667f96b129cdfb4496396507c15994b29..a74653eea5abf1034afb5b47bb8673e950bc3d01 100644
--- a/src/main/scala/inox/transformers/ScopeSimplifier.scala
+++ b/src/main/scala/inox/transformers/ScopeSimplifier.scala
@@ -3,8 +3,6 @@
package inox
package transformers
-import ast.{Identifier, FreshIdentifier}
-
/** Simplifies variable ids in scope */
trait ScopeSimplifier extends Transformer {
import trees._