Skip to content

Commit

Permalink
Extract SymbolTransformerComposition to not be local (#220)
Browse files Browse the repository at this point in the history
  • Loading branch information
sankalpgambhir authored Aug 27, 2024
1 parent 75edeec commit bcf5437
Showing 1 changed file with 31 additions and 23 deletions.
54 changes: 31 additions & 23 deletions src/main/scala/inox/transformers/SymbolTransformer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,29 +13,7 @@ trait SymbolTransformer { self =>
def compose(that: SymbolTransformer { val t: self.s.type }): SymbolTransformer {
val s: that.s.type
val t: self.t.type
} = {
/** Enables equality checks between symbol transformer compositions */
class SymbolTransformerComposition(protected val lhs: self.type,
protected val rhs: that.type)
(override val s: rhs.s.type,
override val t: self.t.type)
extends SymbolTransformer {

override def transform(syms: s.Symbols): t.Symbols = lhs.transform(rhs.transform(syms))

override def equals(that: Any): Boolean = that match {
// NOTE: there is a spurious warning saying:
// "the type test for SymbolTransformerComposition cannot be checked at runtime because it's a local class"
// but the type test actually works as expected
case c: SymbolTransformerComposition => rhs == c.rhs && lhs == c.lhs
case _ => false
}

override def hashCode: Int = 31 * rhs.hashCode + lhs.hashCode
}

new SymbolTransformerComposition(self, that)(that.s, self.t)
}
} = SymbolTransformerComposition(self, that)

def andThen(that: SymbolTransformer {
val s: self.t.type
Expand All @@ -59,6 +37,36 @@ trait SimpleSymbolTransformer extends SymbolTransformer { self =>
.withFunctions(syms.functions.values.toSeq.map(transformFunction))
.withSorts(syms.sorts.values.toSeq.map(transformSort))
}

/** Enables equality checks between symbol transformer compositions */
class SymbolTransformerComposition(protected val left: SymbolTransformer,
protected val right: SymbolTransformer { val t: left.s.type })
(override val s: right.s.type,
override val t: left.t.type)
extends SymbolTransformer {


override def transform(syms: s.Symbols): t.Symbols = left.transform(right.transform(syms))

override def equals(that: Any): Boolean = that match {
// NOTE: there is a spurious warning saying:
// "the type test for SymbolTransformerComposition cannot be checked at runtime because it's a local class"
// but the type test actually works as expected
case c: SymbolTransformerComposition => right == c.right && left == c.left
case _ => false
}

override def hashCode: Int = 31 * right.hashCode + left.hashCode
}

object SymbolTransformerComposition {
def apply(left: SymbolTransformer, right: SymbolTransformer {val t: left.s.type}): SymbolTransformer {
val s: right.s.type
val t: left.t.type
} =
class LocalComposition(lhs: left.type, rhs: right.type, s: right.s.type, t: left.t.type) extends SymbolTransformerComposition(left, right)(s, t)
new LocalComposition(left, right, right.s, left.t)
}

object SymbolTransformer {
def apply(trans: DefinitionTransformer): SymbolTransformer {
Expand Down

0 comments on commit bcf5437

Please sign in to comment.