#include "expr.h"
#include <stdlib.h>
#include <sstream>
#ifdef _MSC_VER
#include <algorithm>
#endif
#include "check.h"

using namespace std;

int HoleExpr::next_id = 0;
int Expr::markedCount = 0;

C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768);

//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768);

#define USE_HOLE_PATH_COMPRESSION

void Expr::debug() {
  print(cout);
  /*
  cout << "\nAt " << this << "\n";
  cout << "marked = " << getmark() << "\n";
  */
  cout << "\n";
  cout.flush();
}

bool destroy_progs = false;

#define destroydec(rr) \
  do { \
    Expr *r = rr;	    \
    int ref = r->data >> 9; \
    ref = ref - 1; \
    r->debugrefcnt(ref,DEC); \
    if (ref == 0) {  \
      _e = r;		  \
      goto start_destroy; \
    } \
    else \
      r->data = (ref << 9) | (r->data & 511); \
  } while(0)


void Expr::destroy(Expr *_e, bool dec_kids) {
 start_destroy:
  switch (_e->getclass()) {
  case INT_EXPR:
    delete (IntExpr *)_e;
    break;
  case SYMS_EXPR:  {
    SymSExpr *e = (SymSExpr *)_e;
    if (e->val && e->val->getop() != PROG) {
      Expr *tmp = e->val;
      delete e;
      destroydec(tmp);
    }
    else
      delete e;
    break;
  }
  case SYM_EXPR: {
    SymExpr *e = (SymExpr *)_e;
    if (e->val && e->val->getop() != PROG) {
      Expr *tmp = e->val;
      delete e;
      destroydec(tmp);
    }
    else
      delete e;
    break;
  }
  case HOLE_EXPR: {
    HoleExpr *e = (HoleExpr *)_e;
    if (e->val) {
      Expr *tmp = e->val;
      delete e;
      destroydec(tmp);
    }
    else
      delete e;
    break;
  }
  case CEXPR: {
    CExpr *e = (CExpr *)_e;
    if (dec_kids) {
      Expr **cur = e->kids;
      Expr *tmp;
      while((tmp = *cur++)) {
	if (*cur)
	  tmp->dec();
	else {
	  delete e;
	  destroydec(tmp);
	  break;
	}
      }
    }
    else
      delete e;
    break;
  }
  }
}

Expr *Expr::clone() {
  switch (getclass()) {
  case INT_EXPR:
  case RAT_EXPR:
    inc();
    return this;
  case SYMS_EXPR: 
  case SYM_EXPR: {
    SymExpr *e = (SymExpr *)this;
    if (e->val)
      if (e->val->getop() != PROG)
	return e->val->clone();
    e->inc();
    return e;
  }
  case HOLE_EXPR: {
    HoleExpr *e = (HoleExpr *)this;
    if (e->val)
      return e->val->clone();
    e->inc();
    return e;
  }
  case CEXPR: {
    CExpr *e = (CExpr *)this;
    int op = e->getop();
    switch(op) {
    case LAM: {
#ifdef DEBUG_SYM_NAMES
      SymSExpr *var = (SymSExpr *)e->kids[0];
      SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
#else
      SymExpr *var = (SymExpr *)e->kids[0];
      SymExpr *newvar = new SymExpr(*var);
#endif
      Expr *prev = var->val;
      var->val = newvar;
      Expr *bod = e->kids[1]->clone();
      var->val = prev;
      return new CExpr(LAM,newvar,bod);
    }
    case PI: {
#ifdef DEBUG_SYM_NAMES
      SymSExpr *var = (SymSExpr *)e->kids[0];
      SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
#else
      SymExpr *var = (SymExpr *)e->kids[0];
      SymExpr *newvar = new SymExpr(*var);
#endif
      Expr *tp = e->kids[1]->clone();
      Expr *prev = var->val;
      var->val = newvar;
      Expr *bod = e->kids[2]->clone();
      var->val = prev;
      Expr* ret = new CExpr(PI,newvar,tp,bod);
      if( data&256 )
         ret->data |=256;
      return ret;
    }
    default: {
      Expr **cur = e->kids;
      Expr *tmp;
      int size = 0;
      while((*cur++))
	      size++;
      Expr **kids = new Expr*[size+1];
      kids[size]=0;
      cur = e->kids;
      bool diff_kid = false;
      int i = 0;
      while((tmp = *cur++)) {
	      Expr *c = tmp->clone();
	      diff_kid |= (c != tmp);
	      kids[i++] = c;
      }
      if (diff_kid)
	      return new CExpr(op, true /* dummy */, kids);
      for (int i = 0, iend = size; i != iend; i++)
	kids[i]->dec();
      delete[] kids;
      e->inc();
      return e;
    }
    }
  }
  }
  return 0; // should never be reached
}


Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) {
#ifndef USE_FLAT_APP
  Expr *ret = hd;
  for (int i = start, iend = args.size(); i < iend; i++)
    ret = new CExpr(APP,ret,args[i]);
  return ret;
#else
  if( start>=(int)args.size() )
    return hd;
  else
  {
    CExpr *ret = new CExpr( APP );
    ret->kids = new Expr* [args.size()-start+2];
    ret->kids[0] = hd;
    for (int i = start, iend = args.size(); i < iend; i++)
        ret->kids[i-start+1] = args[i];
    ret->kids[args.size()-start+1] = NULL;
    return ret;
  }
#endif
}

