package de.uni_hamburg.fs;

import java.util.NoSuchElementException;
import java.util.StringTokenizer;

import collections.CollectionEnumeration;
import collections.HashedSet;
import collections.Set;


/**
 * Represents a conjunction of concepts forming a type in the FS type system.
 * A ConjunctiveType combines multiple concepts with their features and constraints
 * to form a more specific type. This is a key part of the type unification mechanism.
 */
public class ConjunctiveType implements Type {
    /** Logger for this class. */
    public static final org.apache.log4j.Logger LOGGER =
        org.apache.log4j.Logger.getLogger(ConjunctiveType.class);

    /** The set of concepts forming this conjunctive type. */
    ConceptSet _concepts = new ConceptSet();

    // "caches" for aggregated concept attributes:
    /** Cache of features from all included concepts. */
    private OrderedTable _features = new OrderedTable();
    /** Whether this type is extensional (has instances). */
    private boolean _extensional = false;
    /** Whether to print 'Any' for unrestricted types. */
    private boolean _printAny = true;
    /** Whether this type restricts which features are allowed. */
    private boolean _restricted = true;

    /**
     * Set to true if this ConjunctiveType is composed of JavaConcepts.
     * Careful: isJavaConceptType is not monotonic for subsumption, since
     * in Type.TOP, it is false, but e.g. in {Frame} (a subtype of Top), it
     * is true. For type Top, it should really be "unknown".
     */
    private boolean _isJavaConceptType = false;

    /** Set to true if this ConjunctiveType is to be instantiated later. */
    private boolean _toBeInstantiated = false;

    /**
     * Constructs a conjunctive type with the specified restriction status.
     *
     * @param restricted whether this type restricts which features are allowed
     */
    public ConjunctiveType(boolean restricted) {
        this._restricted = restricted;
    }

    /**
     * Constructs a conjunctive type with the specified restriction status and printAny flag.
     *
     * @param restricted whether this type restricts which features are allowed
     * @param printAny whether to print 'Any' for unrestricted types
     */
    public ConjunctiveType(boolean restricted, boolean printAny) {
        this(restricted);
        this._printAny = printAny;
    }

    /**
     * Constructs a conjunctive type containing a single concept.
     *
     * @param concept the concept to include in this type
     * @throws RuntimeException if there is an unexpected failure during concept addition
     */
    public ConjunctiveType(Concept concept) {
        try {
            addConcept(concept);
        } catch (UnificationFailure uff) {
            // Should not happen.
            throw new RuntimeException("***Unexpected failure in addConcept(" + concept + ").");
        }
    }

    /**
     * Constructs a conjunctive type with a single concept and specified restriction status.
     *
     * @param concept the concept to include in this type
     * @param isRestricted whether this type restricts which features are allowed
     * @throws UnificationFailure if the concept cannot be added to this type
     */
    public ConjunctiveType(Concept concept, boolean isRestricted) throws UnificationFailure {
        this(isRestricted);
        addConcept(concept);
    }

    /**
     * Constructs a conjunctive type with the specified set of concepts.
     * The type will be restricted by default.
     *
     * @param concepts the set of concepts to include in this type
     * @throws UnificationFailure if the concepts cannot be unified
     */
    public ConjunctiveType(ConceptSet concepts) throws UnificationFailure {
        this(concepts, true);
    }

    /**
     * Constructs a conjunctive type with the specified set of concepts,
     * restriction status, and printAny flag.
     *
     * @param concepts the set of concepts to include in this type
     * @param isRestricted whether this type restricts which features are allowed
     * @param printAny whether to print 'Any' for unrestricted types
     * @throws UnificationFailure if the concepts cannot be unified
     */
    public ConjunctiveType(ConceptSet concepts, boolean isRestricted, boolean printAny)
        throws UnificationFailure
    {
        this(concepts, isRestricted, printAny, false);
    }

