00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef _cvc3__expr_h_
00024 #include "expr.h"
00025 #endif
00026
00027 #ifndef _cvc3__include__type_h_
00028 #define _cvc3__include__type_h_
00029
00030 namespace CVC3 {
00031
00032 #include "os.h"
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042 class CVC_DLL Type {
00043 Expr d_expr;
00044
00045 public:
00046 Type() {}
00047 Type(Expr expr);
00048
00049
00050 Type(const Type& type) :d_expr(type.d_expr) {}
00051 Type(Expr expr, bool dummy) :d_expr(expr) {}
00052 const Expr& getExpr() const { return d_expr; }
00053
00054
00055 int arity() const { return d_expr.arity(); }
00056 Type operator[](int i) const { return Type(d_expr[i]); }
00057
00058
00059 bool isNull() const { return d_expr.isNull(); }
00060 bool isBool() const { return d_expr.getKind() == BOOLEAN; }
00061 bool isSubtype() const { return d_expr.getKind() == SUBTYPE; }
00062 bool isFunction() const { return d_expr.getKind() == ARROW; }
00063
00064
00065 static Type typeBool(ExprManager* em) { return Type(em->boolExpr(), true); }
00066 static Type anyType(ExprManager* em) { return Type(em->newLeafExpr(ANY_TYPE)); }
00067 static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
00068 Type funType(const Type& typeRan) const
00069 { return Type(Expr(ARROW, d_expr, typeRan.d_expr)); }
00070
00071
00072 std::string toString() const { return getExpr().toString(); }
00073 };
00074
00075 inline bool operator==(const Type& t1, const Type& t2)
00076 { return t1.getExpr() == t2.getExpr(); }
00077
00078 inline bool operator!=(const Type& t1, const Type& t2)
00079 { return t1.getExpr() != t2.getExpr(); }
00080
00081
00082 inline std::ostream& operator<<(std::ostream& os, const Type& t) {
00083 return os << t.getExpr();
00084 }
00085
00086 }
00087
00088 #endif