// Auxiliary structure for compiling an expression -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "CExpression.h"
#include "Variable.h"
#include "VariableDefinition.h"
#include "PlaceContents.h"
#include "Net.h"
#include "Transition.h"
#include "Place.h"
#include "Constant.h"
#include "Value.h"
#include "Type.h"

#include <stdio.h>

/** @file CExpression.C
 * Auxiliary structure for compiling expressions
 */

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

/** Flag: generated the evaluating code for an expression */
#define FLAG_COMPUTED 1
/** Flag: generated conversion from an expression result to a number */
#define FLAG_CONVERTED 2
/** Flag: the expression is a multi-set */
#define FLAG_MULTISET 4

CExpression::CExpression (class StringBuffer& decl,
			  const class Net& net,
			  const class Transition* transition) :
  myNumVariables (0), myVariables (0), myFlags (0),
  myNumIterators (0), myIterators (0),
  myVarCount (false), myVarTmpCount (false), myFlag (false), myTmpFlag (false),
  myNumLabels (0), myValuation (0), myMultiset (0), myFatalError (0),
  myOut (), myDecl (decl), myNet (net), myTransition (transition)
{
}

CExpression::~CExpression ()
{
  delete[] myVariables;
  delete[] myFlags;
  delete[] myIterators;
}

/** Get the built-in name of an expression if available
 * @param cexpr		the compilation
 * @param expr		the expression
 * @return		translation for the expression, or NULL
 */
inline static char*
getVariable (const class CExpression& cexpr,
	     const class Expression& expr)
{
  switch (expr.getKind ()) {
  case Expression::eEmptySet:
    return static_cast<char*>(memcpy (new char[2], "0", 2));
  case Expression::ePlaceContents:
    return static_cast<const class PlaceContents&>
      (expr).getPlace ().getMaxNumTokens () == 1
      ? 0
      : static_cast<const class PlaceContents&>(expr).getName (cexpr);
  case Expression::eConstant:
    if (expr.getType ()->isLeaf ()) {
      const class Value& value =
	static_cast<const class Constant&>(expr).getValue ();
      class StringBuffer buf;
      value.compile (buf);
      return buf.copy ();
    }
    // fall through
  default:
    break;
  }
  return 0;
}

bool
CExpression::getVariable (const class Expression& expr,
			  char*& name)
{
  if ((name = ::getVariable (*this, expr)))
    return false;
  unsigned i;
  if (expr.getKind () == Expression::eConstant) {
    for (i = myNet.getNumConstants (); i--; ) {
      if (&myNet.getConstant (i) == &expr) {
	snprintf (name = new char[22], 22, "c%u", i);
	return false;
      }
    }
    if (myTransition) {
      for (i = myTransition->getNumConstants (); i--; ) {
	if (&myTransition->getConstant (i) == &expr) {
	  snprintf (name = new char[23], 23, "c_%u", i);
	  return false;
	}
      }
    }
  }

  bool isNew = true;
  /** flag: generate a set-valued variable? */
  bool isSet = expr.isSet ();

  if (expr.getKind () == Expression::eVariable) {
    const class VariableDefinition& var =
      static_cast<const class Variable&>(expr).getVariable ();
    for (i = myNumIterators; i--; ) {
      if (myIterators[i] == &var) {
	snprintf (name = new char[22], 22, "i%u", i);
	isNew = false;
	goto found;
      }
    }
    assert (!!myValuation);
    size_t len = strlen (myValuation);
    name = new char[len + 23];
    memcpy (name, myValuation, len);
    snprintf (name + len, 23, var.isUndefined () ? ".y%u" : ".x%u",
	      var.getNumber ());
  }
  else
    name = 0;

 found:
  for (i = myNumVariables; i--; ) {
    if (myVariables[i] == &expr) {
      if (!name) snprintf (name = new char[22], 22, isSet ? "m%u" : "x%u", i);
      if (expr.getKind () != Expression::eVariable)
	isNew = !(myFlags[i] & FLAG_COMPUTED);
      myFlags[i] |= FLAG_COMPUTED;
      return isNew;
    }
  }

  if (myNumVariables) {
    const class Expression** variables =
      new const class Expression*[myNumVariables + 1];
    memcpy (variables, myVariables, myNumVariables * sizeof *variables);
    delete[] myVariables;
    myVariables = variables;
    unsigned* flags = new unsigned[myNumVariables + 1];
    memcpy (flags, myFlags, myNumVariables * sizeof *flags);
    delete[] myFlags;
    myFlags = flags;
  }
  else {
    myVariables = new const class Expression*[1];
    myFlags = new unsigned[1];
  }

  if (!name) snprintf (name = new char[22], 22,
		       isSet ? "m%u" : "x%u", myNumVariables);
  myFlags[myNumVariables] = isSet
    ? FLAG_COMPUTED | FLAG_MULTISET
    : FLAG_COMPUTED;
  myVariables[myNumVariables++] = &expr;
  return isNew;
}

