Migrate more datatype methods to the Node level (#3443)

This adds node-level interfaces for a few missing functions that will be necessary to have a Node-level API for datatypes.

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index c09b92cfe90c14ffa72ef0081f43b776a73a5c48..d52023b4c1ebb9a9f93dd8d7d492e29e770d78fa 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -938,8 +938,13 @@ Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   TypeNode dtt = TypeNode::fromType(dt.getDatatypeType());
   TypeMatcher m(dtt);
   m.doMatching(dtt, TypeNode::fromType(returnType));
-  vector<Type> subst;
-  m.getMatches(subst);
+  std::vector<TypeNode> sns;
+  m.getMatches(sns);
+  std::vector<Type> subst;
+  for (TypeNode& s : sns)
+  {
+    subst.push_back(s.toType());
+  }
   vector<Type> params = dt.getParameters();
   return d_constructor.getType().substitute(params, subst);
 }

diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index a21dc2cc0f929063b8565a94f6b093ce96c938c8..516870e9c63df1b7a20da90e79e9b725f2ac8145 100644 (file)
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -96,26 +96,26 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
   return true;
 }
 
-void TypeMatcher::getTypes(std::vector<Type>& types)
+void TypeMatcher::getTypes(std::vector<TypeNode>& types) const
 {
   types.clear();
-  for (TypeNode& t : d_types)
+  for (const TypeNode& t : d_types)
   {
-    types.push_back(t.toType());
+    types.push_back(t);
   }
 }
-void TypeMatcher::getMatches(std::vector<Type>& types)
+void TypeMatcher::getMatches(std::vector<TypeNode>& types) const
 {
   types.clear();
   for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
   {
     if (d_match[i].isNull())
     {
-      types.push_back(d_types[i].toType());
+      types.push_back(d_types[i]);
     }
     else
     {
-      types.push_back(d_match[i].toType());
+      types.push_back(d_match[i]);
     }
   }
 }

diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 778338df7bce6c6bebfcf28ce66fd5abb65a3a9a..13423f401236a7ee6ee160eb7554baa7a723cf6f 100644 (file)
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -52,11 +52,11 @@ class TypeMatcher
   bool doMatching(TypeNode pattern, TypeNode tn);
 
   /** Get the parameter types that this class matched on */
-  void getTypes(std::vector<Type>& types);
+  void getTypes(std::vector<TypeNode>& types) const;
   /**
    * Get the match for the parameter types based on the last call to doMatching.
    */
-  void getMatches(std::vector<Type>& types);
+  void getMatches(std::vector<TypeNode>& types) const;
 
  private:
   /** The parameter types */

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 0a04d7efe9a02d05be875f7b0808192aa206f76d..c827b77fa449b7943c45aebbf5266d257c787088 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -434,6 +434,22 @@ bool TypeNode::isInstantiatedDatatype() const {
   return true;
 }
 
+TypeNode TypeNode::instantiateParametricDatatype(
+    const std::vector<TypeNode>& params) const
+{
+  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
+  AssertArgument(params.size() == getNumChildren() - 1, *this);
+  NodeManager* nm = NodeManager::currentNM();
+  TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>());
+  std::vector<TypeNode> paramsNodes;
+  paramsNodes.push_back(cons);
+  for (const TypeNode& t : params)
+  {
+    paramsNodes.push_back(t);
+  }
+  return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
+}
+
 /** Is this an instantiated datatype parameter */
 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
@@ -577,5 +593,4 @@ std::string TypeNode::toString() const {
   return ss.str();
 }
 
-
 }/* CVC4 namespace */

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 610dd3b62b6d6ee559ca6d5a8ef295e648980a9d..d2197faf89eef669fcca4c4d8e09821d1f0ed908 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -523,6 +523,12 @@ public:
   /** Get the return type (for constructor types) */
   TypeNode getConstructorRangeType() const;
 
+  /** Get the domain type (for selector types) */
+  TypeNode getSelectorDomainType() const;
+
+  /** Get the return type (for selector types) */
+  TypeNode getSelectorRangeType() const;
+
   /** Get the element type (for set types) */
   TypeNode getSetElementType() const;
 
@@ -630,6 +636,16 @@ public:
   /** Is this a fully instantiated datatype type */
   bool isInstantiatedDatatype() const;
 
+  /**
+   * Get instantiated datatype type. The type on which this method is called
+   * should be a parametric datatype whose parameter list is the same list as
+   * argument params. This constructs the instantiated version of this
+   * parametric datatype, e.g. passing (par (A) (List A)), { Int } ) to this
+   * method returns (List Int).
+   */
+  TypeNode instantiateParametricDatatype(
+      const std::vector<TypeNode>& params) const;
+
   /** Is this an instantiated datatype parameter */
   bool isParameterInstantiatedDatatype(unsigned n) const;
 
@@ -922,6 +938,18 @@ inline TypeNode TypeNode::getConstructorRangeType() const {
   return (*this)[getNumChildren()-1];
 }
 
+inline TypeNode TypeNode::getSelectorDomainType() const
+{
+  Assert(isSelector());
+  return (*this)[0];
+}
+
+inline TypeNode TypeNode::getSelectorRangeType() const
+{
+  Assert(isSelector());
+  return (*this)[1];
+}
+
 inline bool TypeNode::isSet() const {
   return getKind() == kind::SET_TYPE;
 }

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 566fa47aa8b3f6a534ef359a85d84aee8083a94e..219124d8e5fb3f35e1957092122d65f1f2dd6c0f 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -62,9 +62,9 @@ struct DatatypeConstructorTypeRule {
               n, "matching failed for parameterized constructor");
         }
       }
-      std::vector<Type> instTypes;
+      std::vector<TypeNode> instTypes;
       m.getMatches(instTypes);
-      TypeNode range = TypeNode::fromType(dt.instantiate(instTypes));
+      TypeNode range = t.instantiateParametricDatatype(instTypes);
       Debug("typecheck-idt") << "Return " << range << std::endl;
       return range;
     } else {
@@ -147,13 +147,14 @@ struct DatatypeSelectorTypeRule {
             n,
             "matching failed for selector argument of parameterized datatype");
       }
-      std::vector<Type> types, matches;
+      std::vector<TypeNode> types, matches;
       m.getTypes(types);
       m.getMatches(matches);
-      Type range = selType[1].toType();
-      range = range.substitute(types, matches);
+      TypeNode range = selType[1];
+      range = range.substitute(
+          types.begin(), types.end(), matches.begin(), matches.end());
       Debug("typecheck-idt") << "Return " << range << std::endl;
-      return TypeNode::fromType(range);
+      return range;
     } else {
       if (check) {
         Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;