/*

** Copyright (C) 2018 Martin Brain

**

** See the file LICENSE for licensing information.

*/

/*

** unpackedFloat.h

**

** Martin Brain

** martin.brain@cs.ox.ac.uk

** 03/06/14

**

** The working representation of a floating-point number.  This is

** from the packed representation in a few ways:

**

**  1. Explicit flags for NaN, Inf and Zero.

**  2. Significand is biased.

**  3. Hidden bit is explicit.

**  4. Subnormals are normalised.

**

** This makes numbers more uniform and makes it easier to implement

** compact and efficient algorithms.

*/

#include "symfpu/utils/common.h"

#include "symfpu/utils/properties.h"

#include "symfpu/utils/numberOfRoundingModes.h"

#include "symfpu/core/ite.h"

#include "symfpu/core/operations.h"

// For debugging only

#include <iostream>

#ifndef SYMFPU_UNPACKED_FLOAT

#define SYMFPU_UNPACKED_FLOAT

namespace symfpu {

  template<class t>

  public :

    // Typedef the names from the traits for convenience

    typedef typename t::bwt bwt;

    typedef typename t::fpt fpt;

    typedef typename t::prop prop;

    typedef typename t::sbv sbv;

    typedef typename t::ubv ubv;

  protected :

    // TODO : protect these again

  public :

    prop nan;

    prop inf;

    prop zero;

    prop sign;

    sbv exponent;

    ubv significand;

  protected :

    // It is possible, but hopefully as difficult as possible to create,

    // via the constructor an invalid unpacked float

    // A piecewise / literal constructor using fpclass

    enum fpclass { FPCLASS_NAN, FPCLASS_INF, FPCLASS_ZERO, FPCLASS_NUMBER };

    // Should only be used by ite

    friend ite<prop, unpackedFloat<t> >;

    // TODO : See above -- this should only be used by ite

  public :

		   const prop &iteSign, const sbv &iteExponent, const ubv &iteSignificand) :

      nan(iteNaN), inf(iteInf), zero(iteZero),

  private :

    // Used for special values

    // However this will also be passed through the operations, thus

    // if it is also a valid normal number then it will make proving

    // invariants easier.  In this case it is the value 1.0.

    }

    }

  public :

      nan(false), inf(false), zero(false),

    // An intermediate point in some operations is producing a value in an extended

    // format (for example, multiply produces an intermediate value with one extra exponent

    // bit and double the number of significand bits).  However the unpacked size of the

    // significand is larger than the bits given by the format.  This constructor does

    // the appropriate extension so that what is constructed is a valid unpacked float

    // in the given format.

      nan(false), inf(false), zero(false),

    // Copy and over-write sign

    // Swap back-ends

      template <class s> friend class unpackedFloat;

    template <class s>

    }

    }

    }

    //    inline unpackedFloat<t> changeSign(const prop &newSign) {

    //      return unpackedFloat<t>(*this, newSign);

    //    }

    // Get the number of bits in the unpacked format corresponding to a

    // given packed format.  These are the unpacked counter-parts of

    //  format.exponentWidth() and format.significandWidth()

      // This calculation is a little more complex than you might think...

      // Note that there is one more exponent above 0 than there is

      // below.  This is the opposite of 2's compliment but this is not

      // a problem because the highest packed exponent corresponds to

      // inf and NaN and is thus does not need to be represented in the

      // unpacked format.

      // However we do need to increase it to allow subnormals (packed)

      // to be normalised.

      // The smallest exponent is:

      //  -2^(format.exponentWidth() - 1) - 2  -  (format.significandWidth() - 1)

      //

      // We need an unpacked exponent width u such that

      //  -2^(u-1) <= -2^(format.exponentWidth() - 1) - 2  -     (format.significandWidth() - 1)

      //           i.e.

      //   2^(u-1) >=  2^(format.exponentWidth() - 1)      +     (format.significandWidth() - 3)

	// Subnormals fit into the gap between minimum normal exponent and what is represenatble

	// using a signed number

      }

	// Significand is short compared to exponent range,

	// one extra bit should be sufficient

      } else {

	// Significand is long compared to exponent range

      }

    }

      // Hidden bit is already included in the floating-point format

    }

    // These should all evaluate to a literal value but are given as

    // sbv's to make their use easier and to avoid concerns of overflow.

    }

    }

    }

    }

    }

    // Note the different return type as this is used for iteration in remainder

    }

    // knownInFormat uses the format invariant to simplify the test

    }

    // knownInFormat uses the format invariant to simplify the test

      // To share tests with the inNormalRange test...

    }

    }

    // The amount needed to normalise the number

      return max<t>(minNormalExponent(format) - exponent,

    }

    }

    }

    // Likewise, this is a convenience function

    }

    }

      return unpackedFloat<t>(this->nan,

			      this->inf,

			      this->zero,

			      this->sign,

			      this->exponent.extend(expExtension),

    }

    // Moves the leading 1 up to the correct position, adjusting the

    // exponent as required.

      // Optimisation : could move the zero detect version in if used in all cases

      //  catch - it zero detection in unpacking is different.

    }

      return ITE(normal.isZero,

		 unpackedFloat<t>::makeZero(format, this->sign),

    }

