From c8002a7ba9366dd047ed5da60bd28889a068fef0 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 15:45:27 +0200
Subject: [PATCH] Remove implicit contexts from grammars
---
src/main/scala/inox/grammars/Aspects.scala | 2 +-
src/main/scala/inox/grammars/BaseGrammars.scala | 2 +-
src/main/scala/inox/grammars/ClosureGrammars.scala | 2 +-
src/main/scala/inox/grammars/ConstantGrammars.scala | 2 +-
src/main/scala/inox/grammars/ElementaryGrammars.scala | 6 +++---
src/main/scala/inox/grammars/EqualityGrammars.scala | 2 +-
src/main/scala/inox/grammars/ExpressionGrammars.scala | 6 +++---
src/main/scala/inox/grammars/FunctionCallsGrammars.scala | 2 +-
src/main/scala/inox/grammars/SimpleExpressionGrammars.scala | 6 +++---
src/main/scala/inox/grammars/ValueGrammars.scala | 2 +-
.../scala/inox/grammars/aspects/DepthBoundAspects.scala | 2 +-
.../scala/inox/grammars/aspects/ExtraTerminalsAspects.scala | 2 +-
.../scala/inox/grammars/aspects/PersistentAspects.scala | 2 +-
src/main/scala/inox/grammars/aspects/SimilarToAspects.scala | 2 +-
src/main/scala/inox/grammars/aspects/SizeAspects.scala | 2 +-
src/main/scala/inox/grammars/aspects/TaggedAspects.scala | 2 +-
.../scala/inox/grammars/aspects/TypeDepthBoundAspects.scala | 2 +-
17 files changed, 23 insertions(+), 23 deletions(-)
diff --git a/src/main/scala/inox/grammars/Aspects.scala b/src/main/scala/inox/grammars/Aspects.scala
index 027e423f5..7ef23f7b1 100644
--- a/src/main/scala/inox/grammars/Aspects.scala
+++ b/src/main/scala/inox/grammars/Aspects.scala
@@ -27,6 +27,6 @@ trait Aspects { self: GrammarsUniverse =>
trait Aspect extends Printable {
final type Production = ProductionRule[Label, Expr]
- def applyTo(l: Label, ps: Seq[Production])(implicit ctx: InoxContext): Seq[Production]
+ def applyTo(l: Label, ps: Seq[Production]): Seq[Production]
}
}
diff --git a/src/main/scala/inox/grammars/BaseGrammars.scala b/src/main/scala/inox/grammars/BaseGrammars.scala
index f1d4559b6..b5800c333 100644
--- a/src/main/scala/inox/grammars/BaseGrammars.scala
+++ b/src/main/scala/inox/grammars/BaseGrammars.scala
@@ -15,7 +15,7 @@ trait BaseGrammars { self: GrammarsUniverse =>
*/
case object BaseGrammar extends SimpleExpressionGrammar {
- def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+ def computeProductions(t: Type): Seq[Prod] = t match {
case BooleanType =>
List(
terminal(BooleanLiteral(false), BooleanC),
diff --git a/src/main/scala/inox/grammars/ClosureGrammars.scala b/src/main/scala/inox/grammars/ClosureGrammars.scala
index 5695a724f..cbf304ab5 100644
--- a/src/main/scala/inox/grammars/ClosureGrammars.scala
+++ b/src/main/scala/inox/grammars/ClosureGrammars.scala
@@ -9,7 +9,7 @@ trait ClosureGrammars { self: GrammarsUniverse =>
import symbols._
case object Closures extends ExpressionGrammar {
- def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] = lab.getType match {
+ def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]] = lab.getType match {
case FunctionType(argsTpes, ret) =>
val args = argsTpes.zipWithIndex.map { case (tpe, i) =>
ValDef(FreshIdentifier("a"+i), tpe)
diff --git a/src/main/scala/inox/grammars/ConstantGrammars.scala b/src/main/scala/inox/grammars/ConstantGrammars.scala
index 88aa7d5b0..f4b33ade7 100644
--- a/src/main/scala/inox/grammars/ConstantGrammars.scala
+++ b/src/main/scala/inox/grammars/ConstantGrammars.scala
@@ -22,7 +22,7 @@ trait ConstantGrammars { self: GrammarsUniverse =>
BooleanLiteral(false)
)
- def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+ def computeProductions(t: Type): Seq[Prod] = {
val literals = collect[Expr]{
case IsTyped(l:Literal[_], `t`) => Set(l)
case _ => Set()
diff --git a/src/main/scala/inox/grammars/ElementaryGrammars.scala b/src/main/scala/inox/grammars/ElementaryGrammars.scala
index d38b2956a..520d29c6e 100644
--- a/src/main/scala/inox/grammars/ElementaryGrammars.scala
+++ b/src/main/scala/inox/grammars/ElementaryGrammars.scala
@@ -9,7 +9,7 @@ trait ElementaryGrammars { self: GrammarsUniverse =>
/** Generates one production rule for each expression in a sequence that has compatible type */
case class OneOf(inputs: Seq[Expr]) extends SimpleExpressionGrammar {
- def computeProductions(lab: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+ def computeProductions(lab: Type): Seq[Prod] = {
inputs.collect {
case i if isSubtypeOf(i.getType, lab.getType) =>
terminal(i)
@@ -23,13 +23,13 @@ trait ElementaryGrammars { self: GrammarsUniverse =>
case g => Seq(g)
}
- def computeProductions(label: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] =
+ def computeProductions(label: Label): Seq[ProductionRule[Label, Expr]] =
subGrammars.flatMap(_.computeProductions(label))
}
/** The empty expression grammar */
case class Empty() extends ExpressionGrammar {
- def computeProductions(l: Label)(implicit ctx: InoxContext) = Nil
+ def computeProductions(l: Label) = Nil
}
}
diff --git a/src/main/scala/inox/grammars/EqualityGrammars.scala b/src/main/scala/inox/grammars/EqualityGrammars.scala
index 45a031405..e5a7bc729 100644
--- a/src/main/scala/inox/grammars/EqualityGrammars.scala
+++ b/src/main/scala/inox/grammars/EqualityGrammars.scala
@@ -13,7 +13,7 @@ trait EqualityGrammars { self: GrammarsUniverse =>
* @param types The set of types for which equalities will be generated
*/
case class EqualityGrammar(types: Set[Type]) extends SimpleExpressionGrammar {
- def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+ def computeProductions(t: Type): Seq[Prod] = t match {
case BooleanType =>
types.toList map { tp =>
nonTerminal(List(tp, tp), { case Seq(a, b) => equality(a, b) }, Equals)
diff --git a/src/main/scala/inox/grammars/ExpressionGrammars.scala b/src/main/scala/inox/grammars/ExpressionGrammars.scala
index 908a662a1..36c44cd61 100644
--- a/src/main/scala/inox/grammars/ExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/ExpressionGrammars.scala
@@ -18,7 +18,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
* @param lab The nonterminal for which production rules will be generated
* @note This is the cached version of [[computeProductions]]. Clients should use this method.
*/
- final def getProductions(lab: Label)(implicit ctx: InoxContext) = {
+ final def getProductions(lab: Label) = {
cache.getOrElse(lab, {
val res = applyAspects(lab, computeProductions(lab))
cache += lab -> res
@@ -31,7 +31,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
* @param lab The nonterminal for which production rules will be generated
* @note Clients should use the cached version, [[getProductions]] instead
*/
- def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]]
+ def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]]
protected def applyAspects(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: InoxContext) = {
lab.aspects.foldLeft(ps) {
@@ -44,7 +44,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
// Union(Seq(this, that))
//}
- final def printProductions(printer: String => Unit)(implicit ctx: InoxContext) {
+ final def printProductions(printer: String => Unit) {
def sorter(lp1: (Label, Seq[ProductionRule[Label, Expr]]), lp2: (Label, Seq[ProductionRule[Label, Expr]])): Boolean = {
val l1 = lp1._1
val l2 = lp2._1
diff --git a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
index 52b2de1d1..b798e360a 100644
--- a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
+++ b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
@@ -16,7 +16,7 @@ trait FunctionCallsGrammars extends utils.Helpers { self: GrammarsUniverse =>
* @param exclude An additional set of functions for which no calls will be generated
*/
case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type], exclude: Set[FunDef]) extends SimpleExpressionGrammar {
- def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+ def computeProductions(t: Type): Seq[Prod] = {
def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
// Prevents recursive calls
diff --git a/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala b/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
index b571a3254..6282c5254 100644
--- a/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
@@ -25,20 +25,20 @@ trait SimpleExpressionGrammars { self: GrammarsUniverse =>
def filter(f: Prod => Boolean) = {
new SimpleExpressionGrammar {
- def computeProductions(lab: Type)(implicit ctx: InoxContext) = {
+ def computeProductions(lab: Type) = {
SimpleExpressionGrammar.this.computeProductions(lab).filter(f)
}
}
}
// Finalize this to depend only on the type of the label
- final def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] = {
+ final def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]] = {
computeProductions(lab.getType).map { p =>
ProductionRule(p.subTrees.map(Label(_)), p.builder, p.tag, p.cost)
}
}
/** Version of [[ExpressionGrammar.computeProductions]] which depends only a [[Type]] */
- def computeProductions(tpe: Type)(implicit ctx: InoxContext): Seq[Prod]
+ def computeProductions(tpe: Type): Seq[Prod]
}
}
diff --git a/src/main/scala/inox/grammars/ValueGrammars.scala b/src/main/scala/inox/grammars/ValueGrammars.scala
index ea38e87b6..81055c3ba 100644
--- a/src/main/scala/inox/grammars/ValueGrammars.scala
+++ b/src/main/scala/inox/grammars/ValueGrammars.scala
@@ -10,7 +10,7 @@ trait ValueGrammars { self: GrammarsUniverse =>
/** A grammar of values (ground terms) */
case object ValueGrammar extends SimpleExpressionGrammar {
- def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+ def computeProductions(t: Type): Seq[Prod] = t match {
case BooleanType =>
List(
terminal(BooleanLiteral(true), One),
diff --git a/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala b/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
index 82c35c28c..3f617782a 100644
--- a/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
@@ -13,7 +13,7 @@ trait DepthBoundAspects { self: GrammarsUniverse =>
def asString(implicit opts: PrinterOptions): String = s"D$depth"
- def applyTo(l: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ def applyTo(l: Label, ps: Seq[Production]) = {
if (depth == 0) Nil
else if (depth == 1) ps.filter(_.isTerminal)
else {
diff --git a/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala b/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
index a64294ae8..209037698 100644
--- a/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
@@ -19,7 +19,7 @@ trait ExtraTerminalsAspects { self: GrammarsUniverse =>
s.toList.map(_.asString(opts)).mkString("{", ",", "}")
}
- override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ override def applyTo(lab: Label, ps: Seq[Production]) = {
super.applyTo(lab, ps) ++ {
s.filter(e => isSubtypeOf(e.getType, lab.getType)).map { e =>
ProductionRule[Label, Expr](Nil, { (es: Seq[Expr]) => e }, Top, formulaSize(e))
diff --git a/src/main/scala/inox/grammars/aspects/PersistentAspects.scala b/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
index 6f35c218b..ff54abec8 100644
--- a/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
@@ -20,7 +20,7 @@ trait PersistentAspects { self: GrammarsUniverse =>
* e + 1
*/
abstract class PersistentAspect extends Aspect {
- def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ def applyTo(lab: Label, ps: Seq[Production]) = {
ps.map { p =>
p.copy(subTrees = p.subTrees.map(lab => lab.withAspect(this)))
}
diff --git a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
index abbbe29d7..f5ed9bd5c 100644
--- a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
@@ -28,7 +28,7 @@ trait SimilarToAspects { self: GrammarsUniverse =>
* f(a, ~b~)
* f(b, a) // if non-commut
*/
- def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ def applyTo(lab: Label, ps: Seq[Production]) = {
def isCommutative(e: Expr) = e match {
case _: EPlus | _: ETimes => true
case _ => false
diff --git a/src/main/scala/inox/grammars/aspects/SizeAspects.scala b/src/main/scala/inox/grammars/aspects/SizeAspects.scala
index 2d39d2fee..911b79798 100644
--- a/src/main/scala/inox/grammars/aspects/SizeAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/SizeAspects.scala
@@ -15,7 +15,7 @@ trait SizeAspects { self: GrammarsUniverse =>
case class Sized(size: Int) extends Aspect {
def asString(implicit opts: PrinterOptions) = "|"+size+"|"
- def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ def applyTo(lab: Label, ps: Seq[Production]) = {
val optimizeCommut = true
ps.flatMap { p =>
diff --git a/src/main/scala/inox/grammars/aspects/TaggedAspects.scala b/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
index ab9736938..34126a2c5 100644
--- a/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
@@ -19,7 +19,7 @@ trait TaggedAspects { self: GrammarsUniverse =>
*/
def asString(implicit opts: PrinterOptions): String = s"#$tag$cString@$pos"
- def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ def applyTo(lab: Label, ps: Seq[Production]) = {
// Tags to avoid depending on parent aspect
val excludedTags: Set[Tag] = (tag, pos) match {
diff --git a/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala b/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
index 5338f213b..c1fc410a4 100644
--- a/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
@@ -12,7 +12,7 @@ trait TypeDepthBoundAspects { self: GrammarsUniverse =>
case class TypeDepthBound(bound: Int) extends PersistentAspect {
override def asString(implicit opts: PrinterOptions): String = "" // This is just debug pollution to print
- override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+ override def applyTo(lab: Label, ps: Seq[Production]) = {
if (depth(lab.getType) > bound) Nil
else super.applyTo(lab, ps)
}
--
GitLab