From 4caca6f74cc23b185757648bbf6f20daa6e78303 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 2 Aug 2020 08:50:57 -0500
Subject: [PATCH] Updates to dtype constructor in preparation for eliminating
 Expr-level datatype (#4825)

---
 src/expr/dtype_cons.cpp                       | 22 +++++++++++++++++-
 src/expr/dtype_cons.h                         | 23 ++++++++++++++++---
 .../datatypes/theory_datatypes_type_rules.h   |  7 +++---
 3 files changed, 45 insertions(+), 7 deletions(-)

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index b2e3fbd43..85e07866b 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -51,7 +51,7 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
       selectorType,
       "is an unresolved selector type placeholder",
       NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
-  Trace("datatypes") << type << std::endl;
+  Trace("datatypes") << "DTypeConstructor::addArg: " << type << std::endl;
   std::shared_ptr<DTypeSelector> a =
       std::make_shared<DTypeSelector>(selectorName, type);
   addArg(a);
@@ -62,6 +62,14 @@ void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
   d_args.push_back(a);
 }
 
+void DTypeConstructor::addArgSelf(std::string selectorName)
+{
+  Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
+  std::shared_ptr<DTypeSelector> a =
+      std::make_shared<DTypeSelector>(selectorName, Node::null());
+  addArg(a);
+}
+
 std::string DTypeConstructor::getName() const { return d_name; }
 
 Node DTypeConstructor::getConstructor() const
@@ -276,6 +284,18 @@ int DTypeConstructor::getSelectorIndexInternal(Node sel) const
   return -1;
 }
 
+int DTypeConstructor::getSelectorIndexForName(const std::string& name) const
+{
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    if (d_args[i]->getName() == name)
+    {
+      return i;
+    }
+  }
+  return -1;
+}
+
 bool DTypeConstructor::involvesExternalType() const
 {
   for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index d89ed6af7..2553309f1 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -26,8 +26,6 @@
 
 namespace CVC4 {
 
-class DatatypeConstructor;
-
 /**
  * The Node-level representation of a constructor for a datatype, which
  * currently resides in the Expr-level DatatypeConstructor class
@@ -35,7 +33,6 @@ class DatatypeConstructor;
  */
 class DTypeConstructor
 {
-  friend class DatatypeConstructor;
   friend class DType;
 
  public:
@@ -63,6 +60,20 @@ class DTypeConstructor
    * Add an argument, given a pointer to a selector object.
    */
   void addArg(std::shared_ptr<DTypeSelector> a);
+  /**
+   * Add a self-referential (i.e., a data field) of the given name
+   * to this Datatype constructor that refers to the enclosing
+   * Datatype.  For example, using the familiar "nat" Datatype, to
+   * create the "pred" field for "succ" constructor, one uses
+   * succ::addArgSelf("pred")---the actual Type
+   * cannot be passed because the Datatype is still under
+   * construction.  Selector names need not be unique; they are for
+   * convenience and pretty-printing only.
+   *
+   * This is a special case of
+   * DTypeConstructor::addArg(std::string).
+   */
+  void addArgSelf(std::string selectorName);
 
   /** Get the name of this constructor. */
   std::string getName() const;
@@ -195,6 +206,12 @@ class DTypeConstructor
    *   stoa(T,C,index)
    */
   int getSelectorIndexInternal(Node sel) const;
+  /** get selector index for name
+   *
+   * Returns the index of selector with the given name, or -1 if it
+   * does not exist.
+   */
+  int getSelectorIndexForName(const std::string& name) const;
 
   /** involves external type
    *
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index e9df20c2e..5c1a09805 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -282,9 +282,10 @@ struct RecordUpdateTypeRule {
         throw TypeCheckingExceptionPrivate(
             n, "Record-update expression formed over non-record");
       }
-      const Record& rec =
-          DatatypeType(recordType.toType()).getRecord();
-      if (!rec.contains(ru.getField())) {
+      const DType& dt = recordType.getDType();
+      const DTypeConstructor& recCons = dt[0];
+      if (recCons.getSelectorIndexForName(ru.getField()) == -1)
+      {
         std::stringstream ss;
         ss << "Record-update field `" << ru.getField()
            << "' is not a valid field name for the record type";
-- 
2.30.2