/*
 * Licensed to Julian Hyde under one or more contributor license
 * agreements.  See the NOTICE file distributed with this work
 * for additional information regarding copyright ownership.
 * Julian Hyde licenses this file to you under the Apache
 * License, Version 2.0 (the "License"); you may not use this
 * file except in compliance with the License.  You may obtain a
 * copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing,
 * software distributed under the License is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
 * either express or implied.  See the License for the specific
 * language governing permissions and limitations under the
 * License.
 */
package net.hydromatic.morel.compile;

import static java.util.Objects.requireNonNull;
import static net.hydromatic.morel.ast.CoreBuilder.core;
import static net.hydromatic.morel.util.Ord.forEachIndexed;
import static net.hydromatic.morel.util.Static.skip;

import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableMap;
import com.google.common.collect.Iterables;
import java.util.AbstractList;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import net.hydromatic.morel.ast.Core;
import net.hydromatic.morel.ast.Op;
import net.hydromatic.morel.type.DataType;
import net.hydromatic.morel.type.ForallType;
import net.hydromatic.morel.type.Type;
import net.hydromatic.morel.type.TypeSystem;
import net.hydromatic.morel.util.Pair;
import net.hydromatic.morel.util.Sat;

/**
 * Checks whether patterns are exhaustive and/or redundant.
 *
 * <p>The algorithm converts a list of patterns into a boolean formula with
 * several variables, then checks whether the formula is satisfiable (that is,
 * whether there is a combination of assignments of boolean values to the
 * variables such that the formula evaluates to true).
 */
class PatternCoverageChecker {
  final TypeSystem typeSystem;
  final Sat sat = new Sat();
  final Map<Path, DataTypeSlot> pathSlots = new HashMap<>();

  /** Creates a PatternCoverageChecker. */
  private PatternCoverageChecker(TypeSystem typeSystem) {
    this.typeSystem = requireNonNull(typeSystem, "typeSystem");
  }

  /**
   * Returns whether every possible value that could be matched by pattern
   * {@code pat} would already have been matched by one or more of {@code
   * prevPatList}.
   *
   * <p>For example, the pattern "(1, b: bool)" is covered by "[(1, true), (_,
   * false)]" but not by "[(1, true)]" or "[(_, false)]".
   */
  static boolean isCoveredBy(
      TypeSystem typeSystem, List<Core.Pat> prevPatList, Core.Pat pat) {
    if (prevPatList.isEmpty()) {
      return false; // shortcut
    }
    // p isCoveredBy [p0 ... pN ]
    //   iff
    // (f ^ ~f0 ^ ... ^ ~fN) is not satisfiable
    //   where f is the formula for p
    //   and f0 is the formula for p0, etc.
    return new PatternCoverageChecker(typeSystem).isCoveredBy(pat, prevPatList);
  }

  /**
   * Returns whether a list of patterns covers every possible value. If so, any
   * pattern added to this list would be redundant.
   */
  @SuppressWarnings("StaticPseudoFunctionalStyleMethod")
  static boolean isExhaustive(TypeSystem typeSystem, List<Core.Pat> patList) {
    if (patList.isEmpty()) {
      return false; // shortcut
    }
    if (Iterables.any(
        patList, p -> p.op == Op.WILDCARD_PAT || p.op == Op.ID_PAT)) {
      return true; // shortcut
    }
    final Core.WildcardPat wildcardPat = core.wildcardPat(patList.get(0).type);
    return isCoveredBy(typeSystem, patList, wildcardPat);
  }

  /** Converts a pattern to a logical term. */
  private Sat.Term toTerm(Core.Pat pat) {
    final List<Sat.Term> terms = new ArrayList<>();
    toTerm(pat, Path.ROOT, terms);
    return terms.size() == 1 ? terms.get(0) : sat.and(terms);
  }

