// Multi-set mapping expression -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Mapping.h"
#include "Marking.h"
#include "VariableDefinition.h"
#include "Valuation.h"
#include "PlaceMarking.h"
#include "LeafValue.h"
#include "Substitution.h"
#include "Variable.h"
#include "Printer.h"

/** @file Mapping.C
 * Multi-set mapping operation
 */

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

Mapping::Mapping (class VariableDefinition& variable,
		  class VariableDefinition* cardinality,
		  class Expression& marking,
		  class Expression& expr) :
  myVariable (&variable), myCardinality (cardinality),
  myMarking (&marking), myExpr (&expr)
{
  assert (myVariable && myExpr);
  assert (myMarking && myMarking->getType ());
  assert (!myMarking->isTemporal ());
  if (myCardinality) {
    assert (myCardinality->getType ().getKind () == Type::tCard);
    assert (myExpr->getKind () == Expression::eMarking);
  }
  else
    assert (myExpr->isBasic ());
  setType (*myExpr->getType ());
}

Mapping::~Mapping ()
{
  delete myVariable;
  delete myCardinality;
  myMarking->destroy ();
  myExpr->destroy ();
}

class PlaceMarking*
Mapping::meval (const class Valuation& valuation) const
{
  if (class PlaceMarking* p = myMarking->meval (valuation)) {
    p->setPlace (NULL);
    class Valuation v (valuation);
    class PlaceMarking* q = new class PlaceMarking ();
#ifndef NDEBUG
    q->setType (myExpr->getType ());
#endif // NDEBUG
    for (PlaceMarking::iterator i = p->begin (); i != p->end (); i++) {
      if (!PlaceMarking::getCount (i))
	continue;
      v.setValue (*myVariable, *PlaceMarking::getValue (i).copy ());
      if (myCardinality) {
	v.setValue (*myCardinality,
		    *new class LeafValue (myCardinality->getType (),
					  PlaceMarking::getCount (i)));
	if (!static_cast<const class Marking*>(myExpr)->add (*q, 1, v)) {
	error:
	  valuation.copyErrors (v);
	error2:
	  delete p;
	  delete q;
	  return NULL;
	}
      }
      else if (class Value* val = myExpr->eval (v)) {
	if (!q->add (*val, PlaceMarking::getCount (i))) {
	  valuation.flag (errCard, *this);
	  goto error2;
	}
      }
      else
	goto error;
    }

    delete p;
    return q;
  }
  return NULL;
}

/** Create a Mapping, substituting the iterator variables
 * @param variable	the old token iterator variable
 * @param cardinality	the old cardinality iterator variable
 * @param marking	the marking expression
 * @param condition	the mapping expression (iterator substituted)
 * @return		the corresponding Submarking expression
 */
static class Mapping*
newMapping (const class VariableDefinition& variable,
	    const class VariableDefinition* cardinality,
	    class Expression& marking,
	    class Expression& expr)
{
  class VariableDefinition& v = *new class VariableDefinition (variable);
  class VariableDefinition* c = cardinality ?
    new class VariableDefinition (*cardinality)
    : 0;
  class Substitution s;
  s.setExpr (variable, *(new class Variable (v))->cse ());
  if (cardinality)
    s.setExpr (*cardinality, *(new class Variable (*c))->cse ());
  class Expression* e = expr.substitute (s);
  assert (!!e);
  expr.destroy ();
  return static_cast<class Mapping*>
    ((new class Mapping (v, c, marking, *e))->cse ());
}

class Expression*
Mapping::ground (const class Valuation& valuation,
		 class Transition* transition,
		 bool declare)
{
  class Expression* marking =
    myMarking->ground (valuation, transition, declare);
  if (!marking) return NULL;
  class Expression* expr =
    myExpr->ground (valuation, transition, declare);
  if (!expr) { marking->destroy (); return NULL; }

  assert (valuation.isOK ());

  if (marking == myMarking && expr == myExpr) {
    marking->destroy ();
    expr->destroy ();
    return copy ();
  }
  else
    return newMapping (*myVariable, myCardinality, *marking, *expr);
}

class Expression*
Mapping::substitute (class Substitution& substitution)
{
  class Expression* marking = myMarking->substitute (substitution);
  class Expression* expr = myExpr->substitute (substitution);

  if (!marking || !expr) {
    marking->destroy ();
    expr->destroy ();
    return NULL;
  }
  if (marking == myMarking && expr == myExpr) {
    marking->destroy ();
    expr->destroy ();
    return copy ();
  }
  else
    return newMapping (*myVariable, myCardinality, *marking, *expr);
}

bool
Mapping::depends (const class VariableSet& vars,
		  bool complement) const
{
  return
    myMarking->depends (vars, complement) ||
    myExpr->depends (vars, complement);
}

bool
Mapping::forVariables (bool (*operation)
		       (const class Expression&,void*),
		       void* data) const
{
  return
    myMarking->forVariables (operation, data) &&
    myExpr->forVariables (operation, data);
}

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

