package de.uni_hamburg.fs;

import de.renew.util.Types;
import de.renew.util.Value;


/**
 * Represents a basic type with lower and upper bounds,
 * used for typing in the FS type system.
 */
public class BasicType extends JavaClassType {

    /**
     * Represents positive infinity used for upper bound comparisons.
     * When used as an upper bound, it indicates that there is no upper limit
     * for the allowed values in this basic type.
     */
    public final static Object POSINF = new Name("POSINF");

    /**
     * Represents negative infinity used for lower bound comparisons.
     * When used as a lower bound, it indicates that there is no lower limit
     * for the allowed values in this basic type.
     */
    public final static Object NEGINF = new Name("NEGINF");

    /**
     * The lower bound of this basic type.
     * Can be a specific value or NEGINF to indicate no lower limit.
     */
    private Object _lower;

    /**
     * The upper bound of this basic type.
     * Can be a specific value or POSINF to indicate no upper limit.
     */
    private Object _upper;

    /**
     * Indicates whether this type should be instantiated.
     * When true, this type represents an instance rather than a type definition.
     */
    private boolean _toBeInstantiated = false;

    /**
     * Constructs a BasicType for a given primitive or String class.
     *
     * @param type the Java class representing the type
     */
    public BasicType(Class<?> type) {
        if (type != String.class && !type.isPrimitive()) {
            throw new RuntimeException("Class " + type + " cannot be used as a BasicType.");
        }
        this.setJavaClass(type);
        this._lower = NEGINF;
        this._upper = POSINF;
    }

    /**
     * Constructs a BasicType with a single fixed value.
     *
     * @param single the fixed value
     */
    public BasicType(Object single) {
        this(getValueClass(single));
        this._lower = single;
        this._upper = single;
    }

    /**
     * Constructs a BasicType with specified lower and upper bounds.
     *
     * @param lower the lower bound
     * @param upper the upper bound
     * @throws TypeException if bounds are inconsistent or of incorrect type
     */
    public BasicType(Object lower, Object upper) throws TypeException {
        this(getValueClass(lower, upper), lower, upper);
    }

    /**
     * Constructs a BasicType with specified class and bounds.
     *
     * @param type the Java class
     * @param lower the lower bound
     * @param upper the upper bound
     * @throws TypeException if the bounds are not valid for the given type
     */
    public BasicType(Class<?> type, Object lower, Object upper) throws TypeException {
        checkClass(type, lower);
        checkClass(type, upper);
        if (compare(lower, upper) > 0) {
            // upper is smaller than lower.
            throw new TypeException();
        }
        setJavaClass(type);
        this._lower = lower;
        this._upper = upper;
    }

    private BasicType(Class<?> type, Object lower, Object upper, boolean toBeInstantiated) {
        super(type);
        this._lower = lower;
        this._upper = upper;
        this._toBeInstantiated = toBeInstantiated;
    }

    private static Class<?> getValueClass(Object a) {
        if (a instanceof String) {
            return String.class;
        }
        try {
            return Types.typify(((Value) a).value.getClass());
        } catch (ClassCastException cce) {
            throw new RuntimeException("Class " + a.getClass() + " cannot be used as a BasicType.");
        }
    }

    private static Class<?> getValueClass(Object lower, Object upper) throws TypeException {
        if (!NEGINF.equals(lower)) {
            return getValueClass(lower);
        } else if (!POSINF.equals(upper)) {
            return getValueClass(upper);
        } else {
            throw new TypeException();
        }
    }

    private static void checkClass(Class<?> type, Object a) throws TypeException {
        if (!POSINF.equals(a) && !NEGINF.equals(a)) {
            Class<?> aclass = getValueClass(a);
            if (aclass != type) {
                throw new TypeException();
                //RuntimeException("Bound "+a+" is not of BasicType "+aclass+".");
            }
        }
    }

    /**
     * Checks if this BasicType represents a single object (i.e., lower == upper).
     *
     * @return true if the lower and upper bounds are equal, false otherwise
     */
    public boolean isObject() {
        return _lower.equals(_upper);
    }

    @Override
    public boolean isInstanceType() {
        return _toBeInstantiated;
    }

    @Override
    public Type getInstanceType() {
        if (isInstanceType()) {
            return this;
        }
        return new BasicType(getJavaClass(), _lower, _upper, true);
    }

    @Override
    public Object getJavaObject() {
        if (!isObject()) {
            throw new RuntimeException(
                "getJavaObject() called in BasicType although lower and upper did not meet!");
        }
        return _lower;
    }

    /**
     * Converts an object to a readable string representation.
     * Special handling is provided for infinity values, strings, Value objects, and null.
     *
     * @param obj the object to convert to a string
     * @return the string representation of the object
     */
    public static String objToString(Object obj) {
        if (NEGINF.equals(obj) || POSINF.equals(obj)) {
            return "*";
        } else if (obj instanceof String) {
            return "\"" + obj + "\"";
        } else if (obj instanceof Value) {
            return ((Value) obj).value.toString();
        } else if (obj == null) {
            return "null";
        } else {
            return obj.toString();
        }
    }

    /** Return the name of this Type. */
    @Override
    public String getName() {
        StringBuffer output = new StringBuffer();
        if (NEGINF.equals(_lower) && POSINF.equals(_upper)) {
            if (getJavaClass() == String.class) {
                output.append("String");
            } else {
                output.append(getJavaClass().getName());
            }
        } else if (_upper.equals(_lower)) {
            output.append(objToString(_lower));
        } else {
            output.append("{").append(objToString(_lower)).append("..").append(objToString(_upper))
                .append("}");
        }
        return output.toString();
    }

    /** Return the fully qualified name of this Type. */
    @Override
    public String getFullName() {
        return getName();
    }