  private void toTerm(Core.Pat pat, Path path, List<Sat.Term> terms) {
    switch (pat.op) {
      case WILDCARD_PAT:
      case ID_PAT:
        return; // no constraints to add

      case AS_PAT:
        toTerm(((Core.AsPat) pat).pat, path, terms);
        return;

      case BOOL_LITERAL_PAT:
        // Transform false to FALSE and true to TRUE, constructor of the
        // internal $bool datatype:
        //   datatype $bool = FALSE | TRUE
        // Knowing there are only two values allows us to prove that patterns
        // are exhaustive.
        final DataType boolDataType =
            (DataType) typeSystem.lookup(BuiltIn.Datatype.BOOL);
        final Core.LiteralPat literalPat0 = (Core.LiteralPat) pat;
        final Boolean value = (Boolean) literalPat0.value;
        toTerm(
            core.con0Pat(boolDataType, value ? "TRUE" : "FALSE"), path, terms);
        return;

      case CHAR_LITERAL_PAT:
      case INT_LITERAL_PAT:
      case REAL_LITERAL_PAT:
      case STRING_LITERAL_PAT:
        final Core.LiteralPat literalPat = (Core.LiteralPat) pat;
        terms.add(sat.variable(path.toVar(literalPat.value.toString())));
        return;

      case CON0_PAT:
        final Core.Con0Pat con0Pat = (Core.Con0Pat) pat;
        terms.add(typeConstructorTerm(path, con0Pat.tyCon));
        return;

      case CON_PAT:
        final Core.ConPat conPat = (Core.ConPat) pat;
        terms.add(typeConstructorTerm(path, conPat.tyCon));
        final int j =
            ImmutableList.copyOf(
                    ((DataType) conPat.type).typeConstructors.keySet())
                .indexOf(conPat.tyCon);
        if (j < 0) {
          throw new AssertionError("type constructor not found: " + conPat);
        }
        toTerm(conPat.pat, path.sub(j), terms);
        return;

      case CONS_PAT:
        final Core.ConPat consPat = (Core.ConPat) pat;
        addConsTerms(path, terms, (Core.TuplePat) consPat.pat);
        return;

      case TUPLE_PAT:
        final Core.TuplePat tuplePat = (Core.TuplePat) pat;
        forEachIndexed(
            tuplePat.args, (pat2, i) -> toTerm(pat2, path.sub(i), terms));
        return;

      case RECORD_PAT:
        final Core.RecordPat recordPat = (Core.RecordPat) pat;
        forEachIndexed(
            recordPat.args, (pat2, i) -> toTerm(pat2, path.sub(i), terms));
        return;

      case LIST_PAT:
        // For list
        //   [a, b, c]
        // built terms as if they had written
        //   CONS (a, CONS (b, CONS (c, NIL))
        // namely
        //   var(tag.0=CONS)
        //   ^ var(tag.0.1=CONS)
        //   ^ var(tag.0.1.1=CONS)
        //   ^ var(tag.0.1.1.1=NIL
        toTerm(listToCons((Core.ListPat) pat), path, terms);
        return;

      default:
        throw new AssertionError(pat.op);
    }
  }

  /**
   * Converts a list pattern into a pattern made up of the {@code CONS} and
   * {@code NIL} constructors of the built-in {@code datatype list}.
   *
   * <p>For example, converts: "[]" to "NIL", "[x]" to "CONS (x, NIL)", "[x, y]"
   * to "CONS (x, CONS (y, NIL))", etc.
   */
  private Core.Pat listToCons(Core.ListPat listPat) {
    final Type listType = typeSystem.lookup(BuiltIn.Datatype.LIST);
    final DataType listDataType = (DataType) ((ForallType) listType).type;
    return listToConsRecurse(listDataType, listPat.args);
  }

  private Core.Pat listToConsRecurse(
      DataType listDataType, List<Core.Pat> args) {
    if (args.isEmpty()) {
      return core.con0Pat(listDataType, "NIL");
    } else {
      return core.consPat(
          listDataType,
          "CONS",
          core.tuplePat(
              typeSystem,
              ImmutableList.of(
                  args.get(0), listToConsRecurse(listDataType, skip(args)))));
    }
  }

  private void addConsTerms(
      Path path, List<Sat.Term> terms, Core.TuplePat tuplePat) {
    terms.add(typeConstructorTerm(path, "CONS"));
    toTerm(tuplePat, path, terms);
  }

  private Sat.Variable typeConstructorTerm(Path path, String con) {
    final Pair<DataType, Type.Key> pair = typeSystem.lookupTyCon(con);
    final DataType dataType = pair.left;
    DataTypeSlot slot =
        pathSlots.computeIfAbsent(
            path, p -> new DataTypeSlot(dataType, p, sat));
    return slot.constructorMap.get(con);
  }