    /**
     * Constructs a conjunctive type with the specified set of concepts,
     * restriction status, printAny flag, and instantiation status.
     *
     * @param concepts the set of concepts to include in this type
     * @param isRestricted whether this type restricts which features are allowed
     * @param printAny whether to print 'Any' for unrestricted types
     * @param toBeInstantiated whether this type is to be instantiated later
     * @throws UnificationFailure if the concepts cannot be unified
     */
    public ConjunctiveType(
        ConceptSet concepts, boolean isRestricted, boolean printAny, boolean toBeInstantiated)
        throws UnificationFailure
    {
        this(isRestricted);
        this._printAny = printAny;
        this._toBeInstantiated = toBeInstantiated;
        ConceptEnumeration conceptEnum = concepts.elements();
        while (conceptEnum.hasMoreElements()) {
            addConcept(conceptEnum.nextConcept());
        }
    }

    /**
     * Constructs a conjunctive type with the specified set of concepts and restriction status.
     *
     * @param concepts the set of concepts to include in this type
     * @param isRestricted whether this type restricts which features are allowed
     * @throws UnificationFailure if the concepts cannot be unified
     */
    public ConjunctiveType(ConceptSet concepts, boolean isRestricted) throws UnificationFailure {
        this(concepts, isRestricted, true);
    }

    @Override
    public int hashCode() {
        return _concepts.hashCode() + (_restricted ? 3 : 0) + (_toBeInstantiated ? 5 : 0);
    }

    /**
     * Returns an enumeration of all concepts this conjunctive type is composed of.
     *
     * @return an enumeration of all concepts in this type
     */
    public ConceptEnumeration concepts() {
        return _concepts.elements();
    }

    /** Return the name of this Type. */
    @Override
    public String getName() {
        // special case: for _Top, return a space:
        if (_restricted && _toBeInstantiated && _concepts.isEmpty()) {
            return " ";
        }
        return typeToString(_restricted, _printAny, false, _concepts);
    }

    /** Return the fully qualified name of this Type. */
    @Override
    public String getFullName() {
        return typeToString(_restricted, _printAny, true, _concepts);
    }

    /**
     * Returns a string representation of a ConjunctiveType or ParsedConjunctiveType.
     * The string is a comma-separated list of concept names.
     *
     * @param restricted whether the type restricts which features are allowed
     * @param printAny whether to print 'Any' for unrestricted types
     * @param qualified whether to use fully qualified concept names
     * @param concepts the set of concepts in the type
     * @return the string representation of the type
     */
    static String typeToString(
        boolean restricted, boolean printAny, boolean qualified, ConceptSet concepts)
    {
        StringBuffer output = new StringBuffer();
        if (!restricted && printAny) {
            output.append("Any");
        }
        ConceptEnumeration conceptEnum = concepts.elements();
        while (conceptEnum.hasMoreElements()) {
            if (output.length() > 0) {
                output.append(',');
            }
            Concept concept = (Concept) conceptEnum.nextElement();
            if (qualified) {
                output.append(concept.getFullName());
            } else {
                output.append(concept.getName());
            }
        }
        return output.toString();
    }

    /**
     * Finds or constructs a ConjunctiveType consisting of the given concepts.
     * This may fail due to concept incompatibilities.
     *
     * @param concepts the set of concepts to include in the type
     * @return a type containing all the given concepts
     * @throws UnificationFailure if the concepts cannot be unified in a single type
     */
    public static Type getType(Set concepts) throws UnificationFailure {
        if (concepts.isEmpty()) {
            return Type.TOP;
        }
        CollectionEnumeration conceptEnum = concepts.elements();
        ConjunctiveType newtype = new ConjunctiveType(true);
        while (conceptEnum.hasMoreElements()) {
            newtype.addConcept((Concept) conceptEnum.nextElement());
        }
        return newtype;
    }

