package org.checkerframework.checker.index.searchindex;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;
import java.util.TreeSet;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.util.Elements;
import org.checkerframework.checker.index.qual.NegativeIndexFor;
import org.checkerframework.checker.index.qual.SearchIndexBottom;
import org.checkerframework.checker.index.qual.SearchIndexFor;
import org.checkerframework.checker.index.qual.SearchIndexUnknown;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.value.ValueAnnotatedTypeFactory;
import org.checkerframework.common.value.ValueChecker;
import org.checkerframework.framework.type.ElementQualifierHierarchy;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.TreeUtils;

/**
 * The Search Index Checker is used to help type the results of calls to the JDK's binary search
 * methods. It is part of the Index Checker.
 */
public class SearchIndexAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {

  /** The @{@link SearchIndexUnknown} annotation. */
  public final AnnotationMirror UNKNOWN =
      AnnotationBuilder.fromClass(elements, SearchIndexUnknown.class);
  /** The @{@link SearchIndexBottom} annotation. */
  public final AnnotationMirror BOTTOM =
      AnnotationBuilder.fromClass(elements, SearchIndexBottom.class);

  /** The NegativeIndexFor.value field/element. */
  protected final ExecutableElement negativeIndexForValueElement =
      TreeUtils.getMethod(NegativeIndexFor.class, "value", 0, processingEnv);
  /** The SearchIndexFor.value field/element. */
  protected final ExecutableElement searchIndexForValueElement =
      TreeUtils.getMethod(SearchIndexFor.class, "value", 0, processingEnv);

  /**
   * Create a new SearchIndexAnnotatedTypeFactory.
   *
   * @param checker the type-checker associated with this
   */
  public SearchIndexAnnotatedTypeFactory(BaseTypeChecker checker) {
    super(checker);

    this.postInit();
  }

  /**
   * Provides a way to query the Constant Value Checker, which computes the values of expressions
   * known at compile time (constant propagation and folding).
   */
  ValueAnnotatedTypeFactory getValueAnnotatedTypeFactory() {
    return getTypeFactoryOfSubchecker(ValueChecker.class);
  }

