// Maria buffer expression class -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "BufferExpression.h"
#include "BufferValue.h"
#include "Printer.h"
#include <string.h>

/** @file BufferExpression.C
 * Queue or stack constructor
 */

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

BufferExpression::BufferExpression (const class BufferType& type) :
  Expression (),
  myComponents (NULL)
{
  assert (type.getSize () > 0);
  myComponents = new class Expression*[type.getSize ()];
  memset (myComponents, 0, type.getSize () * sizeof *myComponents);
  setType (type);
}

BufferExpression::~BufferExpression ()
{
  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size && myComponents[i]; i++)
    myComponents[i]->destroy ();
  delete[] myComponents;
}

void
BufferExpression::setType (const class Type& type)
{
  assert (type.getKind () == Type::tBuffer);
  const class Type& itemType =
    static_cast<const class BufferType&>(type).getItemType ();

  for (card_t size = static_cast<const class BufferType&>(type).getSize (),
	 i = 0; i < size && myComponents[i]; i++)
    myComponents[i]->setType (itemType);

  Expression::setType (type);
}

class Value*
BufferExpression::do_eval (const class Valuation& valuation) const
{
  class BufferValue* buffer = new class BufferValue (*getType ());

  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size && myComponents[i]; i++) {
    if (class Value* v = myComponents[i]->eval (valuation)) {
      assert (&v->getType () ==
	      &static_cast<const class BufferType*>
	      (getType ())->getItemType ());
      (*buffer)[i] = v;
    }
    else {
      delete buffer;
      return NULL;
    }
  }

  return constrain (valuation, buffer);
}

class Expression*
BufferExpression::ground (const class Valuation& valuation,
			  class Transition* transition,
			  bool declare)
{
  bool same = true;
  const class BufferType* const type =
    static_cast<const class BufferType*>(getType ());
  class BufferExpression* expr = new class BufferExpression (*type);

  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size && myComponents[i]; i++) {
    class Expression* e =
      myComponents[i]->ground (valuation, transition, declare);
    if (!e) {
      expr->destroy ();
      return NULL;
    }

    if (e != myComponents[i])
      same = false;
    expr->myComponents[i] = e;
  }

  assert (valuation.isOK ());

  if (same) {
    expr->destroy ();
    return copy ();
  }

  return static_cast<class Expression*>(expr)->ground (valuation);
}

class Expression*
BufferExpression::substitute (class Substitution& substitution)
{
  bool same = true;
  const class BufferType* const type =
    static_cast<const class BufferType*>(getType ());
  class BufferExpression* expr = new class BufferExpression (*type);

  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size && myComponents[i]; i++) {
    class Expression* e = myComponents[i]->substitute (substitution);
    if (e != myComponents[i])
      same = false;
    expr->myComponents[i] = e;
  }
  if (same) {
    expr->destroy ();
    return copy ();
  }
  else
    return expr->cse ();
}

bool
BufferExpression::depends (const class VariableSet& vars,
			   bool complement) const
{
  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size && myComponents[i]; i++)
    if (myComponents[i]->depends (vars, complement))
      return true;
  return false;
}

bool
BufferExpression::forExpressions (bool (*operation)
				  (const class Expression&,void*),
				  void* data) const
{
  card_t size = static_cast<const class BufferType*>(getType ())->getSize ();
  if (!(*operation) (*this, data))
    return false;
  for (card_t i = 0; i < size && myComponents[i]; i++)
    if (!myComponents[i]->forExpressions (operation, data))
      return false;
  return true;
}

bool
BufferExpression::isCompatible (const class Value& value,
				const class Valuation& valuation) const
{
  assert (value.getKind () == Value::vBuffer &&
	  value.getType ().getKind () == Type::tBuffer);

  const class BufferValue& bv = static_cast<const class BufferValue&>(value);
  const class BufferType* bt =
    static_cast<const class BufferType*>(getType ());

  assert (bv.getSize () ==
	  static_cast<const class BufferType&>(bv.getType ()).getSize ());

  if (!bv.getType ().isAssignable (*getType ()))
    return false;

  for (card_t size = bt->getSize (), i = 0; i < size; i++)
    if (!myComponents[i])
      return !bv[i];
    else if (!bv[i])
      return !myComponents[i];
    else if (!myComponents[i]->isCompatible (*bv[i], valuation))
      return false;

  return true;
}

