// Vector type class -*- c++ -*-

#ifndef VECTORTYPE_H_
# define VECTORTYPE_H_
# ifdef __GNUC__
#  pragma interface
# endif // __GNUC__

# include "Type.h"

/** @file VectorType.h
 * Array data type
 */

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

/** Vector (array) type */
class VectorType : public Type
{
public:
  /** Constructor
   * @param itemType	The vector item type
   * @param indexType	The vector index type
   */
  VectorType (const class Type& itemType,
	      const class Type& indexType) :
    Type (itemType.isOrdered ()),
    myItemType (&itemType), myIndexType (&indexType) {
    assert (myItemType && myIndexType);
    assert (myIndexType->isOrdered ());
#ifndef NDEBUG
    card_t size = myIndexType->getNumValues ();
    assert (size > 0 && size < CARD_T_MAX);
#endif // NDEBUG
  }
  /** Copy constructor */
  VectorType (const class VectorType& old) :
    Type (old), myItemType (old.myItemType), myIndexType (old.myIndexType) {
    assert (myItemType && myIndexType);
    assert (myIndexType->isOrdered ());
#ifndef NDEBUG
    card_t size = myIndexType->getNumValues ();
    assert (size > 0 && size < CARD_T_MAX);
#endif // NDEBUG
  }
private:
  /** Assignment operator */
  class VectorType& operator= (const class VectorType& old);
public:
  /** Destructor */
  ~VectorType () {}
  /** Copy the Type */
  class Type* copy () const { return new class VectorType (*this); }

  /** Determine the kind of the type */
  enum Kind getKind () const { return tVector; }

  /** Get the item type */
  const class Type& getItemType () const { return *myItemType; }
  /** Get the index type */
  const class Type& getIndexType () const { return *myIndexType; }
  /** Determine the vector size */
  card_t getSize () const { return myIndexType->getNumValues (); }

  /** Get the first value of this type */
  class Value& getFirstValue () const;
  /** Get the last value of this type */
  class Value& getLastValue () const;

  /** Convert a value of this type to a number
   * @param value	value to be converted
   * @return		number between 0 and getNumValues () - 1
   */
  card_t convert (const class Value& value) const;

  /** Convert a number to a value of this type
   * @param number	number between 0 and getNumValues () - 1
   * @return		the corresponding value
   */
  class Value* convert (card_t number) const;

  /** See if the type is assignable to another type
   * @param type	the type this type should be assignable to
   * @return		true if this type is assignable to the type
   */
  bool isAssignable (const class Type& type) const;

  /** See if the type is always assignable to another type
   * @param type	the type this type should always be assignable to
   * @return		true if this type always is assignable to the type
   */
  bool isAlwaysAssignable (const class Type& type) const;

  /** Determine whether a value is compatible with the constraints of this type
   * @param value	value to check
   * @return		true if the value passes the constraint check
   */
  bool isConstrained (const class Value& value) const;

  /** Get the number of possible values for this type */
  card_t do_getNumValues () const;

# ifdef EXPR_COMPILE
  /** Generate a C type declaration and auxiliary functions
   * @param out		output stream for the declarations
   */
  void compile (class StringBuffer& out);

  /** Generate a C type declaration
   * @param out		output stream for the declarations
   * @param indent	indentation level
   */
  void compileDefinition (class StringBuffer& out,
			  unsigned indent) const;

  /** Generate equality or inequality comparison expression
   * @param out		output stream
   * @param indent	indentation level
   * @param left	left-hand-side C expression to be compared
   * @param right	right-hand-side C expression to be compared
   * @param equal	type of comparison: true=equality, false=inequality
   * @param first	flag: first component (no indentation)
   * @param last	flag: last component (no expression chaining)
   * @param backslash	flag: prepend all newlines with backslashes
   * @return		true if any code was generated
   */
  bool compileEqual (class StringBuffer& out,
		     unsigned indent,
		     const char* left,
		     const char* right,
		     bool equal,
		     bool first,
		     bool last,
		     bool backslash) const;

  /** Generate three-way comparison statements
   * @param out		output stream
   * @param condition	additional condition for the comparison (NULL=none)
   * @param component	component to be compared
   */
  void compileCompare3 (class StringBuffer& out,
			const char* condition,
			const char* component) const;

  /** Generate statements for incrementing an unconstrained value
   * @param out		output stream
   * @param indent	indentation level
   * @param lvalue	variable to receive the result
   * @param rvalue	variable whose successor is to be computed
   * @param wrap	overflow flag variable (NULL=omit overwrap code)
   */
  void do_compileSuccessor (class StringBuffer& out,
			    unsigned indent,
			    const char* lvalue,
			    const char* rvalue,
			    const char* wrap) const;

  /** Generate statements for decrementing an unconstrained value
   * @param out		output stream
   * @param indent	indentation level
   * @param lvalue	variable to receive the result
   * @param rvalue	variable whose predecessor is to be computed
   * @param wrap	overflow flag variable (NULL=omit overwrap code)
   */
  void do_compilePredecessor (class StringBuffer& out,
			      unsigned indent,
			      const char* lvalue,
			      const char* rvalue,
			      const char* wrap) const;

  /** Emit code for converting a value of this type to another
   * @param cexpr	the compilation
   * @param indent	indentation level
   * @param target	target type
   * @param lvalue	left-hand-side value of the assignment
   * @param rvalue	C expression for the value to be converted
   */
  void compileCast (class CExpression& cexpr,
		    unsigned indent,
		    const class Type& target,
		    const char* lvalue,
		    const char* rvalue) const;

  /** Emit code for converting an unconstrained value to a number
   * @param out		output stream
   * @param indent	indentation level
   * @param value	value to be converted
   * @param number	number to be computed
   * @param add		flag: add to number instead of assigning
   */
  void do_compileConversion (class StringBuffer& out,
			     unsigned indent,
			     const char* value,
			     const char* number,
			     bool add) const;

  /** Emit code for converting a number to a value
   * @param out		output stream
   * @param indent	indentation level
   * @param number	number to be converted
   * @param value	value to be computed
   */
  void compileReverseConversion (class StringBuffer& out,
				 unsigned indent,
				 const char* number,
				 const char* value) const;

  /** Emit code for encoding a value
   * @param cexpr	the compilation
   * @param indent	indentation level
   * @param func	name of the encoding function
   * @param value	value to be encoded
   */
  void compileEncoder (class CExpression& cexpr,
		       unsigned indent,
		       const char* func,
		       const char* value) const;

  /** Emit code for decoding a value
   * @param cexpr	the compilation
   * @param indent	indentation level
   * @param func	name of the decoding function
   * @param value	value to be decoded
   */
  void compileDecoder (class CExpression& cexpr,
		       unsigned indent,
		       const char* func,
		       const char* value) const;
# endif // EXPR_COMPILE

  /** Display the type definition
   * @param printer	the printer object
   */
  void display (const class Printer& printer) const;

private:
  /** The item type */
  const class Type* myItemType;
  /** The index type */
  const class Type* myIndexType;
};

#endif // VECTORTYPE_H_