type.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file type.h
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Dec 12 12:53:28 2002
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

// expr.h Has to be included outside of #ifndef, since it sources us
// recursively (read comments in expr_value.h).
#include "expr.h"

#ifndef _cvcl__include__type_h_
#define _cvcl__include__type_h_

#include <string>
#include <iostream>
#include <vector>
#include "expr_manager.h"

namespace CVCL {

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Type                                                               //
// Author: Clark Barrett                                                     //
// Created: Thu Dec 12 12:53:34 2002                                         //
// Description: Wrapper around expr for api                                  //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class Type {
  Expr d_expr;

public:
  Type() {}
  Type(Expr expr) : d_expr(expr) {}
  const Expr& getExpr() const { return d_expr; }

  // Core testers

  bool isType() const { return d_expr.getKind() == TYPE; }
  bool isBool() const { return d_expr.getKind() == BOOLEAN; }
/*   bool isReal() const { return d_expr.getKind() == REAL; } */
/*   bool isInt() const { return d_expr.getKind() == INT; } */
/*   bool isSubrange() const { return d_expr.getKind() == SUBRANGE; } */
  bool isSubtype() const { return d_expr.getKind() == SUBTYPE; }
/*   bool isTuple() const { return d_expr.getKind() == TUPLE_TYPE; } */
  bool isFunction() const { return d_expr.getKind() == ARROW; }
/*   bool isRecord() const {return d_expr.getKind() == RECORD_TYPE; } */
  bool isTypeDecl() const {return d_expr.getKind() == TYPEDECL; }
  bool isNull() const { return d_expr.isNull(); }
  bool isFinite() const {return isBool();}

  int arity() const { return d_expr.arity(); }
  Type operator[](int i) const { return Type(d_expr[i]); }

  const std::string& getTypeDeclName() const {
    DebugAssert(isTypeDecl(),"TypeDecl expected");
    return d_expr[0].getString();
  }

  // Core constructors

  static Type typeBool(ExprManager* em) { return Type(em->boolExpr()); }
//   static Type typeReal(ExprManager* em) { return Type(newExpr(em, REAL)); }
//   static Type typeInt(ExprManager* em) { return Type(newExpr(em, INT)); }
//   static Type typeSubrange(const Expr& l, const Expr& r) {
//     return Type(newExpr(l.getEM(), SUBRANGE, l, r));
//   }
//   Type tupleType(const Type& type1) const
//     { return Type(newExpr(d_expr.getEM(), TUPLE_TYPE, d_expr, type1.d_expr)); }
//   Type tupleType(const Type& type1, const Type& type2) const
//     { return Type(newExpr(d_expr.getEM(), TUPLE_TYPE, d_expr,
//                        type1.d_expr, type2.d_expr)); }
//   static Type tupleType(const std::vector<Type>& types) {
//     DebugAssert(types.size() > 0, "tupleType()");
//     std::vector<Expr> eVec;
//     for (unsigned i=0; i < types.size(); i++) eVec.push_back(types[i].d_expr);
//     return Type(newExpr(types[0].getExpr().getEM(), TUPLE_TYPE, eVec));
//   }
  Type funType(const Type& typeRan) const
    { return Type(newExpr(d_expr.getEM(), ARROW, d_expr, typeRan.d_expr)); }

  // Printing
  std::string toString() const { return getExpr().toString(); }
};

//! n-ary function type
Type funType(const std::vector<Type>& typeDom, const Type& typeRan);

inline bool operator==(const Type& t1, const Type& t2)
{ return t1.getExpr() == t2.getExpr(); }

inline bool operator!=(const Type& t1, const Type& t2)
{ return t1.getExpr() != t2.getExpr(); }

// Printing
inline std::ostream& operator<<(std::ostream& os, const Type& t) {
  return os << t.getExpr();
}

}

#endif

---