// Buffer remove operator class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "BufferRemove.h"
#include "BufferType.h"
#include "BufferValue.h"
#include "Net.h"
#include "CardType.h"
#include "LeafValue.h"
#include "Printer.h"

/** @file BufferRemove.C
 * Operation for removing queue or stack items
 */

/* Copyright  1999-2002 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA is free software; you can redistribute it and/or modify it
   under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   MARIA is distributed in the hope that it will be useful, but
   WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   General Public License for more details.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

BufferRemove::BufferRemove (class Expression& buffer,
			    class Expression* amount,
			    class Expression* i) :
  myBuffer (&buffer), myAmount (amount), myIndex (i)
{
  assert (myBuffer && myBuffer->getType ()->getKind () == Type::tBuffer);
  assert (!myAmount || myAmount->getType ()->getKind () == Type::tCard);
  assert (!myIndex || myIndex->getType ()->getKind () == Type::tCard);
  assert (myBuffer->isBasic ());
  assert (!myAmount || myAmount->isBasic ());
  assert (!myIndex || myIndex->isBasic ());

  setType (*myBuffer->getType ());
}

BufferRemove::~BufferRemove ()
{
  myBuffer->destroy ();
  myAmount->destroy ();
  myIndex->destroy ();
}

/** Evaluate a cardinality-valued expression
 * @param expr		the expression
 * @param valuation	the variable substitutions
 * @param value		(output) the result
 * @return		true if the evaluation succeeded
 */
inline static bool
eval (const class Expression& expr,
      const class Valuation& valuation,
      card_t& value)
{
  if (class Value* v = expr.eval (valuation)) {
    assert (v->getType ().getKind () == Type::tCard);
    value = card_t (static_cast<const class LeafValue&>(*v));
    delete v;
    return true;
  }
  else
    return false;
}

class Value*
BufferRemove::do_eval (const class Valuation& valuation) const
{
  class Value* buffer = myBuffer->eval (valuation);
  if (!buffer)
    return NULL;
  assert (buffer->getType ().getKind () == Type::tBuffer);

  class BufferValue* bv = static_cast<class BufferValue*>(buffer);
  card_t idx = 0, amount = 1, capacity = bv->getCapacity ();
  if (myAmount && !::eval (*myAmount, valuation, amount)) {
    delete bv;
    return NULL;
  }
  if (myIndex && !::eval (*myIndex, valuation, idx)) {
    delete bv;
    return NULL;
  }
  if (amount + idx > capacity) {
    valuation.flag (errBuf, *this);
    delete bv;
    return NULL;
  }
  if (!amount)
    return bv;

  card_t i;
  for (i = amount; i--; )
    delete (*bv)[idx + i];
  for (i = idx + amount; i < capacity; i++)
    (*bv)[i - amount] = (*bv)[i];
  for (i = capacity - amount; i < capacity; i++)
    (*bv)[i] = NULL;
  return bv;
}

class Expression*
BufferRemove::ground (const class Valuation& valuation,
		      class Transition* transition,
		      bool declare)
{
  class Expression* buffer = myBuffer->ground (valuation, transition, declare);
  if (!buffer) return NULL;
  class Expression* amount =
    myAmount ? myAmount->ground (valuation, transition, declare) : NULL;
  if (myAmount && !amount) { buffer->destroy (); return NULL; }
  class Expression* i =
    myIndex ? myIndex->ground (valuation, transition, declare) : NULL;

  if (myIndex && !i) {
    buffer->destroy ();
    amount->destroy ();
    return NULL;
  }

  assert (valuation.isOK ());

  if (buffer == myBuffer && amount == myAmount && i == myIndex) {
    buffer->destroy ();
    amount->destroy ();
    i->destroy ();
    return copy ();
  }
  else
    return static_cast<class Expression*>
      (new class BufferRemove (*buffer, amount, i))->ground (valuation);
}

class Expression*
BufferRemove::substitute (class Substitution& substitution)
{
  class Expression* buffer = myBuffer->substitute (substitution);
  class Expression* amount =
    myAmount ? myAmount->substitute (substitution) : NULL;
  class Expression* i = myIndex ? myIndex->substitute (substitution) : NULL;

  if (buffer == myBuffer && amount == myAmount && i == myIndex) {
    buffer->destroy ();
    amount->destroy ();
    i->destroy ();
    return copy ();
  }

  return (new class BufferRemove (*buffer, amount, i))->cse ();
}