Expr* Expr::make_app(Expr* e1, Expr* e2 )
{
   //std::cout << "make app from ";
   //e1->print( std::cout );
   //std::cout << " ";
   //e2->print( std::cout );
   //std::cout << std::endl;
   CExpr *ret;
   if( e1->getclass()==CEXPR ){
      int counter = 0;
      while( ((CExpr*)e1)->kids[counter] ){
         counter++;
      }
      ret = new CExpr( APP );
      ret->kids = new Expr* [counter+2];
      counter = 0;
      while( ((CExpr*)e1)->kids[counter] ){
         ret->kids[counter] = ((CExpr*)e1)->kids[counter];
         ret->kids[counter]->inc();
         counter++;
      }
      ret->kids[counter] = e2;
      ret->kids[counter+1] = NULL;
   }else{
      ret = new CExpr( APP, e1, e2 );
   }
   //ret->print( std::cout );
   //std::cout << std::endl;
   return ret;
}

int Expr::cargCount = 0;

Expr *Expr::collect_args(std::vector<Expr *> &args, bool follow_defs) {
   //cargCount++;
   //if( cargCount%1000==0)
   //std::cout << cargCount << std::endl;
#ifndef USE_FLAT_APP
  CExpr *e = (CExpr *)this;
  args.reserve(16);
  while( e->getop() == APP ) {
    args.push_back(e->kids[1]);
    e = (CExpr *)e->kids[0];
    if (follow_defs)
      e = (CExpr *)e->followDefs();
  }
  std::reverse(args.begin(),args.end());
  return e;
#else
  CExpr *e = (CExpr *)this;
  args.reserve(16);
  if( e->getop()==APP ){
      int counter = 1;
      while( e->kids[counter] ) {
         args.push_back(e->kids[counter]);
         counter++;
      }
      e = (CExpr*)e->kids[0];
  }
  if (follow_defs)
      return e->followDefs();
  else
      return e;
#endif
}

Expr *Expr::get_head(bool follow_defs) {
  CExpr *e = (CExpr *)this;
  while( e->getop() == APP ) {
    e = (CExpr *)e->kids[0];
    if (follow_defs)
      e = (CExpr *)e->followDefs();
  }
  return e;
}

Expr *Expr::get_body(int op, bool follow_defs) {
  CExpr *e = (CExpr *)this;
  while( e->getop() == op ) {
    e = (CExpr *)e->kids[2];
    if (follow_defs)
      e = (CExpr *)e->followDefs();
  }
  return e;
}

