package org.infinispan.query.objectfilter.impl.syntax;

import java.util.ArrayList;
import java.util.List;

/**
 * Applies some optimisations to a boolean expression. Most notably, it brings it to NNF (Negation normal form, see
 * http://en.wikipedia.org/wiki/Negation_normal_form). Moves negation directly near the variable by repeatedly applying
 * the De Morgan's laws (see http://en.wikipedia.org/wiki/De_Morgan%27s_laws). Eliminates double negation. Normalizes
 * comparison operators by replacing 'greater' with 'less'. Detects sub-expressions that are boolean constants.
 * Simplifies boolean constants by applying boolean short-circuiting. Eliminates resulting trivial conjunctions or
 * disjunctions that have only one child. Ensures all paths from root to leafs contain an alternation of conjunction and
 * disjunction. This is achieved by absorbing the children whenever a boolean sub-expression if of the same kind as the
 * parent.
 *
 * @author anistor@redhat.com
 * @since 7.0
 */
public final class BooleanFilterNormalizer {

   /**
    * A visitor that removes constant boolean expressions, absorbs sub-expressions (removes needless parentheses) and
    * swaps comparison operand sides to ensure the constant is always on the right side.
    */
   private final ExprVisitor simplifierVisitor = new ExprVisitor() {

      @Override
      public BooleanExpr visit(NotExpr notExpr) {
         // push the negation down the tree until it reaches a PrimaryPredicateExpr

         BooleanExpr child = notExpr.getChild();
         if (child instanceof SpatialWithinCircleExpr) {
            // TODO [anistor] with the exception of spatial predicates, which cannot be logically negated
            return notExpr;
         }

         return child.acceptVisitor(deMorganVisitor);
      }

      @Override
      public BooleanExpr visit(OrExpr orExpr) {
         List<BooleanExpr> children = new ArrayList<>(orExpr.getChildren().size());

         for (BooleanExpr child : orExpr.getChildren()) {
            child = child.acceptVisitor(this);

            if (child instanceof ConstantBooleanExpr) {
               // remove boolean constants or shortcircuit entirely
               if (((ConstantBooleanExpr) child).getValue()) {
                  return ConstantBooleanExpr.TRUE;
               }
            } else if (child instanceof OrExpr) {
               // absorb sub-expressions of the same kind
               children.addAll(((OrExpr) child).getChildren());
            } else {
               children.add(child);
            }
         }

         PredicateOptimisations.optimizePredicates(children, false);

         // simplify trivial expressions
         if (children.size() == 1) {
            return children.get(0);
         }

         return new OrExpr(children);
      }

      @Override
      public BooleanExpr visit(AndExpr andExpr) {
         List<BooleanExpr> children = new ArrayList<>(andExpr.getChildren().size());

         for (BooleanExpr child : andExpr.getChildren()) {
            child = child.acceptVisitor(this);

            if (child instanceof ConstantBooleanExpr) {
               // remove boolean constants or shortcircuit entirely
               if (!((ConstantBooleanExpr) child).getValue()) {
                  return ConstantBooleanExpr.FALSE;
               }
            } else if (child instanceof AndExpr) {
               // absorb sub-expressions of the same kind
               children.addAll(((AndExpr) child).getChildren());
            } else {
               children.add(child);
            }
         }

         PredicateOptimisations.optimizePredicates(children, true);

         // simplify trivial expressions
         if (children.size() == 1) {
            return children.get(0);
         }

         return new AndExpr(children);
      }

      @Override
      public BooleanExpr visit(ComparisonExpr comparisonExpr) {
         // start moving the constant to the right side of the comparison if it's not already there
         ValueExpr leftChild = comparisonExpr.getLeftChild();
         leftChild = leftChild.acceptVisitor(this);

         ValueExpr rightChild = comparisonExpr.getRightChild();
         rightChild = rightChild.acceptVisitor(this);

         ComparisonExpr.Type comparisonType = comparisonExpr.getComparisonType();

         // handle constant expressions
         if (leftChild instanceof ConstantValueExpr leftConstant) {
            if (rightChild instanceof ConstantValueExpr rightConstant) {
               // replace the comparison of the two constants with the actual result
               Comparable leftValue = leftConstant.getConstantValue();
               Comparable rightValue = rightConstant.getConstantValue();
               int compRes = leftValue.compareTo(rightValue);
               return switch (comparisonType) {
                  case LESS -> ConstantBooleanExpr.forBoolean(compRes < 0);
                  case LESS_OR_EQUAL -> ConstantBooleanExpr.forBoolean(compRes <= 0);
                  case EQUAL -> ConstantBooleanExpr.forBoolean(compRes == 0);
                  case NOT_EQUAL -> ConstantBooleanExpr.forBoolean(compRes != 0);
                  case GREATER_OR_EQUAL -> ConstantBooleanExpr.forBoolean(compRes >= 0);
                  case GREATER -> ConstantBooleanExpr.forBoolean(compRes > 0);
                  default -> throw new IllegalStateException("Unexpected comparison type: " + comparisonType);
               };
            }

            // swap operand sides to ensure the constant is always on the right side
            ValueExpr temp = rightChild;
            rightChild = leftChild;
            leftChild = temp;

            // now reverse the operator too to restore the semantics
            comparisonType = comparisonType.reverse();
         }

         // comparison operators are never negated using NotExpr
         return new ComparisonExpr(leftChild, rightChild, comparisonType);
      }

      @Override
      public BooleanExpr visit(BetweenExpr betweenExpr) {
         return new AndExpr(
               new ComparisonExpr(betweenExpr.getLeftChild(), betweenExpr.getFromChild(), ComparisonExpr.Type.GREATER_OR_EQUAL),
               new ComparisonExpr(betweenExpr.getLeftChild(), betweenExpr.getToChild(), ComparisonExpr.Type.LESS_OR_EQUAL)
         );
      }
   };

