// Maria structure (or array) expression class -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "StructExpression.h"
#include "StructType.h"
#include "StructValue.h"
#include "Printer.h"

/** @file StructExpression.C
 * Structure 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. */

StructExpression::StructExpression (const class Type& type) :
  Expression (),
  myComponents ()
{
  assert (type.getKind () == Type::tStruct);
  Expression::setType (type);
}

StructExpression::~StructExpression ()
{
  for (iterator i = begin (); i != end (); i++)
    (*i)->destroy ();
}

void
StructExpression::setType (const class Type& type)
{
  Expression::setType (type);
  assert (type.getKind () == Type::tStruct);
  const class StructType& t = static_cast<const class StructType&>(type);

  assert (t.getSize () == size ());
  card_t i;
  const_iterator j;

  for (i = 0, j = begin (); i < t.getSize (); i++, j++)
    (*j)->setType (t[i]);
}

void
StructExpression::append (class Expression& expr)
{
  assert (expr.isBasic ());
  expr.setType (*getNextType ());
  myComponents.insert (end (), &expr);
}

const class Type*
StructExpression::getNextType () const
{
  assert (getType () && getType ()->getKind () == Type::tStruct);
  const class StructType* type =
    static_cast<const class StructType*>(getType ());
  assert (size () <= type->getSize ());
  if (size () == type->getSize ())
    return NULL;
  else
    return &(*type)[size ()];
}

class Value*
StructExpression::do_eval (const class Valuation& valuation) const
{
  class StructValue* value = new class StructValue (*getType ());
  const_iterator i;
  card_t j;
  for (i = begin (), j = 0; i != end (); i++, j++) {
    if (class Value* v = (*i)->eval (valuation))
      (*value)[j] = v;
    else {
      delete value;
      return NULL;
    }
  }

  return constrain (valuation, value);
}

class Expression*
StructExpression::ground (const class Valuation& valuation,
			  class Transition* transition,
			  bool declare)
{
  bool same = true;
  class StructExpression* expr = new class StructExpression (*getType ());

  for (iterator i = begin (); i != end (); i++) {
    class Expression* e = (*i)->ground (valuation, transition, declare);
    if (!e) {
      expr->destroy ();
      return NULL;
    }

    assert (valuation.isOK ());

    if (e != *i)
      same = false;
    expr->append (*e);
  }

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

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

class Expression*
StructExpression::substitute (class Substitution& substitution)
{
  bool same = true;
  class StructExpression* expr = new class StructExpression (*getType ());

  for (iterator i = begin (); i != end (); i++) {
    class Expression* e = (*i)->substitute (substitution);
    if (e != *i)
      same = false;
    expr->append (*e);
  }

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

bool
StructExpression::depends (const class VariableSet& vars,
			   bool complement) const
{
  for (const_iterator i = begin (); i != end (); i++)
    if ((*i)->depends (vars, complement))
      return true;
  return false;
}

bool
StructExpression::forExpressions (bool (*operation)
				  (const class Expression&,void*),
				  void* data) const
{
  if (!(*operation) (*this, data))
    return false;
  for (const_iterator i = begin (); i != end (); i++)
    if (!(*i)->forExpressions (operation, data))
      return false;
  return true;
}

bool
StructExpression::isCompatible (const class Value& value,
				const class Valuation& valuation) const
{
  assert (value.getKind () == Value::vStruct);
  assert (value.getType ().getKind () == Type::tStruct);

  const class StructValue& sv = static_cast<const class StructValue&>(value);

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

  const_iterator i;
  card_t j;

  for (i = begin (), j = 0; i != end (); i++, j++)
    if (!(*i)->isCompatible (sv[j], valuation))
      return false;

  return true;
}

void
StructExpression::getLvalues (const class Value& value,
			      class Valuation& valuation,
			      const class VariableSet& vars) const
{
  assert (value.getKind () == Value::vStruct);
  assert (&value.getType () == getType ());
  const class StructValue& sv = static_cast<const class StructValue&>(value);

  const_iterator i;
  card_t j;

  for (i = begin (), j = 0; i != end (); i++, j++)
    (*i)->getLvalues (sv[j], valuation, vars);
}

void
StructExpression::getLvalues (const class VariableSet& rvalues,
			      class VariableSet*& lvalues) const
{
  for (const_iterator i = begin (); i != end (); i++)
    (*i)->getLvalues (rvalues, lvalues);
}

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

void
StructExpression::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 + 23];
  char* const suffix = newlvalue + len;
  memcpy (newlvalue, lvalue, len);

  card_t idx = 0;
  for (const_iterator i = begin (); i != end (); i++, idx++) {
    snprintf (suffix, 23, ".s%u", idx);
    (*i)->compileLvalue (cexpr, indent, vars, newlvalue);
  }
  delete[] newlvalue;
}

void
StructExpression::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 + 23];
  char* const suffix = val + len;
  memcpy (val, value, len);

  card_t idx = 0;
  for (const_iterator i = begin (); i != end (); i++, idx++) {
    snprintf (suffix, 23, ".s%u", idx);
    (*i)->compileCompatible (cexpr, indent, vars, val);
  }
  delete[] val;
}

void
StructExpression::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 + 23];
  char* const suffix = newlvalue + len;
  memcpy (newlvalue, lvalue, len);

  card_t idx = 0;
  for (const_iterator i = begin (); i != end (); i++) {
    snprintf (suffix, 23, ".s%u", idx++);
    (*i)->compile (cexpr, indent, newlvalue, vars);
  }
  delete[] newlvalue;
  compileConstraint (cexpr, indent, lvalue);
}

#endif // EXPR_COMPILE

void
StructExpression::display (const class Printer& printer) const
{
  printer.delimiter ('{')++;
  for (const_iterator i = begin (); i != end (); ) {
    (*i)->display (printer);
    if (++i == end ())
      break;
    printer.delimiter (',');
  }
  --printer.delimiter ('}');
}