2 files changed, 65 insertions, 0 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 93651f1a9..7d7c654bf 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -364,6 +364,19 @@ const Datatype::Constructor& Datatype::operator[](size_t index) const {
   return d_constructors[index];
 }
 
+const Datatype::Constructor& Datatype::operator[](std::string name) const {
+  for(const_iterator i = begin(); i != end(); ++i) {
+    if((*i).getName() == name) {
+      return *i;
+    }
+  }
+  CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
+}
+
+Expr Datatype::getConstructor(std::string name) const {
+  return (*this)[name].getConstructor();
+}
+
 void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
                                     const std::map<std::string, DatatypeType>& resolutions,
                                     const std::vector<Type>& placeholders,
@@ -674,6 +687,19 @@ const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index
   return d_args[index];
 }
 
+const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string name) const {
+  for(const_iterator i = begin(); i != end(); ++i) {
+    if((*i).getName() == name) {
+      return *i;
+    }
+  }
+  CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+}
+
+Expr Datatype::Constructor::getSelector(std::string name) const {
+  return (*this)[name].getSelector();
+}
+
 Datatype::Constructor::Arg::Arg(std::string name, Expr selector) :
   d_name(name),
   d_selector(selector),
diff --git a/src/util/datatype.h b/src/util/datatype.h
index b536cdf2b..24a625bd1 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -223,6 +223,14 @@ public:
   public:
     /**
      * Create a new Datatype constructor with the given name for the
+     * constructor and the same name (prefixed with "is_") for the
+     * tester.  The actual constructor and tester aren't created until
+     * resolution time.
+     */
+    explicit Constructor(std::string name);
+
+    /**
+     * Create a new Datatype constructor with the given name for the
      * constructor and the given name for the tester.  The actual
      * constructor and tester aren't created until resolution time.
      */
@@ -257,16 +265,19 @@ public:
 
     /** Get the name of this Datatype constructor. */
     std::string getName() const throw();
+
     /**
      * Get the constructor operator of this Datatype constructor.  The
      * Datatype must be resolved.
      */
     Expr getConstructor() const;
+
     /**
      * Get the tester operator of this Datatype constructor.  The
      * Datatype must be resolved.
      */
     Expr getTester() const;
+
     /**
      * Get the number of arguments (so far) of this Datatype constructor.
      */
@@ -323,6 +334,21 @@ public:
     /** Get the ith Constructor arg. */
     const Arg& operator[](size_t index) const;
 
+    /**
+     * Get the Constructor arg named.  This is a linear search
+     * through the arguments, so in the case of multiple,
+     * similarly-named arguments, the first is returned.
+     */
+    const Arg& operator[](std::string name) const;
+
+    /**
+     * Get the selector named.  This is a linear search
+     * through the arguments, so in the case of multiple,
+     * similarly-named arguments, the selector for the first
+     * is returned.
+     */
+    Expr getSelector(std::string name) const;
+
   };/* class Datatype::Constructor */
 
   /** The type for iterators over constructors. */
@@ -459,6 +485,19 @@ public:
   /** Get the ith Constructor. */
   const Constructor& operator[](size_t index) const;
 
+  /**
+   * Get the Constructor named.  This is a linear search
+   * through the constructors, so in the case of multiple,
+   * similarly-named constructors, the first is returned.
+   */
+  const Constructor& operator[](std::string name) const;
+
+  /**
+   * Get the constructor operator for the named constructor.
+   * This Datatype must be resolved.
+   */
+  Expr getConstructor(std::string name) const;
+
 };/* class Datatype */