// if the return value is different from this, then it is a new reference
Expr *CExpr::whr() {
  vector<Expr *> args;
  if (get_head()->getop() == LAM) {
    CExpr *head = (CExpr *)collect_args(args, true);
    Expr *cloned_head;
    if (head->cloned()) {
      // we must clone
      head = (CExpr *)head->clone();
      cloned_head = head;
    }
    else {
      head->setcloned();
      cloned_head = 0;
    }
    int i = 0;
    int iend = args.size();

    /* we will end up incrementing the ref count for all the args,
       since each is either pointed to by a var (following a
       beta-reduction), or else just an argument in the new
       application we build below. */

    do {
      Expr *tmp = args[i++]->followDefs();
      ((SymExpr *)head->kids[0])->val = tmp;
      tmp->inc();
      head = (CExpr *)head->kids[1];
    } while(head->getop() == LAM && i < iend);
    for (; i < iend; i++)
      args[i]->inc();
    head->inc();
    if (cloned_head)
      cloned_head->dec();
    return build_app(head,args,i);
  }
  else 
    return this;
}

Expr* CExpr::convert_to_tree_app( Expr* e )
{
  if( e->getop()==APP )
  {
    std::vector< Expr* > kds;
    int counter = 1;
    while( ((CExpr*)e)->kids[counter] )
    {
      kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) );
      counter++;
    }
    Expr* app = Expr::build_app( e->get_head(), kds );
    //app->inc();
    return app;
  }
  else
  {
    return e;
  }
}

Expr* CExpr::convert_to_flat_app( Expr* e )
{
  if( e->getop()==APP )
  {
    std::vector< Expr* > args;
    Expr* hd = ((CExpr*)e)->collect_args( args );
    CExpr* nce = new CExpr( APP );
    nce->kids = new Expr *[(int)args.size()+2];
    nce->kids[0] = hd;
    for( int a=0; a<(int)args.size(); a++ )
    {
      nce->kids[a+1] = convert_to_flat_app( args[a] );
    }
    nce->kids[(int)args.size()+1] = 0;
    nce->inc();
    return nce;
  }
  else
  {
    return e;
  }
}