bool
CExpression::getVariable (const class Constant& c,
			  char*& name)
{
  unsigned i;
  name = new char[22];

  for (i = myNet.getNumConstants (); i--; ) {
    if (&myNet.getConstant (i) == &c) {
      snprintf (name, 22, "c%u", i);
      return false;
    }
  }

  if (myTransition) {
    for (i = myTransition->getNumConstants (); i--; ) {
      if (&myTransition->getConstant (i) == &c) {
	snprintf (name, 22, "c_%u", i);
	return false;
      }
    }
  }

  for (i = myNumVariables; i--; ) {
    if (myVariables[i] == &c) {
      snprintf (name, 22, "x%u", i);
      return !(myFlags[i] & FLAG_COMPUTED);
    }
  }

  if (myNumVariables) {
    const class Expression** variables =
      new const class Expression*[myNumVariables + 1];
    memcpy (variables, myVariables, myNumVariables * sizeof *variables);
    delete[] myVariables;
    myVariables = variables;
    unsigned* flags = new unsigned[myNumVariables + 1];
    memcpy (flags, myFlags, myNumVariables * sizeof *flags);
    delete[] myFlags;
    myFlags = flags;
  }
  else {
    myVariables = new const class Expression*[1];
    myFlags = new unsigned[1];
  }

  snprintf (name, 22, "x%u", myNumVariables);
  myFlags[myNumVariables] = FLAG_COMPUTED;
  myVariables[myNumVariables++] = &c;
  return true;
}

bool
CExpression::getConverted (const class Expression& expr,
			   char*& name)
{
  assert (!expr.isSet ());

  for (unsigned i = myNumVariables; i--; ) {
    if (myVariables[i] == &expr) {
      assert (!(myFlags[i] & FLAG_MULTISET));
      snprintf (name = new char[22], 22, "n%u", i);
      bool result = myFlags[i] != FLAG_COMPUTED | FLAG_CONVERTED;
      myFlags[i] |= FLAG_CONVERTED;
      return result;
    }
  }

  assert (false);
  return false;
}

char*
CExpression::getIterator (const class VariableDefinition& var)
{
  assert (!var.getNumber ());
  char* name = new char[22];
  for (unsigned i = myNumIterators; i--; ) {
    if (myIterators[i] == &var) {
      snprintf (name, 22, "i%u", i);
      return name;
    }
  }
  if (myNumIterators) {
    const class VariableDefinition** iterators =
      new const class VariableDefinition*[myNumIterators + 1];
    memcpy (iterators, myIterators, myNumIterators * sizeof *iterators);
    delete[] myIterators;
    myIterators = iterators;
  }
  else
    myIterators = new const class VariableDefinition*[1];
  snprintf (name, 22, "i%u", myNumIterators);
  myIterators[myNumIterators++] = &var;
  return name;
}

char*
CExpression::isIterator (const class VariableDefinition& var) const
{
  for (unsigned i = myNumIterators; i--; ) {
    if (myIterators[i] == &var) {
      char* name = new char[22];
      snprintf (name, 22, "i%u", i);
      return name;
    }
  }

  return 0;
}

void
CExpression::recycle (const class Expression& expr1,
		      const class Expression& expr2)
{
  unsigned i;
  assert (expr1.getType () == expr2.getType ());
  for (i = myNumVariables; i--; )
    if (myVariables[i] == &expr2)
      return;
  for (i = myNumVariables; i--; )
    if (myVariables[i] == &expr1)
      break;
  assert (i + 1);
  myVariables[i] = &expr2;
  myFlags[i] &= ~FLAG_COMPUTED;
}

unsigned
CExpression::getCheckpoint (bool*& variables) const
{
  variables = new bool[myNumVariables];
  for (unsigned i = myNumVariables; i--; )
    variables[i] = bool (myFlags[i] & FLAG_COMPUTED);
  return myNumVariables;
}

void
CExpression::setCheckpoint (unsigned indent,
			    const bool* variables,
			    unsigned number,
			    bool clear)
{
  assert (number <= myNumVariables);
  register unsigned i;
  for (i = myNumVariables; i-- > number; ) {
    if (myFlags[i] & FLAG_COMPUTED && myVariables[i]->isSet ()) {
      myOut.indent (indent);
      myOut.append ("FREE (m"), myOut.append (i), myOut.append (");\n");
    }
    if (clear) myFlags[i] &= ~FLAG_COMPUTED;
  }
  if (!number) return;
  for (; i; i--) {
    if (!variables[i]) {
      if (myFlags[i] & FLAG_COMPUTED && myVariables[i]->isSet ()) {
	myOut.indent (indent);
	myOut.append ("FREE (m"), myOut.append (i), myOut.append (");\n");
      }
      if (clear) myFlags[i] &= ~FLAG_COMPUTED;
    }
  }
}

