package org.checkerframework.common.value;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.stream.Collectors;
import javax.lang.model.element.AnnotationMirror;
import org.checkerframework.checker.regex.qual.Regex;
import org.checkerframework.common.value.util.Range;
import org.checkerframework.framework.type.ElementQualifierHierarchy;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.SystemUtil;

/** The qualifier hierarchy for the Value type system. */
final class ValueQualifierHierarchy extends ElementQualifierHierarchy {

  /** The type factory to use. */
  private final ValueAnnotatedTypeFactory atypeFactory;

  /**
   * Creates a ValueQualifierHierarchy from the given classes.
   *
   * @param atypeFactory ValueAnnotatedTypeFactory
   * @param qualifierClasses classes of annotations that are the qualifiers for this hierarchy
   */
  ValueQualifierHierarchy(
      ValueAnnotatedTypeFactory atypeFactory,
      Collection<Class<? extends Annotation>> qualifierClasses) {
    super(qualifierClasses, atypeFactory.getElementUtils());
    this.atypeFactory = atypeFactory;
  }

  /**
   * Computes greatest lower bound of a @StringVal annotation with another Value Checker annotation.
   *
   * @param stringValAnno annotation of type @StringVal
   * @param otherAnno annotation from the value checker hierarchy
   * @return greatest lower bound of {@code stringValAnno} and {@code otherAnno}
   */
  private AnnotationMirror glbOfStringVal(
      AnnotationMirror stringValAnno, AnnotationMirror otherAnno) {
    List<String> values = atypeFactory.getStringValues(stringValAnno);
    switch (AnnotationUtils.annotationName(otherAnno)) {
      case ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        // Intersection of value lists
        List<String> otherValues = atypeFactory.getStringValues(otherAnno);
        values.retainAll(otherValues);
        break;
      case ValueAnnotatedTypeFactory.ARRAYLEN_NAME:
        // Retain strings of correct lengths
        List<Integer> otherLengths = atypeFactory.getArrayLength(otherAnno);
        ArrayList<String> result = new ArrayList<>();
        for (String s : values) {
          if (otherLengths.contains(s.length())) {
            result.add(s);
          }
        }
        values = result;
        break;
      case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
        // Retain strings of lengths from a range
        Range otherRange = atypeFactory.getRange(otherAnno);
        ArrayList<String> range = new ArrayList<>();
        for (String s : values) {
          if (otherRange.contains(s.length())) {
            range.add(s);
          }
        }
        values = range;
        break;
      case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME:
        List<@Regex String> regexes =
            AnnotationUtils.getElementValueArray(
                otherAnno, atypeFactory.matchesRegexValueElement, String.class);
        values =
            values.stream()
                .filter(value -> regexes.stream().anyMatch(value::matches))
                .collect(Collectors.toList());
        break;
      default:
        return atypeFactory.BOTTOMVAL;
    }

    return atypeFactory.createStringAnnotation(values);
  }

  @Override
  public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) {
    if (isSubtype(a1, a2)) {
      return a1;
    } else if (isSubtype(a2, a1)) {
      return a2;
    } else {

      // Implementation of GLB where one of the annotations is StringVal is needed for
      // length-based refinement of constant string values. Other cases of length-based
      // refinement are handled by subtype check.
      if (AnnotationUtils.areSameByName(a1, ValueAnnotatedTypeFactory.STRINGVAL_NAME)) {
        return glbOfStringVal(a1, a2);
      } else if (AnnotationUtils.areSameByName(a2, ValueAnnotatedTypeFactory.STRINGVAL_NAME)) {
        return glbOfStringVal(a2, a1);
      }

      // Simply return BOTTOMVAL in other cases. Refine this if we discover use cases
      // that need a more precise GLB.
      return atypeFactory.BOTTOMVAL;
    }
  }

  @Override
  public int numberOfIterationsBeforeWidening() {
    return ValueAnnotatedTypeFactory.MAX_VALUES + 1;
  }

  @Override
  public AnnotationMirror widenedUpperBound(
      AnnotationMirror newQualifier, AnnotationMirror previousQualifier) {
    AnnotationMirror lub = leastUpperBound(newQualifier, previousQualifier);
    if (AnnotationUtils.areSameByName(lub, ValueAnnotatedTypeFactory.INTRANGE_NAME)) {
      Range lubRange = atypeFactory.getRange(lub);
      Range newRange = atypeFactory.getRange(newQualifier);
      Range oldRange = atypeFactory.getRange(previousQualifier);
      Range wubRange = widenedRange(newRange, oldRange, lubRange);
      return atypeFactory.createIntRangeAnnotation(wubRange);
    } else if (AnnotationUtils.areSameByName(lub, ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME)) {
      Range lubRange = atypeFactory.getRange(lub);
      Range newRange = atypeFactory.getRange(newQualifier);
      Range oldRange = atypeFactory.getRange(previousQualifier);
      Range wubRange = widenedRange(newRange, oldRange, lubRange);
      return atypeFactory.createArrayLenRangeAnnotation(wubRange);
    } else {
      return lub;
    }
  }

  /**
   * Determine the widened range from other ranges.
   *
   * @param newRange the new range
   * @param oldRange the old range
   * @param lubRange the LUB range
   * @return the widened range
   */
  private Range widenedRange(Range newRange, Range oldRange, Range lubRange) {
    if (newRange == null || oldRange == null || lubRange.equals(oldRange)) {
      return lubRange;
    }
    // If both bounds of the new range are bigger than the old range, then returned range
    // should use the lower bound of the new range and a MAX_VALUE.
    if ((newRange.from >= oldRange.from && newRange.to >= oldRange.to)) {
      long max = lubRange.to;
      if (max < Byte.MAX_VALUE) {
        max = Byte.MAX_VALUE;
      } else if (max < Short.MAX_VALUE) {
        max = Short.MAX_VALUE;
      } else if (max < Integer.MAX_VALUE) {
        max = Integer.MAX_VALUE;
      } else {
        max = Long.MAX_VALUE;
      }
      return Range.create(newRange.from, max);
    }

    // If both bounds of the old range are bigger than the new range, then returned range
    // should use a MIN_VALUE and the upper bound of the new range.
    if ((newRange.from <= oldRange.from && newRange.to <= oldRange.to)) {
      long min = lubRange.from;
      if (min > Byte.MIN_VALUE) {
        min = Byte.MIN_VALUE;
      } else if (min > Short.MIN_VALUE) {
        min = Short.MIN_VALUE;
      } else if (min > Integer.MIN_VALUE) {
        min = Integer.MIN_VALUE;
      } else {
        min = Long.MIN_VALUE;
      }
      return Range.create(min, newRange.to);
    }

    if (lubRange.isWithin(Byte.MIN_VALUE + 1, Byte.MAX_VALUE)
        || lubRange.isWithin(Byte.MIN_VALUE, Byte.MAX_VALUE - 1)) {
      return Range.BYTE_EVERYTHING;
    } else if (lubRange.isWithin(Short.MIN_VALUE + 1, Short.MAX_VALUE)
        || lubRange.isWithin(Short.MIN_VALUE, Short.MAX_VALUE - 1)) {
      return Range.SHORT_EVERYTHING;
    } else if (lubRange.isWithin(Long.MIN_VALUE + 1, Long.MAX_VALUE)
        || lubRange.isWithin(Long.MIN_VALUE, Long.MAX_VALUE - 1)) {
      return Range.INT_EVERYTHING;
    } else {
      return Range.EVERYTHING;
    }
  }

  /**
   * Determines the least upper bound of a1 and a2, which contains the union of their sets of
   * possible values.
   *
   * @return the least upper bound of a1 and a2
   */
  @Override
  public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) {
    if (!AnnotationUtils.areSameByName(getTopAnnotation(a1), getTopAnnotation(a2))) {
      // The annotations are in different hierarchies
      return null;
    }

    a1 = atypeFactory.convertSpecialIntRangeToStandardIntRange(a1);
    a2 = atypeFactory.convertSpecialIntRangeToStandardIntRange(a2);

    if (isSubtype(a1, a2)) {
      return a2;
    } else if (isSubtype(a2, a1)) {
      return a1;
    }
    String qual1 = AnnotationUtils.annotationName(a1);
    String qual2 = AnnotationUtils.annotationName(a2);

    if (qual1.equals(qual2)) {
      // If both are the same type, determine the type and merge
      switch (qual1) {
        case ValueAnnotatedTypeFactory.INTRANGE_NAME:
          // special handling for IntRange
          Range intrange1 = atypeFactory.getRange(a1);
          Range intrange2 = atypeFactory.getRange(a2);
          return atypeFactory.createIntRangeAnnotation(intrange1.union(intrange2));
        case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
          // special handling for ArrayLenRange
          Range range1 = atypeFactory.getRange(a1);
          Range range2 = atypeFactory.getRange(a2);
          return atypeFactory.createArrayLenRangeAnnotation(range1.union(range2));
        case ValueAnnotatedTypeFactory.INTVAL_NAME:
          List<Long> longs = atypeFactory.getIntValues(a1);
          SystemUtil.addWithoutDuplicates(longs, atypeFactory.getIntValues(a2));
          return atypeFactory.createIntValAnnotation(longs);
        case ValueAnnotatedTypeFactory.ARRAYLEN_NAME:
          List<Integer> arrayLens = atypeFactory.getArrayLength(a1);
          SystemUtil.addWithoutDuplicates(arrayLens, atypeFactory.getArrayLength(a2));
          return atypeFactory.createArrayLenAnnotation(arrayLens);
        case ValueAnnotatedTypeFactory.STRINGVAL_NAME:
          List<String> strings = atypeFactory.getStringValues(a1);
          SystemUtil.addWithoutDuplicates(strings, atypeFactory.getStringValues(a2));
          return atypeFactory.createStringAnnotation(strings);
        case ValueAnnotatedTypeFactory.BOOLVAL_NAME:
          List<Boolean> bools = atypeFactory.getBooleanValues(a1);
          SystemUtil.addWithoutDuplicates(bools, atypeFactory.getBooleanValues(a2));
          return atypeFactory.createBooleanAnnotation(bools);
        case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME:
          List<Double> doubles = atypeFactory.getDoubleValues(a1);
          SystemUtil.addWithoutDuplicates(doubles, atypeFactory.getDoubleValues(a2));
          return atypeFactory.createDoubleAnnotation(doubles);
        case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME:
          List<@Regex String> regexes = atypeFactory.getMatchesRegexValues(a1);
          SystemUtil.addWithoutDuplicates(regexes, atypeFactory.getMatchesRegexValues(a2));
          return atypeFactory.createMatchesRegexAnnotation(regexes);
        default:
          throw new BugInCF("default case: %s %s %s%n", qual1, a1, a2);
      }
    }

    // Special handling for dealing with the lub of two annotations that are distinct but
    // convertible (e.g. a StringVal and a MatchesRegex, or an IntVal and an IntRange).
    // Each of these variables is an annotation of the given type, or is null if neither of
    // the arguments to leastUpperBound is of the given types.
    AnnotationMirror arrayLenAnno = null;
    AnnotationMirror arrayLenRangeAnno = null;
    AnnotationMirror stringValAnno = null;
    AnnotationMirror matchesRegexAnno = null;
    AnnotationMirror intValAnno = null;
    AnnotationMirror intRangeAnno = null;
    AnnotationMirror doubleValAnno = null;

    switch (qual1) {
      case ValueAnnotatedTypeFactory.ARRAYLEN_NAME:
        arrayLenAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
        arrayLenRangeAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        stringValAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME:
        matchesRegexAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.INTVAL_NAME:
        intValAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.INTRANGE_NAME:
        intRangeAnno = a1;
        break;
      case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME:
        doubleValAnno = a1;
        break;
      default:
        // Do nothing
    }

    switch (qual2) {
      case ValueAnnotatedTypeFactory.ARRAYLEN_NAME:
        arrayLenAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
        arrayLenRangeAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        stringValAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME:
        matchesRegexAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.INTVAL_NAME:
        intValAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.INTRANGE_NAME:
        intRangeAnno = a2;
        break;
      case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME:
        doubleValAnno = a2;
        break;
      default:
        // Do nothing
    }

    // Special handling for dealing with the lub of an ArrayLenRange and an ArrayLen,
    // a StringVal with one of them, or a StringVal and a MatchesRegex.
    if (arrayLenAnno != null && arrayLenRangeAnno != null) {
      return leastUpperBound(
          arrayLenRangeAnno, atypeFactory.convertArrayLenToArrayLenRange(arrayLenAnno));
    } else if (stringValAnno != null && arrayLenAnno != null) {
      return leastUpperBound(arrayLenAnno, atypeFactory.convertStringValToArrayLen(stringValAnno));
    } else if (stringValAnno != null && arrayLenRangeAnno != null) {
      return leastUpperBound(
          arrayLenRangeAnno, atypeFactory.convertStringValToArrayLenRange(stringValAnno));
    } else if (stringValAnno != null && matchesRegexAnno != null) {
      return leastUpperBound(
          matchesRegexAnno, atypeFactory.convertStringValToMatchesRegex(stringValAnno));
    }

    // Annotations are both in the same hierarchy, but they are not the same.
    // If a1 and a2 are not the same type of *Value annotation, they may still be mergeable
    // because some values can be implicitly cast as others. For example, if a1 and a2 are
    // both in {DoubleVal, IntVal} then they will be converted upwards: IntVal -> DoubleVal
    // to arrive at a common annotation type.

    if (doubleValAnno != null) {
      if (intRangeAnno != null) {
        intValAnno = atypeFactory.convertIntRangeToIntVal(intRangeAnno);
        if (AnnotationUtils.areSameByName(intValAnno, ValueAnnotatedTypeFactory.UNKNOWN_NAME)) {
          intValAnno = null;
        }
      }
      if (intValAnno != null) {
        // Convert intValAnno to a @DoubleVal AnnotationMirror
        AnnotationMirror doubleValAnno2 = atypeFactory.convertIntValToDoubleVal(intValAnno);
        return leastUpperBound(doubleValAnno, doubleValAnno2);
      }
      return atypeFactory.UNKNOWNVAL;
    }
    if (intRangeAnno != null && intValAnno != null) {
      // Convert intValAnno to an @IntRange AnnotationMirror
      AnnotationMirror intRangeAnno2 = atypeFactory.convertIntValToIntRange(intValAnno);
      return leastUpperBound(intRangeAnno, intRangeAnno2);
    }

    // In all other cases, the LUB is UnknownVal.
    return atypeFactory.UNKNOWNVAL;
  }

  /**
   * Computes subtyping as per the subtyping in the qualifier hierarchy structure unless both
   * annotations are Value. In this case, subAnno is a subtype of superAnno iff superAnno contains
   * at least every element of subAnno.
   *
   * @return true if subAnno is a subtype of superAnno, false otherwise
   */
  @Override
  public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
    subAnno = atypeFactory.convertSpecialIntRangeToStandardIntRange(subAnno);
    superAnno = atypeFactory.convertSpecialIntRangeToStandardIntRange(superAnno);
    String subQual = AnnotationUtils.annotationName(subAnno);
    if (subQual.equals(ValueAnnotatedTypeFactory.UNKNOWN_NAME)) {
      superAnno = atypeFactory.convertToUnknown(superAnno);
    }
    String superQual = AnnotationUtils.annotationName(superAnno);
    if (superQual.equals(ValueAnnotatedTypeFactory.UNKNOWN_NAME)
        || subQual.equals(ValueAnnotatedTypeFactory.BOTTOMVAL_NAME)) {
      return true;
    } else if (superQual.equals(ValueAnnotatedTypeFactory.BOTTOMVAL_NAME)
        || subQual.equals(ValueAnnotatedTypeFactory.UNKNOWN_NAME)) {
      return false;
    } else if (superQual.equals(ValueAnnotatedTypeFactory.POLY_NAME)) {
      return subQual.equals(ValueAnnotatedTypeFactory.POLY_NAME);
    } else if (subQual.equals(ValueAnnotatedTypeFactory.POLY_NAME)) {
      return false;
    } else if (superQual.equals(subQual)) {
      // Same type, so might be subtype
      if (subQual.equals(ValueAnnotatedTypeFactory.INTRANGE_NAME)
          || subQual.equals(ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME)) {
        // Special case for range-based annotations
        Range superRange = atypeFactory.getRange(superAnno);
        Range subRange = atypeFactory.getRange(subAnno);
        return superRange.contains(subRange);
      } else {
        // The annotations are one of: ArrayLen, BoolVal, DoubleVal, EnumVal, StringVal.
        @SuppressWarnings("deprecation") // concrete annotation class is not known
        List<Object> superValues =
            AnnotationUtils.getElementValueArray(superAnno, "value", Object.class, false);
        @SuppressWarnings("deprecation") // concrete annotation class is not known
        List<Object> subValues =
            AnnotationUtils.getElementValueArray(subAnno, "value", Object.class, false);
        return superValues.containsAll(subValues);
      }
    }
    switch (superQual + subQual) {
      case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME + ValueAnnotatedTypeFactory.INTVAL_NAME:
        List<Double> superValues = atypeFactory.getDoubleValues(superAnno);
        List<Double> subValues =
            atypeFactory.convertLongListToDoubleList(atypeFactory.getIntValues(subAnno));
        return superValues.containsAll(subValues);
      case ValueAnnotatedTypeFactory.INTRANGE_NAME + ValueAnnotatedTypeFactory.INTVAL_NAME:
      case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME + ValueAnnotatedTypeFactory.ARRAYLEN_NAME:
        Range superRange = atypeFactory.getRange(superAnno);
        List<Long> subLongValues = atypeFactory.getArrayLenOrIntValue(subAnno);
        Range subLongRange = Range.create(subLongValues);
        return superRange.contains(subLongRange);
      case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME + ValueAnnotatedTypeFactory.INTRANGE_NAME:
        Range subRange = atypeFactory.getRange(subAnno);
        if (subRange.isWiderThan(ValueAnnotatedTypeFactory.MAX_VALUES)) {
          return false;
        }
        List<Double> superDoubleValues = atypeFactory.getDoubleValues(superAnno);
        List<Double> subDoubleValues = ValueCheckerUtils.getValuesFromRange(subRange, Double.class);
        return superDoubleValues.containsAll(subDoubleValues);
      case ValueAnnotatedTypeFactory.INTVAL_NAME + ValueAnnotatedTypeFactory.INTRANGE_NAME:
      case ValueAnnotatedTypeFactory.ARRAYLEN_NAME + ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
        Range subRange2 = atypeFactory.getRange(subAnno);
        if (subRange2.isWiderThan(ValueAnnotatedTypeFactory.MAX_VALUES)) {
          return false;
        }
        List<Long> superValues2 = atypeFactory.getArrayLenOrIntValue(superAnno);
        List<Long> subValues2 = ValueCheckerUtils.getValuesFromRange(subRange2, Long.class);
        return superValues2.containsAll(subValues2);
      case ValueAnnotatedTypeFactory.STRINGVAL_NAME + ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME:
      case ValueAnnotatedTypeFactory.STRINGVAL_NAME + ValueAnnotatedTypeFactory.ARRAYLEN_NAME:

        // Allow @ArrayLen(0) to be converted to @StringVal("")
        List<String> superStringValues = atypeFactory.getStringValues(superAnno);
        return superStringValues.contains("") && atypeFactory.getMaxLenValue(subAnno) == 0;
      case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME + ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        List<String> strings = atypeFactory.getStringValues(subAnno);
        List<String> regexes =
            AnnotationUtils.getElementValueArray(
                superAnno, atypeFactory.matchesRegexValueElement, String.class);
        return strings.stream().allMatch(string -> regexes.stream().anyMatch(string::matches));
      case ValueAnnotatedTypeFactory.ARRAYLEN_NAME + ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        // StringVal is a subtype of ArrayLen, if all the strings have one of the correct lengths.
        List<Integer> superIntValues = atypeFactory.getArrayLength(superAnno);
        List<String> subStringValues = atypeFactory.getStringValues(subAnno);
        for (String value : subStringValues) {
          if (!superIntValues.contains(value.length())) {
            return false;
          }
        }
        return true;
      case ValueAnnotatedTypeFactory.ARRAYLENRANGE_NAME + ValueAnnotatedTypeFactory.STRINGVAL_NAME:
        // StringVal is a subtype of ArrayLenRange, if all the strings have a length in the range.
        Range superRange2 = atypeFactory.getRange(superAnno);
        List<String> subValues3 = atypeFactory.getStringValues(subAnno);
        for (String value : subValues3) {
          if (!superRange2.contains(value.length())) {
            return false;
          }
        }
        return true;
      default:
        return false;
    }
  }
}