bool Expr::defeq(Expr *e) {

  /* we handle a few special cases up front, where this Expr might
     equal e, even though they have different opclass (i.e., different
     structure). */

  if (this == e)
    return true;
  int op1 = getop();
  int op2 = e->getop();
  switch (op1) {
  case ASCRIBE:
    return ((CExpr *)this)->kids[0]->defeq(e);
  case APP: {
    Expr *tmp = ((CExpr *)this)->whr();
    if (tmp != this) {
      bool b = tmp->defeq(e);
      tmp->dec();
      return b;
    }
    if (get_head()->getclass() == HOLE_EXPR) {
      vector<Expr *> args;
      Expr *head = collect_args(args, true);
      Expr *t = e;
      t->inc();
      for (int i = 0, iend = args.size(); i < iend; i++) {
	      // don't worry about SYMS_EXPR's, since we should not be in code here.
	      if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark())
	        /* we cannot fill the hole in this case.  Either this is not
	          a variable or we are using a variable again. */
	        return false;
	      SymExpr *v = (SymExpr *)args[i];

	      // we may have been mapping from expected var v to a computed var
	      Expr *tmp = (v->val ? v->val : v);

	      tmp->inc();
	      t = new CExpr(LAM, tmp, t);
	      args[i]->setexmark();
      }
      for (int i = 0, iend = args.size(); i < iend; i++) 
	      args[i]->clearexmark();
#ifdef DEBUG_HOLES
      cout << "Filling hole ";
      head->debug();
      cout << "with ";
      t->debug();
#endif
      ((HoleExpr *)head)->val = t;
      return true;
    }
    break;
  }
  case NOT_CEXPR:
    switch (getclass()) {
    case HOLE_EXPR: {
      HoleExpr *h = (HoleExpr *)this;
      if (h->val)
	      return h->val->defeq(e);
#ifdef DEBUG_HOLES
      cout << "Filling hole ";
      h->debug();
      cout << "with ";
      e->debug();
#endif
#ifdef USE_HOLE_PATH_COMPRESSION
      Expr *tmp = e->followDefs();
#else
      Expr *tmp = e;
#endif
      h->val = tmp;
      tmp->inc();
      return true;
    }
    case SYMS_EXPR: 
    case SYM_EXPR: {
      SymExpr *s = (SymExpr *)this;
      if (s->val)
	return s->val->defeq(e);
      break;
    }
    }
    break;
  }
  
  switch (op2) {
  case ASCRIBE:
    return defeq(((CExpr *)e)->kids[0]);
  case APP: {
    Expr *tmp = ((CExpr *)e)->whr();
    if (tmp != e) {
      bool b = defeq(tmp);
      tmp->dec();
      return b;
    }
    break;
  }
  case NOT_CEXPR:
    switch (e->getclass()) {
    case HOLE_EXPR: {
      HoleExpr *h = (HoleExpr *)e;
      if (h->val)
	return defeq(h->val);

#ifdef DEBUG_HOLES
      cout << "Filling hole ";
      h->debug();
      cout << "with ";
      debug();
#endif
#ifdef USE_HOLE_PATH_COMPRESSION
      Expr *tmp = followDefs();
#else
      Expr *tmp = this;
#endif
      h->val = tmp;
      tmp->inc();
      return true;
    }
    case SYMS_EXPR: 
    case SYM_EXPR: {
      SymExpr *s = (SymExpr *)e;
      if (s->val)
	return defeq(s->val);
      break;
    }
    }
    break;
  }

  /* at this point, e1 and e2 must have the same opclass if they are 
     to be equal. */

  if (op1 != op2)
    return false;
  
  if (op1 == NOT_CEXPR) {
    switch(getclass()) {
    case INT_EXPR: {
      IntExpr *i1 = (IntExpr *)this;
      IntExpr *i2 = (IntExpr *)e;
      return (mpz_cmp(i1->n,i2->n) == 0);
    }
    case RAT_EXPR: {
      RatExpr *r1 = (RatExpr *)this;
      RatExpr *r2 = (RatExpr *)e;
      return (mpq_cmp(r1->n,r2->n) == 0);
    }
    case SYMS_EXPR: 
    case SYM_EXPR: 
      return (this == e);
    }
  }

  /* Now op1 and op2 must both be CExprs, and must have the same op to be
     equal. */

  CExpr *e1 = (CExpr *)this;
  CExpr *e2 = (CExpr *)e;

  int last = 1;
  switch (op1) {
  case PI:
    if (!e1->kids[1]->defeq(e2->kids[1]))
      return false;
    last++;
    // fall through to LAM case
  case LAM: {

    /* It is critical that we point e1's var. (v1) back to e2's (call
       it v2).  The reason this is critical is that we assume any
       holes are in e1.  So we could end up with (_ v1) = t. We wish
       to fill _ in this case with (\ v2 t).  If v2 pointed to v1, we
       could not return (\ v1 t), because the fact that v2 points to
       v1 would then be lost.
    */
    SymExpr *v1 = (SymExpr *)e1->kids[0];
    Expr *prev_v1_val = v1->val;
    v1->val = e2->kids[0]->followDefs();
    bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]);
    v1->val = prev_v1_val;
    return bodies_equal;
  }
  case APP: 
#ifndef USE_FLAT_APP
    return (e1->kids[0]->defeq(e2->kids[0]) &&
	    e1->kids[1]->defeq(e2->kids[1]));
#else
    {
      int counter = 0;
      while( e1->kids[counter] ){
         if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) )
            return false;
         counter++;
      }
      return e2->kids[counter]==NULL;
    }
#endif
  case TYPE:
  case KIND:
  case MPZ:
    // already checked that both exprs have the same opclass.
    return true;
  } // switch(op1)
  
  return false; // never reached.
}

int Expr::fiCounter = 0;

