package components.naturalnumber;

import components.stack.Stack;
import components.stack.Stack1L;

/**
 * {@code NaturalNumber} represented as a {@link Stack<Integer>} with
 * implementations of primary methods.
 *
 * <p>
 * Execution-time performance of all methods implemented in this class is O(1),
 * except the constructors from {@code String} (which is O(|{@code s}|)) and
 * from {@code NaturalNumber} (which is O(log {@code n})).
 *
 * @mathdefinitions {@code
 * HAS_ONLY_DIGITS (
 *   s: string of integer
 *  ): boolean satisfies
 *  if s = empty_string
 *   then HAS_ONLY_DIGITS (s) = true
 *   else for all a: string of integer, k: integer where (s = a * <k>)
 *         (HAS_ONLY_DIGITS (s) = (HAS_ONLY_DIGITS (a)  and  0 <= k < 10))
 *
 * IS_WELL_FORMED_RADIX_REPRESENTATION (
 *   s: string of integer
 *  ): boolean is
 *  s = empty_string  or
 *      there exists k: integer, a: string of integer
 *       (s = <k> * a  and
 *        1 <= k < 10  and
 *        HAS_ONLY_DIGITS (a))
 *
 * NUMERICAL_VALUE (
 *   s: string of integer
 *  ): integer satisfies
 *  if s = empty_string
 *   then NUMERICAL_VALUE (s) = 0
 *   else for all a: string of integer, k: integer where (s = a * <k>)
 *         (NUMERICAL_VALUE (s) = NUMERICAL_VALUE (a) * 10 + k)
 *
 * REVERSED_STRING_OF_DIGITS (
 *   n: NATURAL
 *  ): string of integer satisfies
 *  if n = 0
 *  then REVERSED_STRING_OF_DIGITS (n) = empty_string
 *  else REVERSED_STRING_OF_DIGITS (n) = <n mod 10> * REVERSED_STRING_OF_DIGITS (n / 10)
 * }
 * @convention IS_WELL_FORMED_RADIX_REPRESENTATION (rev($this.digits))
 * @correspondence this = NUMERICAL_VALUE (rev($this.digits))
 */
public class NaturalNumber2 extends NaturalNumberSecondary {

    /*
     * Private members --------------------------------------------------------
     */

    /**
     * Representation of {@code this}.
     */
    private Stack<Integer> digits;

    /**
     * Prepends onto the front of a {@code Stack} the digits of a given integer
     * i, in reverse order, if i is positive; otherwise, does nothing.
     *
     * @param digits
     *            the stack of digits
     * @param i
     *            the integer to convert
     * @updates digits
     * @requires i >= 0
     * @ensures digits = REVERSED_STRING_OF_DIGITS(i) * #digits
     */
    private static void prependRepFromInt(Stack<Integer> digits, int i) {
        /**
         * @decreases i
         */
        if (i > 0) {
            int lastDigit = i % RADIX;
            prependRepFromInt(digits, i / RADIX);
            digits.push(lastDigit);
        }
    }

    /**
     * Prepends onto the front of a {@code Stack} the digits in a given
     * {@code String} s, in reverse order, if s is not "0"; otherwise, does
     * nothing.
     *
     * @param digits
     *            the stack of digits
     * @param s
     *            the {@code String} to convert
     * @updates digits
     * @requires there exists n: NATURAL (s = TO_STRING(n))
     * @ensures <pre>
     * there exists n: NATURAL
     *  (s = TO_STRING(n)  and  digits = REVERSED_STRING_OF_DIGITS(n) * #digits
     * </pre>
     */
    private static void prependRepFromString(Stack<Integer> digits, String s) {
        /**
         * @decreases |s|
         */
        if (!s.equals("0")) {
            if (s.length() > 1) {
                prependRepFromString(digits, s.substring(0, s.length() - 1));
            }
            digits.push(Character.digit(s.charAt(s.length() - 1), RADIX));
        }
    }

    /**
     * Creator of initial representation.
     */
    private void createNewRep() {
        this.digits = new Stack1L<Integer>();
    }

    /*
     * Constructors -----------------------------------------------------------
     */

    /**
     * No-argument constructor.
     */
    public NaturalNumber2() {
        this.createNewRep();
    }

    /**
     * Constructor from {@code int}.
     *
     * @param i
     *            {@code int} to initialize from
     */
    public NaturalNumber2(int i) {
        assert i >= 0 : "Violation of: i >= 0";
        this.createNewRep();
        prependRepFromInt(this.digits, i);
    }

    /**
     * Constructor from {@code String}.
     *
     * @param s
     *            {@code String} to initialize from
     */
    public NaturalNumber2(String s) {
        assert s != null : "Violation of: s is not null";
        assert s.matches("0|[1-9]\\d*")
                : "Violation of: there exists n: NATURAL (s = TO_STRING(n))";
        this.createNewRep();
        prependRepFromString(this.digits, s);
    }

    /**
     * Constructor from {@code NaturalNumber}.
     *
     * @param n
     *            {@code NaturalNumber} to initialize from
     */
    public NaturalNumber2(NaturalNumber n) {
        assert n != null : "Violation of: n is not null";
        this.createNewRep();
        /*
         * The following call to the NaturalNumber method toString is not a
         * violation of the kernel purity rule because the parameter n is viewed
         * only through its declared type (the interface NaturalNumber) and
         * therefore can be safely handled from the client's point of view.
         */
        String s = n.toString();
        prependRepFromString(this.digits, s);
    }

    /*
     * Standard methods -------------------------------------------------------
     */

    @Override
    public final NaturalNumber newInstance() {
        try {
            return this.getClass().getConstructor().newInstance();
        } catch (ReflectiveOperationException e) {
            throw new AssertionError(
                    "Cannot construct object of type " + this.getClass());
        }
    }

    @Override
    public final void clear() {
        this.createNewRep();
    }

    @Override
    public final void transferFrom(NaturalNumber source) {
        assert source != null : "Violation of: source is not null";
        assert source != this : "Violation of: source is not this";
        assert source instanceof NaturalNumber2
                : "Violation of: source is of dynamic type NaturalNumber2";
        /*
         * This cast cannot fail since the assert above would have stopped
         * execution in that case.
         */
        NaturalNumber2 localSource = (NaturalNumber2) source;
        this.digits = localSource.digits;
        localSource.createNewRep();
    }

    /*
     * Kernel methods ---------------------------------------------------------
     */

    @Override
    public final void multiplyBy10(int k) {
        assert 0 <= k : "Violation of: 0 <= k";
        assert k < RADIX : "Violation of: k < 10";
        if (this.digits.length() > 0 || k > 0) {
            this.digits.push(k);
        }
    }

    @Override
    public final int divideBy10() {
        int k = 0;
        if (this.digits.length() > 0) {
            k = this.digits.pop();
        }
        return k;
    }

    @Override
    public final boolean isZero() {
        return this.digits.length() == 0;
    }

}