// Enumerated type class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "EnumType.h"
#include "LeafValue.h"
#include "util.h"
#include "Constraint.h"
#include "Printer.h"

/** @file EnumType.C
 * Enumerated data type
 */

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

EnumType::EnumType () :
  Type (true),
  myEnums (),
  myReverseMap (),
  myNextValue (0)
{
}

EnumType::EnumType (const class EnumType& old) :
  Type (old),
  myEnums (),
  myReverseMap (),
  myNextValue (old.myNextValue)
{
  for (EnumMap::const_iterator i = old.myEnums.begin ();
       i != old.myEnums.end (); i++) {
    char* comp = newString (i->first);
    myEnums[comp] = i->second;
    myReverseMap[i->second] = comp;
  }
}

EnumType::~EnumType ()
{
  for (EnumMap::iterator i = myEnums.begin (); i != myEnums.end (); i++)
    delete[] i->first;
}

void
EnumType::addEnumeration (char* name, card_t value)
{
  assert (!getValue (name));
  assert (!hasValue (value));

  myEnums[name] = value;
  myReverseMap[value] = name;
  assert (myEnums.size () == myReverseMap.size ());

  myNextValue = value + 1;
}

const card_t*
EnumType::getValue (const char* name) const
{
  EnumMap::const_iterator i = myEnums.find (const_cast<char*>(name));
  return i == myEnums.end () ? NULL : &i->second;
}

class Value&
EnumType::getFirstValue () const
{
  const class Value* v = myConstraint ? &myConstraint->getFirstValue () : NULL;
  assert (!v || &v->getType () == this);
  return v
    ? *static_cast<class LeafValue*>(v->copy ())
    : *new class LeafValue (*this, getFirstEnum ());
}

class Value&
EnumType::getLastValue () const
{
  const class Value* v = myConstraint ? &myConstraint->getLastValue () : NULL;
  assert (!v || &v->getType () == this);
  return v
    ? *static_cast<class LeafValue*>(v->copy ())
    : *new class LeafValue (*this, getLastEnum ());
}

card_t
EnumType::getFirstEnum () const
{
  assert (!myReverseMap.empty ());
  return myReverseMap.begin ()->first;
}

card_t
EnumType::getLastEnum () const
{
  assert (!myReverseMap.empty ());
  return (--myReverseMap.end ())->first;
}

bool
EnumType::hasValue (card_t value) const
{
  return myReverseMap.find (value) != myReverseMap.end ();
}

const char*
EnumType::getEnumName (card_t value) const
{
  ReverseMap::const_iterator i = myReverseMap.find (value);
  return (i != myReverseMap.end ()) ? i->second : NULL;
}

bool
EnumType::isConstrained (const class Value& value) const
{
  assert (value.getType ().isAssignable (*this));

  if (!myConstraint) {
    card_t v = card_t (static_cast<const class LeafValue&>(value));
    return v >= getFirstEnum () && v <= getLastEnum ();
  }
  else
    return Type::isConstrained (value);
}

card_t
EnumType::do_getNumValues () const
{
  assert (!myConstraint);
  card_t numValues = getLastEnum () - getFirstEnum ();
  if (numValues < CARD_T_MAX) numValues++;
  return numValues;
}

card_t
EnumType::convert (const class Value& value) const
{
  assert (value.getKind () == Value::vLeaf);
  if (myConstraint)
    return Type::convert (value);
  return
    card_t (static_cast<const class LeafValue&>(value)) - getFirstEnum ();
}

class Value*
EnumType::convert (card_t number) const
{
  assert (number < getNumValues ());
  if (myConstraint)
    return Type::convert (number);
  return new class LeafValue (*this, getFirstEnum () + number);
}

#ifdef EXPR_COMPILE
# include "StringBuffer.h"

void
EnumType::compileDefinition (class StringBuffer& out,
			     unsigned indent) const
{
  out.indent (indent);
  out.append ("unsigned");
}

void
EnumType::do_compileConversion (class StringBuffer& out,
				unsigned indent,
				const char* value,
				const char* number,
				bool add) const
{
  out.indent (indent);
  out.append (number);
  out.append (add ? "+=" : "=");
  out.append (value);
  out.append (";\n");
}

#endif // EXPR_COMPILE

void
EnumType::display (const class Printer& printer) const
{
  printer.printRaw ("enum ");
  printer.delimiter ('{')++;

  ReverseMap::const_iterator i = myReverseMap.begin ();

  if (i != myReverseMap.end ())
    for (;;) {
      ReverseMap::const_iterator j = i++;
      printer.print ((*j).second);
      printer.delimiter ('=');
      printer.print ((*j).first);
      if (i == myReverseMap.end ())
	break;
      printer.delimiter (',');
    }

  --printer.delimiter ('}');

  if (myConstraint)
    myConstraint->display (printer);
}