diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-02 19:32:14 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-02 20:47:48 -0500 |
commit | 866941628950af27f33b03311a8839570ed92eca (patch) | |
tree | f3b3a48bf0091e9c6445a575c5faa5bbfeef7af8 /src | |
parent | fe31c46e11df64da6a9c4741525e09952ba016cf (diff) |
Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real). Resolves bug #541.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type_node.cpp | 50 |
1 files changed, 49 insertions, 1 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 54fd2f3e8..335dd2b6d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -133,6 +133,19 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType()); } + if(isParametricDatatype() && t.isParametricDatatype()) { + Assert(getKind() == kind::PARAMETRIC_DATATYPE); + Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); + if((*this)[0] != t[0] || getNumChildren() != t.getNumChildren()) { + return false; + } + for(size_t i = 1; i < getNumChildren(); ++i) { + if(!((*this)[i].isSubtypeOf(t[i]))) { + return false; + } + } + return true; + } if(isPredicateSubtype()) { return getSubtypeParentType().isSubtypeOf(t); } @@ -186,7 +199,20 @@ bool TypeNode::isComparableTo(TypeNode t) const { } else if(isDatatype() && (t.isTuple() || t.isRecord())) { Assert(!isTuple() && !isRecord());// should have been handled above return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t); + } else if(isParametricDatatype() && t.isParametricDatatype()) { + Assert(getKind() == kind::PARAMETRIC_DATATYPE); + Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); + if((*this)[0] != t[0] || getNumChildren() != t.getNumChildren()) { + return false; + } + for(size_t i = 1; i < getNumChildren(); ++i) { + if(!((*this)[i].isComparableTo(t[i]))) { + return false; + } + } + return true; } + if(isPredicateSubtype()) { return t.isComparableTo(getSubtypeParentType()); } @@ -211,6 +237,13 @@ TypeNode TypeNode::getBaseType() const { return NodeManager::currentNM()->getDatatypeForTupleRecord(*this); } else if (isPredicateSubtype()) { return getSubtypeParentType().getBaseType(); + } else if (isParametricDatatype()) { + vector<Type> v; + for(size_t i = 1; i < getNumChildren(); ++i) { + v.push_back((*this)[i].getBaseType().toType()); + } + TypeNode tn = TypeNode::fromType((*this)[0].getDatatype().getDatatypeType(v)); + return tn; } return *this; } @@ -339,7 +372,6 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ case kind::ARRAY_TYPE: case kind::BITVECTOR_TYPE: case kind::SORT_TYPE: - case kind::PARAMETRIC_DATATYPE: case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: @@ -444,6 +476,22 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ } // otherwise no common ancestor return TypeNode(); + case kind::PARAMETRIC_DATATYPE: { + if(!t1.isParametricDatatype()) { + return TypeNode(); + } + while(t1.getKind() != kind::PARAMETRIC_DATATYPE) { + t1 = t1.getSubtypeParentType(); + } + if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { + return TypeNode(); + } + vector<Type> v; + for(size_t i = 1; i < t0.getNumChildren(); ++i) { + v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType()); + } + return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v)); + } default: Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); return TypeNode(); |