void
Mapping::compileMset (class CExpression& cexpr,
		      unsigned indent,
		      const char* resulttype,
		      const char* result,
		      const class VariableSet* vars) const
{
  assert (myVariable && myMarking && myExpr);
  /** the multi-set iterator */
  char* iter;
  /** the mapping expression */
  char* expr;
  /** the item iterator */
  char* var;
  /** the multiplicity iterator */
  char* card;
  if (myExpr->getKind () == Expression::eConstant) {
    if (cexpr.getVariable (static_cast<const class Constant&>(*myExpr), expr))
      myExpr->compile (cexpr, indent, expr, vars);
    var = card = 0;
  }
  else {
    var = cexpr.getIterator (*myVariable);
    card = myCardinality ? cexpr.getIterator (*myCardinality) : 0;
    cexpr.getVariable (*myExpr, expr);
  }

  class StringBuffer& out = cexpr.getOut ();
  /** flag: is the marking the contents of a place with at most one token? */
  bool place1 = myMarking->getKind () == Expression::ePlaceContents &&
    static_cast<const class PlaceContents*>
    (myMarking)->getPlace ().getMaxNumTokens () == 1;

  if (place1) {
    iter = static_cast<const class PlaceContents*>(myMarking)->getName (cexpr);
    out.indent (indent);
    out.append ("if ("), out.append (iter), out.append (") {\n");
    if (myExpr->getKind () != Expression::eConstant) {
      out.indent (indent + 2);
      myVariable->getType ().appendName (out);
      out.append (" "), out.append (var), out.append (" = *");
      out.append (iter);
      out.append (";\n");
      if (card) {
	out.indent (indent + 2);
	out.append ("card_t "), out.append (card), out.append ("=1;\n");
	myExpr->compileMset (cexpr, indent + 2, resulttype, result, vars);
      }
      else
	myExpr->compile (cexpr, indent + 2, expr, vars);
    }
    if (!card) {
      out.indent (indent + 2);
      out.append (result);
      out.append ("=insert");
      getType ()->appendIndex (out);
      out.append (" (");
      if (resulttype)
	out.append (resulttype);
      out.append (result), out.append (", ");
      out.append ("&"), out.append (expr), out.append (", 1);\n");
    }
  }
  else {
    /** the multi-set */
    char* mset;
    if (cexpr.getVariable (*myMarking, mset))
      myMarking->compileMset (cexpr, indent, 0, mset, vars);
    iter = cexpr.getLabel ();
    out.indent (indent), out.append ("{\n");
    out.indent (indent + 2);
    myMarking->getType ()->appendMSetName (out);
    out.append ("* "), out.append (iter), out.append (" = ");
    out.append (mset), out.append (";\n");
    delete[] mset;
    out.indent (indent + 2);
    out.append ("FIRST ("), out.append (iter), out.append (");\n");
    out.indent (indent + 2);
    out.append ("while ("), out.append (iter), out.append (") {\n");
    out.indent (indent + 4);
    out.append ("if ("), out.append (iter), out.append ("->count) {\n");
    /** checkpoint in the while iteration loop */
    bool* checkpoint;
    const unsigned checkpointSize = cexpr.getCheckpoint (checkpoint);
    if (myExpr->getKind () != Expression::eConstant) {
      out.indent (indent + 6);
      myVariable->getType ().appendName (out);
      out.append (" "), out.append (var), out.append ("=");
      out.append (iter), out.append ("->item;\n");
      if (card) {
	out.indent (indent + 6);
	out.append ("card_t "), out.append (card), out.append ("=");
	out.append (iter), out.append ("->count;\n");
	myExpr->compileMset (cexpr, indent + 6, resulttype, result, vars);
      }
      else
	myExpr->compile (cexpr, indent + 6, expr, vars);
    }
    if (!card) {
      out.indent (indent + 6);
      out.append (result);
      out.append ("=insert");
      getType ()->appendIndex (out);
      out.append (" (");
      if (resulttype)
	out.append (resulttype);
      out.append (result), out.append (", ");
      out.append ("&"), out.append (expr), out.append (", ");
      out.append (iter), out.append ("->count");
      out.append (");\n");
    }
    cexpr.setCheckpoint (indent + 6, checkpoint, checkpointSize);
    out.indent (indent + 4), out.append ("}\n");
    out.indent (indent + 4);
    out.append ("NEXT ("), out.append (iter), out.append (");\n");
    out.indent (indent + 2), out.append ("}\n");
  }
  out.indent (indent), out.append ("}\n");

  delete[] card;
  delete[] var;
  delete[] expr;
  delete[] iter;
}

#endif // EXPR_COMPILE

void
Mapping::display (const class Printer& printer) const
{
  printer.printRaw ("map");
  printer.delimiter (' ');
  printer.print (myVariable->getName ());
  if (myCardinality) {
    printer.delimiter ('#');
    printer.print (myCardinality->getName ());
  }
  printer.delimiter ('{')++;
  myMarking->display (printer);
  --printer.delimiter ('}');
  printer.delimiter ('(')++;
  myExpr->display (printer);
  --printer.delimiter (')');
}