// Data type base class -*- c++ -*-

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

# include "util.h"
# include <string.h>
# include <assert.h>

/** @file Type.h
 * Abstract base class for data types
 */

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

/** Data type base class */
class Type
{
public:
  /** Type kinds (@see getKind) */
  enum Kind {
    tInt, tCard, tBool, tChar, tEnum, tId, tStruct, tVector, tUnion, tBuffer
  };

  /** Constructor
   * @param ordered	flag: is this an ordered type?
   */
  Type (bool ordered);
protected:
  /** Copy constructor */
  Type (const class Type& old);
private:
  /** Assignment operator */
  class Type& operator= (const class Type& old);
public:
  /** Destructor */
  virtual ~Type ();
  /** Copy Type */
  virtual class Type* copy () const = 0;

  /** Determine the kind of the type */
  virtual enum Kind getKind () const = 0;

  /** Set the name of the type */
  void setName (char* name) { assert (!myName); myName = name; }
  /** Determine the name of the type */
  const char* getName () const { return myName; }

  /** Determine the syntactic name of the type */
  const char* getSyntacticName () const;

  /** Determine whether the type is ordered */
  bool isOrdered () const { return myIsOrdered; }
  /** Get the first value of this type (only for ordered types) */
  virtual class Value& getFirstValue () const = 0;
  /** Get the last value of this type (only for ordered types) */
  virtual class Value& getLastValue () const = 0;

  /** 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
   */
  virtual 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
   */
  virtual bool isAlwaysAssignable (const class Type& type) const;

  /** See if two types are assignable to each other
   * @param type1	first type to be checked
   * @param type2	second type to be checked
   * @return 		true if the types are compatible with each other
   */
  static bool isCompatible (const class Type& type1, const class Type& type2) {
    return type1.isAssignable (type2) && type2.isAssignable (type1);
  }

  /** See if two types always are assignable to each other
   * @param type1	first type to be checked
   * @param type2	second type to be checked
   * @return 		true if the types always are compatible with each other
   */
  static bool isAlwaysCompatible (const class Type& type1,
				  const class Type& type2) {
    return
      type1.isAlwaysAssignable (type2) && type2.isAlwaysAssignable (type1);
  }

  /** 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
   */
  virtual bool isConstrained (const class Value& value) const;

  /**
   * Determine the number of possible values for this type or CARD_T_MAX,
   * if there are >= CARD_T_MAX possible values
   * @return            number of possible values
   */
  card_t getNumValues () const {
    if (myNumValues);
    else if (myConstraint)
      myNumValues = getNumConstrainedValues ();
    else
      myNumValues = do_getNumValues ();
    assert (myNumValues);
    return myNumValues;
  }

private:
  /**
   * Determine the number of possible values for this constrained type
   * @return            number of possible values
   */
  card_t getNumConstrainedValues () const;

  /** Determine the number of possible values for this type or CARD_T_MAX,
   * if there are >= CARD_T_MAX possible values
   * @return		number of possible values
   */
  virtual card_t do_getNumValues () const = 0;
public:

  /** Set the constraint */
  void setConstraint (class Constraint& constraint);

  /** Get the constraint */
  const class Constraint* getConstraint () const { return myConstraint; }
  /** Get the constraint */
  class Constraint* getConstraint () { return myConstraint; }

  /** Convert a value of this type to a number
   * @param value	value to be converted
   * @return		number between 0 and getNumValues () - 1
   */
  virtual 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
   */
  virtual class Value* convert (card_t number) const;

  /** Determine whether this is a leaf type */
  bool isLeaf () const {
    switch (getKind ()) {
    case tInt: case tCard: case tBool: case tChar: case tEnum: case tId:
      return true;
    case tStruct: case tVector: case tUnion: case tBuffer:
      return false;
    }
    assert (false);
    return false;
  }

# ifdef EXPR_COMPILE
  /** Get the type this is derived from, or NULL */
  const class Type* getFather () const { return myFather; }
  /** Cancel the compilation */
  void uncompile ();
  /** Determine if the comparison code for the type has been generated */
  bool isGenerated ();
  /** Reset the counter of compiled types */
  static void uncompileAll ();

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

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

  /** Generate auxiliary definitions
   * @param out		output stream for the declarations
   * @param indent	indentation level
   * @param interface	flag: generate interface declarations
   */
  virtual void compileExtraDefinitions (class StringBuffer& out,
					unsigned indent,
					bool interface) 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
   */
  virtual 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
   */
  void compileCompare3 (class StringBuffer& out) const {
    compileCompare3 (out, 0, "");
  }

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

  /** Generate statements for incrementing a 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 compileSuccessor (class StringBuffer& out,
			 unsigned indent,
			 const char* lvalue,
			 const char* rvalue,
			 const char* wrap) const;

  /** Generate statements for decrementing a 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 compilePredecessor (class StringBuffer& out,
			   unsigned indent,
			   const char* lvalue,
			   const char* rvalue,
			   const char* wrap) 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)
   */
  virtual 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)
   */
  virtual void do_compilePredecessor (class StringBuffer& out,
				      unsigned indent,
				      const char* lvalue,
				      const char* rvalue,
				      const char* wrap) const;

  /** Emit an assignment to the first value of the compiled type
   * @param out		output stream
   * @param indent	indentation level (0=generate a compound expression)
   * @param value	value to be assigned to
   */
  void compileBottom (class StringBuffer& out,
		      unsigned indent,
		      const char* value) const;

  /** Emit an assignment to the last value of the compiled type
   * @param out		output stream
   * @param indent	indentation level (0=generate a compound expression)
   * @param value	value to be assigned to
   */
  void compileTop (class StringBuffer& out,
		   unsigned indent,
		   const char* value) 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
   */
  virtual void compileCast (class CExpression& cexpr,
			    unsigned indent,
			    const class Type& target,
			    const char* lvalue,
			    const char* rvalue) const;

  /** Emit code for converting a 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 compileConversion (class StringBuffer& out,
			  unsigned indent,
			  const char* value,
			  const char* number,
			  bool add) 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
   */
  virtual void do_compileConversion (class StringBuffer& out,
				     unsigned indent,
				     const char* value,
				     const char* number,
				     bool add) const = 0;

  /** 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
   */
  virtual 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
   */
  virtual 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
   */
  virtual void compileDecoder (class CExpression& cexpr,
			       unsigned indent,
			       const char* func,
			       const char* value) const;

  /** Emit the index of the compiled type
   * @param out		output stream
   */
  void appendIndex (class StringBuffer& out) const;

  /** Emit the name of the compiled type
   * @param out		output stream
   */
  void appendName (class StringBuffer& out) const;

  /** Emit the name of the compiled multi-set type
   * @param out		output stream
   */
  void appendMSetName (class StringBuffer& out) const;
# endif // EXPR_COMPILE

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

private:
  /** Number of possible values in the type */
  mutable card_t myNumValues;
  /** Name of the type (may be NULL) */
  char* myName;
  /** Flag: is the type ordered? */
  const bool myIsOrdered;
protected:
  /** Constraint associated with the type */
  class Constraint* myConstraint;
# ifdef EXPR_COMPILE
  /** Index number of the compiled type */
  unsigned myIndex;
  /** Flag: have the comparison functions been generated? */
  bool myGenerated;
  /** Original type */
  const class Type* myFather;
# endif // EXPR_COMPILE
};

#endif // TYPE_H_