void
CExpression::compileError (unsigned indent, enum Error error)
{
  const char* err = 0;
  switch (error) {
  case errNone: err = "errNone"; break;
  case errConst: err = "errConst"; break;
  case errVar: err = "errVar"; break;
  case errUndef: err = "errUndef"; break;
  case errFatal: err = "errFatal"; break;
  case errDiv0: err = "errDiv0"; break;
  case errOver: err = "errOver"; break;
  case errMod: err = "errMod"; break;
  case errShift: err = "errShift"; break;
  case errUnion: err = "errUnion"; break;
  case errBuf: err = "errBuf"; break;
  case errCard: err = "errCard"; break;
  case errComp: err = "errComp"; break;
  }
  assert (!!err);
  /** flag: was any multi-set clean-up code generated? */
  bool cleanup = false;
  for (unsigned i = 0; i < myNumVariables; i++) {
    if (myFlags[i] & FLAG_COMPUTED && myVariables[i]->isSet ()) {
      if (!cleanup) {
	myOut.indent (indent - 2), myOut.append ("{\n");
	cleanup = true;
      }
      myOut.indent (indent);
      myOut.append ("FREE (m"), myOut.append (i), myOut.append (");\n");
    }
  }
  myOut.indent (indent);
  if (error == errFatal && myFatalError)
    myOut.append (myFatalError);
  else
    myOut.append ("ERROR ("), myOut.append (err), myOut.append (");\n");
  if (cleanup)
    myOut.indent (indent - 2), myOut.append ("}\n");
}

void
CExpression::compileCleanup (unsigned indent)
{
  for (unsigned i = 0; i < myNumVariables; i++) {
    if (myFlags[i] & FLAG_COMPUTED && myVariables[i]->isSet ()) {
      myFlags[i] &= ~FLAG_COMPUTED;
      myOut.indent (indent);
      myOut.append ("FREE (m"), myOut.append (i), myOut.append (");\n");
    }
  }
}

const char*
CExpression::getVarCount ()
{
  return myVarCount = true, "count";
}

const char*
CExpression::getVarTmpCount ()
{
  return myVarTmpCount = true, "tcount";
}

const char*
CExpression::getFlag ()
{
  return myFlag = true, "flag";
}

const char*
CExpression::getTmpFlag ()
{
  return myTmpFlag = true, "flag2";
}

char*
CExpression::getLabel ()
{
  char* label = new char[22];
  snprintf (label, 22, "l%u", ++myNumLabels);
  return label;
}

void
CExpression::generate ()
{
  unsigned i;
  for (i = 0; i < myNumVariables; i++) {
    if (myFlags[i] & FLAG_CONVERTED) {
      myDecl.indent (2);
      myDecl.append ("card_t n");
      myDecl.append (i);
      myDecl.append (";\n");
    }
    switch (myVariables[i]->getKind ()) {
    case Expression::eVariable:
    case Expression::eEmptySet:
      continue;
    default:
      break;
    }
    myDecl.indent (2);
    if (myFlags[i] & FLAG_MULTISET) {
      myVariables[i]->getType ()->appendMSetName (myDecl);
      myDecl.append ("* m");
    }
    else {
      myVariables[i]->getType ()->appendName (myDecl);
      myDecl.append (" x");
    }
    myDecl.append (i);
    if (myFlags[i] & FLAG_MULTISET)
      myDecl.append (" = 0");
    myDecl.append (";\n");
  }

  if (myVarCount || myVarTmpCount) {
    myDecl.indent (2);
    myDecl.append ("card_t ");
    if (myVarCount) {
      myDecl.append (getVarCount ());
      if (myVarTmpCount) {
	myDecl.append (", ");
	myDecl.append (getVarTmpCount ());
      }
    }
    else
      myDecl.append (getVarTmpCount ());
    myDecl.append (";\n");
  }

  if (myFlag || myTmpFlag) {
    myDecl.indent (2);
    myDecl.append ("bool_t ");
    if (myFlag) {
      myDecl.append (getFlag ());
      if (myTmpFlag) {
	myDecl.append (", ");
	myDecl.append (getTmpFlag ());
      }
    }
    else
      myDecl.append (getTmpFlag ());
    myDecl.append (";\n");
  }

  myDecl.append (myOut);

  delete[] myVariables;
  delete[] myFlags;
  delete[] myIterators;
  myNumVariables = 0, myVariables = 0, myFlags = 0;
  myNumIterators = 0, myIterators = 0;
  myVarCount = myVarTmpCount = myFlag = myTmpFlag = false;
  myNumLabels = 0;
  myOut.create (0);
}