//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using Microsoft.Contracts;
using Microsoft.Boogie.VCExprAST;

namespace Microsoft.Boogie.Simplify
{
  // Simplify does not understand the LET operator, so we have to replace
  // it with implications (previously, this was done in the VCExprGenerator), or
  // we have to apply the let as a substitution (in the case of terms)

  // This visitor expects that let-bindings are sorted, so that bound
  // variables only occur after their declaration

  public class Let2ImpliesMutator : SubstitutingVCExprVisitor {

    public Let2ImpliesMutator(VCExpressionGenerator! gen) {
      this(gen, false, false);
    }
    public Let2ImpliesMutator(VCExpressionGenerator! gen, bool keepLetTerm, bool keepLetFormula) {
      base(gen);
      this.keepLetTerm = keepLetTerm;
      this.keepLetFormula = keepLetFormula;
    }
    
    readonly bool keepLetTerm;
    readonly bool keepLetFormula;

    public VCExpr! Mutate(VCExpr! expr) {
      return Mutate(expr, new VCExprSubstitution ());
    }

    ////////////////////////////////////////////////////////////////////////////

    private int polarity = 1;  // 1 for positive, -1 for negative, 0 for both

    // we also track which variables occur in positive, negative, or
    // in both positions (to decide whether implications or equations
    // have to be used to define such a variable)
    private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
    private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
      switch(o1) {
      case OccurrenceTypes.None: return o2;
      case OccurrenceTypes.Pos:
        switch(o2) {
        case OccurrenceTypes.None:
        case OccurrenceTypes.Pos:
          return OccurrenceTypes.Pos;
        default:
          return OccurrenceTypes.PosNeg;
        }
      case OccurrenceTypes.Neg:
        switch(o2) {
        case OccurrenceTypes.None:
        case OccurrenceTypes.Neg:
          return OccurrenceTypes.Neg;
        default:
          return OccurrenceTypes.PosNeg;
        }
      default:
        return OccurrenceTypes.PosNeg;
      }
    }

    private IDictionary<VCExprVar!, OccurrenceTypes>! VarOccurrences =
      new Dictionary<VCExprVar!, OccurrenceTypes>();

    ////////////////////////////////////////////////////////////////////////////

    public override VCExpr! Visit(VCExprVar! node,
                                  VCExprSubstitution! substitution) {
      VCExpr! res = base.Visit(node, substitution);

      VCExprVar resAsVar = res as VCExprVar;
      if (resAsVar != null) {
        OccurrenceTypes occ;
        if (polarity > 0)
          occ = OccurrenceTypes.Pos;
        else if (polarity < 0)
          occ = OccurrenceTypes.Neg;
        else
          occ = OccurrenceTypes.PosNeg;

        OccurrenceTypes oldOcc;
        if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
          occ = Union(occ, oldOcc);
        VarOccurrences[resAsVar] = occ;
      }

      return res;
    }

    public override VCExpr! Visit(VCExprNAry! node,
                                  VCExprSubstitution! substitution) {
      // track the polarity to ensure that no implications are introduced
      // in negative positions
      // UGLY: the code for tracking polarities should be factored out
      // (similar code is used in the TypeEraser)

      VCExpr! res;
      if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
        polarity = -polarity;
        res = base.Visit(node, substitution);
        polarity = -polarity;
      } else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
        polarity = -polarity;
        VCExpr! newArg0 = Mutate(node[0], substitution);
        polarity = -polarity;
        VCExpr! newArg1 = Mutate(node[1], substitution);

        res = Gen.Implies(newArg0, newArg1);
      } else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
                 !node.Op.Equals(VCExpressionGenerator.OrOp) &&
                 !(node.Op is VCExprLabelOp)) {
        // standard is to set the polarity to 0 (fits most operators)
        int oldPolarity = polarity;
        polarity = 0;
        res = base.Visit(node, substitution);
        polarity = oldPolarity;
      } else {
        res = base.Visit(node, substitution);
      }

      return res;
    }

    public override VCExpr! Visit(VCExprLet! originalNode,
                                  VCExprSubstitution! substitution) {
      // first sort the bindings to be able to apply substitutions
      LetBindingSorter! letSorter = new LetBindingSorter (Gen);
      VCExpr! newNode = letSorter.Mutate(originalNode, true);
      VCExprLet node = newNode as VCExprLet;

      if (node == null)
        // it can happen that the complete let-expressions gets eliminated by the
        // sorter, which also checks whether let-bindings are actually used
        return newNode;

      substitution.PushScope(); try {

      // the bindings that remain and that are later handled using an implication
      List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!> ();
      List<VCExprLetBinding!> keepBindings = new List<VCExprLetBinding!> ();

      foreach (VCExprLetBinding! binding in node) {
        // in all cases we apply the substitution up to this point
        // to the bound formula
        VCExpr! newE = Mutate(binding.E, substitution);

        if (binding.V.Type.IsBool) {
          // a bound formula is handled using an implication; we introduce
          // a fresh variable to avoid clashes
          assert polarity > 0;
          
          if (keepLetFormula) {
            keepBindings.Add(Gen.LetBinding(binding.V, newE));
            
          } else {
            VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
            substitution[binding.V] = newVar;

            bindings.Add(Gen.LetBinding(newVar, newE));
          }
        } else {
          if (keepLetTerm) {
            keepBindings.Add(Gen.LetBinding(binding.V, newE));
          } else {
            // a bound term is substituted
            substitution[binding.V] = newE;
          }
        }
      }

      VCExpr! newBody = Mutate(node.Body, substitution);
      if (keepBindings.Count > 0) {
        newBody = Gen.Let(keepBindings, newBody);
      }

      // Depending on the places where the variable occurs, we would
      // have to introduce implications or equations to define the
      // bound variables. For the time being, we just assert that all
      // occurrences are positive
      foreach (VCExprLetBinding! b in bindings) {
        OccurrenceTypes occ;
        if (VarOccurrences.TryGetValue(b.V, out occ))
          assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
      }

      return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);

      } finally {
        substitution.PopScope();
      }
    }
  }

}