bool
BufferRemove::depends (const class VariableSet& vars,
		       bool complement) const
{
  return
    myBuffer->depends (vars, complement) ||
    (myAmount && myAmount->depends (vars, complement)) ||
    (myIndex && myIndex->depends (vars, complement));
}

bool
BufferRemove::forExpressions (bool (*operation)
			      (const class Expression&,void*),
			      void* data) const
{
  return
    (*operation) (*this, data) &&
    myBuffer->forExpressions (operation, data) &&
    (!myAmount || myAmount->forExpressions (operation, data)) &&
    (!myIndex || myIndex->forExpressions (operation, data));
}

#ifdef EXPR_COMPILE
# include "CExpression.h"
# include "Constant.h"

void
BufferRemove::compile (class CExpression& cexpr,
		       unsigned indent,
		       const char* lvalue,
		       const class VariableSet* vars) const
{
  char* buf;
  if (cexpr.getVariable (*myBuffer, buf))
    myBuffer->compile (cexpr, indent, buf, vars);
  char* amvalue = 0;
  if (myAmount && myAmount->getKind () != Expression::eConstant &&
      cexpr.getVariable (*myAmount, amvalue))
    myAmount->compile (cexpr, indent, amvalue, vars);
  char* ixvalue = 0;
  if (myIndex && myIndex->getKind () != Expression::eConstant &&
      cexpr.getVariable (*myIndex, ixvalue))
    myIndex->compile (cexpr, indent, ixvalue, vars);
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append ("if (");
  out.append (buf);
  out.append (".s<");
  if (amvalue)
    out.append (amvalue), out.append ("+");
  else if (myAmount) {
    assert (myAmount->getKind () == Expression::eConstant);
    static_cast<const class Constant*>(myAmount)->getValue ().compile (out);
    out.append ("+");
  }
  else
    out.append ("=");
  if (ixvalue)
    out.append (ixvalue);
  else if (myIndex) {
    assert (myIndex->getKind () == Expression::eConstant);
    static_cast<const class Constant*>(myIndex)->getValue ().compile (out);
  }
  else
    out.append ("0");
  out.append (")\n");
  cexpr.compileError (indent + 2, errBuf);
  out.indent (indent);
  out.append (lvalue);
  out.append (".s=");
  out.append (buf);
  out.append (".s-");
  if (amvalue)
    out.append (amvalue);
  else if (myAmount)
    static_cast<const class Constant*>(myAmount)->getValue ().compile (out);
  else
    out.append ("1");
  out.append (";\n");
  if (myIndex) {
    out.indent (indent);
    out.append ("memcpy (");
    out.append (lvalue);
    out.append (".a");
    out.append (", ");
    out.append (buf);
    out.append (".a");
    out.append (", ");
    if (ixvalue)
      out.append (ixvalue);
    else
      static_cast<const class Constant*>(myIndex)->getValue ().compile (out);
    out.append (" * sizeof *");
    out.append (buf);
    out.append (".a);\n");
  }
  out.indent (indent);
  out.append ("memcpy (");
  out.append (lvalue);
  out.append (".a");
  if (myIndex) {
    out.append ("+");
    if (ixvalue)
      out.append (ixvalue);
    else
      static_cast<const class Constant*>(myIndex)->getValue ().compile (out);
  }
  out.append (", ");
  out.append (buf);
  out.append (".a");
  if (myIndex) {
    out.append ("+");
    if (ixvalue)
      out.append (ixvalue);
    else {
      assert (myIndex->getKind () == Expression::eConstant);
      static_cast<const class Constant*>(myIndex)->getValue ().compile (out);
    }
  }
  if (amvalue)
    out.append ("+"), out.append (amvalue);
  else if (myAmount) {
    out.append ("+");
    static_cast<const class Constant*>(myAmount)->getValue ().compile (out);
  }
  else
    out.append ("+1");
  out.append (",\n");
  out.indent (indent + 8);
  out.append ("(");
  out.append (lvalue);
  out.append (".s");
  if (myIndex) {
    out.append ("-");
    if (ixvalue)
      out.append (ixvalue);
    else {
      assert (myIndex->getKind () == Expression::eConstant);
      static_cast<const class Constant*>(myIndex)->getValue ().compile (out);
    }
  }
  out.append (") * sizeof *");
  out.append (buf);
  out.append (".a);\n");

  delete[] buf;
  delete[] amvalue;
  delete[] ixvalue;
  compileConstraint (cexpr, indent, lvalue);
}

