From 11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 14 May 2011 00:15:43 +0000 Subject: add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation --- src/expr/declaration_scope.cpp | 8 ++++---- src/expr/declaration_scope.h | 2 +- src/expr/expr_manager_template.cpp | 17 +++++++++-------- src/expr/type.cpp | 18 ++++++++---------- src/expr/type.h | 5 +++-- src/expr/type_node.cpp | 4 ++-- src/expr/type_node.h | 3 ++- 7 files changed, 29 insertions(+), 28 deletions(-) (limited to 'src/expr') diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 79accf43a..ae91efa68 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -144,10 +144,10 @@ Type DeclarationScope::lookupType(const std::string& name, Debug("sort") << "instance is " << instantiation << endl; return instantiation; - }else if( p.second.isDatatype() ){ - Assert( DatatypeType( p.second ).isParametric() ); + } else if(p.second.isDatatype()) { + Assert( DatatypeType(p.second).isParametric() ); return DatatypeType(p.second).instantiate(params); - }else { + } else { if(Debug.isOn("sort")) { Debug("sort") << "instantiating using a sort substitution" << endl; Debug("sort") << "have formals ["; @@ -170,7 +170,7 @@ Type DeclarationScope::lookupType(const std::string& name, } } -size_t DeclarationScope::lookupArity( const std::string& name ){ +size_t DeclarationScope::lookupArity(const std::string& name) { pair, Type> p = (*d_typeMap->find(name)).second; return p.first.size(); } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 4cdb71ddc..d695a3bf8 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -177,7 +177,7 @@ public: /** * Lookup the arity of a bound parameterized type. */ - size_t lookupArity( const std::string& name ); + size_t lookupArity(const std::string& name); /** * Pop a scope level. Deletes all bindings since the last call to diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index c32dbbc7d..038f58f95 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -506,16 +506,17 @@ ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes, i != i_end; ++i) { TypeNode* typeNode; - if( (*i).getNumParameters()==0 ){ + if( (*i).getNumParameters() == 0 ) { typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); - }else{ + } else { TypeNode cons = d_nodeManager->mkTypeConst(*i); std::vector< TypeNode > params; params.push_back( cons ); - for( unsigned int ip=0; ip<(*i).getNumParameters(); ip++ ){ + 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 ) ); + + typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params)); } Type type(d_nodeManager, typeNode); DatatypeType dtt(type); @@ -546,9 +547,9 @@ ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes, i != i_end; ++i) { std::string name; - if( (*i).isSort() ){ + if( (*i).isSort() ) { name = SortType(*i).getName(); - }else{ + } else { Assert( (*i).isSortConstructor() ); name = SortConstructorType(*i).getName(); } @@ -562,10 +563,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes, // unresolved SortType used as a placeholder in complex types) // with "(*resolver).second" (the DatatypeType we created in the // first step, above). - if( (*i).isSort() ){ + if( (*i).isSort() ) { placeholders.push_back(*i); replacements.push_back( (*resolver).second ); - }else{ + } else { Assert( (*i).isSortConstructor() ); paramTypes.push_back( SortConstructorType(*i) ); paramReplacements.push_back( (*resolver).second ); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 2bcdcedfa..8320a7053 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -222,7 +222,7 @@ Type::operator DatatypeType() const throw(AssertionException) { return DatatypeType(*this); } -/** Is this the Datatype type? */ +/** Is this a datatype type? */ bool Type::isDatatype() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype(); @@ -388,14 +388,12 @@ string SortType::getName() const { return d_typeNode->getAttribute(expr::VarNameAttr()); } -bool SortType::isParameterized() const -{ +bool SortType::isParameterized() const { return false; } /** Get the parameter types */ -std::vector SortType::getParamTypes() const -{ +std::vector SortType::getParamTypes() const { vector params; return params; } @@ -526,11 +524,11 @@ std::vector ConstructorType::getArgTypes() const { } const Datatype& DatatypeType::getDatatype() const { - if( d_typeNode->isParametricDatatype() ){ - Assert( (*d_typeNode)[0].getKind()==kind::DATATYPE_TYPE ); + if( d_typeNode->isParametricDatatype() ) { + Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE ); const Datatype& dt = (*d_typeNode)[0].getConst(); return dt; - }else{ + } else { return d_typeNode->getConst(); } } @@ -544,13 +542,13 @@ size_t DatatypeType::getArity() const { return d_typeNode->getNumChildren() - 1; } -std::vector DatatypeType::getParamTypes() const{ +std::vector DatatypeType::getParamTypes() const { NodeManagerScope nms(d_nodeManager); vector params; vector paramNodes = d_typeNode->getParamTypes(); vector::iterator it = paramNodes.begin(); vector::iterator it_end = paramNodes.end(); - for(; it != it_end; ++ it) { + for(; it != it_end; ++it) { params.push_back(makeType(*it)); } return params; diff --git a/src/expr/type.h b/src/expr/type.h index 096336b0c..4b260185b 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -470,11 +470,12 @@ public: /** Get the name of the sort */ std::string getName() const; - /** is parameterized */ + /** Is this type parameterized? */ bool isParameterized() const; /** Get the parameter types */ std::vector getParamTypes() const; + };/* class SortType */ /** @@ -539,7 +540,7 @@ public: /** Get the underlying datatype */ const Datatype& getDatatype() const; - /** is parameterized */ + /** Is this this datatype parametric? */ bool isParametric() const; /** Get the parameter types */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9283da13a..f77182d5d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -138,7 +138,7 @@ std::vector TypeNode::getArgTypes() const { std::vector TypeNode::getParamTypes() const { vector params; - Assert( isParametricDatatype() ); + Assert(isParametricDatatype()); for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) { params.push_back((*this)[i]); } @@ -194,7 +194,7 @@ bool TypeNode::isDatatype() const { return getKind() == kind::DATATYPE_TYPE; } -/** Is this a datatype type */ +/** Is this a parametric datatype type */ bool TypeNode::isParametricDatatype() const { return getKind() == kind::PARAMETRIC_DATATYPE; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d6c685a75..90fee7f1b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -452,7 +452,8 @@ public: std::vector getArgTypes() const; /** - * Get the paramater types of a parameterized datatype. + * Get the paramater types of a parameterized datatype. Fails an + * assertion if this type is not a parametric datatype. */ std::vector getParamTypes() const; -- cgit v1.2.3