Skip to content

@Ricordel /scala_sign_detection.scala
Last active

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Sign detection in Scala
////////////////////////////////////////////////////////////////////////////////
//
// To implement the Sign arithmetic, we can do it in several steps:
// - first we must define the arithmetic on the "base" values:
// Pos, Neg, Zero, NoneA, ErrA
// - then we can deduce the arithmetic of the whole domain by using
// upper bounds
//
// The aforementioned reduction to core signs can be performed on both
// operands: the left and the right.
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// Here is defined the arithmetic, in its own object. It's more centralized
// and more symmetric to have it that way than spread among all the objects
// representing the signs.
//
///////////////////////////////////////////////////////////////////////////////
trait Arithmetic {
def add(x: Sign, y: Sign): Sign
def sub(x: Sign, y: Sign): Sign
def mult(x: Sign, y: Sign): Sign
def div(x: Sign, y: Sign): Sign
def le(x: Sign, y: Sign): Bool
def eq(x: Sign, y: Sign): Bool
}
object SignArithmetic extends Arithmetic {
// The following functions define the basic operations on core types
val addCore: (CoreSign, CoreSign) => Sign =
(x, y) => (x, y) match {
case (Neg, Neg) => Neg ; case (Neg, Zero) => Neg ; case (Neg, Pos) => Z
case (Zero, Neg) => Neg ; case (Zero, Zero) => Zero ; case (Zero, Pos) => Pos
case (Pos, Neg) => Z ; case (Pos, Zero) => Pos ; case (Pos, Pos) => Pos
case (ErrA, _) | (_, ErrA) => ErrA
case (NoneA, _) | (_, NoneA) => NoneA
}
val subCore: (CoreSign, CoreSign) => Sign =
(x, y) => (x, y) match {
case (Neg, Neg) => Z ; case (Neg, Zero) => Neg ; case (Neg, Pos) => Neg
case (Zero, Neg) => Pos ; case (Zero, Zero) => Zero ; case (Zero, Pos) => Neg
case (Pos, Neg) => Pos ; case (Pos, Zero) => Pos ; case (Pos, Pos) => Z
case (ErrA, _) | (_, ErrA) => ErrA
case (NoneA, _) | (_, NoneA) => NoneA
}
val multCore: (CoreSign, CoreSign) => Sign =
(x, y) => (x, y) match {
case (Neg, Neg) => Pos ; case (Neg, Zero) => Zero ; case (Neg, Pos) => Neg
case (Zero, Neg) => Zero ; case (Zero, Zero) => Zero ; case (Zero, Pos) => Zero
case (Pos, Neg) => Neg ; case (Pos, Zero) => Zero ; case (Pos, Pos) => Pos
case (ErrA, _) | (_, ErrA) => ErrA
case (NoneA, _) | (_, NoneA) => NoneA
}
// Be careful: ineger division can give zero even with two non-zero arguments
val divCore: (CoreSign, CoreSign) => Sign =
(x, y) => (x, y) match {
case (Neg, Neg) => NonNeg ; case (Neg, Zero) => ErrA ; case (Neg, Pos) => NonPos
case (Zero, Neg) => Zero ; case (Zero, Zero) => ErrA ; case (Zero, Pos) => Zero
case (Pos, Neg) => NonPos ; case (Pos, Zero) => ErrA ; case (Pos, Pos) => NonNeg
case (ErrA, _) | (_, ErrA) => ErrA
case (NoneA, _) | (_, NoneA) => NoneA
}
val eqCore: (CoreSign, CoreSign) => Bool =
(x, y) => (x, y) match {
case (Neg, Neg) => T ; case (Neg, Zero) => FF ; case (Neg, Pos) => FF
case (Zero, Neg) => FF ; case (Zero, Zero) => TT ; case (Zero, Pos) => FF
case (Pos, Neg) => FF ; case (Pos, Zero) => FF ; case (Pos, Pos) => T
case (ErrA, _) | (_, ErrA) => ErrB
case (NoneA, _) | (_, NoneA) => NoneB
}
val leCore: (CoreSign, CoreSign) => Bool =
(x, y) => (x, y) match {
case (Neg, Neg) => T ; case (Neg, Zero) => TT ; case (Neg, Pos) => TT
case (Zero, Neg) => FF ; case (Zero, Zero) => TT ; case (Zero, Pos) => TT
case (Pos, Neg) => FF ; case (Pos, Zero) => FF ; case (Pos, Pos) => T
case (ErrA, _) | (_, ErrA) => ErrB
case (NoneA, _) | (_, NoneA) => NoneB
}
// This function contains the logic to use the operations on core types on every
// composed types by decomposing them down to their core types
def composedOp(op: (CoreSign, CoreSign) => Sign, x: Sign, y: Sign) = (x, y) match {
case (xc: CoreSign, yc: CoreSign) => op(xc, yc)
case (xc: CoreSign, yub: UpperBoundSign) => yub.signs map { s => op(xc, s) } reduce { _ | _ }
case (xub: UpperBoundSign, yc: CoreSign) => xub.signs map { s => op(s, yc) } reduce { _ | _ }
case (xub: UpperBoundSign, yub: UpperBoundSign) => {
val allCombs = for {
s1 <- xub.signs
s2 <- yub.signs
} yield op(s1, s2)
allCombs reduce { _ | _ }
}
}
// This is the same for Bool. I cannot find how to remove the duplication as
// I don't manage to coherce the types correctly. Definitely need to learn
// Scala for real...
def composedOp(op: (CoreSign, CoreSign) => Bool, x: Sign, y: Sign) = (x, y) match {
case (xc: CoreSign, yc: CoreSign) => op(xc, yc)
case (xc: CoreSign, yub: UpperBoundSign) => yub.signs map { s => op(xc, s) } reduce { _ | _ }
case (xub: UpperBoundSign, yc: CoreSign) => xub.signs map { s => op(s, yc) } reduce { _ | _ }
case (xub: UpperBoundSign, yub: UpperBoundSign) => {
val allCombs = for {
s1 <- xub.signs
s2 <- yub.signs
} yield op(s1, s2)
allCombs reduce { _ | _ }
}
}
// These are the actual methods that will be called on the arithmetic
def add(x: Sign, y: Sign) = composedOp(addCore, x, y)
def sub(x: Sign, y: Sign) = composedOp(subCore, x, y)
def mult(x: Sign, y: Sign) = composedOp(multCore, x, y)
def div(x: Sign, y: Sign) = composedOp(divCore, x, y)
def eq(x: Sign, y: Sign) = composedOp(eqCore, x, y)
def le(x: Sign, y: Sign) = composedOp(leCore, x, y)
}
////////////////////////////////////////////////////////////////////////////////
//
// This trait represents what is a Sign in Sign analysis, and uses the
// previously defined Arithmetic to define its behaviour.
//
////////////////////////////////////////////////////////////////////////////////
sealed trait Sign {
val arith = SignArithmetic
def +(other: Sign): Sign = arith.add(this, other)
def -(other: Sign): Sign = arith.sub(this, other)
def *(other: Sign): Sign = arith.mult(this, other)
def /(other: Sign): Sign = arith.div(this, other)
def <=(other: Sign): Bool = arith.le(this, other)
def ===(other: Sign): Bool = arith.le(this, other)
// Upper bound
def |(other: Sign): Sign
}
// Companion object, be able to construct Sign instances from real numbers
object Sign {
def apply(n: Int) = if (n < 0) Neg
else if (n == 0) Zero
else Pos
}
// This trait will represent the 'basic' signs
sealed trait CoreSign extends Sign
//////// Here follows the instances of the basic signs /////////
case object Pos extends CoreSign {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case NoneA | Pos => Pos
case NonNeg | Zero => NonNeg
case NonZero | Neg => NonZero
case NonPos | Z => Z
}
}
case object Neg extends CoreSign {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case NonNeg | Z => Z
case NoneA | Neg => Neg
case NonPos | Zero => NonPos
case NonZero | Pos => NonZero
}
}
case object Zero extends CoreSign {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case NonZero | Z => Z
case NoneA | Zero => Zero
case NonPos | Neg => NonPos
case NonNeg | Pos => NonNeg
}
}
case object NoneA extends CoreSign {
def |(other: Sign): Sign = other
}
case object ErrA extends CoreSign {
def |(other: Sign): Sign = other match {
case ErrA => ErrA
case _ => AnyA
}
}
///////////////////////////////////////////////////////////////////////////////
//
// Here follows the declaration of all the 'composed' Signs we have, that
// actually correspond to the upper-bounds of diverse subsets of P(CoreSign)
//
////////////////////////////////////////////////////////////////////////////////
// This is the global trait
sealed abstract class UpperBoundSign(val signs: CoreSign*) extends Sign
// And below the diverse implementations
case object NonNeg extends UpperBoundSign(Pos, Zero) {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case NonPos | Neg | Z | NonZero => Z
case NonNeg | Zero | Pos | NoneA => NonNeg
}
}
case object NonPos extends UpperBoundSign(Neg, Zero) {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case NonNeg | Pos | Z | NonZero => Z
case NonPos | Zero | Neg | NoneA => NonPos
}
}
case object NonZero extends UpperBoundSign(Neg, Pos) {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case Zero | NonPos | NonNeg | Z => Z
case Pos | Neg | NonZero | NoneA => NonZero
}
}
case object Z extends UpperBoundSign(Neg, Pos, Zero) {
def |(other: Sign) = other match {
case AnyA | ErrA => AnyA
case _ => Z
}
}
case object AnyA extends UpperBoundSign(Neg, Pos, Zero, ErrA) {
def |(other: Sign) = AnyA
}
///////////////////////////////////////////////////////////////////////////////
//
// Following is the implementation of the abstract Bool domain, abstracting
// over boolean operations. We don't go with the same factorization than
// for the Signs as here there are a lot less values, this would be far
// less interesting.
//
///////////////////////////////////////////////////////////////////////////////
sealed trait Bool {
def unary_! : Bool
def &&(other: Bool): Bool
def |(other: Bool): Bool
}
// A valid boolean which value is uncertain
case object T extends Bool {
def unary_! = T
def &&(other: Bool) = other match {
case FF => FF
case ErrB => ErrB
case AnyB => AnyB
case _ => T
}
def |(other: Bool) = other match {
case AnyB | ErrB => AnyB
case _ => T
}
}
// True, for sure
case object TT extends Bool {
def unary_! = FF
def &&(other: Bool) = other match {
case TT => TT
case FF => FF
case ErrB => ErrB
case AnyB => AnyB
case _ => T
}
def |(other: Bool): Bool = other match {
case TT => TT
case AnyB | ErrB => AnyB
case _ => T
}
}
// False, for sure
case object FF extends Bool {
def unary_! = TT
def &&(other: Bool) = other match {
case ErrB => ErrB
case _ => FF
}
def |(other: Bool): Bool = other match {
case FF => FF
case AnyB | ErrB => AnyB
case _ => T
}
}
// Error (results of an error in the evaluation of operands for EQ or LE)
case object ErrB extends Bool {
def unary_! = ErrB
def &&(other: Bool) = ErrB
def |(other: Bool): Bool = other match {
case ErrB => ErrB
case _ => AnyB
}
}
// Anything, possibly an error
case object AnyB extends Bool {
def unary_! = AnyB
def &&(other: Bool) = AnyB
def |(other: Bool) = AnyB
}
// Not initialized yet, bottom value of the lattice
case object NoneB extends Bool {
def unary_! = NoneB
def &&(other: Bool) = NoneB
def |(other: Bool) = other
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.