From 682d8a5980de52e998e86a59b0ec9851c97b32f8 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 17 Oct 2016 19:55:32 +0200
Subject: [PATCH] Documented Trees#Identifier and added ADTDefinition transform
---
src/main/scala/inox/ast/TreeOps.scala | 62 ++++++++++---------
src/main/scala/inox/ast/Trees.scala | 15 +++++
.../scala/inox/datagen/ModelEnumerator.scala | 1 -
.../scala/inox/datagen/SolverDataGen.scala | 1 -
.../inox/evaluators/RecursiveEvaluator.scala | 1 -
.../scala/inox/grammars/ClosureGrammars.scala | 2 -
.../inox/grammars/ExpressionGrammars.scala | 1 -
.../scala/inox/grammars/ValueGrammars.scala | 2 -
.../scala/inox/grammars/utils/Helpers.scala | 2 -
src/main/scala/inox/solvers/ADTManagers.scala | 1 -
.../inox/solvers/smtlib/CVC4Target.scala | 1 -
.../inox/solvers/smtlib/SMTLIBTarget.scala | 1 -
.../scala/inox/solvers/smtlib/Z3Target.scala | 1 -
.../inox/solvers/theories/BagEncoder.scala | 2 -
.../inox/solvers/theories/StringEncoder.scala | 1 -
.../solvers/unrolling/DatatypeTemplates.scala | 1 -
.../solvers/unrolling/FunctionTemplates.scala | 1 -
.../solvers/unrolling/LambdaTemplates.scala | 1 -
.../unrolling/QuantificationTemplates.scala | 1 -
.../solvers/unrolling/TemplateGenerator.scala | 1 -
.../inox/solvers/unrolling/Templates.scala | 1 -
.../solvers/unrolling/UnrollingSolver.scala | 1 -
.../inox/solvers/z3/AbstractZ3Solver.scala | 1 -
src/main/scala/inox/tip/Parser.scala | 1 -
src/main/scala/inox/tip/Printer.scala | 2 -
.../inox/transformers/ScopeSimplifier.scala | 2 -
26 files changed, 47 insertions(+), 60 deletions(-)
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index b4af9cdc1..5013774f7 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 272ff38c5..7b0f89a1a 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 060168a4a..6cfbc50d8 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 432635247..257674268 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 4af6b1d73..d3b0e2da2 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 2e9ad0ad5..cbf304ab5 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 85b15fc40..0bc1bf875 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 7e09acb64..cf3f60cc8 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 2b17c5680..08e91da1a 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 47e401349..22d8617d8 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 00c319d35..b28755ba2 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 598264d90..890761d96 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 9b9825eba..e803c54a3 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 4cd485c72..b91f3e52d 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 b572373e4..b37b9aaef 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 795a7f799..9a2f915e3 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 84e5a31ca..eada1e7e8 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 ebe84c69c..8442624ba 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 33f7f2fe5..4cd8f09a2 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 255c25bd1..62c214b69 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 9bf18c367..ddf72be38 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 d1601e651..57daddc41 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 461f33d40..a2fc56cf3 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 bf1e99c77..72245aeb8 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 324c3c880..e33a078f4 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 183623266..a74653eea 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._
--
GitLab