summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/declaration_scope.cpp10
-rw-r--r--src/expr/declaration_scope.h5
-rw-r--r--src/expr/expr_manager_template.cpp42
-rw-r--r--src/expr/expr_manager_template.h2
-rw-r--r--src/expr/node_manager.h3
-rw-r--r--src/expr/type.cpp57
-rw-r--r--src/expr/type.h19
-rw-r--r--src/expr/type_node.cpp14
-rw-r--r--src/expr/type_node.h8
9 files changed, 146 insertions, 14 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 8dd329b83..79accf43a 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -144,7 +144,10 @@ Type DeclarationScope::lookupType(const std::string& name,
Debug("sort") << "instance is " << instantiation << endl;
return instantiation;
- } else {
+ }else if( p.second.isDatatype() ){
+ Assert( DatatypeType( p.second ).isParametric() );
+ return DatatypeType(p.second).instantiate(params);
+ }else {
if(Debug.isOn("sort")) {
Debug("sort") << "instantiating using a sort substitution" << endl;
Debug("sort") << "have formals [";
@@ -167,6 +170,11 @@ Type DeclarationScope::lookupType(const std::string& name,
}
}
+size_t DeclarationScope::lookupArity( const std::string& name ){
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ return p.first.size();
+}
+
void DeclarationScope::popScope() throw(ScopeException) {
if( d_context->getLevel() == 0 ) {
throw ScopeException();
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 699dca6fa..4cdb71ddc 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -175,6 +175,11 @@ public:
const std::vector<Type>& params) const throw(AssertionException);
/**
+ * Lookup the arity of a bound parameterized type.
+ */
+ size_t lookupArity( const std::string& name );
+
+ /**
* Pop a scope level. Deletes all bindings since the last call to
* <code>pushScope</code>. Calls to <code>pushScope</code> and
* <code>popScope</code> must be "properly nested." I.e., a call to
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index f0c90ebdb..c32dbbc7d 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -486,12 +486,12 @@ DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
std::vector<DatatypeType>
ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
- return mkMutualDatatypeTypes(datatypes, set<SortType>());
+ return mkMutualDatatypeTypes(datatypes, set<Type>());
}
std::vector<DatatypeType>
ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<SortType>& unresolvedTypes) {
+ const std::set<Type>& unresolvedTypes) {
NodeManagerScope nms(d_nodeManager);
std::map<std::string, DatatypeType> nameResolutions;
std::vector<DatatypeType> dtts;
@@ -505,7 +505,18 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
i_end = datatypes.end();
i != i_end;
++i) {
- TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+ TypeNode* typeNode;
+ if( (*i).getNumParameters()==0 ){
+ typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+ }else{
+ TypeNode cons = d_nodeManager->mkTypeConst(*i);
+ std::vector< TypeNode > params;
+ params.push_back( cons );
+ for( unsigned int ip=0; ip<(*i).getNumParameters(); ip++ ){
+ params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
+ }
+ typeNode = new TypeNode( d_nodeManager->mkTypeNode( kind::PARAMETRIC_DATATYPE, params ) );
+ }
Type type(d_nodeManager, typeNode);
DatatypeType dtt(type);
CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
@@ -526,13 +537,21 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
//
// @TODO get rid of named resolutions altogether and handle
// everything with these resolutions?
+ std::vector< SortConstructorType > paramTypes;
+ std::vector< DatatypeType > paramReplacements;
std::vector<Type> placeholders;// to hold the "unresolved placeholders"
std::vector<Type> replacements;// to hold our final, resolved types
- for(std::set<SortType>::const_iterator i = unresolvedTypes.begin(),
+ for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
i_end = unresolvedTypes.end();
i != i_end;
++i) {
- std::string name = (*i).getName();
+ std::string name;
+ if( (*i).isSort() ){
+ name = SortType(*i).getName();
+ }else{
+ Assert( (*i).isSortConstructor() );
+ name = SortConstructorType(*i).getName();
+ }
std::map<std::string, DatatypeType>::const_iterator resolver =
nameResolutions.find(name);
CheckArgument(resolver != nameResolutions.end(),
@@ -543,8 +562,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
// unresolved SortType used as a placeholder in complex types)
// with "(*resolver).second" (the DatatypeType we created in the
// first step, above).
- placeholders.push_back(*i);
- replacements.push_back((*resolver).second);
+ if( (*i).isSort() ){
+ placeholders.push_back(*i);
+ replacements.push_back( (*resolver).second );
+ }else{
+ Assert( (*i).isSortConstructor() );
+ paramTypes.push_back( SortConstructorType(*i) );
+ paramReplacements.push_back( (*resolver).second );
+ }
}
// Lastly, perform the final resolutions and checks.
@@ -555,7 +580,8 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
const Datatype& dt = (*i).getDatatype();
if(!dt.isResolved()) {
const_cast<Datatype&>(dt).resolve(this, nameResolutions,
- placeholders, replacements);
+ placeholders, replacements,
+ paramTypes, paramReplacements);
}
// Now run some checks, including a check to make sure that no
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f395d781c..712273473 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -357,7 +357,7 @@ public:
*/
std::vector<DatatypeType>
mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<SortType>& unresolvedTypes);
+ const std::set<Type>& unresolvedTypes);
/**
* Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 9974df6ca..8b803e696 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -53,10 +53,12 @@ namespace expr {
namespace attr {
struct VarNameTag {};
struct SortArityTag {};
+ struct DatatypeTag {};
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+typedef Attribute<attr::SortArityTag, void*> DatatypeAttr;
}/* CVC4::expr namespace */
@@ -1188,7 +1190,6 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
return NodeBuilder<>(this, kind).append(children).constructTypeNode();
}
-
inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
Node n = mkVar(type);
n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 567bb2d40..2bcdcedfa 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -225,7 +225,7 @@ Type::operator DatatypeType() const throw(AssertionException) {
/** Is this the Datatype type? */
bool Type::isDatatype() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isDatatype();
+ return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
}
/** Cast to a Constructor type */
@@ -388,6 +388,18 @@ string SortType::getName() const {
return d_typeNode->getAttribute(expr::VarNameAttr());
}
+bool SortType::isParameterized() const
+{
+ return false;
+}
+
+/** Get the parameter types */
+std::vector<Type> SortType::getParamTypes() const
+{
+ vector<Type> params;
+ return params;
+}
+
string SortConstructorType::getName() const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->getAttribute(expr::VarNameAttr());
@@ -514,7 +526,48 @@ std::vector<Type> ConstructorType::getArgTypes() const {
}
const Datatype& DatatypeType::getDatatype() const {
- return d_typeNode->getConst<Datatype>();
+ if( d_typeNode->isParametricDatatype() ){
+ Assert( (*d_typeNode)[0].getKind()==kind::DATATYPE_TYPE );
+ const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
+ return dt;
+ }else{
+ return d_typeNode->getConst<Datatype>();
+ }
+}
+
+bool DatatypeType::isParametric() const {
+ return d_typeNode->isParametricDatatype();
+}
+
+size_t DatatypeType::getArity() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getNumChildren() - 1;
+}
+
+std::vector<Type> DatatypeType::getParamTypes() const{
+ NodeManagerScope nms(d_nodeManager);
+ vector<Type> params;
+ vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
+ vector<TypeNode>::iterator it = paramNodes.begin();
+ vector<TypeNode>::iterator it_end = paramNodes.end();
+ for(; it != it_end; ++ it) {
+ params.push_back(makeType(*it));
+ }
+ return params;
+}
+
+DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
+ NodeManagerScope nms(d_nodeManager);
+ TypeNode cons = d_nodeManager->mkTypeConst( getDatatype() );
+ vector<TypeNode> paramsNodes;
+ paramsNodes.push_back( cons );
+ for(vector<Type>::const_iterator i = params.begin(),
+ iend = params.end();
+ i != iend;
+ ++i) {
+ paramsNodes.push_back(*getTypeNode(*i));
+ }
+ return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE,paramsNodes)));
}
DatatypeType SelectorType::getDomain() const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 980a750d5..096336b0c 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -469,6 +469,12 @@ public:
/** Get the name of the sort */
std::string getName() const;
+
+ /** is parameterized */
+ bool isParameterized() const;
+
+ /** Get the parameter types */
+ std::vector<Type> getParamTypes() const;
};/* class SortType */
/**
@@ -533,8 +539,19 @@ public:
/** Get the underlying datatype */
const Datatype& getDatatype() const;
-};/* class DatatypeType */
+ /** is parameterized */
+ bool isParametric() const;
+
+ /** Get the parameter types */
+ std::vector<Type> getParamTypes() const;
+ /** Get the arity of the datatype constructor */
+ size_t getArity() const;
+
+ /** Instantiate a datatype using this datatype constructor */
+ DatatypeType instantiate(const std::vector<Type>& params) const;
+
+};/* class DatatypeType */
/**
* Class encapsulating the constructor type
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a6ca39015..9283da13a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -136,6 +136,15 @@ std::vector<TypeNode> TypeNode::getArgTypes() const {
return args;
}
+std::vector<TypeNode> TypeNode::getParamTypes() const {
+ vector<TypeNode> params;
+ Assert( isParametricDatatype() );
+ for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
+ params.push_back((*this)[i]);
+ }
+ return params;
+}
+
TypeNode TypeNode::getRangeType() const {
if(isTester()) {
return NodeManager::currentNM()->booleanType();
@@ -185,6 +194,11 @@ bool TypeNode::isDatatype() const {
return getKind() == kind::DATATYPE_TYPE;
}
+/** Is this a datatype type */
+bool TypeNode::isParametricDatatype() const {
+ return getKind() == kind::PARAMETRIC_DATATYPE;
+}
+
/** Is this a constructor type */
bool TypeNode::isConstructor() const {
return getKind() == kind::CONSTRUCTOR_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 7f6ebd471..d6c685a75 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -452,6 +452,11 @@ public:
std::vector<TypeNode> getArgTypes() const;
/**
+ * Get the paramater types of a parameterized datatype.
+ */
+ std::vector<TypeNode> getParamTypes() const;
+
+ /**
* Get the range type (i.e., the type of the result) of a function,
* datatype constructor, datatype selector, or datatype tester.
*/
@@ -479,6 +484,9 @@ public:
/** Is this a datatype type */
bool isDatatype() const;
+ /** Is this a parameterized datatype type */
+ bool isParametricDatatype() const;
+
/** Is this a constructor type */
bool isConstructor() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback