From 6fc6e8c3e8ee92578bd51b15054e5061f1e548c7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 12 Oct 2016 15:01:36 +0200
Subject: [PATCH] Identifier is not a dep. type. Small changes to
CollectorWithPC
---
src/main/scala/inox/ast/Trees.scala | 4 ----
src/main/scala/inox/datagen/ModelEnumerator.scala | 1 +
src/main/scala/inox/datagen/SolverDataGen.scala | 1 +
src/main/scala/inox/evaluators/RecursiveEvaluator.scala | 1 +
src/main/scala/inox/grammars/ClosureGrammars.scala | 2 ++
src/main/scala/inox/grammars/ExpressionGrammars.scala | 1 +
src/main/scala/inox/grammars/ValueGrammars.scala | 2 ++
src/main/scala/inox/grammars/utils/Helpers.scala | 2 ++
src/main/scala/inox/package.scala | 2 ++
src/main/scala/inox/solvers/ADTManagers.scala | 1 +
src/main/scala/inox/solvers/smtlib/CVC4Target.scala | 1 +
src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala | 1 +
src/main/scala/inox/solvers/smtlib/Z3Target.scala | 1 +
src/main/scala/inox/solvers/theories/BagEncoder.scala | 2 ++
src/main/scala/inox/solvers/theories/StringEncoder.scala | 1 +
.../scala/inox/solvers/unrolling/DatatypeTemplates.scala | 1 +
.../scala/inox/solvers/unrolling/FunctionTemplates.scala | 3 +--
.../scala/inox/solvers/unrolling/LambdaTemplates.scala | 2 +-
.../inox/solvers/unrolling/QuantificationTemplates.scala | 1 +
.../scala/inox/solvers/unrolling/TemplateGenerator.scala | 1 +
src/main/scala/inox/solvers/unrolling/Templates.scala | 1 +
.../scala/inox/solvers/unrolling/UnrollingSolver.scala | 1 +
src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala | 1 +
src/main/scala/inox/tip/Parser.scala | 5 +++--
src/main/scala/inox/tip/Printer.scala | 3 ++-
src/main/scala/inox/transformers/CollectorWithPC.scala | 7 +++++--
src/main/scala/inox/transformers/ScopeSimplifier.scala | 2 ++
27 files changed, 39 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 57a9bdc17..272ff38c5 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -3,7 +3,6 @@
package inox
package ast
-import utils._
import scala.language.implicitConversions
case object DebugSectionTrees extends DebugSection("trees")
@@ -16,9 +15,6 @@ trait Trees
with Printers
with TreeOps {
- type Identifier = ast.Identifier
- 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 6cfbc50d8..060168a4a 100644
--- a/src/main/scala/inox/datagen/ModelEnumerator.scala
+++ b/src/main/scala/inox/datagen/ModelEnumerator.scala
@@ -6,6 +6,7 @@ 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 257674268..432635247 100644
--- a/src/main/scala/inox/datagen/SolverDataGen.scala
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -6,6 +6,7 @@ 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 d3b0e2da2..4af6b1d73 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -4,6 +4,7 @@ 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 cbf304ab5..2e9ad0ad5 100644
--- a/src/main/scala/inox/grammars/ClosureGrammars.scala
+++ b/src/main/scala/inox/grammars/ClosureGrammars.scala
@@ -3,6 +3,8 @@
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 0bc1bf875..85b15fc40 100644
--- a/src/main/scala/inox/grammars/ExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/ExpressionGrammars.scala
@@ -3,6 +3,7 @@
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 cf3f60cc8..7e09acb64 100644
--- a/src/main/scala/inox/grammars/ValueGrammars.scala
+++ b/src/main/scala/inox/grammars/ValueGrammars.scala
@@ -3,6 +3,8 @@
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 08e91da1a..2b17c5680 100644
--- a/src/main/scala/inox/grammars/utils/Helpers.scala
+++ b/src/main/scala/inox/grammars/utils/Helpers.scala
@@ -4,6 +4,8 @@ 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/package.scala b/src/main/scala/inox/package.scala
index 14426583e..6b9220f40 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,5 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
+import inox.ast.Identifier
+
/** Core package of the Inox solving interface
*
* == Structure ==
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
index 22d8617d8..47e401349 100644
--- a/src/main/scala/inox/solvers/ADTManagers.scala
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -4,6 +4,7 @@ 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 b28755ba2..00c319d35 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -6,6 +6,7 @@ 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 890761d96..598264d90 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -4,6 +4,7 @@ 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 e803c54a3..9b9825eba 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -4,6 +4,7 @@ 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 b91f3e52d..4cd485c72 100644
--- a/src/main/scala/inox/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/BagEncoder.scala
@@ -4,6 +4,8 @@ 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 b37b9aaef..b572373e4 100644
--- a/src/main/scala/inox/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/StringEncoder.scala
@@ -4,6 +4,7 @@ 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 9a2f915e3..795a7f799 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -4,6 +4,7 @@ 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 1b06f3de2..84e5a31ca 100644
--- a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
@@ -5,8 +5,7 @@ package solvers
package unrolling
import utils._
-
-import scala.collection.generic.CanBuildFrom
+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 1194bcea1..ebe84c69c 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -5,7 +5,7 @@ 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 4cd8f09a2..33f7f2fe5 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -4,6 +4,7 @@ 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 62c214b69..255c25bd1 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -4,6 +4,7 @@ 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 ddf72be38..9bf18c367 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -4,6 +4,7 @@ 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 57daddc41..d1601e651 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -4,6 +4,7 @@ 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 a2fc56cf3..461f33d40 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -3,6 +3,7 @@
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 51024b61a..bf1e99c77 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -3,6 +3,9 @@
package inox
package tip
+import ast.{Identifier, FreshIdentifier}
+import utils._
+
import smtlib.lexer._
import smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import smtlib.parser.Terms.{Let => SMTLet, Forall => SMTForall, Identifier => SMTIdentifier, _}
@@ -15,8 +18,6 @@ import smtlib.extensions.tip.Commands._
import scala.collection.BitSet
import java.io.{Reader, File, BufferedReader, FileReader}
-import utils._
-
import scala.language.implicitConversions
class MissformedTIPException(reason: String, pos: Position)
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index aff75f944..324c3c880 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -3,7 +3,7 @@
package inox
package tip
-import java.io.{File, Writer}
+import ast.Identifier
import smtlib.parser.Terms.{Forall => SMTForall, Identifier => SMTIdentifier, _}
import smtlib.parser.Commands.{Constructor => SMTConstructor, _}
@@ -11,6 +11,7 @@ import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTAppli
import smtlib.extensions.tip.Commands._
import smtlib.Interpreter
+import java.io.Writer
import scala.collection.mutable.{Map => MutableMap}
class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.SMTLIBTarget {
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
index 11f5c26bc..0681991d3 100644
--- a/src/main/scala/inox/transformers/CollectorWithPC.scala
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -7,7 +7,7 @@ package transformers
trait CollectorWithPC extends TransformerWithPC with Collector
object CollectorWithPC {
- def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]) = {
+ def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]): CollectorWithPC { type R = T; val program: p.type } = {
new CollectorWithPC {
type R = T
@@ -17,10 +17,13 @@ object CollectorWithPC {
import trees._
val initEnv: Path = Path.empty
+ private val fLifted = f.lift
+
protected def step(e: Expr, env: Path): List[(T, Path)] = {
- f.lift((e, env)).map((_, env)).toList
+ fLifted((e, env)).map((_, env)).toList
}
}
}
+
}
diff --git a/src/main/scala/inox/transformers/ScopeSimplifier.scala b/src/main/scala/inox/transformers/ScopeSimplifier.scala
index a74653eea..183623266 100644
--- a/src/main/scala/inox/transformers/ScopeSimplifier.scala
+++ b/src/main/scala/inox/transformers/ScopeSimplifier.scala
@@ -3,6 +3,8 @@
package inox
package transformers
+import ast.{Identifier, FreshIdentifier}
+
/** Simplifies variable ids in scope */
trait ScopeSimplifier extends Transformer {
import trees._
--
GitLab