    /**
     * Finds or constructs a ConjunctiveType from a comma-separated string of concept names.
     *
     * @param conceptsStr a comma-separated string of concept names
     * @return a type containing all the specified concepts
     * @throws UnificationFailure if the concepts cannot be unified in a single type
     * @throws TypeException if any concept name is not found in the type system
     */
    public static Type getType(String conceptsStr) throws UnificationFailure, TypeException {
        StringTokenizer conceptNames = new StringTokenizer(conceptsStr, ",");
        HashedSet concepts = new HashedSet();
        TypeSystem ts = TypeSystem.instance();
        while (conceptNames.hasMoreElements()) {
            try {
                concepts.include(ts.conceptForName(conceptNames.nextToken()));
            } catch (NoSuchElementException e) {
                throw new TypeException();
            }
        }
        return getType(concepts);
    }

    @Override
    public boolean isExtensional() {
        return _extensional;
    }

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

    @Override
    public Type getInstanceType() {
        if (isInstanceType()) {
            return this;
        }
        ConjunctiveType instType = duplicate();
        instType._toBeInstantiated = true;
        return instType;
    }

    @Override
    public boolean isApprop(Name featureName) {
        if (_restricted) {
            return _features.includesKey(featureName);
        } else {
            return true;
        }
    }

    @Override
    public Type appropType(Name featureName) {
        try {
            Type appropType;
            if (_restricted || _features.includesKey(featureName)) {
                // logger.debug(seqNo + " is queried for type of feature "
                //              + featureName + ", includes: "
                //              + features.includesKey(featureName) + ", result: "
                //              + features.at(featureName));
                ParsedType pt = (ParsedType) _features.at(featureName);


                // logger.debug("this: " + this + ", restricted: " + restricted
                //              + ", PT: " + pt);
                appropType = pt.asType();
                if (_toBeInstantiated) {
                    appropType = appropType.getInstanceType();
                }
            } else {
                appropType = Type.TOP;
            }
            return appropType;
        } catch (UnificationFailure uff) {
            throw new RuntimeException(
                "Conjunctive type for ConceptSet " + _features.at(featureName) + " not defined!",
                uff);
        }
    }

    @Override
    public CollectionEnumeration appropFeatureNames() {
        return _features.keys();
    }

    @Override
    public boolean subsumes(Type that) {
        if (equals(Type.TOP)) {
            return true;
        }
        if (that instanceof ConjunctiveType) {
            ConjunctiveType thatCT = (ConjunctiveType) that;
            if (!_restricted && thatCT._restricted) {
                return false;
            }
            if (_toBeInstantiated && !thatCT._toBeInstantiated) {
                return false;
            }
            ConceptEnumeration conceptEnum = _concepts.elements();
            forAllConcepts: while (conceptEnum.hasMoreElements()) {
                Concept concept = (Concept) conceptEnum.nextElement();
                ConceptEnumeration thatConceptEnum = thatCT.concepts();
                while (thatConceptEnum.hasMoreElements()) {
                    Concept thatConcept = (Concept) thatConceptEnum.nextElement();
                    if (thatConcept.isa(concept)) {
                        continue forAllConcepts;
                    }
                }
                return false; // No that-concept found!
            }
            return true;
        } else if (_restricted && (_concepts.isEmpty() || _isJavaConceptType)) {
            // Java types/objects may only be compatible with Top or
            // with a concept set of JavaConcepts.
            if (that instanceof JavaClassType) {
                JavaConcept jc =
                    TypeSystem.instance().getJavaConcept(((JavaClassType) that).getJavaClass());
                ConceptEnumeration conceptEnum = _concepts.elements();
                while (conceptEnum.hasMoreElements()) {
                    Concept concept = (Concept) conceptEnum.nextElement();
                    if (!jc.isa(concept)) {
                        return false;
                    }
                }
                return true;
            } else if (that instanceof NullObject) {
                return true;
            }
        }
        return false;
    }

    @Override
    public boolean canUnify(Type that) {
        try {
            unify(that);
            return true;
        } catch (UnificationFailure uff) {
            return false;
        }
    }

