From bef9df667e2788cab327b0c8c6590ba833297670 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Nov 2019 11:11:28 -0600 Subject: [PATCH] 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. --- src/expr/datatype.cpp | 9 ++++-- src/expr/type_matcher.cpp | 12 ++++---- src/expr/type_matcher.h | 4 +-- src/expr/type_node.cpp | 17 ++++++++++- src/expr/type_node.h | 28 +++++++++++++++++++ .../datatypes/theory_datatypes_type_rules.h | 13 +++++---- 6 files changed, 66 insertions(+), 17 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index c09b92cfe..d52023b4c 100644 --- 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 subst; - m.getMatches(subst); + std::vector sns; + m.getMatches(sns); + std::vector subst; + for (TypeNode& s : sns) + { + subst.push_back(s.toType()); + } vector 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 a21dc2cc0..516870e9c 100644 --- 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& types) +void TypeMatcher::getTypes(std::vector& 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& types) +void TypeMatcher::getMatches(std::vector& 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 778338df7..13423f401 100644 --- 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& types); + void getTypes(std::vector& types) const; /** * Get the match for the parameter types based on the last call to doMatching. */ - void getMatches(std::vector& types); + void getMatches(std::vector& types) const; private: /** The parameter types */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 0a04d7efe..c827b77fa 100644 --- 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& 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()); + std::vector 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 610dd3b62..d2197faf8 100644 --- 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& 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 566fa47aa..219124d8e 100644 --- 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 instTypes; + std::vector 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 types, matches; + std::vector 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; -- 2.30.2