// Maria if-then-else expression class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "IfThenElse.h"
#include "Type.h"
#include "Printer.h"

/** @file IfThenElse.C
 * Selection expression
 */

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

IfThenElse::IfThenElse (class Expression& condition,
			class ExpressionList& exprList) :
  Expression (),
  myCondition (&condition), myExprList (&exprList)
{
  assert (myCondition->getType ()->getNumValues () == exprList.size ());
  setType (*myExprList->getType ());
}

IfThenElse::~IfThenElse ()
{
  myCondition->destroy ();
  myExprList->destroy ();
}

bool
IfThenElse::isBasic () const
{
  return
    myCondition->isBasic () &&
    myExprList->isBasic ();
}

bool
IfThenElse::isTemporal () const
{
  return
    myCondition->isTemporal () ||
    myExprList->isTemporal ();
}

bool
IfThenElse::isSet () const
{
  return myExprList->isSet ();
}

void
IfThenElse::setType (const class Type& type)
{
  Expression::setType (type);
  assert (myExprList->getType () == &type);
}

class Value*
IfThenElse::do_eval (const class Valuation& valuation) const
{
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    return (*myExprList)[i].eval (valuation);
  }
  else
    return NULL;
}

class PlaceMarking*
IfThenElse::meval (const class Valuation& valuation) const
{
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    return (*myExprList)[i].meval (valuation);
  }
  else
    return NULL;
}

class Expression*
IfThenElse::ground (const class Valuation& valuation,
		    class Transition* transition,
		    bool declare)
{
  class Expression* expr = NULL;
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    if (!(expr = (*myExprList)[i].ground (valuation, transition, declare)))
      return NULL;
  }
  else {
    assert (!valuation.isOK ());
    valuation.clearErrors ();
    class Expression* condition =
      myCondition->ground (valuation, transition, declare);
    if (!condition) return NULL;
    class ExpressionList* exprList =
      myExprList->ground (valuation, transition, declare);
    if (!exprList) { condition->destroy (); return NULL; }

    if (condition == myCondition && exprList == myExprList) {
      condition->destroy ();
      exprList->destroy ();

      return copy ();
    }
    else
      expr = (new class IfThenElse (*condition, *exprList))->cse ();
  }

  return expr->ground (valuation);
}

class Expression*
IfThenElse::substitute (class Substitution& substitution)
{
  class Expression* condition = myCondition->substitute (substitution);
  class ExpressionList* exprList = myExprList->substitute (substitution);

  if (condition == myCondition && exprList == myExprList) {
    condition->destroy ();
    exprList->destroy ();

    return copy ();
  }
  else
    return (new class IfThenElse (*condition, *exprList))->cse ();
}

bool
IfThenElse::depends (const class VariableSet& vars,
		     bool complement) const
{
  return
    myCondition->depends (vars, complement) ||
    myExprList->depends (vars, complement);
}

bool
IfThenElse::forExpressions (bool (*operation)
			    (const class Expression&,void*),
			    void* data) const
{
  return
    (*operation) (*this, data) &&
    myCondition->forExpressions (operation, data) &&
    myExprList->forExpressions (operation, data);
}

#ifdef EXPR_COMPILE
# include "CExpression.h"

void
IfThenElse::compile (class CExpression& cexpr,
		     unsigned indent,
		     const char* lvalue,
		     const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* cond;
  if (cexpr.getVariable (*myCondition, cond))
    myCondition->compile (cexpr, indent, cond, vars);
  char* condconv = 0;
  if (!getType ()->isLeaf () &&
      cexpr.getConverted (*myCondition, condconv))
    myCondition->getType ()->compileConversion (out, indent,
						cond, condconv, false);
  bool* checkpoint;
  unsigned checkpointSize = cexpr.getCheckpoint (checkpoint);
  out.indent (indent);
  out.append ("switch (");
  if (getType ()->isLeaf ())
    out.append (cond);
  else
    out.append (condconv);
  out.append (") {\n");
  for (card_t i = 0; i < myExprList->size (); i++) {
    out.indent (indent);
    out.append ("case ");
    if (getType ()->isLeaf ()) {
      class Value* v = myCondition->getType ()->convert (i);
      v->compile (out);
      delete v;
    }
    else
      out.append (i);
    out.append (":\n");
    (*myExprList)[i].compile (cexpr, indent + 2, lvalue, vars);
    cexpr.setCheckpoint (indent + 2, checkpoint, checkpointSize);
    out.indent (indent + 2);
    out.append ("break;\n");
  }
  out.indent (indent);
  out.append ("}\n");
  delete[] checkpoint;
  delete[] cond;
  delete[] condconv;
}