  @Override
  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
    return new LinkedHashSet<>(
        Arrays.asList(
            SearchIndexFor.class,
            SearchIndexBottom.class,
            SearchIndexUnknown.class,
            NegativeIndexFor.class));
  }

  @Override
  protected QualifierHierarchy createQualifierHierarchy() {
    return new SearchIndexQualifierHierarchy(this.getSupportedTypeQualifiers(), elements);
  }

  /**
   * Returns the {@code value} field/element of the given annotation.
   *
   * @param am a @NegativeIndexFor or @SearchIndexFor annotation
   * @return the {@code value} field/element of the given annotation
   */
  private List<String> getValueElement(AnnotationMirror am) {
    if (areSameByClass(am, NegativeIndexFor.class)) {
      return AnnotationUtils.getElementValueArray(am, negativeIndexForValueElement, String.class);
    } else if (areSameByClass(am, SearchIndexFor.class)) {
      return AnnotationUtils.getElementValueArray(am, searchIndexForValueElement, String.class);
    } else {
      throw new BugInCF("indexForValue(%s)", am);
    }
  }

  /** SearchIndexQualifierHierarchy. */
  private final class SearchIndexQualifierHierarchy extends ElementQualifierHierarchy {

    /**
     * Creates a SearchIndexQualifierHierarchy from the given classes.
     *
     * @param qualifierClasses classes of annotations that are the qualifiers
     * @param elements element utils
     */
    public SearchIndexQualifierHierarchy(
        Set<Class<? extends Annotation>> qualifierClasses, Elements elements) {
      super(qualifierClasses, elements);
    }

    @Override
    public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) {
      if (AnnotationUtils.areSame(a1, UNKNOWN)) {
        return a2;
      }
      if (AnnotationUtils.areSame(a2, UNKNOWN)) {
        return a1;
      }
      if (AnnotationUtils.areSame(a1, BOTTOM)) {
        return a1;
      }
      if (AnnotationUtils.areSame(a2, BOTTOM)) {
        return a2;
      }
      if (isSubtype(a1, a2)) {
        return a1;
      }
      if (isSubtype(a2, a1)) {
        return a2;
      }
      // If neither is a subtype of the other, then create an
      // annotation that combines their values.

      // Each annotation is either NegativeIndexFor or SearchIndexFor.
      Set<String> combinedArrays = new HashSet<>(getValueElement(a1));
      combinedArrays.addAll(getValueElement(a2));

      // NegativeIndexFor <: SearchIndexFor.
      if (areSameByClass(a1, NegativeIndexFor.class)
          || areSameByClass(a2, NegativeIndexFor.class)) {
        return createNegativeIndexFor(Arrays.asList(combinedArrays.toArray(new String[0])));
      } else {
        return createSearchIndexFor(Arrays.asList(combinedArrays.toArray(new String[0])));
      }
    }

    @Override
    public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) {
      if (AnnotationUtils.areSame(a1, UNKNOWN)) {
        return a1;
      }
      if (AnnotationUtils.areSame(a2, UNKNOWN)) {
        return a2;
      }
      if (AnnotationUtils.areSame(a1, BOTTOM)) {
        return a2;
      }
      if (AnnotationUtils.areSame(a2, BOTTOM)) {
        return a1;
      }
      if (isSubtype(a1, a2)) {
        return a2;
      }
      if (isSubtype(a2, a1)) {
        return a1;
      }
      // If neither is a subtype of the other, then create an
      // annotation that includes only their overlapping values.

      // Each annotation is either NegativeIndexFor or SearchIndexFor.
      List<String> arrayIntersection = getValueElement(a1);
      arrayIntersection.retainAll(getValueElement(a2)); // intersection

      if (arrayIntersection.isEmpty()) {
        return UNKNOWN;
      }

      if (areSameByClass(a1, SearchIndexFor.class) || areSameByClass(a2, SearchIndexFor.class)) {
        return createSearchIndexFor(arrayIntersection);
      } else {
        return createNegativeIndexFor(arrayIntersection);
      }
    }

    @Override
    public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
      if (areSameByClass(superAnno, SearchIndexUnknown.class)) {
        return true;
      }
      if (areSameByClass(subAnno, SearchIndexBottom.class)) {
        return true;
      }
      if (areSameByClass(subAnno, SearchIndexUnknown.class)) {
        return false;
      }
      if (areSameByClass(superAnno, SearchIndexBottom.class)) {
        return false;
      }

      // Each annotation is either NegativeIndexFor or SearchIndexFor.
      List<String> superArrays = getValueElement(superAnno);
      List<String> subArrays = getValueElement(subAnno);

      // Subtyping requires:
      //  * subtype is NegativeIndexFor or supertype is SearchIndexFor
      //  * subtype's arrays are a superset of supertype's arrays
      return ((areSameByClass(subAnno, NegativeIndexFor.class)
              || areSameByClass(superAnno, SearchIndexFor.class))
          && subArrays.containsAll(superArrays));
    }
  }

  /** Create a new {@code @NegativeIndexFor} annotation with the given arrays as its arguments. */
  AnnotationMirror createNegativeIndexFor(List<String> arrays) {
    if (arrays.isEmpty()) {
      return UNKNOWN;
    }

    arrays = new ArrayList<>(new TreeSet<>(arrays)); // remove duplicates and sort

    AnnotationBuilder builder = new AnnotationBuilder(processingEnv, NegativeIndexFor.class);
    builder.setValue("value", arrays);
    return builder.build();
  }

  /** Create a new {@code @SearchIndexFor} annotation with the given arrays as its arguments. */
  AnnotationMirror createSearchIndexFor(List<String> arrays) {
    if (arrays.isEmpty()) {
      return UNKNOWN;
    }

    arrays = new ArrayList<>(new TreeSet<>(arrays)); // remove duplicates and sort

    AnnotationBuilder builder = new AnnotationBuilder(processingEnv, SearchIndexFor.class);
    builder.setValue("value", arrays);
    return builder.build();
  }
}