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

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

/** @file BufferUnop.C
 * Unary operators on queues and stacks
 */

/* 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. */

BufferUnop::BufferUnop (enum BufferUnop::Op op,
			class Expression& buffer,
			class Expression* i) :
  myOp (op), myBuffer (&buffer), myIndex (i)
{
  assert (myBuffer && myBuffer->getType ()->getKind () == Type::tBuffer);
  assert (!myIndex || myIndex->getType ()->getKind () == Type::tCard);
  assert (myBuffer->isBasic ());
  assert (!myIndex || myIndex->isBasic ());

  switch (myOp) {
  case bPeek:
    setType (static_cast<const class BufferType*>
	     (myBuffer->getType ())->getItemType ());
    break;
  case bFree:
  case bUsed:
    assert (!myIndex);
    setType (Net::getCardType ());
    break;
  default:
    assert (false);
  }
}

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

class Value*
BufferUnop::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, capacity = bv->getCapacity ();
  if (myIndex) {
    if (class Value* iv = myIndex->eval (valuation)) {
      assert (iv->getType ().getKind () == Type::tCard);
      card_t i = card_t (static_cast<const class LeafValue&>(*iv));
      delete iv;
      if (i >= capacity) {
	valuation.flag (errBuf, *this);
	delete bv;
	return NULL;
      }
      idx = i;
    }
    else {
      delete bv;
      return NULL;
    }
  }

  switch (myOp) {
  case bPeek:
    if (!capacity) {
      valuation.flag (errBuf, *this);
      delete bv;
      return NULL;
    }
    else {
      class Value* item = (*bv)[idx]->copy ();
      delete bv;
      return item;
    }

  case bFree:
    {
      class Value* result =
	constrain (valuation,
		   new class LeafValue
		   (*getType (), bv->getSize () - capacity));
      delete bv;
      return result;
    }
  case bUsed:
    delete bv;
    return constrain (valuation,
		      new class LeafValue (*getType (), capacity));
  }

  assert (false);
  return NULL;
}

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

  assert (valuation.isOK ());

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

class Expression*
BufferUnop::substitute (class Substitution& substitution)
{
  class Expression* buffer = myBuffer->substitute (substitution);
  class Expression* i = myIndex ? myIndex->substitute (substitution) : 0;

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

  return (new class BufferUnop (myOp, *buffer, i))->cse ();
}

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

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

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

void
BufferUnop::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* ixvalue = 0;
  if (myIndex && myIndex->getKind () != Expression::eConstant &&
      cexpr.getVariable (*myIndex, ixvalue))
    myIndex->compile (cexpr, indent, ixvalue, vars);
  class StringBuffer& out = cexpr.getOut ();
  switch (myOp) {
  case bPeek:
    out.indent (indent);
    out.append ("if (");
    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 (">=");
    out.append (buf);
    out.append (".s)\n");
    cexpr.compileError (indent + 2, errBuf);
    out.indent (indent);
    out.append (lvalue);
    out.append ("=");
    out.append (buf);
    out.append (".a[");
    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");
    break;
  case bFree:
  case bUsed:
    out.indent (indent);
    out.append (lvalue);
    out.append ("=");
    if (myOp == bFree) {
      out.append (static_cast<const class BufferType*>(myBuffer->getType ())
		  ->getSize ());
      out.append ("-");
    }
    out.append (buf);
    out.append (".s;\n");
    break;
  }

  delete[] buf;
  delete[] ixvalue;
  if (myOp != bPeek)
    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;
}

void
BufferUnop::display (const class Printer& printer) const
{
  char op = '?';
  switch (myOp) {
  case bPeek:
    op = '*'; break;
  case bFree:
    op = '%'; break;
  case bUsed:
    op = '/'; break;
  }
  printer.delimiter (op);
  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);
}