From 0a6076715b1d290b58b99cdaa0014d30d4d8308f Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 29 Mar 2022 01:33:05 -0700
Subject: [PATCH] TypeNode: Refactor get param types handling. (#8428)

This introduces TypeNode::getInstantiatedParamTypes() and deletes
TypeNode::getParamTypes(). This is in preparation for adding
api::Sort::getInstantiatedParameters().
---
 src/api/cpp/cvc5.cpp      |  2 +-
 src/expr/dtype_cons.cpp   |  6 +++---
 src/expr/type_matcher.cpp | 12 +++++++++++-
 src/expr/type_node.cpp    |  8 +++++---
 src/expr/type_node.h      | 12 +++++++++---
 5 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 8b16ea8bc..487977963 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1727,7 +1727,7 @@ std::vector<Sort> Sort::getDatatypeParamSorts() const
   CVC5_API_CHECK(d_type->isParametricDatatype())
       << "Not a parametric datatype sort.";
   //////// all checks before this line
-  return typeNodeVectorToSorts(d_solver, d_type->getParamTypes());
+  return typeNodeVectorToSorts(d_solver, d_type->getDType().getParameters());
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 269f3ebca..c9c70f778 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -199,7 +199,7 @@ std::pair<CardinalityClass, bool> DTypeConstructor::computeCardinalityInfo(
   if (isParam)
   {
     paramTypes = t.getDType().getParameters();
-    instTypes = t.getParamTypes();
+    instTypes = t.getInstantiatedParamTypes();
   }
   for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
   {
@@ -328,7 +328,7 @@ Cardinality DTypeConstructor::computeCardinality(
   if (isParam)
   {
     paramTypes = t.getDType().getParameters();
-    instTypes = t.getParamTypes();
+    instTypes = t.getInstantiatedParamTypes();
   }
   for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
   {
@@ -390,7 +390,7 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t,
   if (isParam)
   {
     paramTypes = t.getDType().getParameters();
-    instTypes = TypeNode(t).getParamTypes();
+    instTypes = TypeNode(t).getInstantiatedParamTypes();
   }
   for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
   {
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index cd244df14..cc33494d8 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -15,6 +15,8 @@
 
 #include "type_matcher.h"
 
+#include "expr/dtype.h"
+
 namespace cvc5 {
 
 TypeMatcher::TypeMatcher(TypeNode dt)
@@ -25,7 +27,15 @@ TypeMatcher::TypeMatcher(TypeNode dt)
 
 void TypeMatcher::addTypesFromDatatype(TypeNode dt)
 {
-  std::vector<TypeNode> argTypes = dt.getParamTypes();
+  std::vector<TypeNode> argTypes;
+  if (dt.isInstantiated())
+  {
+    argTypes = dt.getInstantiatedParamTypes();
+  }
+  else
+  {
+    argTypes = dt.getDType().getParameters();
+  }
   addTypes(argTypes);
   Trace("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
   for (unsigned i = 0, narg = argTypes.size(); i < narg; ++i)
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a90efd055..b784e8ce1 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -360,10 +360,12 @@ std::vector<TypeNode> TypeNode::getArgTypes() const {
   return args;
 }
 
-std::vector<TypeNode> TypeNode::getParamTypes() const {
+std::vector<TypeNode> TypeNode::getInstantiatedParamTypes() const
+{
+  Assert(isInstantiated());
   vector<TypeNode> params;
-  Assert(isParametricDatatype());
-  for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
+  for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i)
+  {
     params.push_back((*this)[i]);
   }
   return params;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 8f8985d86..60b24d57e 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -529,10 +529,16 @@ private:
   std::vector<TypeNode> getArgTypes() const;
 
   /**
-   * Get the paramater types of a parameterized datatype.  Fails an
-   * assertion if this type is not a parametric datatype.
+   * Get the types used to instantiate the type parameters of a parametric
+   * type (parametric datatype or uninterpreted sort constructor type,
+   * see TypeNode::instantiate(const std::vector<TypeNode>& const).
+   *
+   * Asserts that this type is an instantiated type.
+   *
+   * @return the types used to instantiate the type parameters of a
+   *         parametric type
    */
-  std::vector<TypeNode> getParamTypes() const;
+  std::vector<TypeNode> getInstantiatedParamTypes() const;
 
   /**
    * Get the range type (i.e., the type of the result) of a function,
-- 
2.30.2