    private void basicAddConcept(Concept newConcept) throws UnificationFailure {
        CollectionEnumeration featenumeration = newConcept.appropFeatureNames();
        while (featenumeration.hasMoreElements()) {
            Name feature = (Name) featenumeration.nextElement();
            ParsedType newType = newConcept.appropParsedType(feature);
            if (_features.includesKey(feature)) {
                // this may fail and return null:
                newType = newType.unite((ParsedType) _features.at(feature));
                if (newType == null) {
                    throw new UnificationFailure();
                }
            }
            _features.putAt(feature, newType);
        }
        _extensional = _extensional || newConcept.isExtensional();
    }

    /**
     * Adds a new concept to this conjunctive type during type construction.
     * This method integrates the given concept into the type's concept set
     * and updates associated features and attributes.
     *
     * <p>The method performs several validations:</p>
     * <ul>
     * <li>Prevents String class from being wrapped as a JavaConcept</li>
     * <li>Ensures Java concepts are not added to unrestricted types</li>
     * <li>Maintains consistency between Java and non-Java concepts</li>
     * <li>Validates feature compatibility between concepts</li>
     * </ul>
     *
     * <p>Upon successful validation, the method:</p>
     * <ul>
     * <li>Updates the internal concept set</li>
     * <li>Integrates the concept's features into the feature cache</li>
     * <li>Updates the type's extensionality if needed</li>
     * </ul>
     *
     * @param newConcept the concept to be added to this conjunctive type
     * @throws UnificationFailure if the concept cannot be unified with existing concepts,
     * or if attempting to add a Java concept to an unrestricted type,
     * or if mixing Java and non-Java concepts
     * @throws RuntimeException if attempting to wrap String class as a JavaConcept
     */
    public void addConcept(Concept newConcept) throws UnificationFailure {
        if (newConcept instanceof JavaConcept
            && ((JavaConcept) newConcept).getJavaClass().equals(String.class)) {
            throw new RuntimeException("String wrapped in ConjunctiveType!");
        }
        boolean newIsJavaConcept = newConcept instanceof JavaConcept;
        if (_printAny) { // not a dummy type
            if (_concepts.isEmpty()) {
                if (!_restricted && newIsJavaConcept) {
                    throw new UnificationFailure();
                }
                _isJavaConceptType = newIsJavaConcept;
            } else if (_isJavaConceptType != newIsJavaConcept) {
                throw new UnificationFailure();
            }
        }

        _concepts.joinConcept(newConcept);

        // logger.debug(seqNo + " hashcode " + previousHashCode + " changed to "
        //             + hashCode());
        basicAddConcept(newConcept); // add features & extensionality of newConcept
    }

    private ConjunctiveType duplicate() {
        ConjunctiveType typ = new ConjunctiveType(_restricted);
        typ._concepts = new ConceptSet(_concepts);
        typ._features = (OrderedTable) _features.duplicate();
        typ._extensional = _extensional;
        typ._printAny = _printAny;
        typ._toBeInstantiated = _toBeInstantiated;
        typ._isJavaConceptType = _isJavaConceptType;
        return typ;
    }

    @Override
    public Type unify(Type that) throws UnificationFailure {
        if (subsumes(that)) {
            return that;
        } else if (that.subsumes(this)) {
            return this;
        } else if (that instanceof ConjunctiveType) {
            ConjunctiveType typ = duplicate();
            ConjunctiveType thatCT = (ConjunctiveType) that;
            typ._restricted = typ._restricted && thatCT._restricted;
            if (!(_concepts.isEmpty() || thatCT._concepts.isEmpty()
                || _isJavaConceptType == thatCT._isJavaConceptType)) {
                throw new UnificationFailure();
            }
            typ._isJavaConceptType = _isJavaConceptType || thatCT._isJavaConceptType;
            if (typ._isJavaConceptType && !typ._restricted) {
                throw new UnificationFailure();
            }
            typ._toBeInstantiated = typ._toBeInstantiated || thatCT._toBeInstantiated;
            ConceptEnumeration thatConceptEnum = thatCT.concepts();
            while (thatConceptEnum.hasMoreElements()) {
                Concept thatConcept = (Concept) thatConceptEnum.nextElement();
                typ.addConcept(thatConcept);
            }
            return typ;
        }
        throw new UnificationFailure();
    }

