diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
commit | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (patch) | |
tree | c7b5351b372cb360780ce62935fb2cfb5792299a /src/expr | |
parent | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (diff) |
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/declaration_scope.cpp | 10 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 5 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 42 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 | ||||
-rw-r--r-- | src/expr/type.cpp | 57 | ||||
-rw-r--r-- | src/expr/type.h | 19 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 14 | ||||
-rw-r--r-- | src/expr/type_node.h | 8 |
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; |