Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris!

3 files changed, 9 insertions, 9 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 22cf368eb..2d659cfe3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1486,7 +1486,7 @@ postfixTerm[CVC4::Expr& f]
       { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
           std::vector<CVC4::Expr> v;
           Expr e = f.getOperator();
-          const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+          const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
           v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
                                MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
           v.insert(v.end(), f.begin(), f.end());
@@ -1783,14 +1783,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 constructorDef[CVC4::Datatype& type]
 @init {
   std::string id;
-  CVC4::Datatype::Constructor* ctor = NULL;
+  CVC4::DatatypeConstructor* ctor = NULL;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
       std::string testerId("is_");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
-      ctor = new CVC4::Datatype::Constructor(id, testerId);
+      ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN
       selector[*ctor]
@@ -1804,7 +1804,7 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
 @init {
   std::string id;
   Type t, t2;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f1ad4b330..4418ea18f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -286,7 +286,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
           j_end = dt.end();
         j != j_end;
         ++j) {
-      const Datatype::Constructor& ctor = *j;
+      const DatatypeConstructor& ctor = *j;
       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
       Expr constructor = ctor.getConstructor();
       Debug("parser-idt") << "+ define " << constructor << std::endl;
@@ -302,7 +302,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
         throw ParserException(testerName + " already declared");
       }
       defineVar(testerName, tester);
-      for(Datatype::Constructor::const_iterator k = ctor.begin(),
+      for(DatatypeConstructor::const_iterator k = ctor.begin(),
             k_end = ctor.end();
           k != k_end;
           ++k) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 974de29b2..a093aa1ef 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -824,14 +824,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 constructorDef[CVC4::Datatype& type]
 @init {
   std::string id;
-  CVC4::Datatype::Constructor* ctor = NULL;
+  CVC4::DatatypeConstructor* ctor = NULL;
 }
   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
       std::string testerId("is_");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
-      ctor = new CVC4::Datatype::Constructor(id, testerId);
+      ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
@@ -841,7 +841,7 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
 @init {
   std::string id;
   Type t, t2;