  /**
   * Returns whether a pattern is covered by a list of patterns.
   *
   * <p>A pattern {@code pat} is said to be <dfn>covered by</dfn> a list of
   * patterns {@code patList} if any possible value would be caught by one of
   * the patterns in {@code patList} before reaching {@code pat}. Thus {@code
   * pat} is said to be <dfn>redundant</dfn> in that context, and could be
   * removed without affecting behavior.
   */
  public boolean isCoveredBy(Core.Pat pat, List<Core.Pat> patList) {
    final List<Sat.Term> terms = new ArrayList<>();
    patList.forEach(p -> terms.add(toTerm(p)));
    final Sat.Term term = toTerm(pat);

    final List<Sat.Term> terms1 = new ArrayList<>();
    terms1.add(term);
    terms.forEach(t -> terms1.add(sat.not(t)));

    // Add constraints for tags, which are mutually exclusive.
    // For example, for a type with constructors A, B, C
    //   (tag=A or tag=B or tag=C)
    // because at least one tag must be present, and
    //   (not (tag=A or tag=B)
    //   or not (tag=B or tag=C)
    //   or not (tag=C or tag=A))
    // because at most one tag must be present.
    pathSlots
        .values()
        .forEach(
            slot -> {
              final List<Sat.Term> terms2 =
                  new ArrayList<>(slot.constructorMap.values());
              terms1.add(sat.or(terms2));

              final List<Sat.Term> terms3 = new ArrayList<>();
              for (int i = 0; i < terms2.size(); i++) {
                terms3.add(sat.not(sat.or(new ElideList<>(terms2, i))));
              }
              terms1.add(sat.or(terms3));
            });
    final Sat.Term formula = sat.and(terms1);
    final Map<Sat.Variable, Boolean> solve = sat.solve(formula);
    return solve == null;
  }

  /**
   * List that removes one particular element from a backing list.
   *
   * @param <E> element type
   */
  private static class ElideList<E> extends AbstractList<E> {
    private final List<E> list;
    private final int elide;

    ElideList(List<E> list, int elide) {
      this.list = requireNonNull(list, "list");
      this.elide = elide;
    }

    @Override
    public E get(int index) {
      return list.get(index < elide ? index : index + 1);
    }

    @Override
    public int size() {
      return list.size() - 1;
    }
  }

  /**
   * Identifies a point in a nested pattern.
   *
   * <p>Paths are basically immutable lists of integers, built by appending one
   * element at a time.
   */
  private abstract static class Path {
    /** Root path. */
    static final Path ROOT =
        new Path() {
          @Override
          protected void path(StringBuilder b) {}
        };

    @Override
    public String toString() {
      return toVar("");
    }

    /** Creates a sub-path. */
    Path sub(int i) {
      return new SubPath(this, i);
    }

    /**
     * Converts this to a variable.
     *
     * <p>{@code ROOT.sub(2).sub(1).toVar("x")} will return "2.1.x".
     */
    String toVar(String name) {
      final StringBuilder builder = new StringBuilder();
      path(builder);
      builder.append(name);
      return builder.toString();
    }

    protected abstract void path(StringBuilder b);
  }

  /**
   * Path that is a child of a given parent path. The {@code ordinal} makes it
   * unique within its parent. For tuple and record patterns, {@code ordinal} is
   * the field ordinal.
   */
  private static class SubPath extends Path {
    final Path parent;
    final int ordinal;

    SubPath(Path parent, int ordinal) {
      this.parent = parent;
      this.ordinal = ordinal;
    }

    @Override
    protected void path(StringBuilder b) {
      parent.path(b);
      b.append(ordinal).append('.');
    }
  }

  /**
   * Payload of a {@code Sat.Variable} that is an algebraic type. There are
   * sub-variables representing whether the tag holds each of its allowed values
   * (each of which is a constructor).
   */
  private static class DataTypeSlot {
    final DataType dataType;
    final ImmutableMap<String, Sat.Variable> constructorMap;

    DataTypeSlot(DataType dataType, Path path, Sat sat) {
      this.dataType = dataType;
      final ImmutableMap.Builder<String, Sat.Variable> b =
          ImmutableMap.builder();
      dataType.typeConstructors.forEach(
          (name, type) -> b.put(name, sat.variable(path.toVar(name))));
      this.constructorMap = b.build();
    }
  }
}

// End PatternCoverageChecker.java
