diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 21:27:26 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 21:27:26 -0400 |
commit | ecc45b22ce41b6cde8e42a4c1baca4a0cd7c3ea3 (patch) | |
tree | b9f74db645d78eb544ca082d9c3a2a751dacfaa3 /src/expr | |
parent | 1c494313662b664a606f6f745f67cbd964c61927 (diff) | |
parent | 5cee91676e0c0faf1f1fffcb8ffb71baaa6f8a60 (diff) |
Merge branch '1.4.x'
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index be3749021..d0a477b9a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -397,6 +397,44 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { Assert(t.isTuple() || t.isRecord()); + TypeNode tOrig = t; + if(t.isTuple()) { + vector<TypeNode> v; + bool changed = false; + for(size_t i = 0; i < t.getNumChildren(); ++i) { + TypeNode tn = t[i]; + TypeNode base; + if(tn.isTuple() || tn.isRecord()) { + base = getDatatypeForTupleRecord(tn); + } else { + base = tn.getBaseType(); + } + changed = changed || (tn != base); + v.push_back(base); + } + if(changed) { + t = mkTupleType(v); + } + } else { + const Record& r = t.getRecord(); + std::vector< std::pair<std::string, Type> > v; + bool changed = false; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + Type tn = (*i).second; + Type base; + if(tn.isTuple() || tn.isRecord()) { + base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType(); + } else { + base = tn.getBaseType(); + } + changed = changed || (tn != base); + v.push_back(std::make_pair((*i).first, base)); + } + if(changed) { + t = mkRecordType(Record(v)); + } + } + // if the type doesn't have an associated datatype, then make one for it TypeNode& dtt = d_tupleAndRecordTypes[t]; if(dtt.isNull()) { |