diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 70 | ||||
-rw-r--r-- | src/util/datatype.h | 43 |
2 files changed, 102 insertions, 11 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index ab52e7f93..ecb089658 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -54,13 +54,15 @@ const Datatype& Datatype::datatypeOf(Expr item) { TypeNode t = Node::fromExpr(item).getType(); switch(t.getKind()) { case kind::CONSTRUCTOR_TYPE: - return t[t.getNumChildren() - 1].getConst<Datatype>(); + //return t[t.getNumChildren() - 1].getConst<Datatype>(); + return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype(); case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - return t[0].getConst<Datatype>(); + //return t[0].getConst<Datatype>(); + return DatatypeType(t[0].toType()).getDatatype(); default: Unhandled("arg must be a datatype constructor, selector, or tester"); - } + } } size_t Datatype::indexOf(Expr item) { @@ -77,9 +79,12 @@ size_t Datatype::indexOf(Expr item) { void Datatype::resolve(ExprManager* em, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, - const std::vector<Type>& replacements) + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) throw(AssertionException, DatatypeResolutionException) { + //cout << "resolve " << *this << "..." << std::endl; AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!d_resolved, "cannot resolve a Datatype twice"); AssertArgument(resolutions.find(d_name) != resolutions.end(), @@ -92,13 +97,15 @@ void Datatype::resolve(ExprManager* em, d_resolved = true; size_t index = 0; for(iterator i = begin(), i_end = end(); i != i_end; ++i) { - (*i).resolve(em, self, resolutions, placeholders, replacements); + (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); Assert((*i).isResolved()); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; Assert(index == getNumConstructors()); + + //cout << "done resolve " << *this << std::endl; } void Datatype::addConstructor(const Constructor& c) { @@ -263,10 +270,16 @@ Expr Datatype::mkGroundTerm() const throw(AssertionException) { DatatypeType Datatype::getDatatypeType() const throw(AssertionException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); - Assert(!d_self.isNull()); + Assert(!d_self.isNull() && !DatatypeType(d_self).isParametric()); return DatatypeType(d_self); } +DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const throw(AssertionException) { + CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + Assert(!d_self.isNull() && DatatypeType(d_self).isParametric()); + return DatatypeType(d_self).instantiate(params); +} + bool Datatype::operator==(const Datatype& other) const throw() { // two datatypes are == iff the name is the same and they have // exactly matching constructors (in the same order) @@ -349,8 +362,13 @@ const Datatype::Constructor& Datatype::operator[](size_t index) const { void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, - const std::vector<Type>& replacements) + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) throw(AssertionException, DatatypeResolutionException) { + + //cout << "resolve " << *this << "..." << std::endl; + AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!isResolved(), "cannot resolve a Datatype constructor twice; " @@ -383,6 +401,9 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, if(!placeholders.empty()) { range = range.substitute(placeholders, replacements); } + if(!paramTypes.empty() ){ + range = doParametricSubstitution( range, paramTypes, paramReplacements ); + } (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, range)); } Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); @@ -403,6 +424,37 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, for(iterator i = begin(), i_end = end(); i != i_end; ++i) { (*i).d_constructor = d_constructor; } + + //cout << "done resolve " << *this << std::endl; +} + +Type Datatype::Constructor::doParametricSubstitution( Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements ){ + TypeNode typn = TypeNode::fromType( range ); + if(typn.getNumChildren() == 0) { + return range; + } else { + std::vector< Type > origChildren; + std::vector< Type > children; + for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) { + origChildren.push_back( (*i).toType() ); + children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) ); + } + for( int i=0; i<(int)paramTypes.size(); i++ ){ + if( paramTypes[i].getArity()==origChildren.size() ){ + Type tn = paramTypes[i].instantiate( origChildren ); + if( range==tn ){ + return paramReplacements[i].instantiate( children ); + } + } + } + NodeBuilder<> nb(typn.getKind()); + for( int i=0; i<(int)children.size(); i++ ){ + nb << TypeNode::fromType( children[i] ); + } + return nb.constructTypeNode().toType(); + } } Datatype::Constructor::Constructor(std::string name, std::string tester) : @@ -615,6 +667,10 @@ Expr Datatype::Constructor::Arg::getConstructor() const { return d_constructor; } +Type Datatype::Constructor::Arg::getSelectorType() const{ + return getSelector().getType(); +} + bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() { return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 7d9ae6f39..abc9e3258 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -175,6 +175,12 @@ public: Expr getConstructor() const; /** + * Get the selector for this constructor argument; this call is + * only permitted after resolution. + */ + Type getSelectorType() const; + + /** * Get the name of the type of this constructor argument * (Datatype field). Can be used for not-yet-resolved Datatypes * (in which case the name of the unresolved type, or "[self]" @@ -204,10 +210,16 @@ public: void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, - const std::vector<Type>& replacements) + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) throw(AssertionException, DatatypeResolutionException); friend class Datatype; + /** */ + Type doParametricSubstitution( Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements ); public: /** * Create a new Datatype constructor with the given name for the @@ -314,6 +326,7 @@ public: private: std::string d_name; + std::vector<Type> d_params; std::vector<Constructor> d_constructors; bool d_resolved; Type d_self; @@ -330,14 +343,16 @@ private: void resolve(ExprManager* em, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, - const std::vector<Type>& replacements) + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) throw(AssertionException, DatatypeResolutionException); friend class ExprManager;// for access to resolve() public: /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name); + inline explicit Datatype(std::string name, std::vector<Type>& params); /** Add a constructor to this Datatype. */ void addConstructor(const Constructor& c); @@ -347,6 +362,11 @@ public: /** Get the number of constructors (so far) for this Datatype. */ inline size_t getNumConstructors() const throw(); + /** Get the nubmer of parameters */ + inline size_t getNumParameters() const throw(); + /** Get parameter */ + inline Type getParameter( unsigned int i ) const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -382,6 +402,12 @@ public: DatatypeType getDatatypeType() const throw(AssertionException); /** + * Get the DatatypeType associated to this (parameterized) Datatype. Can only be + * called post-resolution. + */ + DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(AssertionException); + + /** * Return true iff the two Datatypes are the same. * * We need == for mkConst(Datatype) to properly work---since if the @@ -466,8 +492,9 @@ inline std::string Datatype::UnresolvedType::getName() const throw() { return d_name; } -inline Datatype::Datatype(std::string name) : +inline Datatype::Datatype(std::string name, std::vector<Type>& params) : d_name(name), + d_params(params), d_constructors(), d_resolved(false), d_self() { @@ -481,6 +508,14 @@ inline size_t Datatype::getNumConstructors() const throw() { return d_constructors.size(); } +inline size_t Datatype::getNumParameters() const throw() { + return d_params.size(); +} + +inline Type Datatype::getParameter( unsigned int i ) const { + return d_params[i]; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } |