package org.checkerframework.framework.testchecker.util;

import java.lang.annotation.Annotation;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashSet;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.util.Elements;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.subtyping.qual.Bottom;
import org.checkerframework.common.subtyping.qual.Unqualified;
import org.checkerframework.framework.qual.TypeUseLocation;
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.framework.util.defaults.QualifierDefaults;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;

public class FlowTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
  protected final AnnotationMirror VALUE, BOTTOM, TOP;

  public FlowTestAnnotatedTypeFactory(BaseTypeChecker checker) {
    super(checker, true);
    VALUE = AnnotationBuilder.fromClass(elements, Value.class);
    BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class);
    TOP = AnnotationBuilder.fromClass(elements, Unqualified.class);

    this.postInit();
  }

  @Override
  protected void addCheckedCodeDefaults(QualifierDefaults defs) {
    defs.addCheckedCodeDefault(BOTTOM, TypeUseLocation.LOWER_BOUND);
    defs.addCheckedCodeDefault(TOP, TypeUseLocation.OTHERWISE);
  }

  @Override
  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
    return new HashSet<Class<? extends Annotation>>(
        Arrays.asList(Value.class, Odd.class, MonotonicOdd.class, Unqualified.class, Bottom.class));
  }

  @Override
  @SuppressWarnings("deprecation") // TODO: REVERT: Just testing backward compatibility.
  public QualifierHierarchy createQualifierHierarchy() {
    return org.checkerframework.framework.util.MultiGraphQualifierHierarchy
        .createMultiGraphQualifierHierarchy(this);
  }

  @Override
  @SuppressWarnings("deprecation") // TODO: REVERT: Just testing backward compatibility.
  public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory(
      org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory factory) {
    return new OldFlowQualifierHierarchy(factory, BOTTOM);
  }

  @SuppressWarnings("deprecation") // TODO: REVERT: Just testing backward compatibility.
  class OldFlowQualifierHierarchy
      extends org.checkerframework.framework.util.GraphQualifierHierarchy {

    public OldFlowQualifierHierarchy(MultiGraphFactory f, AnnotationMirror bottom) {
      super(f, bottom);
    }

    @Override
    public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
      if (AnnotationUtils.areSameByName(superAnno, VALUE)
          && AnnotationUtils.areSameByName(subAnno, VALUE)) {
        return AnnotationUtils.areSame(superAnno, subAnno);
      }
      if (AnnotationUtils.areSameByName(superAnno, VALUE)) {
        superAnno = VALUE;
      }
      if (AnnotationUtils.areSameByName(subAnno, VALUE)) {
        subAnno = VALUE;
      }
      return super.isSubtype(subAnno, superAnno);
    }
  }

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

  /** FlowQualifierHierarchy: {@code @Value(a) <: @Value(b) iff a == b} */
  class FlowQualifierHierarchy extends MostlyNoElementQualifierHierarchy {
    final QualifierKind VALUE_KIND;

    /**
     * Creates a FlowQualifierHierarchy from the given classes.
     *
     * @param qualifierClasses classes of annotations that are the qualifiers for this hierarchy
     * @param elements element utils
     */
    public FlowQualifierHierarchy(
        Collection<Class<? extends Annotation>> qualifierClasses, Elements elements) {
      super(qualifierClasses, elements);
      this.VALUE_KIND = getQualifierKind(VALUE);
    }

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

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

    @Override
    protected AnnotationMirror leastUpperBoundWithElements(
        AnnotationMirror a1,
        QualifierKind qualifierKind1,
        AnnotationMirror a2,
        QualifierKind qualifierKind2,
        QualifierKind lubKind) {
      if (qualifierKind1 == qualifierKind2) {
        // Both are Value
        if (AnnotationUtils.areSame(a1, a2)) {
          return a1;
        } else {
          return TOP;
        }
      } else if (qualifierKind1 == VALUE_KIND) {
        return a1;
      } else if (qualifierKind2 == VALUE_KIND) {
        return a2;
      }
      throw new BugInCF("Unexpected annotations: leastUpperBoundWithElements(%s, %s)", a1, a2);
    }

    @Override
    protected AnnotationMirror greatestLowerBoundWithElements(
        AnnotationMirror a1,
        QualifierKind qualifierKind1,
        AnnotationMirror a2,
        QualifierKind qualifierKind2,
        QualifierKind glbKind) {
      if (qualifierKind1 == qualifierKind2) {
        // Both are Value
        if (AnnotationUtils.areSame(a1, a2)) {
          return a1;
        } else {
          return BOTTOM;
        }
      } else if (qualifierKind1 == VALUE_KIND) {
        return a1;
      } else if (qualifierKind2 == VALUE_KIND) {
        return a2;
      }
      throw new BugInCF("Unexpected annotations: greatestLowerBoundWithElements(%s, %s)", a1, a2);
    }
  }
}