   /**
    * Handles negation by applying De Morgan laws.
    */
   private final ExprVisitor deMorganVisitor = new ExprVisitor() {

      @Override
      public BooleanExpr visit(ConstantBooleanExpr constantBooleanExpr) {
         // negated constants are simplified immediately
         return constantBooleanExpr.negate();
      }

      @Override
      public BooleanExpr visit(NotExpr notExpr) {
         // double negation is eliminated, child is simplified
         return notExpr.getChild().acceptVisitor(simplifierVisitor);
      }

      @Override
      public BooleanExpr visit(OrExpr orExpr) {
         List<BooleanExpr> children = new ArrayList<>(orExpr.getChildren().size());

         for (BooleanExpr child : orExpr.getChildren()) {
            child = child.acceptVisitor(this);

            if (child instanceof ConstantBooleanExpr) {
               // remove boolean constants
               if (!((ConstantBooleanExpr) child).getValue()) {
                  return ConstantBooleanExpr.FALSE;
               }
            } else if (child instanceof AndExpr) {
               // absorb sub-expressions of the same kind
               children.addAll(((AndExpr) child).getChildren());
            } else {
               children.add(child);
            }
         }

         // simplify trivial expressions
         if (children.size() == 1) {
            return children.get(0);
         }

         return new AndExpr(children);
      }

      @Override
      public BooleanExpr visit(AndExpr andExpr) {
         List<BooleanExpr> children = new ArrayList<>(andExpr.getChildren().size());

         for (BooleanExpr child : andExpr.getChildren()) {
            child = child.acceptVisitor(this);

            if (child instanceof ConstantBooleanExpr) {
               // remove boolean constants
               if (((ConstantBooleanExpr) child).getValue()) {
                  return ConstantBooleanExpr.TRUE;
               }
            } else if (child instanceof OrExpr) {
               // absorb sub-expressions of the same kind
               children.addAll(((OrExpr) child).getChildren());
            } else {
               children.add(child);
            }
         }

         // simplify trivial expressions
         if (children.size() == 1) {
            return children.get(0);
         }

         return new OrExpr(children);
      }

      @Override
      public BooleanExpr visit(ComparisonExpr comparisonExpr) {
         BooleanExpr booleanExpr = comparisonExpr.acceptVisitor(simplifierVisitor);

         // simplify negated constants immediately
         if (booleanExpr instanceof ConstantBooleanExpr) {
            return ((ConstantBooleanExpr) booleanExpr).negate();
         }

         // eliminate double negation
         if (booleanExpr instanceof NotExpr) {
            return ((NotExpr) booleanExpr).getChild();
         }

         // interval predicates are never negated, they are converted instead into the opposite interval
         if (booleanExpr instanceof ComparisonExpr c) {
            return new ComparisonExpr(c.getLeftChild(), c.getRightChild(), c.getComparisonType().negate());
         }

         return new NotExpr(booleanExpr);
      }

      @Override
      public BooleanExpr visit(BetweenExpr betweenExpr) {
         return new OrExpr(
               new ComparisonExpr(betweenExpr.getLeftChild(), betweenExpr.getFromChild(), ComparisonExpr.Type.LESS),
               new ComparisonExpr(betweenExpr.getLeftChild(), betweenExpr.getToChild(), ComparisonExpr.Type.GREATER)
         );
      }

      @Override
      public BooleanExpr visit(IsNullExpr isNullExpr) {
         return new NotExpr(isNullExpr);
      }

      @Override
      public BooleanExpr visit(LikeExpr likeExpr) {
         return new NotExpr(likeExpr);
      }
   };

   public BooleanExpr normalize(BooleanExpr booleanExpr) {
      return booleanExpr == null ? null : booleanExpr.acceptVisitor(simplifierVisitor);
   }
}