#endif // EXPR_COMPILE

/** Determine whether an expression needs to be enclosed in parentheses
 * @param kind	kind of the expression
 * @return	whether parentheses are necessary
 */
inline static bool
needParentheses (enum Expression::Kind kind)
{
  switch (kind) {
  case Expression::eVariable:
  case Expression::eConstant:
  case Expression::eUndefined:
  case Expression::eStructComponent:
  case Expression::eUnionComponent:
  case Expression::eVectorIndex:
  case Expression::eNot:
  case Expression::eTypecast:
  case Expression::eUnop:
  case Expression::eBufferUnop:
  case Expression::eCardinality:
    return false;
  case Expression::eMarking:
  case Expression::eTransitionQualifier:
  case Expression::ePlaceContents:
  case Expression::eSubmarking:
  case Expression::eMapping:
  case Expression::eEmptySet:
  case Expression::eBooleanBinop:
  case Expression::eUnionType:
  case Expression::eSet:
  case Expression::eTemporalBinop:
  case Expression::eTemporalUnop:
  case Expression::eStruct:
  case Expression::eUnion:
  case Expression::eVector:
  case Expression::eBinop:
  case Expression::eRelop:
  case Expression::eStructAssign:
  case Expression::eVectorAssign:
  case Expression::eVectorShift:
    assert (false);
  case Expression::eIfThenElse:
  case Expression::eBuffer:
  case Expression::eBufferRemove:
  case Expression::eBufferWrite:
  case Expression::eBufferIndex:
    break;
  }

  return true;
}

/** Determine whether an amount expression needs to be enclosed in parentheses
 * @param kind	kind of the expression
 * @return	whether parentheses are necessary
 */
inline static bool
needParentheses2 (enum Expression::Kind kind)
{
  switch (kind) {
  case Expression::eVariable:
  case Expression::eConstant:
  case Expression::eStructComponent:
  case Expression::eUnionComponent:
  case Expression::eVectorIndex:
  case Expression::eTypecast:
    return false;
  case Expression::eUndefined:
  case Expression::eNot:
  case Expression::eMarking:
  case Expression::eTransitionQualifier:
  case Expression::ePlaceContents:
  case Expression::eSubmarking:
  case Expression::eMapping:
  case Expression::eEmptySet:
  case Expression::eBooleanBinop:
  case Expression::eUnionType:
  case Expression::eSet:
  case Expression::eTemporalBinop:
  case Expression::eTemporalUnop:
  case Expression::eStruct:
  case Expression::eUnion:
  case Expression::eVector:
  case Expression::eRelop:
  case Expression::eStructAssign:
  case Expression::eVectorAssign:
  case Expression::eVectorShift:
  case Expression::eBuffer:
  case Expression::eBufferRemove:
  case Expression::eBufferWrite:
  case Expression::eBufferIndex:
    assert (false);
  case Expression::eIfThenElse:
  case Expression::eUnop:
  case Expression::eBufferUnop:
  case Expression::eCardinality:
  case Expression::eBinop:
    break;
  }

  return true;
}

void
BufferRemove::display (const class Printer& printer) const
{
  if (!myAmount)
    printer.delimiter ('-');
  if (myIndex) {
    printer.delimiter ('(')++;
    myBuffer->display (printer);
    printer.delimiter ('[')++;
    myIndex->display (printer);
    --printer.delimiter (']');
    --printer.delimiter (')');
  }
  else if (::needParentheses (myBuffer->getKind ())) {
    printer.delimiter ('(')++;
    myBuffer->display (printer);
    --printer.delimiter (')');
  }
  else
    myBuffer->display (printer);
  if (myAmount) {
    printer.delimiter ('-');
    if (::needParentheses2 (myAmount->getKind ())) {
      printer.delimiter ('(')++;
      myAmount->display (printer);
      --printer.delimiter (')');
    }
    else
      myAmount->display (printer);
  }
}