package org.checkerframework.checker.fenum;

import java.lang.annotation.Annotation;
import java.util.Collection;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.util.Elements;
import org.checkerframework.checker.fenum.qual.Fenum;
import org.checkerframework.checker.fenum.qual.FenumBottom;
import org.checkerframework.checker.fenum.qual.FenumTop;
import org.checkerframework.checker.fenum.qual.FenumUnqualified;
import org.checkerframework.checker.fenum.qual.PolyFenum;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.framework.type.MostlyNoElementQualifierHierarchy;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.util.DefaultQualifierKindHierarchy;
import org.checkerframework.framework.util.QualifierKind;
import org.checkerframework.framework.util.QualifierKindHierarchy;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.UserError;
import org.plumelib.reflection.Signatures;

/** The type factory for the Fenum Checker. */
public class FenumAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {

  /** AnnotationMirror for {@link FenumUnqualified}. */
  protected AnnotationMirror FENUM_UNQUALIFIED;
  /** AnnotationMirror for {@link FenumBottom}. */
  protected AnnotationMirror FENUM_BOTTOM;
  /** AnnotationMirror for {@link FenumTop}. */
  protected AnnotationMirror FENUM_TOP;

  /**
   * Create a FenumAnnotatedTypeFactory.
   *
   * @param checker checker
   */
  public FenumAnnotatedTypeFactory(BaseTypeChecker checker) {
    super(checker);

    FENUM_BOTTOM = AnnotationBuilder.fromClass(elements, FenumBottom.class);
    FENUM_UNQUALIFIED = AnnotationBuilder.fromClass(elements, FenumUnqualified.class);
    FENUM_TOP = AnnotationBuilder.fromClass(elements, FenumTop.class);

    this.postInit();
  }

  /**
   * Copied from SubtypingChecker. Instead of returning an empty set if no "quals" option is given,
   * we return Fenum as the only qualifier.
   *
   * @return the supported type qualifiers
   */
  @Override
  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
    // Load everything in qual directory, and top, bottom, unqualified, and fake enum
    Set<Class<? extends Annotation>> qualSet =
        getBundledTypeQualifiers(
            FenumTop.class,
            Fenum.class,
            FenumUnqualified.class,
            FenumBottom.class,
            PolyFenum.class);

    // Load externally defined quals given in the -Aquals and/or -AqualDirs options
    String qualNames = checker.getOption("quals");
    String qualDirectories = checker.getOption("qualDirs");

    // load individually named qualifiers
    if (qualNames != null) {
      for (String qualName : qualNames.split(",")) {
        if (!Signatures.isBinaryName(qualName)) {
          throw new UserError("Malformed qualifier \"%s\" in -Aquals=%s", qualName, qualNames);
        }
        qualSet.add(loader.loadExternalAnnotationClass(qualName));
      }
    }

    // load directories of qualifiers
    if (qualDirectories != null) {
      for (String dirName : qualDirectories.split(":")) {
        qualSet.addAll(loader.loadExternalAnnotationClassesFromDirectory(dirName));
      }
    }

    // TODO: warn if no qualifiers given?
    // Just Fenum("..") is still valid, though...
    return qualSet;
  }

  @Override
  public QualifierHierarchy createQualifierHierarchy() {
    return new FenumQualifierHierarchy(getSupportedTypeQualifiers(), elements);
  }

  /** Fenum qualifier hierarchy. */
  protected class FenumQualifierHierarchy extends MostlyNoElementQualifierHierarchy {

    /** QualifierKind for {@link Fenum} qualifier. */
    private final QualifierKind FENUM_KIND;

    /**
     * Creates FenumQualifierHierarchy.
     *
     * @param qualifierClasses qualifier classes
     * @param elements element utils
     */
    public FenumQualifierHierarchy(
        Collection<Class<? extends Annotation>> qualifierClasses, Elements elements) {
      super(qualifierClasses, elements);
      this.FENUM_KIND =
          this.qualifierKindHierarchy.getQualifierKind(Fenum.class.getCanonicalName());
    }

    @Override
    protected QualifierKindHierarchy createQualifierKindHierarchy(
        @UnderInitialization FenumQualifierHierarchy this,
        Collection<Class<? extends Annotation>> qualifierClasses) {
      return new DefaultQualifierKindHierarchy(qualifierClasses, FenumBottom.class);
    }

    @Override
    protected boolean isSubtypeWithElements(
        AnnotationMirror subAnno,
        QualifierKind subKind,
        AnnotationMirror superAnno,
        QualifierKind superKind) {
      return AnnotationUtils.areSame(subAnno, superAnno);
    }

    @Override
    protected AnnotationMirror leastUpperBoundWithElements(
        AnnotationMirror a1,
        QualifierKind qualifierKind1,
        AnnotationMirror a2,
        QualifierKind qualifierKind2,
        QualifierKind lubKind) {
      if (qualifierKind1 == FENUM_KIND && qualifierKind2 == FENUM_KIND) {
        if (AnnotationUtils.areSame(a1, a2)) {
          return a1;
        }
        return FENUM_TOP;
      } else if (qualifierKind1 == FENUM_KIND) {
        return a1;
      } else if (qualifierKind2 == FENUM_KIND) {
        return a2;
      }
      throw new BugInCF("Unexpected QualifierKinds %s %s", qualifierKind1, qualifierKind2);
    }

    @Override
    protected AnnotationMirror greatestLowerBoundWithElements(
        AnnotationMirror a1,
        QualifierKind qualifierKind1,
        AnnotationMirror a2,
        QualifierKind qualifierKind2,
        QualifierKind glbKind) {
      if (qualifierKind1 == FENUM_KIND && qualifierKind2 == FENUM_KIND) {
        return FENUM_BOTTOM;
      } else if (qualifierKind1 == FENUM_KIND) {
        return a2;
      } else if (qualifierKind2 == FENUM_KIND) {
        return a1;
      }
      throw new BugInCF("Unexpected QualifierKinds %s %s", qualifierKind1, qualifierKind2);
    }
  }
}