///////////////////////////////////////////////////////////////////////////////
//                                                                           //
//  Copyright (C) 1995-2002 by the Board of Trustees of Leland Stanford      //
//  Junior University.  See LICENSE for details.                             //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////


#include <flags.h>
#include <arraylist.h>
#include "store.h"


///////////////////////////////////////////////////////////////////////////////
// Initialize statics and constants                                          //
///////////////////////////////////////////////////////////////////////////////


const Symbol Read_Expr::READ_SYM = "read";
int Read_Expr::READ_SORT;

const Symbol Write_Expr::WRITE_SYM = "write";
int Write_Expr::WRITE_SORT;


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: init_store_library						     //
// Description: Initialize store library                                     //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void init_store_library()
{
  cerr << "initializing libstore..." << endl;
  Read_Expr::Init();
  Write_Expr::Init();
}


///////////////////////////////////////////////////////////////////////////////
// Read_Expr class methods                                                   //
///////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::TypeCheck					     //
// Description: Typecheck a Read_Expr                                        //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
Bool Read_Expr::TypeCheck()
{
  if (!_store->UnifyType(Constructed_Type::NewArrayType(_addr->Type(),Type())))
    return FALSE;

  ASSERT_MSG(_store->Type()->TypeConstructor() == TC_ARRAY,
	     ("Illegal type in Read_Expr::TypeCheck"));

  if (!UnifyType(PConstructed_Type(_store->Type())->GetArrayType()))
    return FALSE;
  if (!_addr->UnifyType(PConstructed_Type(_store->Type())->GetArrayIndexType()))
    return FALSE;

  if (Type()->IsComplete())
    SetFlag(TYPECHECKED);
  return TRUE;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::Print1						     //
// Description: Print a Read_Expr                                            //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void Read_Expr::Print1(ostream& os) const
{
  FLAGS::indentcount++;
  os << '\n' << indent
     << '$' << ExprNum() << ':' << StartInterp << READ_SYM << ' ';
  Print1Ptr(os,_store);
  os << ' ';
  Print1Ptr(os,_addr);
  os << FinishInterp;
  FLAGS::indentcount--;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::IsSimplerThan1					     //
// Description: Compare two Read_Expr's                                      //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
Bool Read_Expr::IsSimplerThan1(PExpr e)
{
  const PRead_Expr &pread = PRead_Expr(e);
  if (_store == pread->_store) {
    return _addr->IsSimplerThan(pread->_addr);
  }
  return _store->IsSimplerThan(pread->_store);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::Hash1						     //
// Description: Hash function for Read_Expr's                                //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
int Read_Expr::Hash1() const
{
  return abs(int(_store) * 17 + int(_addr));
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::Match1						     //
// Description: Match function for Read_Expr's                               //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
int Read_Expr::Match1(PCExpr pexpr) const
{
  const PRead_Expr &pread = PRead_Expr(pexpr);
  return (_store == pread->_store && _addr == pread->_addr);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::NewSig						     //
// Description: Create a new Read_Expr                                       //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Read_Expr::NewSig(PExpr store, PExpr addr, PExpr sigx)
{
  if (store->Sort() == Write_Expr::WRITE_SORT) {
    const PWrite_Expr &w = PWrite_Expr(store);
    
    PExpr e = New(w->store(), addr);
    PExpr pexpr;
    for (int i=0; i<w->numUpdates(); i++) {
      pexpr = Eq_Expr::New(w->addr(i), addr);
      e = ITE_Expr::New(pexpr, w->value(i), e);
    }
    return e;
  }

  // STUFF BELOW HERE IS OPTIONAL @JL

  if (FLAGS::ReadITELift_store_switch && store->Sort() == ITE_SORT) {
    const PITE_Expr &pite = PITE_Expr(store);
    return ITE_Expr::NewSig(pite->ifpart(),
			    New(pite->thenpart(),addr),
			    New(pite->elsepart(),addr), sigx);
  }

  if (FLAGS::ReadITELift_addr_switch && addr->Sort() == ITE_SORT) {
    const PITE_Expr &pite = PITE_Expr(addr);
    return ITE_Expr::NewSig(pite->ifpart(),
			    New(store,pite->thenpart()),
			    New(store,pite->elsepart()), sigx);
  }

  Read_Expr expr(store, addr);
  return NewExpr(&expr, sigx);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Read_Expr::Parse						     //
// Description: Parse a Read_Expr                                            //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Read_Expr::Parse(Symbol, int numargs, PExpr *args)
{
  if (numargs!=2) goto wrong_number_of_args;

  return New(args[0], args[1]);

 wrong_number_of_args:
  cout << "bad number of args for Read_Expr" << endl;
  return NULL;
}


///////////////////////////////////////////////////////////////////////////////
// End of Read_Expr class methods                                            //
///////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////
// Write_Expr class methods                                                  //
///////////////////////////////////////////////////////////////////////////////


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Write_Expr					     //
// Description: Write_Expr constructor                                       //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
Write_Expr::Write_Expr(PExpr store, const Array_List<Update_Type> &updates)
  : Gen_Expr(WRITE_SORT), _store(store), _updates(updates)
{
  SetFlag(INTERP);
  SetFlag(SOLVABLE);
}   


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::PopLastUpdate					     //
// Description: Remove the last update from the current expression and       //
// return a new Write_Expr containing it.                                    //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Write_Expr::PopLastUpdate()
{
  ASSERT_MSG(IsAtomic(), ("assumption violated"));
  int n = numUpdates() - 1;

  if (n==0)
    return _store;

  Array_List<Update_Type> updates = _updates;
  updates.Delete(n);

  Write_Expr expr(_store, updates);
  return NewExpr(&expr, NULL);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::TypeCheck					     //
// Description: Typecheck a Write_Expr                                       //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
Bool Write_Expr::TypeCheck()
{
  if (!UnifyType(Constructed_Type::NewArrayType(addr(0)->Type(),
						value(0)->Type())) ||
      !_store->UnifyType(Type()) ||
      !UnifyType(_store->Type()))
    return FALSE;

  ASSERT_MSG(Type()->TypeConstructor() == TC_ARRAY,
	     ("Illegal type in Write_Expr::TypeCheck"));

  int i;
  for (i=1; i<numUpdates(); i++) {
    if (!UnifyType(Constructed_Type::NewArrayType(addr(i)->Type(),
						  value(i)->Type())))
      return FALSE;
  }

  for (i=0; i<numUpdates(); i++) {
    if (!addr(i)->UnifyType(PConstructed_Type(Type())->GetArrayIndexType()) ||
	!value(i)->UnifyType(PConstructed_Type(Type())->GetArrayType()))
	
      return FALSE;
  }

  if (Type()->IsComplete())
    SetFlag(TYPECHECKED);
  return TRUE;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Print1						     //
// Description: Print a Write_Expr                                           //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void Write_Expr::Print1(ostream& os) const
{
  int i;
  FLAGS::indentcount++;

  os << '\n' << indent
     << '$' << ExprNum() << ':' << StartInterp << WRITE_SYM << ' ';
  Print1Ptr(os,_store); os << ' ';

  for (i=0; i<numUpdates(); i++) {
    Print1Ptr(os,_updates[i]._addr);  os << ' ';
    Print1Ptr(os,_updates[i]._value); os << ' ';  
  }

  os << FinishInterp << '\n';
  FLAGS::indentcount--;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Hash1						     //
// Description: Hash function for Write_Expr's                               //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
int Write_Expr::Hash1() const
{
  int h = 43*int(store());
  for (int i=0; i<numUpdates(); i++)
    h += 17*int(addr(i)) + 31*int(value(i)) + int(imp(i));
  return abs(h);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Match1						     //
// Description: Match function for Write_Expr's                              //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
int Write_Expr::Match1(PCExpr pexpr) const
{
  const PWrite_Expr &pwrite = PWrite_Expr(pexpr);
  if (_store != pwrite->_store || numUpdates()!=pwrite->numUpdates())
    return FALSE;

  for (int i=0; i<numUpdates(); i++) {
    if (_updates[i]._addr!=pwrite->_updates[i]._addr
	|| _updates[i]._value!=pwrite->_updates[i]._value
	|| _updates[i]._imp!=pwrite->_updates[i]._imp)
      return FALSE;
  }

  return TRUE;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Solve						     //
// Description: Solve an equation in which a Write_Expr appears on the lhs   //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void Write_Expr::Solve(PExpr e2, PExpr &lhs, PExpr &rhs)
{
  ASSERT_MSG(IsAtomic() && e2->IsAtomic(), ("arguments must be atomic!"));

  PExpr e1 = this;
  PExpr s1 = PWrite_Expr(e1)->store();
  PExpr s2 = (e2->Sort()==WRITE_SORT) ? PWrite_Expr(e2)->store() : e2;
  PExpr tmp1,tmp2;

  if (s1==s2) {
    rhs = TrueVal();

    int n1 = PWrite_Expr(e1)->numUpdates();
    int n2 = (e2->Sort()==WRITE_SORT) ? PWrite_Expr(e2)->numUpdates() : 0;

    /* the last term is needed to deal with the rare situation   @JL */
    /* where i1 is a renamed version of i2 -- although the       @JL */
    /* goal should already be predicated with i1=i2, we must     @JL */
    /* state this again to avoid causing an assertion failure    @JL */
    /* in NewEqExpr()                                            @JL */

    // write(S,a,v) = write(S,a',v') ==>
    // ( ite  a=a'  v=v'  v=read(S,a) ) && ( a'!=a => v'=read(S,a') )
    // && ( a=a' ==> i=i' )

    lhs = TrueVal();
    for (int i=0; i<n1; i++) {
      Update_Type &u1 = PWrite_Expr(e1)->_updates[i];
      PExpr e = Eq_Expr::TryNew(u1._value, u1._imp);
      if (e == NULL) goto abort;
      for (int j=0; j<n2; j++) {
	Update_Type &u2 = PWrite_Expr(e2)->_updates[j];
	tmp1 = Eq_Expr::TryNew(u1._addr, u2._addr);
	tmp2 = Eq_Expr::TryNew(u1._value, u2._value);
	if (tmp1 == NULL || tmp2 == NULL) goto abort;
	e = ITE_Expr::New(tmp1, tmp2, e);
      }
      lhs = ITE_Expr::New(lhs, e, FalseVal());
    }

    for (int j=0; j<n2; j++) {
      Update_Type &u2 = PWrite_Expr(e2)->_updates[j];
      PExpr e = Eq_Expr::TryNew(u2._value, u2._imp);
      if (e == NULL) goto abort;
      for (int i=0; i<n1; i++) {
	Update_Type &u1 = PWrite_Expr(e1)->_updates[i];
	tmp1 = Eq_Expr::TryNew(u2._addr, u1._addr);
	tmp2 = Eq_Expr::TryNew(u2._imp, u1._imp);
	if (tmp1 == NULL || tmp2 == NULL) goto abort;
	e = ITE_Expr::New(tmp1, tmp2, e);
      }
      lhs = ITE_Expr::New(lhs, e, FalseVal());
    }
  }

  else {
    // swap ``s1'' and ``s2'' so that ``s2'' is simpler than ``s1''

    Bool swap = s1->IsSimplerThan(s2);
    PExpr tmp = e1;  e1 = (swap) ? e2 : e1;  e2 = (swap) ? tmp : e2;
    tmp = s1;  s1 = (swap) ? s2 : s1;  s2 = (swap) ? tmp : s2;
    Bool renamed = FALSE;

    // ensure that ``e2'' will be simpler than ``s1''

    if (s1->IsSimplerThan(e2)) {
      ASSERT_MSG(e2->Sort()==WRITE_SORT, ("assumption violated"));
      PWrite_Expr w = PWrite_Expr(e2);

      for (int i=0; i<w->numUpdates(); i++) {
	if (s1->IsSimplerThan(w->addr(i))) {
	  Expr::MakeSimplerThan(w->addr(i), s1);
	  renamed = TRUE;
	}

	if (s1->IsSimplerThan(w->value(i))) {
	  Expr::MakeSimplerThan(w->value(i), s1);
	  renamed = TRUE;
	}

	if (s1->IsSimplerThan(w->imp(i))) {
	  Expr::MakeSimplerThan(w->imp(i), s1);
	  renamed = TRUE;
	}
      }
      ASSERT_MSG(renamed, ("Unable to make expression simpler"));
      goto abort;
    }

    if (e1->Sort()==WRITE_SORT) {
      PWrite_Expr w = PWrite_Expr(e1);
      int n = w->numUpdates() - 1;

      // ensure that ``a'' and ``read(S,a)'' will
      // be simpler than ``S''

      /* can't we sometimes not rename anything if imp is non-atomic? @JL */
      /* don't we have to rename everything, maybe? @JL */

      if (s1->IsSimplerThan(w->addr(n))) {
	Expr::MakeSimplerThan(w->addr(n), s1);
	renamed = TRUE;
      }

      if (s1->IsSimplerThan(w->imp(n))) {
	Expr::MakeSimplerThan(w->imp(n), s1);
	renamed = TRUE;
      }
      if (renamed) goto abort;

      // write(S,a,v) = S' ==>
      // S = write(S',a,read(S,a)) && v = read(S',a)

      // where read(S',a) = r, S' = e2, v = e1->value(),
      //       a = e1->addr(), and S = e1->store()

      PExpr imp = Read_Expr::New(e2, w->addr(n));
      if (imp->IsAtomic() && w->store()->IsSimplerThan(imp)) {
	imp = Expr::MakeSimplerThan(imp, w->store());
      }
      Array_List<Update_Type> update(Update_Type(w->addr(n), w->imp(n), imp));
      tmp1 = Eq_Expr::TryNew(w->value(n), imp);
      tmp2 = Eq_Expr::TryNew(w->PopLastUpdate(), Write_Expr::New(e2, update));
      if (tmp1 == NULL || tmp2 == NULL) goto abort;
      lhs = ITE_Expr::New(tmp1, tmp2, FalseVal());
      rhs = TrueVal();
    }

    else {
      ASSERT_MSG(e1==s1, ("internal error -- unexpected situation"));

      lhs = s1->Simp();
      rhs = e2->Simp();

      // it's weird, but e2 could have been renamed something
      // more complex than s1 requiring us to reverse lhs & rhs

      if (rhs->IsRenamed() && lhs->IsSimplerThan(rhs)) {
	PExpr tmp = lhs;
	lhs = rhs;
	rhs = tmp;
      }
    }
  }
  return;
abort:
  lhs = rhs = NULL;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::ForAllChildren					     //
// Description: Execute a function on all children of a Write_Expr           //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
void Write_Expr::ForAllChildren(void (Expr::*f)())
{
  (_store->*f)();
  for (int i=0; i<_updates.NumItems(); i++) {
    (_updates[i]._addr->*f)();
    (_updates[i]._value->*f)();
    (_updates[i]._imp->*f)();
  }
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::ReplaceChildren				     //
// Description: Transform all children and then rebuild the Write_Expr       //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Write_Expr::ReplaceChildren(PExpr (Expr::*f)())
{ 
  Array_List<Update_Type> updates(_updates);

  for (int i=0; i<updates.NumItems(); i++) {
    updates[i]._addr = (updates[i]._addr->*f)();
    updates[i]._value = (updates[i]._value->*f)();
    updates[i]._imp = (updates[i]._imp->*f)();
  }

  return Write_Expr::NewSig((_store->*f)(), updates, this);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::NewSig						     //
// Description: Create a new Write_Expr                                      //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Write_Expr::NewSig(PExpr store,
			 Array_List<Write_Expr::Update_Type> updates,
			 PExpr sigx)
{
  ASSERT_MSG(store->Sort() == WRITE_SORT || !store->IsSolvable(),
	     ("Unexpected solvable expression of type store"));
  Bool is_all_atomic = store->IsAtomic();

  // throw out updates that don't change the value already in
  // the store (ie. write(S, a, Read(S,a)) ==> S) and determine 
  // if the terms are all atomic

  ASSERT_MSG(store->Simp() == store, ("subexprs should be simplest"));
  for (int i=updates.NumItems()-1; 0<=i; i--) {
    if (updates[i]._value != updates[i]._imp) {
      is_all_atomic = is_all_atomic 
	&& updates[i]._addr->IsAtomic()
	&& updates[i]._value->IsAtomic()
     	&& updates[i]._imp->IsAtomic();
      ASSERT_MSG(updates[i]._addr->Simp() == updates[i]._addr &&
		 updates[i]._value->Simp() == updates[i]._value &&
		 updates[i]._imp->Simp() == updates[i]._imp,
		 ("subexprs should be simplest"));
    }
    else
      updates.Delete(i);
  }

  // are there any updates?

  if (updates.NumItems()==0)
    return store;

  // if the arguments are all atomic, then we have a lot
  // of work to do to generate a canonical Write_Expr

  if (is_all_atomic) {
    Array_List<Write_Expr::Update_Type> newUpdates = 
      (store->Sort()==WRITE_SORT) ? 
      PWrite_Expr(store)->_updates : Array_List<Write_Expr::Update_Type>();

    // go through the updates one update at a time

    for (int i=0; i<updates.NumItems(); i++) {
      PExpr &addr = updates[i]._addr;
      PExpr &value = updates[i]._value;
      PExpr &imp = updates[i]._imp;

      Array_List<PExpr> eq_stack;
      Bool is_distinct_addr = TRUE;
      Bool is_equiv_addr = FALSE;
      Bool is_still_all_atomic = TRUE;

      // figure out if "addr" is distinct, or if it is equivalent
      // to an addr already being updated

      for (int j=0; j<newUpdates.NumItems(); j++) {
	PExpr eq = Eq_Expr::New(newUpdates[j]._addr, addr);
	is_distinct_addr = is_distinct_addr && eq==FalseVal();
	is_equiv_addr = is_equiv_addr || eq==TrueVal();
	is_still_all_atomic = is_still_all_atomic && eq->IsDistinct();
	eq_stack.Append(eq);
      }

      if (is_still_all_atomic) {
	if (is_distinct_addr){

	  // insert the update at the appropriate position

	  Bool inserted_update = FALSE;

	  for (int j=0; j<newUpdates.NumItems(); j++) {
	    if (addr->IsSimplerThan(newUpdates[j]._addr)) {
	      newUpdates.Insert(j, Write_Expr::Update_Type(addr, value, imp));
	      inserted_update = TRUE;
	      break;
	    }
	  }

	  if (!inserted_update)
	    newUpdates.Append(Write_Expr::Update_Type(addr, value, imp));
	}

	else {
	  ASSERT_MSG(is_equiv_addr, ("internal error -- unexpected state"));

	  // if the update undoes an earlier update, then
	  // just remove it;  otherwise, replace it
	  // eg.  write(write(write(S,a,v),a',v'),a,read(S,a))

	  for (int j=0; j<newUpdates.NumItems(); j++) {
	    if (eq_stack[j]==TrueVal()) {
	      if (newUpdates[j]._imp==value) newUpdates.Delete(j);
	      else newUpdates[j]._value = value;
	      break;
	    }
	  }
	}
      }

      else {

	// here we have to be conservative, since we don't know
	// whether or not the addr for this update is distinct
	// from the addrs for all the other updates

	for (int j=0; j<newUpdates.NumItems(); j++) {
	  if (!eq_stack[j]->IsDistinct()) {
	    PExpr newAddr
	      = ITE_Expr::New(eq_stack[j], addr, newUpdates[j]._addr);
	    PExpr newValue
	      = ITE_Expr::New(eq_stack[j], value, newUpdates[j]._value);
	    newUpdates[j]._addr = newAddr;
	    newUpdates[j]._value = newValue;

	    // newAddr must be non-atomic to guarentee that the store
	    // expr is non-atomic, since it may be in canoncial form

	    ASSERT_MSG(!newAddr->IsAtomic(), ("addr must be NON-atomic"));
	    break;
	  }
	}

	for (; i<updates.NumItems(); i++)
	  newUpdates.Append(updates[i]);
	
	break;
      }
    }
    
    PExpr newStore = (store->Sort()==WRITE_SORT) ? 
      PWrite_Expr(store)->store() : store;
  
    if (newUpdates.NumItems()==0)
      return newStore->Simp();

    Write_Expr expr(newStore, newUpdates);
    PExpr e = NewExpr(&expr, sigx);

    
#ifdef DEGUG

    if (e->IsAtomic() && e->Sort()==WRITE_SORT) {
      PWrite_Expr w = PWrite_Expr(e);
      int i;

      // check that all the addrs that are updated
      // are all distinct

      for (i=0; i<w->numUpdates(); i++) {
	for (int j=i+1; j<w->numUpdates(); j++) {
	  ASSERT_MSG(Eq_Expr::New(w->addr(i), w->addr(j)) == FalseVal(),
		     ("addr are not all distinct!"));
	}
      }

      // check that the updates are properly ordered

      for (i=1; i<w->numUpdates(); i++) {
	ASSERT_MSG((w->addr(i-1))->IsSimplerThan(w->addr(i)),
		   ("updates are not ordered correctly"));
      }

      // check that there are no redundent updates

      for (i=0; i<w->numUpdates(); i++) {
	ASSERT_MSG(Eq_Expr::New(w->value(i),w->imp(i))!=TrueVal(),
		   ("redundent update"));
      }
    }

    // make sure e is still a simplest!

    ASSERT(e == e->Simp());

#endif /* DEBUG */

    
    return e;

  }

  // add in updates from the store

  if (store->Sort()==WRITE_SORT) {
    Array_List<Write_Expr::Update_Type> tmp = updates;
    updates = PWrite_Expr(store)->_updates;
    updates.Append(tmp);
    store = PWrite_Expr(store)->store();
  }

  Write_Expr expr(store, updates);
  return NewExpr(&expr, sigx);
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: Write_Expr::Parse						     //
// Description: Parse a Write_Expr                                           //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
PExpr Write_Expr::Parse(Symbol, int numargs, PExpr *args)
{
  if (numargs%2 != 1) goto wrong_number_of_args;

  {
    PExpr pwrite = args[0];

    for (int i=1; i<numargs; i+=2) {
      PExpr imp = Read_Expr::New(pwrite, args[i])->Simp();
      Write_Expr::Update_Type update(args[i], args[i+1], imp);
      Array_List<Write_Expr::Update_Type> updates(update);
      pwrite = Write_Expr::New(pwrite, updates);
    }

    return pwrite;
  }

 wrong_number_of_args:
  cout << "bad number of args for Write_Expr" << endl;
  return NULL;
}


///////////////////////////////////////////////////////////////////////////////
// End of Write_Expr class methods                                           //
///////////////////////////////////////////////////////////////////////////////


// TODO: register this function
PExpr rewrite_stores(PExpr i, PExpr t, PExpr e)
{
  // these rewrite rules have been shown to be very effective 
  // on the dlx and pp examples -- almost doubling performance

  if (i->Sort() == EQ_SORT
      && e->Sort() == Write_Expr::WRITE_SORT
      && t == PWrite_Expr(e)->store()
      && PWrite_Expr(e)->numUpdates()==1) {

    const PWrite_Expr &pwrite = PWrite_Expr(e);
    const PEq_Expr &peq = PEq_Expr(i);

    if (peq->right()==pwrite->addr(0)) {
      Write_Expr::Update_Type update(peq->left(),
				     Read_Expr::New(t, peq->left()),
				     Read_Expr::New(pwrite, peq->left()));
      Array_List<Write_Expr::Update_Type> updates(update);
      return Write_Expr::New(pwrite, updates)->Simp();
    }

    if (peq->left()==pwrite->addr(0)) {
      Write_Expr::Update_Type update(peq->right(),
				     Read_Expr::New(t, peq->right()),
				     Read_Expr::New(pwrite, peq->right()));
      Array_List<Write_Expr::Update_Type> updates(update);
      return Write_Expr::New(pwrite, updates)->Simp();
    }
  }

  return NULL;
}