#include "clang/Analysis/Analyses/Interval.h"
#include "clang/AST/Stmt.h"
#include "clang/Analysis/CFG.h"
#include "clang/Analysis/AnalysisContext.h"
#include "clang/AST/StmtVisitor.h"

#include "clang/Analysis/Analyses/IntervalSolver/Log.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/Complete.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp"
  
#include "llvm/ADT/PostOrderIterator.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/Support/Process.h"
  
#include <deque>
#include <algorithm>
#include <vector>
#include <map>

using namespace clang;

typedef EquationSystem<Complete<int> > EqnSys;
typedef Expression<Complete<int> > EqnExpr;

#include <sstream>
template<typename T>
std::string toString(const T& obj) {
  std::stringstream stream;
  stream << obj;
  return stream.str();
}

IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
  : context(&context) {
}

IntervalAnalysis :: ~IntervalAnalysis() {
}

// Two pieces of state:
//  -> condition protecting a node
//  -> node's expression itself
// We can then combine these in a straightforward way to
// get out equation system, whereupon we can solve for what
// we want to know. Then we can have program invariants!
//
// Hooray!

EqnExpr* fromStmt(const Stmt*, EqnSys&);

EqnExpr* fromInteger(const IntegerLiteral* expr, EqnSys& system) {
  return &system.constant(*expr->getValue().getRawData());
}

EqnExpr* fromDeclExpr(const DeclRefExpr* expr, EqnSys& system) {
  return &system.variable(expr->getNameInfo().getAsString());
}

EqnExpr* fromUnary(const UnaryOperator* op, EqnSys& system) {
  switch (op->getOpcode()) {
  case UO_PreInc:
    break;
  case UO_PostInc:
    break;
  }
  return NULL;
}


Addition<Complete<int> >* add = new Addition<Complete<int> >();
Subtraction<Complete<int> >* sub = new Subtraction<Complete<int> >();
Multiplication<Complete<int> >* mul = new Multiplication<Complete<int> >();

EqnExpr* fromBinary(const BinaryOperator* op, EqnSys& system) {
  EqnExpr* left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
  EqnExpr* right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
  
  std::vector<EqnExpr*> args;
  args.push_back(left);
  args.push_back(right);
  
  switch (op->getOpcode()) {
  case BO_Add:
    return &system.expression(add, args);
  case BO_Sub:
    return &system.expression(sub, args);
  case BO_Mul:
    return &system.expression(mul, args);
  case BO_LT:
  case BO_LE:
  case BO_GT:
  case BO_GE:
    break;
  } 
  return NULL;
}

EqnExpr* fromDeclStmt(const DeclStmt* stmt, EqnSys& system) {
  for (DeclStmt::const_decl_iterator it = stmt->decl_begin(),
                                     ei = stmt->decl_end();
       it != ei;
       ++it) {
    if ((*it)->getKind() == Decl::Var) {
      const VarDecl* decl = static_cast<const VarDecl*>(*it);
      Variable<Complete<int> > var = system.variable(decl->getNameAsString());
      std::vector<EqnExpr*> args;
      args.push_back(&system.constant(-infinity<Complete<int> >()));
      args.push_back(fromStmt(decl->getInit(), system));
      system[var] = &system.maxExpression(args);
    }
  }
  return NULL;
}

EqnExpr* fromAssignment(const BinaryOperator* op, EqnSys& system) {
  EqnExpr* left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
  EqnExpr* right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
  Variable<Complete<int> >* var = static_cast<Variable<Complete<int> >*>(left);

  std::vector<EqnExpr*> args;
  args.push_back(&system.constant(-infinity<Complete<int> >()));
  args.push_back(right);
  if (system[*var] != NULL)
    args.push_back(system[*var]);
  system[*var] = &system.maxExpression(args);

  return NULL;
}

EqnExpr* fromStmt(const Stmt* stmt, EqnSys& system) {
  if (!stmt)
    return NULL;
  switch (stmt->getStmtClass()) {
  case Stmt::IntegerLiteralClass:
    return fromInteger(static_cast<const IntegerLiteral*>(stmt), system);
  case Stmt::DeclRefExprClass:
    return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt), system);
  case Stmt::UnaryOperatorClass:
    return fromUnary(static_cast<const UnaryOperator*>(stmt), system);
  case Stmt::DeclStmtClass:
    return fromDeclStmt(static_cast<const DeclStmt*>(stmt), system);
  case Stmt::BinaryOperatorClass:
    {
      const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
      if (binop->isAssignmentOp())
        return fromAssignment(binop, system);
      else
        return fromBinary(binop, system);
    }
  }
  return NULL;
}

void runOnBlock(std::string id, const CFGBlock* block, EqnSys& system) {
  for (CFGBlock::const_iterator it = block->begin(),
                                ei = block->end();
       it != ei;
       ++it) {
    const CFGStmt* cfg_stmt = it->getAs<CFGStmt>();
    const Stmt* stmt = static_cast<const Stmt*>(cfg_stmt->getStmt());
    EqnExpr* expr = fromStmt(stmt, system);
  }
  fromStmt(block->getTerminatorCondition(), system);

  /*if (terminator.getStmt() != NULL) {
    if (terminator.getStmt()->getStmtClass() == Stmt::IfStmtClass) {
      const IfStmt* if_stmt = static_cast<const IfStmt*>(terminator.getStmt());
      llvm::errs() << "If: \n";
      if_stmt->dump();
    } else {
      llvm::errs() << "\n";
      terminator.getStmt()->dump();
    }
    }*/
  return; // TODO: return a generated expression
}

void IntervalAnalysis::runOnAllBlocks() {
  llvm::errs() << "Enter run on all blocks\n";

  const CFG *cfg = this->context->getCFG();

  EqnSys system;

  std::set<const CFGBlock*> seen;
  std::deque<const CFGBlock*> todo;
  todo.push_back(&cfg->getEntry());

  while (!todo.empty()) {
    const CFGBlock* block = todo.front();
    if (seen.find(todo.front()) != seen.end()) {
      todo.pop_front();
      continue;
    }
    llvm::errs() << (void*)block << "\n";
    seen.insert(block);
    todo.pop_front();
    runOnBlock(toString(block), block, system);
    llvm::errs() << "-> ";
    for (CFGBlock::const_succ_iterator it = block->succ_begin(),
                                       ei = block->succ_end();
         it != ei;
         it++ ) {
      llvm::errs() << (void*) *it << ", ";
      todo.push_back(*it);
    }
    llvm::errs() << "\n\n";
  }

  llvm::errs() << "Exit run on all blocks\n";

  llvm::errs() << toString(system) << "\n";

  system.indexMaxExpressions();
  DynamicMaxStrategy<Complete<int> > strategy(system);
  DynamicVariableAssignment<Complete<int> > rho(system, strategy);
  strategy.setRho(rho);

  for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
    Variable<Complete<int> >& var = system.variable(i);
    llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
  }

  //  cfg->dump(context->getASTContext().getLangOpts(),
  //            llvm::sys::Process::StandardErrHasColors());
}


const void *IntervalAnalysis::getTag() { static int x; return &x; }