Changeset 933f32f for src/ResolvExpr/ResolveAssertions.cc
- Timestamp:
- May 24, 2019, 10:19:41 AM (6 years ago)
- Branches:
- ADT, arm-eh, ast-experimental, cleanup-dtors, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum
- Children:
- d908563
- Parents:
- 6a9d4b4 (diff), 292642a (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the(diff)links above to see all the changes relative to each parent. - File:
-
- 1 edited
-
src/ResolvExpr/ResolveAssertions.cc (modified) (14 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ResolvExpr/ResolveAssertions.cc
r6a9d4b4 r933f32f 20 20 #include <list> // for list 21 21 #include <memory> // for unique_ptr 22 #include <string> 22 #include <sstream> // for ostringstream 23 #include <string> // for string 23 24 #include <unordered_map> // for unordered_map, unordered_multimap 24 25 #include <utility> // for move … … 27 28 #include "Alternative.h" // for Alternative, AssertionItem, AssertionList 28 29 #include "Common/FilterCombos.h" // for filterCombos 30 #include "Common/Indenter.h" // for Indenter 29 31 #include "Common/utility.h" // for sort_mins 30 32 #include "ResolvExpr/RenameVars.h" // for renameTyVars … … 33 35 #include "SynTree/Expression.h" // for InferredParams 34 36 #include "TypeEnvironment.h" // for TypeEnvironment, etc. 35 #include "typeops.h" // for adjustExprType 37 #include "typeops.h" // for adjustExprType, specCost 36 38 #include "Unify.h" // for unify 37 39 … … 56 58 using CandidateList = std::vector<AssnCandidate>; 57 59 58 /// Unique identifier for a yet-to-be-resolved assertion59 struct AssnId {60 DeclarationWithType* decl; ///< Declaration of assertion61 AssertionSetValue info; ///< Information about assertion62 63 AssnId(DeclarationWithType* decl, const AssertionSetValue& info) : decl(decl), info(info) {}64 };65 66 /// Cached assertion items67 struct AssnCacheItem {68 CandidateList matches; ///< Possible matches for this assertion69 std::vector<AssnId> deferIds; ///< Deferred assertions which resolve to this item70 71 AssnCacheItem( CandidateList&& m ) : matches(std::move(m)), deferIds() {}72 };73 74 /// Cache of resolved assertions75 using AssnCache = std::unordered_map<std::string, AssnCacheItem>;76 77 60 /// Reference to single deferred item 78 61 struct DeferRef { 79 const AssnCacheItem& item; 62 const DeclarationWithType* decl; 63 const AssertionSetValue& info; 80 64 const AssnCandidate& match; 81 65 }; … … 84 68 /// Acts like indexed list of DeferRef 85 69 struct DeferItem { 86 const AssnCache* cache; ///< Cache storing assertion item 87 std::string key; ///< Key into cache 88 89 DeferItem( const AssnCache& cache, const std::string& key ) : cache(&cache), key(key) {} 90 91 bool empty() const { return cache->at(key).matches.empty(); } 92 93 CandidateList::size_type size() const { return cache->at(key).matches.size(); } 94 95 DeferRef operator[] ( unsigned i ) const { 96 const AssnCacheItem& item = cache->at(key); 97 return { item, item.matches[i] }; 98 } 99 100 // sortable by key 101 // TODO look into optimizing combination process with other sort orders (e.g. by number 102 // of matches in candidate) 103 bool operator< ( const DeferItem& o ) const { return key < o.key; } 104 bool operator== ( const DeferItem& o ) const { return key == o.key; } 70 const DeclarationWithType* decl; 71 const AssertionSetValue& info; 72 CandidateList matches; 73 74 DeferItem( DeclarationWithType* decl, const AssertionSetValue& info, CandidateList&& matches ) 75 : decl(decl), info(info), matches(std::move(matches)) {} 76 77 bool empty() const { return matches.empty(); } 78 79 CandidateList::size_type size() const { return matches.size(); } 80 81 DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; } 105 82 }; 106 83 … … 177 154 for ( const auto& assn : x.assns ) { 178 155 k += computeConversionCost( 179 assn.match.adjType, assn.item.deferIds[0].decl->get_type(), indexer, 180 x.env ); 156 assn.match.adjType, assn.decl->get_type(), indexer, x.env ); 157 158 // mark vars+specialization cost on function-type assertions 159 PointerType* ptr = dynamic_cast< PointerType* >( assn.decl->get_type() ); 160 if ( ! ptr ) continue; 161 FunctionType* func = dynamic_cast< FunctionType* >( ptr->base ); 162 if ( ! func ) continue; 163 164 for ( DeclarationWithType* formal : func->parameters ) { 165 k.decSpec( specCost( formal->get_type() ) ); 166 } 167 k.incVar( func->forall.size() ); 168 for ( TypeDecl* td : func->forall ) { 169 k.decSpec( td->assertions.size() ); 170 } 181 171 } 182 172 it = cache.emplace_hint( it, &x, k ); … … 249 239 250 240 /// Resolve a single assertion, in context 251 bool resolveAssertion( AssertionItem& assn, ResnState& resn , AssnCache& cache) {241 bool resolveAssertion( AssertionItem& assn, ResnState& resn ) { 252 242 // skip unused assertions 253 243 if ( ! assn.info.isUsed ) return true; 254 244 255 // check cache for this assertion 256 std::string assnKey = SymTab::Mangler::mangleAssnKey( assn.decl, resn.alt.env ); 257 auto it = cache.find( assnKey ); 258 259 // attempt to resolve assertion if this is the first time seen 260 if ( it == cache.end() ) { 261 // lookup candidates for this assertion 262 std::list< SymTab::Indexer::IdData > candidates; 263 resn.indexer.lookupId( assn.decl->name, candidates ); 264 265 // find the candidates that unify with the desired type 266 CandidateList matches; 267 for ( const auto& cdata : candidates ) { 268 DeclarationWithType* candidate = cdata.id; 269 270 // build independent unification context for candidate 271 AssertionSet have, newNeed; 272 TypeEnvironment newEnv{ resn.alt.env }; 273 OpenVarSet newOpenVars{ resn.alt.openVars }; 274 Type* adjType = candidate->get_type()->clone(); 275 adjustExprType( adjType, newEnv, resn.indexer ); 276 renameTyVars( adjType ); 277 278 // keep unifying candidates 279 if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 280 resn.indexer ) ) { 281 // set up binding slot for recursive assertions 282 UniqueId crntResnSlot = 0; 283 if ( ! newNeed.empty() ) { 284 crntResnSlot = ++globalResnSlot; 285 for ( auto& a : newNeed ) { 286 a.second.resnSlot = crntResnSlot; 287 } 288 } 289 290 matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 291 std::move(newNeed), std::move(newOpenVars), crntResnSlot ); 292 } else { 293 delete adjType; 294 } 245 // lookup candidates for this assertion 246 std::list< SymTab::Indexer::IdData > candidates; 247 resn.indexer.lookupId( assn.decl->name, candidates ); 248 249 // find the candidates that unify with the desired type 250 CandidateList matches; 251 for ( const auto& cdata : candidates ) { 252 DeclarationWithType* candidate = cdata.id; 253 254 // build independent unification context for candidate 255 AssertionSet have, newNeed; 256 TypeEnvironment newEnv{ resn.alt.env }; 257 OpenVarSet newOpenVars{ resn.alt.openVars }; 258 Type* adjType = candidate->get_type()->clone(); 259 adjustExprType( adjType, newEnv, resn.indexer ); 260 renameTyVars( adjType ); 261 262 // keep unifying candidates 263 if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 264 resn.indexer ) ) { 265 // set up binding slot for recursive assertions 266 UniqueId crntResnSlot = 0; 267 if ( ! newNeed.empty() ) { 268 crntResnSlot = ++globalResnSlot; 269 for ( auto& a : newNeed ) { 270 a.second.resnSlot = crntResnSlot; 271 } 272 } 273 274 matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 275 std::move(newNeed), std::move(newOpenVars), crntResnSlot ); 276 } else { 277 delete adjType; 295 278 } 296 297 it = cache.emplace_hint( it, assnKey, AssnCacheItem{ std::move(matches) } ); 298 } 299 300 CandidateList& matches = it->second.matches; 279 } 301 280 302 281 // break if no suitable assertion … … 305 284 // defer if too many suitable assertions 306 285 if ( matches.size() > 1 ) { 307 it->second.deferIds.emplace_back( assn.decl, assn.info ); 308 resn.deferred.emplace_back( cache, assnKey ); 286 resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) ); 309 287 return true; 310 288 } … … 314 292 addToIndexer( match.have, resn.indexer ); 315 293 resn.newNeed.insert( match.need.begin(), match.need.end() ); 316 resn.alt.env = match.env;317 resn.alt.openVars = match.openVars;294 resn.alt.env = std::move(match.env); 295 resn.alt.openVars = std::move(match.openVars); 318 296 319 297 bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred ); … … 364 342 static const int recursionLimit = /* 10 */ 4; 365 343 366 void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out ) {344 void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) { 367 345 // finish early if no assertions to resolve 368 346 if ( alt.need.empty() ) { … … 376 354 ResnList resns{ ResnState{ alt, root_indexer } }; 377 355 ResnList new_resns{}; 378 AssnCache assnCache;379 356 380 357 // resolve assertions in breadth-first-order up to a limited number of levels deep … … 385 362 for ( auto& assn : resn.need ) { 386 363 // fail early if any assertion is not resolvable 387 if ( ! resolveAssertion( assn, resn, assnCache ) ) goto nextResn; 364 if ( ! resolveAssertion( assn, resn ) ) { 365 Indenter tabs{ Indenter::tabsize, 3 }; 366 std::ostringstream ss; 367 ss << tabs << "Unsatisfiable alternative:\n"; 368 resn.alt.print( ss, ++tabs ); 369 ss << --tabs << "Could not satisfy assertion:\n"; 370 assn.decl->print( ss, ++tabs ); 371 372 errors.emplace_back( ss.str() ); 373 goto nextResn; 374 } 388 375 } 389 376 … … 396 383 } 397 384 } else { 398 // only resolve each deferred assertion once399 std::sort( resn.deferred.begin(), resn.deferred.end() );400 auto last = std::unique( resn.deferred.begin(), resn.deferred.end() );401 resn.deferred.erase( last, resn.deferred.end() );402 385 // resolve deferred assertions by mutual compatibility 403 386 std::vector<CandidateEnvMerger::OutType> compatible = filterCombos( 404 387 resn.deferred, 405 388 CandidateEnvMerger{ resn.alt.env, resn.alt.openVars, resn.indexer } ); 389 // fail early if no mutually-compatible assertion satisfaction 390 if ( compatible.empty() ) { 391 Indenter tabs{ Indenter::tabsize, 3 }; 392 std::ostringstream ss; 393 ss << tabs << "Unsatisfiable alternative:\n"; 394 resn.alt.print( ss, ++tabs ); 395 ss << --tabs << "No mutually-compatible satisfaction for assertions:\n"; 396 ++tabs; 397 for ( const auto& d : resn.deferred ) { 398 d.decl->print( ss, tabs ); 399 } 400 401 errors.emplace_back( ss.str() ); 402 goto nextResn; 403 } 406 404 // sort by cost 407 405 CandidateCost coster{ resn.indexer }; … … 429 427 new_resn.newNeed.insert( match.need.begin(), match.need.end() ); 430 428 431 // for each deferred assertion with the same form 432 for ( AssnId id : r.item.deferIds ) { 433 bindAssertion( 434 id.decl, id.info, new_resn.alt, match, new_resn.inferred ); 435 } 429 bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred ); 436 430 } 437 431
Note:
See TracChangeset
for help on using the changeset viewer.
