summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/datatype.cpp70
-rw-r--r--src/util/datatype.h43
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback