// Maria vector shifter class -*- c++ -*-

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

/** @file VectorShift.C
 * Vector shift 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. */

VectorShift::VectorShift (class Expression& vect,
			  class Expression& amount) :
  Expression (),
  myVector (vect), myAmount (amount)
{
  assert (myVector.getType () &&
	  myVector.getType ()->getKind () == Type::tVector);
  assert (myVector.isBasic () && myAmount.isBasic ());
  assert (myAmount.getType () &&
	  myAmount.getType ()->getKind () == Type::tCard);
  setType (*myVector.getType ());
}

VectorShift::~VectorShift ()
{
  myVector.destroy ();
  myAmount.destroy ();
}

class Value*
VectorShift::do_eval (const class Valuation& valuation) const
{
  class Value* v = myAmount.eval (valuation);
  if (!v)
    return NULL;

  assert (v->getKind () == Value::vLeaf);
  card_t i = card_t (*static_cast<class LeafValue*>(v));
  delete v;

  card_t size =
    static_cast<const class VectorType*>(getType ())->getSize ();

  v = myVector.eval (valuation);
  assert (!v || &v->getType () == getType ());
  if (!v || !(i %= size))
    return v;

  class VectorValue& vector = *static_cast<class VectorValue*>(v);

  class Value** t = new class Value*[i];
  card_t j;
  for (j = i; j--; t[j] = vector[j]);
  for (j = 0; j < size - i; j++)
    vector[j] = vector[i + j];
  for (j = i; j--; vector[size - i + j] = t[j]);
  delete[] t;

  return constrain (valuation, &vector);
}

class Expression*
VectorShift::ground (const class Valuation& valuation,
		     class Transition* transition,
		     bool declare)
{
  class Expression* vect = myVector.ground (valuation, transition, declare);
  if (!vect) return NULL;
  class Expression* amount = myAmount.ground (valuation, transition, declare);
  if (!amount) { vect->destroy (); return NULL; }

  assert (valuation.isOK ());

  if (vect == &myVector && amount == &myAmount) {
    vect->destroy (), amount->destroy ();
    return copy ();
  }
  else
    return static_cast<class Expression*>
      (new class VectorShift (*vect, *amount))->ground (valuation);
}

class Expression*
VectorShift::substitute (class Substitution& substitution)
{
  class Expression* vect = myVector.substitute (substitution);
  class Expression* amount = myAmount.substitute (substitution);

  if (vect == &myVector && amount == &myAmount) {
    vect->destroy (), amount->destroy ();
    return copy ();
  }
  else
    return (new class VectorShift (*vect, *amount))->cse ();
}

bool
VectorShift::depends (const class VariableSet& vars,
		      bool complement) const
{
  return
    myVector.depends (vars, complement) ||
    myAmount.depends (vars, complement);
}

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

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

void
VectorShift::compile (class CExpression& cexpr,
		      unsigned indent,
		      const char* lvalue,
		      const class VariableSet* vars) const
{
  myVector.compile (cexpr, indent, lvalue, vars);
  class StringBuffer& out = cexpr.getOut ();
  class StringBuffer amount;
  size_t size = static_cast<const class VectorType*>(getType ())->getSize ();
  if (myAmount.getKind () == Expression::eConstant) {
    const class Value& v =
      static_cast<const class Constant&>(myAmount).getValue ();
    assert (v.getKind () == Value::vLeaf);
    amount.append (card_t (static_cast<const class LeafValue&>(v)));
  }
  else {
    class LeafValue v (Net::getCardType (), card_t (size));
    char* var = 0;
    if (cexpr.getVariable (myAmount, var))
      myAmount.compile (cexpr, indent, var, vars);
    out.indent (indent);
    out.append ("if (");
    v.compileOrder (out, indent + 4, var, true, false, true, true);
    out.append (")\n");
    cexpr.compileError (indent + 2, errShift);
    amount.append (var);
    delete[] var;
  }

  out.indent (indent);
  out.append ("if (");
  out.append (amount);
  if (myAmount.getKind () != Expression::eConstant)
    out.append (" %= "), out.append (unsigned (size));
  out.append (") {\n");
  out.indent (indent + 2);
  static_cast<const class VectorType*>(getType ())
    ->getItemType ().appendName (out);
  out.append (" t["), out.append (amount), out.append ("];\n");

  out.indent (indent + 2);
  out.append ("memcpy (t, ");
  out.append (lvalue), out.append (".a, sizeof t);\n");
  out.indent (indent + 2);
  out.append ("memmove (");
  out.append (lvalue), out.append (".a, ");
  out.append (lvalue), out.append (".a + "), out.append (amount);
  out.append (", (");
  out.append (unsigned (size)), out.append (" - "), out.append (amount);
  out.append (") * sizeof *t);\n");
  out.indent (indent + 2);
  out.append ("memcpy (");
  out.append (lvalue), out.append (".a + "), out.append (unsigned (size));
  out.append (" - "), out.append (amount), out.append (", t, ");
  out.append (amount);
  out.append (" * sizeof * t);\n");

  compileConstraint (cexpr, indent + 2, lvalue);
  out.indent (indent);
  out.append ("}\n");
}

#endif // EXPR_COMPILE

void
VectorShift::display (const class Printer& printer) const
{
  myVector.display (printer);
  printer.printRaw ("<<");
  myAmount.display (printer);
}