src/expr/type.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** type.h
   3  ** Original author: cconway
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Interface for expression types
  14  **/
  15
  16 #ifndef __CVC4__TYPE_H
  17 #define __CVC4__TYPE_H
  18
  19 #include "cvc4_config.h"
  20
  21 #include <string>
  22 #include <vector>
  23
  24 namespace CVC4 {
  25
  26 class ExprManager;
  27
  28 /**
  29  * Class encapsulating CVC4 expression types.
  30  */
  31 class Type {
  32 public:
  33   /** Comparision for equality */
  34   bool operator==(const Type& t) const;
  35
  36   /** Comparison for disequality */
  37   bool operator!=(const Type& e) const;
  38
  39   /** Get the ExprManager associated with this type. May be NULL for
  40       singleton types. */
  41   ExprManager* getExprManager() const;
  42
  43   /** Get the name of this type. May be empty for composite types. */
  44   std::string getName() const;
  45
  46   /** Is this the boolean type? */
  47   virtual bool isBoolean() const {
  48     return false;
  49   }
  50
  51   /** Is this a function type? */
  52   virtual bool isFunction() const {
  53     return false;
  54   }
  55
  56   /** Is this a predicate type? NOTE: all predicate types are also
  57       function types. */
  58   virtual bool isPredicate() const {
  59     return false;
  60   }
  61
  62   /** Is this a kind type (i.e., the type of a type)? */
  63   virtual bool isKind() const {
  64     return false;
  65   }
  66
  67   /** Outputs a string representation of this type to the stream. */
  68   virtual void toStream(std::ostream& out) const {
  69     out << getName();
  70   }
  71
  72 protected:
  73   /** Create a type associated with exprManager. */
  74   Type(ExprManager* const exprManager);
  75
  76   /** Create a type associated with exprManager with the given name. */
  77   Type(ExprManager* const exprManager, std::string name);
  78
  79   /** Create a type with the given name. */
  80   Type(std::string name);
  81
  82   /** Destructor */
  83   virtual ~Type() { };
  84
  85   /** The associated ExprManager */
  86   ExprManager* d_exprManager;
  87
  88   /** The name of the type (may be empty). */
  89   std::string d_name;
  90 };
  91
  92 /**
  93  * Singleton class encapsulating the boolean type.
  94  */
  95 class BooleanType : public Type {
  96
  97 public:
  98   static BooleanType* getInstance();
  99
 100   /** Is this the boolean type? (Returns true.) */
 101   bool isBoolean() const;
 102
 103 private:
 104   /** Create a type associated with exprManager. */
 105   BooleanType();
 106
 107   /** Do-nothing private copy constructor operator, to prevent
 108       copy-construction. */
 109   BooleanType(const BooleanType&);
 110
 111   /** Destructor */
 112   ~BooleanType();
 113
 114   /** Do-nothing private assignment operator, to prevent
 115      assignment. */
 116   BooleanType& operator=(const BooleanType&);
 117
 118   /** The singleton instance */
 119   static BooleanType s_instance;
 120 };
 121
 122 /**
 123  * Class encapsulating a function type.
 124  * TODO: Override == to check component types?
 125  */
 126 class FunctionType : public Type {
 127
 128 public:
 129   static FunctionType* getInstance(ExprManager* exprManager,
 130                                    const Type* domain,
 131                                    const Type* range);
 132
 133   static FunctionType* getInstance(ExprManager* exprManager,
 134                                    const std::vector<const Type*>& argTypes,
 135                                    const Type* range);
 136
 137
 138   /** Retrieve the argument types. The vector will be non-empty. */
 139   const std::vector<const Type*> getArgTypes() const;
 140
 141   /** Get the range type (i.e., the type of the result). */
 142   const Type* getRangeType() const;
 143
 144   /** Is this as function type? (Returns true.) */
 145   bool isFunction() const;
 146
 147   /** Is this as predicate type? (Returns true if range is
 148       boolean.) */
 149   bool isPredicate() const;
 150
 151   /** Outputs a string representation of this type to the stream,
 152       in the format "D -> R" or "(A, B, C) -> R". */
 153   void toStream(std::ostream& out) const;
 154
 155 private:
 156
 157   /** Construct a function type associated with exprManager,
 158       given a vector of argument types and the range type.
 159
 160       @param argTypes a non-empty vector of input types
 161       @param range the result type
 162   */
 163   FunctionType(ExprManager* exprManager,
 164                const std::vector<const Type*>& argTypes,
 165                const Type* range);
 166
 167   /** Destructor */
 168   ~FunctionType();
 169
 170   /** The list of input types. */
 171   const std::vector<const Type*> d_argTypes;
 172
 173   /** The result type. */
 174   const Type* d_rangeType;
 175
 176 };
 177
 178
 179 /** Class encapsulating the kind type (the type of types).
 180     TODO: Should be a singleton per-ExprManager.
 181 */
 182 class KindType : public Type {
 183
 184 public:
 185
 186   /** Create a type associated with exprManager. */
 187   static KindType* getInstance();
 188
 189   /** Is this the kind type? (Returns true.) */
 190   bool isKind() const;
 191
 192 private:
 193
 194   /** Create a type associated with exprManager. */
 195   KindType();
 196
 197   /* Do-nothing private copy constructor, to prevent
 198      copy construction. */
 199   KindType(const KindType&);
 200
 201   /** Destructor */
 202   ~KindType();
 203
 204   /* Do-nothing private assignment operator, to prevent
 205      assignment. */
 206   KindType& operator=(const KindType&);
 207
 208   /** The singleton instance */
 209   static KindType s_instance;
 210 };
 211
 212 /** Class encapsulating a user-defined sort.
 213     TODO: Should sort be uniquely named per-exprManager and not conflict
 214     with any builtins? */
 215 class SortType : public Type {
 216
 217 public:
 218
 219   /** Create a sort associated with exprManager with the given name. */
 220   SortType(ExprManager* exprManager, std::string name);
 221
 222   /** Destructor */
 223   ~SortType();
 224 };
 225
 226 /**
 227  * Output operator for types
 228  * @param out the stream to output to
 229  * @param e the type to output
 230  * @return the stream
 231  */
 232 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 233
 234 }
 235
 236 #endif /* __CVC4__TYPE_H */