void
IfThenElse::compileMset (class CExpression& cexpr,
			 unsigned indent,
			 const char* resulttype,
			 const char* result,
			 const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* cond;
  if (cexpr.getVariable (*myCondition, cond))
    myCondition->compile (cexpr, indent, cond, vars);
  char* condconv = 0;
  if (!getType ()->isLeaf () &&
      cexpr.getConverted (*myCondition, condconv))
    myCondition->getType ()->compileConversion (out, indent,
						cond, condconv, false);
  bool* checkpoint;
  unsigned checkpointSize = cexpr.getCheckpoint (checkpoint);
  out.indent (indent);
  out.append ("switch (");
  if (getType ()->isLeaf ())
    out.append (cond);
  else
    out.append (condconv);
  out.append (") {\n");
  for (card_t i = 0; i < myExprList->size (); i++) {
    out.indent (indent);
    out.append ("case ");
    if (getType ()->isLeaf ()) {
      class Value* v = myCondition->getType ()->convert (i);
      v->compile (out);
      delete v;
    }
    else
      out.append (i);
    out.append (":\n");
    (*myExprList)[i].compileMset (cexpr, indent + 2, resulttype, result, vars);
    cexpr.setCheckpoint (indent + 2, checkpoint, checkpointSize);
    out.indent (indent + 2);
    out.append ("break;\n");
  }
  out.indent (indent);
  out.append ("}\n");
  delete[] checkpoint;
  delete[] cond;
  delete[] condconv;
}

#endif // EXPR_COMPILE

void
IfThenElse::display (const class Printer& printer) const
{
  myCondition->display (printer);
  printer.delimiter ('?');
  for (card_t i = myExprList->size (); i--; ) {
    const class Expression& expr = (*myExprList)[i];
    switch (expr.getKind ()) {
    case Expression::eVariable:
    case Expression::eUndefined:
    case Expression::eStructComponent:
    case Expression::eStructAssign:
    case Expression::eUnionComponent:
    case Expression::eUnionType:
    case Expression::eVectorIndex:
    case Expression::eVectorAssign:
    case Expression::eVectorShift:
    case Expression::eUnop:
    case Expression::eBinop:
    case Expression::eBooleanBinop:
    case Expression::eNot:
    case Expression::eRelop:
    case Expression::eBufferUnop:
    case Expression::eBufferRemove:
    case Expression::eBufferWrite:
    case Expression::eBufferIndex:
    case Expression::eSet:
    case Expression::eTemporalBinop:
    case Expression::eTemporalUnop:
    case Expression::eTypecast:
    case Expression::eCardinality:
    case Expression::eTransitionQualifier:
    case Expression::ePlaceContents:
    case Expression::eSubmarking:
    case Expression::eMapping:
    case Expression::eEmptySet:
      break;
    case Expression::eIfThenElse:
    case Expression::eMarking:
      printer.delimiter ('(')++;
      expr.display (printer);
      --printer.delimiter (')');
      if (i) printer.delimiter (':');
      continue;
    case Expression::eConstant:
    case Expression::eStruct:
    case Expression::eUnion:
    case Expression::eVector:
    case Expression::eBuffer:
      if (const char* name = expr.getType ()->getName ()) {
	printer.printRaw ("is");
	printer.delimiter (' ');
	printer.print (name);
	printer.delimiter (' ');
      }
      else {
	switch (expr.getType ()->getKind ()) {
	case Type::tInt:
	case Type::tCard:
	  printer.printRaw ("is");
	  printer.delimiter (' ');
	  printer.print (expr.getType ()->getSyntacticName ());
	  printer.delimiter (' ');
	  break;
	default:
	  break;
	}
      }
      break;
    }
    expr.display (printer);
    if (i)
      printer.delimiter (':');
  }
}