    /** Return whether this Type is extensional. */
    @Override
    public boolean isExtensional() {
        return isObject();
    }

    @Override
    public boolean subsumes(Type that) {
        if (that instanceof BasicType) {
            BasicType thatBasic = (BasicType) that;
            if (_toBeInstantiated && !thatBasic._toBeInstantiated
                || thatBasic.getJavaClass() != getJavaClass()) {
                return false;
            }
            return compare(_lower, thatBasic._lower) <= 0 && compare(_upper, thatBasic._upper) >= 0;
        } else if (that instanceof NullObject) {
            return getJavaClass() == String.class && _lower.equals(NEGINF) && _upper.equals(POSINF);
        }
        return false;
    }

    @Override
    public Type unify(Type that) throws UnificationFailure {
        // has to be a BasicType or (TOP).
        if (that.equals(Type.TOP)) {
            return this;
        }
        if (subsumes(that)) {
            return that;
        }
        if (that instanceof BasicType) {
            BasicType thatBasic = (BasicType) that;
            if (thatBasic.getJavaClass() == getJavaClass()) {
                Object newLower = max(_lower, thatBasic._lower);
                Object newUpper = min(_upper, thatBasic._upper);
                if (compare(newLower, newUpper) > 0) {
                    // upper is smaller than lower.
                    throw new TypeException();
                }
                return new BasicType(
                    getJavaClass(), newLower, newUpper,
                    _toBeInstantiated || thatBasic._toBeInstantiated);
            }
        } else if (that.subsumes(this)) {
            return this;
        }
        throw new UnificationFailure();
    }

    @Override
    public boolean canUnify(Type that) {
        if (that.equals(Type.TOP)) {
            return true;
        }
        if (that instanceof BasicType) {
            BasicType thatBasic = (BasicType) that;
            if (thatBasic.getJavaClass() == getJavaClass()) {
                return compare(_lower, thatBasic._upper) <= 0
                    && compare(thatBasic._lower, _upper) <= 0;
            }
            return false;
        }
        return subsumes(that);
    }

    // Return a new node from this type.
    //
    //    public Node newNode() {
    //      if (lower.equals(upper))
    //        return new BasicObjectNode(this);
    //      else
    //        return new NoFeatureNode(this);
    //    }


    /** Look for the most general common extensional supertype of this and {@literal <that>}. */
    @Override
    public Type mostGeneralExtensionalSupertype(Type that) {
        // TODO
        return null;
    }

    @Override
    public boolean equals(Object that) {
        if (that instanceof BasicType) {
            BasicType thatBasic = (BasicType) that;
            return _toBeInstantiated == thatBasic._toBeInstantiated && super.equals(that)
                && thatBasic._lower.equals(_lower) && thatBasic._upper.equals(_upper);
        }
        return false;
    }

    @Override
    public int hashCode() {
        return getJavaClass().hashCode() + _lower.hashCode() + _upper.hashCode();
    }

    /**
     * Compares two objects for ordering.
     * Handles special cases like infinity values and performs type-specific comparisons.
     *
     * @param a the first object to compare
     * @param b the second object to compare
     * @return -1 if a < b, 0 if a == b, 1 if a > b
     * @throws RuntimeException if the objects are of incompatible types or unsupported types
     */
    int compare(Object a, Object b) {
        if (a.equals(b)) {
            return 0;
        }
        if (NEGINF.equals(a) || POSINF.equals(b)) {
            return -1; // NEGINF is smaller than everything and
        }

        // everything is smaller than POSINF
        if (POSINF.equals(a) || NEGINF.equals(b)) {
            return 1; // POSINF is larger than everything and
        }

        // everything is larger than NEGINF
        if (a instanceof String && b instanceof String) {
            return ((String) a).compareTo((String) b);
        }
        if (a instanceof Value && b instanceof Value) {
            Value av = (Value) a;
            Value bv = (Value) b;
            Object ao = av.value;
            Object bo = bv.value;
            if (!ao.getClass().equals(bo.getClass())) {
                throw new RuntimeException(
                    "Different BasicType Classes: " + ao.getClass() + " and " + bo.getClass());
            }
            if (ao instanceof Boolean) {
                return bv.booleanValue() ? -1 : 1;
            } else if (ao instanceof Character) {
                return av.charValue() < bv.charValue() ? -1 : 1;
            } else if (ao instanceof Byte) {
                return av.byteValue() < bv.byteValue() ? -1 : 1;
            } else if (ao instanceof Short) {
                return av.shortValue() < bv.shortValue() ? -1 : 1;
            } else if (ao instanceof Integer) {
                return av.intValue() < bv.intValue() ? -1 : 1;
            } else if (ao instanceof Long) {
                return av.longValue() < bv.longValue() ? -1 : 1;
            } else if (ao instanceof Float) {
                return av.floatValue() < bv.floatValue() ? -1 : 1;
            } else if (ao instanceof Double) {
                return av.doubleValue() < bv.doubleValue() ? -1 : 1;
            } else {
                a = ao;
                b = bo; // for exception!
            }
        }
        throw new RuntimeException(
            "Wrong BasicType classes: " + a.getClass() + " and/or " + b.getClass());
    }

    /**
     * Returns the maximum of two objects according to their natural ordering.
     *
     * @param a the first object
     * @param b the second object
     * @return the maximum object
     */
    Object max(Object a, Object b) {
        return compare(a, b) >= 0 ? a : b;
    }

    /**
     * Returns the minimum of two objects according to their natural ordering.
     *
     * @param a the first object
     * @param b the second object
     * @return the minimum object
     */
    Object min(Object a, Object b) {
        return compare(a, b) <= 0 ? a : b;
    }
}