bool Expr::free_in(Expr *x) {
   //fiCounter++;
   //if( fiCounter%1==0 )
   //   std::cout << fiCounter << std::endl;
   switch(getop()) {
   case NOT_CEXPR:
      switch (getclass()) {
      case HOLE_EXPR: {
         HoleExpr *h = (HoleExpr *)this;
         if (h->val)
	         return h->val->free_in(x);
         return (h == x);
      }
      case SYMS_EXPR: 
      case SYM_EXPR: {
         SymExpr *s = (SymExpr *)this;
         if (s->val && s->val->getclass() == HOLE_EXPR)
	   /* we do not need to follow the "val" pointer except in this
	      one case, when x is a hole (which we do not bother to check
	      here) */
	         return s->val->free_in(x);
         return (s == x);
      }
      case INT_EXPR:
         return false;
      }
      break;
   case LAM:
   case PI:
      if (x == ((CExpr *)this)->kids[0])
         return false;
      // fall through
   default: {
      // must be a CExpr
      CExpr *e = (CExpr *)this;
      Expr *tmp;
      Expr **cur = e->kids;
      while ((tmp = *cur++))
         if (tmp->free_in(x))
	         return true;
      return false;
   }
   }
   return false; // should not be reached
}

void Expr::calc_free_in(){
   data &= ~256;
   data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] );
}

string Expr::toString() {
  ostringstream oss;
  print(oss);
  return oss.str();
}

static void print_kids(ostream &os, Expr **kids) {
  Expr *tmp;
  while ((tmp = *kids++)) {
    os << " ";
    tmp->print(os);
  }
}

static void print_vector(ostream &os, const vector<Expr *> &v) {
  for(int i = 0, iend = v.size(); i < iend; i++) {
    os << " ";
    v[i]->print(os);
  }
}

