// Unsigned integer (cardinality) type class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "CardType.h"
#include "LeafValue.h"
#include "Constraint.h"
#include "Range.h"

/** @file CardType.C
 * Unsigned integer data type
 */

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

class Value&
CardType::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, 0);
}

class Value&
CardType::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, CARD_T_MAX);
}

card_t
CardType::do_getNumValues () const
{
  return myConstraint ? myConstraint->getNumValues () : CARD_T_MAX;
}

card_t
CardType::convert (const class Value& value) const
{
  assert (value.getKind () == Value::vLeaf);
  card_t v = card_t (static_cast<const class LeafValue&>(value));
  if (myConstraint) {
    card_t number;
    if (!convert (number, v, *myConstraint))
      assert (false);
    return number;
  }
  else
    return v;
}

class Value*
CardType::convert (card_t number) const
{
  assert (number < static_cast<const class Type*>(this)->getNumValues ());
  return new class LeafValue (*this, myConstraint
			      ? convert (number, *myConstraint)
			      : number);
}

bool
CardType::convert (card_t& number, card_t value, const class Constraint& c)
{
  number = 0;

  for (Constraint::const_iterator i = c.begin (); !(i == c.end ()); i++) {
    const class Range* r = *i;
    card_t lowLimit =
      card_t (static_cast<const class LeafValue&>(r->getLow ()));
    card_t highLimit =
      card_t (static_cast<const class LeafValue&>(r->getHigh ()));

    assert (lowLimit <= highLimit);

    if (value < lowLimit || value > highLimit) {
      if (card_t diff = highLimit - lowLimit + 1)
	number += diff;
      else
	return false;
    }
    else {
      number += value - lowLimit;
      assert (number <= c.getNumValues ());
      return true;
    }
  }

  return false;
}

card_t
CardType::convert (card_t number, const class Constraint& c)
{
  for (Constraint::const_iterator i = c.begin (); !(i == c.end ()); i++) {
    const class Range* r = *i;
    card_t lowLimit =
      card_t (static_cast<const class LeafValue&>(r->getLow ()));
    card_t highLimit =
      card_t (static_cast<const class LeafValue&>(r->getHigh ()));

    assert (lowLimit <= highLimit);

    card_t diff = highLimit - lowLimit;
    if (number <= diff)
      return lowLimit + number;
    else
      number -= diff, number--;
  }

  assert (false);
  return 0;
}

#ifdef EXPR_COMPILE
# include "StringBuffer.h"

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

void
CardType::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");
}

void
CardType::compileConv (class StringBuffer& out,
		       unsigned indent,
		       const class Constraint& c,
		       const char* value,
		       const char* number)
{
  bool next = false;

  for (Constraint::const_iterator i = c.end ();; next = true) {
    const class Range* range = *--i;
    const class Value& low = range->getLow ();
    const class Value& high = range->getHigh ();
    const bool notfirst = i != c.begin ();
    card_t num;
    if (!convert (num,
		  card_t (static_cast<const class LeafValue&>(low)), c))
      assert (false);
    if (notfirst) {
      out.indent (indent);
      if (next)
	out.append ("else ");
      out.append ("if (");
      if (&low == &high)
	low.compileEqual (out, next ? indent + 9 : indent + 4,
			  value, true, true, true);
      else
	low.compileOrder (out, next ? indent + 9 : indent + 4,
			  value, false, true, true, true);
      out.append (")\n");
      indent += 2;
    }
    else if (next)
      out.indent (indent), out.append ("else\n"), indent += 2;

    out.indent (indent);
    if (&low == &high) {
      out.append (number), out.append ("="), out.append (num);
      out.append (";\n");
    }
    else {
      out.append (number), out.append ("=");
      out.append ("(card_t) ("), out.append (value);
      out.append (" - ");
      low.compile (out);
      out.append (")");
      if (num)
	out.append ("+"), out.append (num);
      out.append (";\n");
    }

    if (notfirst || next)
      indent -= 2;
    if (!notfirst)
      break;
  }
}

void
CardType::compileReverseConv (class StringBuffer& out,
			      unsigned indent,
			      const class Constraint& c,
			      const char* number,
			      const char* value)
{
  bool next = false;
  for (Constraint::const_iterator i = c.end (); i != c.begin (); next = true) {
    const class Range* range = *--i;
    const class Value& low = range->getLow ();
    const class Value& high = range->getHigh ();
    card_t num;
    if (!convert (num,
		  card_t (static_cast<const class LeafValue&>(low)), c))
      assert (false);
    if (num) {
      out.indent (indent);
      if (next)
	out.append ("else ");
      out.append ("if ("), out.append (number);
      out.append (&low == &high ? "==" : ">="), out.append (num);
      out.append (")");
    }
    else if (next)
      out.indent (indent), out.append ("else");
    if (num || next)
      out.append (" {\n"), indent += 2;

    low.compileInit (value, indent, out);

    if (&low != &high) {
      out.indent (indent);
      out.append (value);
      out.append ("+=");
      out.append (number);
      if (num)
	out.append ("-"), out.append (num);
      out.append (";\n");
    }

    if (num || next)
      out.indent (indent -= 2), out.append ("}\n");
  }
}

#endif // EXPR_COMPILE