diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:15:43 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:15:43 +0000 |
commit | 11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21 (patch) | |
tree | 1c975ba91df4f5ffcee6b53d164d00e1181b83c8 /src/expr/expr_manager_template.cpp | |
parent | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (diff) |
add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 17 |
1 files changed, 9 insertions, 8 deletions
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<Datatype>& 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<Datatype>& 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<Datatype>& 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 ); |