src/util/datatype.i

   1 %{
   2 #include "util/datatype.h"
   3 namespace CVC4 {
   4 //typedef CVC4::Datatype::Constructor DatatypeConstructor;
   5 }
   6 %}
   7
   8 namespace CVC4 {
   9 %rename(DatatypeConstructor) CVC4::Datatype::Constructor;
  10 %rename(DatatypeConstructor) CVC4::Constructor;
  11 }
  12
  13 %extend std::vector< CVC4::Datatype > {
  14   %ignore vector(size_type);
  15 };
  16 %template(vectorDatatype) std::vector< CVC4::Datatype >;
  17
  18 %extend std::vector< CVC4::Datatype::Constructor > {
  19   %ignore vector(size_type);
  20 };
  21 %template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
  22
  23 %rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
  24 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
  25
  26 %rename(beginConst) CVC4::Datatype::begin() const;
  27 %rename(endConst) CVC4::Datatype::end() const;
  28
  29 %rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
  30
  31 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
  32 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
  33 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
  34 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
  35
  36 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
  37 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
  38 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
  39
  40 %feature("valuewrapper") CVC4::Datatype::UnresolvedType;
  41
  42 %include "util/datatype.h"
  43
  44 namespace CVC4 {
  45     class CVC4_PUBLIC Arg {
  46
  47       std::string d_name;
  48       Expr d_selector;
  49       /** the constructor associated with this selector */
  50       Expr d_constructor;
  51       bool d_resolved;
  52
  53       explicit Arg(std::string name, Expr selector);
  54       friend class Constructor;
  55       friend class Datatype;
  56
  57       bool isUnresolvedSelf() const throw();
  58
  59     public:
  60
  61       /** Get the name of this constructor argument. */
  62       std::string getName() const throw();
  63
  64       /**
  65        * Get the selector for this constructor argument; this call is
  66        * only permitted after resolution.
  67        */
  68       Expr getSelector() const;
  69
  70       /**
  71        * Get the associated constructor for this constructor argument;
  72        * this call is only permitted after resolution.
  73        */
  74       Expr getConstructor() const;
  75
  76       /**
  77        * Get the selector for this constructor argument; this call is
  78        * only permitted after resolution.
  79        */
  80       Type getSelectorType() const;
  81
  82       /**
  83        * Get the name of the type of this constructor argument
  84        * (Datatype field).  Can be used for not-yet-resolved Datatypes
  85        * (in which case the name of the unresolved type, or "[self]"
  86        * for a self-referential type is returned).
  87        */
  88       std::string getSelectorTypeName() const;
  89
  90       /**
  91        * Returns true iff this constructor argument has been resolved.
  92        */
  93       bool isResolved() const throw();
  94
  95     };/* class Datatype::Constructor::Arg */
  96
  97   class Constructor {
  98   public:
  99
 100     /** The type for iterators over constructor arguments. */
 101     typedef std::vector<Arg>::iterator iterator;
 102     /** The (const) type for iterators over constructor arguments. */
 103     typedef std::vector<Arg>::const_iterator const_iterator;
 104
 105   private:
 106
 107     std::string d_name;
 108     Expr d_constructor;
 109     Expr d_tester;
 110     std::vector<Arg> d_args;
 111
 112     void resolve(ExprManager* em, DatatypeType self,
 113                  const std::map<std::string, DatatypeType>& resolutions,
 114                  const std::vector<Type>& placeholders,
 115                  const std::vector<Type>& replacements,
 116                  const std::vector< SortConstructorType >& paramTypes,
 117                  const std::vector< DatatypeType >& paramReplacements)
 118       throw(AssertionException, DatatypeResolutionException);
 119     friend class Datatype;
 120
 121     /** @FIXME document this! */
 122     Type doParametricSubstitution(Type range,
 123                                   const std::vector< SortConstructorType >& paramTypes,
 124                                   const std::vector< DatatypeType >& paramReplacements);
 125   public:
 126     /**
 127      * Create a new Datatype constructor with the given name for the
 128      * constructor and the given name for the tester.  The actual
 129      * constructor and tester aren't created until resolution time.
 130      */
 131     explicit Constructor(std::string name, std::string tester);
 132
 133     /**
 134      * Add an argument (i.e., a data field) of the given name and type
 135      * to this Datatype constructor.
 136      */
 137     void addArg(std::string selectorName, Type selectorType);
 138
 139     /**
 140      * Add an argument (i.e., a data field) of the given name to this
 141      * Datatype constructor that refers to an as-yet-unresolved
 142      * Datatype (which may be mutually-recursive).
 143      */
 144     void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
 145
 146     /**
 147      * Add a self-referential (i.e., a data field) of the given name
 148      * to this Datatype constructor that refers to the enclosing
 149      * Datatype.  For example, using the familiar "nat" Datatype, to
 150      * create the "pred" field for "succ" constructor, one uses
 151      * succ::addArg("pred", Datatype::SelfType())---the actual Type
 152      * cannot be passed because the Datatype is still under
 153      * construction.
 154      *
 155      * This is a special case of
 156      * Constructor::addArg(std::string, Datatype::UnresolvedType).
 157      */
 158     void addArg(std::string selectorName, Datatype::SelfType);
 159
 160     /** Get the name of this Datatype constructor. */
 161     std::string getName() const throw();
 162     /**
 163      * Get the constructor operator of this Datatype constructor.  The
 164      * Datatype must be resolved.
 165      */
 166     Expr getConstructor() const;
 167     /**
 168      * Get the tester operator of this Datatype constructor.  The
 169      * Datatype must be resolved.
 170      */
 171     Expr getTester() const;
 172     /**
 173      * Get the number of arguments (so far) of this Datatype constructor.
 174      */
 175     inline size_t getNumArgs() const throw();
 176
 177     /**
 178      * Get the specialized constructor type for a parametric
 179      * constructor; this call is only permitted after resolution.
 180      */
 181     Type getSpecializedConstructorType(Type returnType) const;
 182
 183     /**
 184      * Return the cardinality of this constructor (the product of the
 185      * cardinalities of its arguments).
 186      */
 187     Cardinality getCardinality() const throw(AssertionException);
 188
 189     /**
 190      * Return true iff this constructor is finite (it is nullary or
 191      * each of its argument types are finite).  This function can
 192      * only be called for resolved constructors.
 193      */
 194     bool isFinite() const throw(AssertionException);
 195
 196     /**
 197      * Return true iff this constructor is well-founded (there exist
 198      * ground terms).  The constructor must be resolved or an
 199      * exception is thrown.
 200      */
 201     bool isWellFounded() const throw(AssertionException);
 202
 203     /**
 204      * Construct and return a ground term of this constructor.  The
 205      * constructor must be both resolved and well-founded, or else an
 206      * exception is thrown.
 207      */
 208     Expr mkGroundTerm( Type t ) const throw(AssertionException);
 209
 210     /**
 211      * Returns true iff this Datatype constructor has already been
 212      * resolved.
 213      */
 214     inline bool isResolved() const throw();
 215
 216     /** Get the beginning iterator over Constructor args. */
 217     inline iterator begin() throw();
 218     /** Get the ending iterator over Constructor args. */
 219     inline iterator end() throw();
 220     /** Get the beginning const_iterator over Constructor args. */
 221     inline const_iterator begin() const throw();
 222     /** Get the ending const_iterator over Constructor args. */
 223     inline const_iterator end() const throw();
 224
 225     /** Get the ith Constructor arg. */
 226     const Arg& operator[](size_t index) const;
 227
 228   };/* class Datatype::Constructor */
 229 }
 230
 231   class SelfType {
 232   };/* class Datatype::SelfType */
 233
 234   /**
 235    * An unresolved type (used in calls to
 236    * Datatype::Constructor::addArg()) to allow a Datatype to refer to
 237    * itself or to other mutually-recursive Datatypes.  Unresolved-type
 238    * fields of Datatypes will be properly typed when a Type is created
 239    * for the Datatype by the ExprManager (which calls
 240    * Datatype::resolve()).
 241    */
 242   class UnresolvedType {
 243     std::string d_name;
 244   public:
 245     inline UnresolvedType(std::string name);
 246     inline std::string getName() const throw();
 247   };/* class Datatype::UnresolvedType */
 248
 249 %{
 250 namespace CVC4 {
 251 typedef Datatype::Constructor Constructor;
 252 typedef Datatype::Constructor::Arg Arg;
 253 typedef Datatype::SelfType SelfType;
 254 typedef Datatype::UnresolvedType UnresolvedType;
 255 }
 256 %}
 257