package dk.brics.defuse.impl.lattice.value

import dk.brics.defuse.framework.lattice.value.{BooleanClass, StringClass, NumberClass}

object Polarity {

  implicit object Witness extends NumberClass[Polarity] {
    /**
     * Returns the minimum representable integer.
     */
    def MinValue: Polarity = ???

    /**
     * Returns the maximum representable integer.
     */
    def MaxValue: Polarity = ???

    /**
     * Abstraction of Positive Infinity.
     */
    def PosInf: Polarity = ???

    /**
     * Abstraction of Negative Infinity.
     */
    def NegInf: Polarity = ???

    /**
     * Abstraction of Not A Number.
     */
    def NaN: Polarity = ???

    /**
     * Lifts the given integer `i` into the abstraction.
     */
    def lift(i: Int): Polarity = ???;

    /**
     * Lifts the given double `d` into the abstraction.
     */
    def lift(d: Double): Polarity = ???;

    /**
     * Lifts the given range `r` into the abstraction.
     */
    def lift(r: Range): Polarity = ???

    /**
     * Returns true iff the given abstract number `n` represents a single concrete number.
     */
    def isConcrete(n: Polarity): Boolean = ???;

    /**
     * Returns the increment of `n`.
     */
    def increment(n: Polarity): Polarity = ???

    /**
     * Returns the decrement of `n`.
     */
    def decrement(n: Polarity): Polarity = ???

    /**
     * Returns the complement of `n`.
     */
    def complement(n: Polarity): Polarity = ???

    /**
     * Returns the unary plus of `n`.
     */
    def unaryPlus(n: Polarity): Polarity = ???

    /**
     * Returns the unary minus of `n`.
     */
    def unaryMinus(n: Polarity): Polarity = ???

    /**
     * Returns the sum of `n1` and `n2`.
     */
    def plus(n1: Polarity, n2: Polarity): Polarity = ???;

    /**
     * Returns the difference of `n1` and `n2`.
     */
    def minus(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the product of `n1` and `n2`.
     */
    def times(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the quotient of `n1` and `n2`.
     */
    def divide(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the modulus of `n1 % n2`.
     */
    def modulo(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the left shift of `n1` by `n2`.
     */
    def shiftLeft(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the right shift of `n1` by `n2`.
     */
    def shiftRight(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the unsigned right shift of `n1` by `n2`.
     */
    def unsignedShiftRight(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the bitwise and of `n1` and `n2`.
     */
    def bitwiseAnd(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the bitwise or of `n1` and `n2`.
     */
    def bitwiseOr(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the bitwise xor of `n1` and `n2`.
     */
    def bitwiseXOr(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the absolute value of `n`.
     */
    def abs(n: Polarity): Polarity = ???

    /**
     * Returns the ceiling of `n`.
     */
    def ceil(n: Polarity): Polarity = ???

    /**
     * Returns the floor of `n`.
     */
    def floor(n: Polarity): Polarity = ???

    /**
     * Returns the nearest integer of `n`.
     */
    def round(n: Polarity): Polarity = ???

    /**
     * Returns the minimum value of `n1` and `n2`.
     */
    def min(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the maximum value of `n1` and `n2`.
     */
    def max(n1: Polarity, n2: Polarity): Polarity = ???

    /**
     * Returns the exponentiation of `n`.
     */
    def exp(n: Polarity): Polarity = ???

    /**
     * Returns the natural logarithm of `n`.
     */
    def log(n: Polarity): Polarity = ???

    /**
     * Returns `b` lifted to the power of `e`.
     */
    def pow(b: Polarity, e: Polarity): Polarity = ???

    /**
     * Returns the square root of `n`.
     */
    def sqrt(n: Polarity): Polarity = ???

    /**
     * Returns the arc tangent of the quotient.
     */
    def atan2(y: Polarity, x: Polarity): Polarity = ???

    /**
     * Returns the arc cosine of `n`.
     */
    def acos(n: Polarity): Polarity = ???

    /**
     * Returns the arc sine of `n`.
     */
    def asin(n: Polarity): Polarity = ???

    /**
     * Returns the arc tangent of `n`.
     */
    def atan(n: Polarity): Polarity = ???

    /**
     * Returns the cosine of `n`.
     */
    def cos(n: Polarity): Polarity = ???

    /**
     * Returns the sine of `n`.
     */
    def sin(n: Polarity): Polarity = ???

    /**
     * Returns the tangent of `n`.
     */
    def tan(n: Polarity): Polarity = ???

    /**
     * Returns an abstract boolean indicating whether `n1 < n2`.
     */
    def less[B: BooleanClass](n1: Polarity, n2: Polarity): B = ???

    /**
     * Returns an abstract boolean indicating whether `n1 <= n2`.
     */
    def lessEqual[B: BooleanClass](n1: Polarity, n2: Polarity): B = ???

    /**
     * Returns an abstract boolean indicating whether `n1 > n2`.
     */
    def greater[B: BooleanClass](n1: Polarity, n2: Polarity): B = ???

    /**
     * Returns an abstract boolean indicating whether `n1 >= n2`.
     */
    def greaterEqual[B: BooleanClass](n1: Polarity, n2: Polarity): B = ???

    /**
     * Returns an abstract boolean indicating whether `n1 == n2`.
     */
    def equal[B: BooleanClass](n1: Polarity, n2: Polarity): B = ???

    /**
     * Coerces the given number `n` to a string.
     */
    def coerce2str[S: StringClass](n: Polarity): S = ???

    /**
     * Returns a human readable string representation of the given number `n`.
     */
    def toString(n: Polarity): String = n.toString;

    /**
     * Returns the bottom element.
     */
    def bot: Polarity = BotPolarity;

    /**
     * Returns the join (least upper bound) of `e1` and `e2`.
     */
    def join(e1: Polarity, e2: Polarity): Polarity = ???;

    /**
     * Returns true iff `e1` is smaller (= more precise than) or equal to `e2`.
     */
    def <=(e1: Polarity, e2: Polarity): Boolean = ???;

    /**
     * Returns the top element.
     */
    def top: Polarity = ???;

    /**
     * Returns the meet (the greatest lower bound) of `b1` and `b2`.
     */
    def meet(e1: Polarity, e2: Polarity): Polarity = ???
  }

}

trait Polarity;

protected case object TopPolarity extends Polarity;

protected case object Odd extends Polarity;

protected case object Even extends Polarity;

protected case object BotPolarity extends Polarity;