void Expr::print(ostream &os) {
  CExpr *e = (CExpr *)this; // for CEXPR cases

  //std::cout << e->getop() << " ";
  /*
#ifdef DEBUG_REFCNT
  os << "<";
  char tmp[10];
  sprintf(tmp,"%d",getrefcnt());
  os << tmp << "> ";
#endif
*/

  switch(getop()) {
  case NOT_CEXPR: {
    switch(getclass()) {
    case INT_EXPR: 
    {
      IntExpr *e = (IntExpr *)this;
      if (mpz_sgn(e->n) < 0) {
	      os << "(~ ";
	      mpz_t tmp;
	      mpz_init(tmp);
	      mpz_neg(tmp,e->n);
	      char *s = mpz_get_str(0,10,tmp);
	      os << s;
	      free(s);
	      mpz_clear(tmp);
	      os << ")";
        //os << "mpz";
      }
      else {
	      char *s = mpz_get_str(0,10,e->n);
	      os << s;
	      free(s);
        //os << "mpz";
      }
      break;
    }
    case RAT_EXPR: 
    {
      RatExpr *e = (RatExpr *)this;
      char *s = mpq_get_str(0,10,e->n);
      os << s;
      if (mpq_sgn(e->n) < 0) {
	      os << "(~ ";
	      mpq_t tmp;
	      mpq_init(tmp);
	      mpq_neg(tmp,e->n);
	      char *s = mpq_get_str(0,10,tmp);
	      os << s;
	      free(s);
	      mpq_clear(tmp);
	      os << ")";
      }
      else {
	      char *s = mpq_get_str(0,10,e->n);
	      os << s;
	      free(s);
      }
      break;
    }
#ifndef DEBUG_SYM_NAMES
    case SYM_EXPR: 
    {
      SymExpr *e = (SymExpr *)this;
      if (e->val) {
	      if (e->val->getop() == PROG) {
	        os << e;
#ifdef DEBUG_SYMS
	        os << "[PROG]";
#endif
	      }else{
#ifdef DEBUG_SYMS
	        os << e;
	        os << "[SYM ";
#endif
	        e->val->print(os);
#ifdef DEBUG_SYMS
	        os << "]";
#endif
        }
      }
      else
	      os << e;
      break;
    }
#else
    case SYM_EXPR: /* if we are debugging sym names, then
		      SYM_EXPRs are really SymSExprs. */
#endif
    case SYMS_EXPR: {
      SymSExpr *e = (SymSExpr *)this;
      if (e->val) {
	      if (e->val->getop() == PROG) {
	        os << e->s;
#ifdef DEBUG_SYMS
	        os << "[PROG]";
#endif
	      }else{
#ifdef DEBUG_SYMS
	        os << e->s;
	        os << "[SYM ";
#endif
	        e->val->print(os);
#ifdef DEBUG_SYMS
	        os << "]";
#endif
	      }
      }
      else
	      os << e->s;
      break;
    }
    case HOLE_EXPR: 
    {
      HoleExpr *e = (HoleExpr *)this;
      if (e->val) {
#ifdef DEBUG_SYMS
	      os << "_" << "[HOLE ";
#endif
	      e->val->print(os);
#ifdef DEBUG_SYMS
	      os << "]";
#endif
      }else {
	      os << "_";
#ifdef DEBUG_HOLE_NAMES
	      char tmp[100];
	      sprintf(tmp,"%d",e->id);
	      os << "[ " << tmp << "]";
#else
	      os << "[ " << e << "]";
#endif
      }
      break;
    }
    default:
      os << "; unrecognized form of expr";
      break;
    }
    break;
  } // case NOT_CEXPR
  case APP: {
    os << "(";
    vector<Expr *> args;
    Expr *head = collect_args(args, false /* follow_defs */);
    head->print(os);
    print_vector(os, args);
    os << ")";
    break;
  }
  case LAM: 
    os << "(\\";
    print_kids(os, e->kids);
    os << ")";
    break;
  case PI: 
    os << "(!";
    print_kids(os, e->kids);
    os << ")";
    break;
  case TYPE: 
    os << "type";
    break;
  case KIND: 
    os << "kind";
    break;
  case MPZ: 
    os << "mpz";
    break;
  case MPQ:
    os << "mpq";
    break;
  case ADD: 
    os << "(mp_add";  
    print_kids(os,e->kids);
    os << ")";
    break;
  case MUL:
    os << "(mp_mul";  
    print_kids(os,e->kids);
    os << ")";
    break;
  case DIV:
    os << "(mp_div";  
    print_kids(os,e->kids);
    os << ")";
    break;
  case NEG: 
    os << "(mp_neg";
    print_kids(os,e->kids);
    os << ")";
    break;
  case IFNEG:
    os << "(ifneg";
    print_kids(os,e->kids);
    os << ")";
    break;
  case IFZERO:
    os << "(ifzero";
    print_kids(os,e->kids);
    os << ")";
    break;
  case RUN: 
    os << "(run";
    print_kids(os,e->kids);
    os << ")";
    break;
  case PROG: 
    os << "(prog";
    print_kids(os,e->kids);
    os << ")";
    break;
  case PROGVARS: 
    os << "(";
    print_kids(os,e->kids);
    os << ")";
    break;
  case MATCH: 
    os << "(match";
    print_kids(os,e->kids);
    os << ")";
    break;
  case CASE: 
    os << "(";
    print_kids(os,e->kids);
    os << ")";
    break;
  case LET: 
    os << "(let";
    print_kids(os,e->kids);
    os << ")";
    break;
  case DO: 
    os << "(do";
    print_kids(os,e->kids);
    os << ")";
    break;
  case IFMARKED: 
    os << "(ifmarked";
    print_kids(os,e->kids);
    os << ")";
    break;
  case COMPARE:
    os << "(compare";
    print_kids(os,e->kids);
    os << ")";
    break;
  case MARKVAR: 
    os << "(markvar";
    print_kids(os,e->kids);
    os << ")";
    break;
  case FAIL: 
    os << "(fail ";
    print_kids(os, e->kids);
    os << ")";
    break;
  case ASCRIBE: 
    os << "(:";
    print_kids(os, e->kids);
    os << ")";
    break;
  default:
    os << "; unrecognized form of expr(2) " << getop() << " " << getclass();
  } // switch(getop())
}

bool Expr::isType( Expr* statType ){
  Expr* typ = this;
  while( typ!=statType ){
    if( typ->getop()==PI ){
      typ = ((CExpr*)typ)->kids[2];
    }else{
      return false;
    }
  }
  return true;
}

int SymExpr::symmCount = 0;
#ifdef MARKVAR_32
int SymExpr::mark()
{
  if( mark_map.find( this )== mark_map.end() )
  {
    symmCount++;
    mark_map[this] = 0;
  }
  return mark_map[this];
}
void SymExpr::smark( int m )
{
  mark_map[this] = m;
}
#endif