SDouble { {{
  public double doubleValue() {
    if (this instanceof PDouble) {
      return v.doubleValue();
    }
    return -1.0 * v.doubleValue();
  }
}} }