    @Override
    public Type mostGeneralExtensionalSupertype(Type that) {
        return null;
        /*
        //     System.out.println("Finding most general extensional supertype for "+this+" and "+that+".");
            UpdatableSet thisSupers = new HashedSet();
            Enumeration conceptEnum = concepts.elements();
            while (conceptEnum.hasMoreElements()) {
              Type type = (Concept)conceptEnum.nextElement();
              thisSupers.includeElements(type.extensionalSuperconcepts());
            }
        //    System.out.println("Supertype of "+this+": "+new ConjunctiveType(thisSupers));
            UpdatableSet commonSupers = new HashedSet();
            Enumeration thatConcs = that.concepts();
            while (thatConcs.hasMoreElements()) {
              Type thattype = (Concept)thatConcs.nextElement();
              Enumeration thatSupers = thattype.extensionalSuperconcepts();
              while (thatSupers.hasMoreElements()) {
                 Type thatSuper = (Type)thatSupers.nextElement();
        //    System.out.print("Supertype of "+that+" "+thatSuper.getName());
                 if (thisSupers.includes(thatSuper)) {
        //            System.out.println(" is added!");
                    if (!(new ConjunctiveType(commonSupers).subsumes(new ConjunctiveType(thatSuper)))) {
                       UpdatableSet newCS = new HashedSet();
        //               System.out.print("...and removes some more special concepts:");
                       Enumeration oldCSenum = commonSupers.elements();
                       while (oldCSenumeration.hasMoreElements()) {
                         Type oldSuper = (Type)oldCSenumeration.nextElement();
                         if (!thatSuper.subsumes(oldSuper)) {
                            newCS.include(oldSuper);
                         }
        //                 else
        //                    System.out.print(" "+oldSuper.getName());
                       }
                       commonSupers = newCS;
        //               System.out.println();
                    }
                    commonSupers.include(thatSuper);
                 }
        //         else
        //           System.out.println(" ruled out.");
              }
            }
        //    System.out.println("Most general extensional supertype for "+this+" and "+that+" is "+new ConjunctiveType(commonSupers)+".");
            return new ConjunctiveType(commonSupers);
        */
    }

    /**
     * Return a new node from this type.
     */
    @Override
    public Node newNode() {
        if (_restricted && _features.isEmpty()) {
            return new NoFeatureNode(this);
        } else {
            //        if (concepts.size()==1) {
            //      Concept onlyConcept=concepts.elements().nextConcept();
            //      if (onlyConcept instanceof JavaConcept &&
            //          ((JavaConcept)onlyConcept).canInstantiate()) {
            //          return new JavaObjectNode((JavaConcept)onlyConcept);
            //      }
            //        }
            return new FSNode(this);
        }
    }

    @Override
    public String toString() {
        String name = getName();
        if (name.length() == 0) {
            return "Top";
        } else {
            return name;
        }
    }

    /** Compares this ConjunctiveType with another Object. Two ConjunctiveTypes
     * are considered equal iff they consist of the same set of Concepts.
     */
    @Override
    public boolean equals(Object that) {
        if (that instanceof ConjunctiveType) {
            ConjunctiveType thatType = (ConjunctiveType) that;
            return _restricted == thatType._restricted
                && _toBeInstantiated == thatType._toBeInstantiated
                && _isJavaConceptType == thatType._isJavaConceptType
                && _concepts.equals(thatType._concepts);
        } else {
            return false;
        }
    }

    /**
     * Returns the only instantiable JavaConcept in this type, if there is exactly one.
     * This is used for optimization in node creation.
     *
     * @return the only instantiable JavaConcept, or null if there isn't exactly one
     */
    JavaConcept getOnlyInstantiableJavaConcept() {
        // check if there is exactly one JavaConcept to instantiate:
        if (_isJavaConceptType && _concepts.size() == 1) {
            Concept onlyConcept = _concepts.elements().nextConcept();
            if (((JavaConcept) onlyConcept).canInstantiate()) {
                return (JavaConcept) onlyConcept;
            }
        }
        return null;
    }
}