void
BufferExpression::getLvalues (const class Value& value,
			      class Valuation& valuation,
			      const class VariableSet& vars) const
{
  assert (value.getKind () == Value::vBuffer);
  assert (&value.getType () == getType ());
  const class BufferValue& bv = static_cast<const class BufferValue&>(value);

  card_t size = getSize ();
  if (bv.getCapacity () == size)
    for (card_t i = 0; i < size; i++)
      myComponents[i]->getLvalues (*bv[i], valuation, vars);
}

void
BufferExpression::getLvalues (const class VariableSet& rvalues,
			      class VariableSet*& lvalues) const
{
  for (card_t size = getSize (), i = 0; i < size; i++)
    myComponents[i]->getLvalues (rvalues, lvalues);
}

#ifdef EXPR_COMPILE
# include <stdio.h>
# include "CExpression.h"

void
BufferExpression::compileLvalue (class CExpression& cexpr,
				 unsigned indent,
				 const class VariableSet& vars,
				 const char* lvalue) const
{
  assert (!!lvalue);
  const size_t len = strlen (lvalue);
  char* const newlvalue = new char[len + 25];
  char* const suffix = newlvalue + len;
  memcpy (newlvalue, lvalue, len);

  const card_t size =
    static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size; i++) {
    snprintf (suffix, 25, ".a[%u]", i);
    myComponents[i]->compileLvalue (cexpr, indent, vars, newlvalue);
  }
  delete[] newlvalue;
}

void
BufferExpression::compileCompatible (class CExpression& cexpr,
				     unsigned indent,
				     const class VariableSet& vars,
				     const char* value) const
{
  const size_t len = strlen (value);
  char* const val = new char[len + 25];
  char* const suffix = val + len;
  memcpy (val, value, len);

  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent), out.append ("if (");
  out.append (value), out.append (".s!=");
  out.append (getSize ());
  out.append (")\n");
  cexpr.compileError (indent + 2, errComp);

  const card_t size =
    static_cast<const class BufferType*>(getType ())->getSize ();
  for (card_t i = 0; i < size; i++) {
    snprintf (suffix, 25, ".a[%u]", i);
    myComponents[i]->compileCompatible (cexpr, indent, vars, val);
  }
  delete[] val;
}

void
BufferExpression::compile (class CExpression& cexpr,
			   unsigned indent,
			   const char* lvalue,
			   const class VariableSet* vars) const
{
  size_t len = strlen (lvalue);
  char* const newlvalue = new char[len + 25];
  char* const suffix = newlvalue + len;
  memcpy (newlvalue, lvalue, len);

  class StringBuffer& out = cexpr.getOut ();
  card_t size = getSize ();
  snprintf (suffix, 25, ".s=%u", size);
  out.indent (indent), out.append (newlvalue);
  out.append (";\n");
  for (card_t i = 0; i < size; i++) {
    snprintf (suffix, 25, ".a[%u]", i);
    myComponents[i]->compile (cexpr, indent, newlvalue, vars);
  }
  delete[] newlvalue;
  compileConstraint (cexpr, indent, lvalue);
}

#endif // EXPR_COMPILE

void
BufferExpression::display (const class Printer& printer) const
{
  const class BufferType* type =
    static_cast<const class BufferType*>(getType ());
  printer.delimiter ('{')++;
  for (card_t i = 0; myComponents[i]; ) {
    myComponents[i]->display (printer);
    if (++i == type->getSize () || !myComponents[i])
      break;
    printer.delimiter (',');
  }
  --printer.delimiter ('}');
}