#if 0

    // Moves the leading 1 up to the correct position, adjusting the

    // exponent as required.

    unpackedFloat<t> normaliseUp (const fpt &/*format*/) const {

      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.

      ubv alignAmount(countLeadingZeros<t>(this->significand));

      ubv alignedSignificand(this->significand.modularLeftShift(alignAmount)); // CLZ means data is not lost

      sbv signedAlignAmount(alignAmount.extract(this->exponent.getWidth() - 1,0).toSigned());

      // May loose data / be incorrect for very small exponents and very large significands

      sbv correctedExponent(this->exponent - signedAlignAmount);

      // Optimisation : could move the zero detect version in if used in all cases

      return unpackedFloat<t>(this->sign, correctedExponent, alignedSignificand);

    }

    unpackedFloat<t> normaliseUpDetectZero (const fpt &format) const {

      unpackedFloat<t> normal(this->normaliseUp(format));

      return ITE(this->significand.isAllZeros(),

		 unpackedFloat<t>::makeZero(format, this->sign),

		 normal);

    }

#endif

#if 0

    unpackedFloat<t> normaliseUp (const fpt &format) const {

      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.

      unpackedFloat<t> working(*this);

      bwt sigWidth = unpackedFloat<t>::significandWidth(format);

      bwt exWidth = unpackedFloat<t>::exponentWidth(format);

      // TODO : is range checking needed here?  Only in obscure use cases.

      for (bwt power = previousPowerOfTwo(sigWidth); power != 0; power >>= 1) {

	bwt rem = sigWidth - power;

	INVARIANT(rem > 0);

	ubv mask(ubv::allOnes(power).extend(rem) << rem);

	prop shiftNeeded((mask & working.significand).isAllZeros());

	// Has to be modular as in the case it is not needed,

	// performing the shift will loose information.

	working.significand = ITE(shiftNeeded, working.significand.modularLeftShift(power), working.significand);

	working.exponent = ITE(shiftNeeded, working.exponent - sbv(exWidth,power), working.exponent);

        // Optimisation : rather than add each cycle, build shiftNeeded into a number and add once.

      }

      return working;

    }

#endif

    // Is a well formed unpacked struct of the given format?

    // The format is needed to ensure that subnormals are correct.

    // This invariant does not hold at all points in the code!

		   (sigWidth == significand.getWidth()));

      // At most one flag is true

      // If one flag is true then exponent and significand are defaults

      // NaN has sign = 0

      // Exponent is in range

      // Has a leading one

      // Subnormal numbers require an additional check to make sure they

      // do not have an unrepresentable amount of significand bits.

		(subnormalAmount <= sbv(exWidth,sigWidth)));

      // Invariant implies this following steps do not loose data

			      subnormalAmount.toUnsigned().matchWidth(significand) :

			      subnormalAmount.toUnsigned().extract(sigWidth - 1, 0)

			      ));

    }

      /* Older version

       * Correct but replaced with a version which gives more propagation friendly assertions.

       */

#if 0

    prop valid(const fpt &format) const {

      bwt exWidth = exponentWidth(format);

      bwt sigWidth = significandWidth(format);

      PRECONDITION((exWidth == exponent.getWidth()) &&

		   (sigWidth == significand.getWidth()));

      prop hasLeadingOne(!(leadingOne(unpackedFloat<t>::significandWidth(format)) & significand).isAllZeros());

      // Subnormal numbers require an additional check to make sure they

      // do not have an unrepresentable amount of significand bits.

      sbv subnormalAmount(this->getSubnormalAmount(format));

      INVARIANT((sbv::zero(exWidth) <= subnormalAmount) &&

		(subnormalAmount <= sbv(exWidth,sigWidth)));

      // Invariant implies this following steps do not loose data

      ubv trimmedSubnormalAmount(subnormalAmount.toUnsigned().extract(positionOfLeadingOne(sigWidth),0));

      ubv mask(trimmedSubnormalAmount.orderEncode(sigWidth));

      prop correctlyAbbreviated((mask & significand).isAllZeros());

      prop normalCase   (!nan && !inf && !zero && inNormalRange(format, prop(false))    && hasLeadingOne);

      prop subnormalCase(!nan && !inf && !zero && inSubnormalRange(format, prop(false)) && hasLeadingOne && correctlyAbbreviated);

      prop exponentIsDefault(defaultExponent(format) == exponent);

      prop significandIsDefault(defaultSignificand(format) == significand);

      prop NaNCase ( nan && !inf && !zero && exponentIsDefault && significandIsDefault && !sign);

      prop InfCase (!nan &&  inf && !zero && exponentIsDefault && significandIsDefault);

      prop ZeroCase(!nan && !inf &&  zero && exponentIsDefault && significandIsDefault);

      return (NaNCase || InfCase || ZeroCase || normalCase || subnormalCase);

    }

#endif

    // Just for debugging

    void print (void) const {

      std::cerr << "nan : " << this->nan << '\t'

		<< "inf : " << this->inf << '\t'

		<< "zero : " << this->zero << '\t'

		<< "sign : " << this->sign << '\t'

		<< "exponent : " << this->exponent << '\t'

		<< "significand : " << this->significand << std::endl;

    }

  };

template <class t>

  struct ite<typename t::prop, unpackedFloat<t> > {

			    const unpackedFloat<t> &l,

			    const unpackedFloat<t> &r) {

			    ITE(cond, l.exponent, r.exponent),

    }

 };

}

#endif