// Maria vector component assignment class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "VectorAssign.h"
#include "VectorValue.h"
#include "VectorType.h"
#include "Printer.h"
#include <string.h>

/** @file VectorAssign.C
 * Vector component assignment operation
 */

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

VectorAssign::VectorAssign (class Expression& vect,
			    class Expression& i,
			    class Expression& item) :
  Expression (),
  myVector (vect), myIndex (i), myItem (item)
{
  assert (myVector.getType () &&
	  myVector.getType ()->getKind () == Type::tVector);
  assert (myVector.isBasic () && myIndex.isBasic () && myItem.isBasic ());
  const class VectorType& type =
    *static_cast<const class VectorType*>(myVector.getType ());
  assert (myItem.getType () && myItem.getType () == &type.getItemType ());
  assert (myIndex.getType () && myIndex.getType () == &type.getIndexType ());
  setType (type);
}

VectorAssign::~VectorAssign ()
{
  myVector.destroy ();
  myIndex.destroy ();
  myItem.destroy ();
}

class Value*
VectorAssign::do_eval (const class Valuation& valuation) const
{
  class Value* idx = myIndex.eval (valuation);
  if (!idx)
    return NULL;
  const class Type& indexType =
    static_cast<const class VectorType*>(myVector.getType ())->getIndexType ();

  assert (idx->getType ().isAssignable (indexType));
  assert (indexType.isConstrained (*idx));

  card_t i = indexType.convert (*idx);
  assert (i < CARD_T_MAX && i < indexType.getNumValues ());
  delete idx;

  class Value* vector = myVector.eval (valuation);
  if (!vector)
    return NULL;
  assert (&vector->getType () == myVector.getType ());
  class Value*& v = static_cast<class VectorValue&>(*vector)[i];
  delete v;
  if (!(v = myItem.eval (valuation))) {
    delete vector;
    return NULL;
  }
  return constrain (valuation, vector);
}

class Expression*
VectorAssign::ground (const class Valuation& valuation,
		      class Transition* transition,
		      bool declare)
{
  class Expression* vect = myVector.ground (valuation, transition, declare);
  if (!vect) return NULL;
  class Expression* i = myIndex.ground (valuation, transition, declare);
  if (!i) { vect->destroy (); return NULL; }
  class Expression* item = myItem.ground (valuation, transition, declare);
  if (!item) { vect->destroy (); i->destroy (); return NULL; }

  assert (valuation.isOK ());

  if (vect == &myVector && i == &myIndex && item == &myItem) {
    vect->destroy (), i->destroy (), item->destroy ();
    return copy ();
  }
  else
    return static_cast<class Expression*>
      (new class VectorAssign (*vect, *i, *item))->ground (valuation);
}

class Expression*
VectorAssign::substitute (class Substitution& substitution)
{
  class Expression* vect = myVector.substitute (substitution);
  class Expression* i = myIndex.substitute (substitution);
  class Expression* item = myItem.substitute (substitution);

  if (vect == &myVector && i == &myIndex && item == &myItem) {
    vect->destroy (), i->destroy (), item->destroy ();
    return copy ();
  }
  else
    return (new class VectorAssign (*vect, *i, *item))->cse ();
}

bool
VectorAssign::depends (const class VariableSet& vars,
		       bool complement) const
{
  return
    myVector.depends (vars, complement) ||
    myIndex.depends (vars, complement) ||
    myItem.depends (vars, complement);
}

bool
VectorAssign::forExpressions (bool (*operation)
			      (const class Expression&,void*),
			      void* data) const
{
  return
    (*operation) (*this, data) &&
    myVector.forExpressions (operation, data) &&
    myIndex.forExpressions (operation, data) &&
    myItem.forExpressions (operation, data);
}

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

void
VectorAssign::compile (class CExpression& cexpr,
		       unsigned indent,
		       const char* lvalue,
		       const class VariableSet* vars) const
{
  myVector.compile (cexpr, indent, lvalue, vars);
  char* ixconv = 0;
  class StringBuffer& out = cexpr.getOut ();
  if (myIndex.getKind () != Expression::eConstant) {
    char* ixvalue = 0;
    if (cexpr.getVariable (myIndex, ixvalue))
      myIndex.compile (cexpr, indent, ixvalue, vars);
    if (cexpr.getConverted (myIndex, ixconv))
      myIndex.getType ()->compileConversion (out, indent,
					     ixvalue, ixconv, false);
    delete[] ixvalue;
  }
  class StringBuffer item;
  item.append (lvalue);
  item.append (".a[");
  if (myIndex.getKind () == Expression::eConstant)
    item.append (myIndex.getType ()->convert
		 (static_cast<const class Constant&>(myIndex).getValue ()));
  else
    item.append (ixconv);
  item.append ("]");
  delete[] ixconv;
  myItem.compile (cexpr, indent, item.getString (), vars);

  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::eUndefined:
  case Expression::eStructComponent:
  case Expression::eUnionComponent:
  case Expression::eVectorIndex:
  case Expression::eVectorAssign:
    return false;
  case Expression::eCardinality:
  case Expression::eBuffer:
  case Expression::eBufferRemove:
  case Expression::eBufferWrite:
  case Expression::eBufferIndex:
  case Expression::eBinop:
  case Expression::eBooleanBinop:
  case Expression::eNot:
  case Expression::eRelop:
  case Expression::eSet:
  case Expression::eTemporalBinop:
  case Expression::eTemporalUnop:
  case Expression::eMarking:
  case Expression::eTransitionQualifier:
  case Expression::ePlaceContents:
  case Expression::eSubmarking:
  case Expression::eMapping:
  case Expression::eEmptySet:
  case Expression::eUnionType:
  case Expression::eUnion:
  case Expression::eStruct:
  case Expression::eStructAssign:
    assert (false);
  case Expression::eUnop:
  case Expression::eBufferUnop:
  case Expression::eConstant:
  case Expression::eIfThenElse:
  case Expression::eVector:
  case Expression::eVectorShift:
  case Expression::eTypecast:
    break;
  }

  return true;
}

void
VectorAssign::display (const class Printer& printer) const
{
  if (::needParentheses (myVector.getKind ())) {
    printer.delimiter ('(')++;
    myVector.display (printer);
    --printer.delimiter (')');
  }
  else
    myVector.display (printer);
  printer.delimiter ('.');
  printer.delimiter ('{')++;
  printer.delimiter ('[')++;
  myIndex.display (printer);
  --printer.delimiter (']');
  myItem.display (printer);
  --printer.delimiter ('}');
}