- File:
-
- 1 edited
-
src/ResolvExpr/SatisfyAssertions.cpp (modified) (22 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ResolvExpr/SatisfyAssertions.cpp
r1958fec ref1da0e2 36 36 #include "AST/SymbolTable.hpp" 37 37 #include "AST/TypeEnvironment.hpp" 38 #include "FindOpenVars.h" 38 39 #include "Common/FilterCombos.h" 39 40 #include "Common/Indenter.h" … … 57 58 ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs 58 59 59 AssnCandidate( 60 const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 60 AssnCandidate( 61 const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 61 62 ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) 62 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 63 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 63 64 need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {} 64 65 }; … … 73 74 const AssnCandidate & match; 74 75 }; 75 76 /// Wrapper for the deferred items from a single assertion satisfaction. 76 77 /// Wrapper for the deferred items from a single assertion satisfaction. 77 78 /// Acts like an indexed list of DeferRef 78 79 struct DeferItem { … … 81 82 AssnCandidateList matches; 82 83 83 DeferItem( 84 DeferItem( 84 85 const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) 85 86 : expr( d ), info( i ), matches( std::move( ms ) ) {} … … 117 118 /// Initial satisfaction state for a candidate 118 119 SatState( CandidateRef & c, const ast::SymbolTable & syms ) 119 : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 120 : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 120 121 symtab( syms ) { need.swap( c->need ); } 121 122 122 123 /// Update satisfaction state for next step after previous state 123 124 SatState( SatState && o, IterateFlag ) 124 : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 125 deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 125 : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 126 deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 126 127 symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } 127 128 128 129 /// Field-wise next step constructor 129 130 SatState( 130 CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 131 CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 131 132 ast::SymbolTable && syms ) 132 : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 133 : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 133 134 inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) 134 135 { costs.emplace_back( Cost::zero ); } … … 143 144 144 145 /// Binds a single assertion, updating satisfaction state 145 void bindAssertion( 146 const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 146 void bindAssertion( 147 const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 147 148 AssnCandidate & match, InferCache & inferred 148 149 ) { 149 150 const ast::DeclWithType * candidate = match.cdata.id; 150 assertf( candidate->uniqueId, 151 assertf( candidate->uniqueId, 151 152 "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); 152 153 153 154 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost ); 154 155 varExpr->result = match.adjType; … … 161 162 162 163 /// Satisfy a single assertion 163 bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat 164 bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool allowConversion = false, bool skipUnbound = false) { 164 165 // skip unused assertions 165 166 if ( ! assn.second.isUsed ) return true; … … 180 181 if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer; 181 182 else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams); 183 else if (skipUnbound) return false; 182 184 183 185 candidates = sat.symtab.specialLookupId(kind, otypeKey); … … 201 203 ast::OpenVarSet newOpen{ sat.cand->open }; 202 204 ast::ptr< ast::Type > toType = assn.first->result; 203 ast::ptr< ast::Type > adjType = 205 ast::ptr< ast::Type > adjType = 204 206 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false ); 205 207 206 208 // only keep candidates which unify 207 if ( unify( toType, adjType, newEnv, newNeed, have, newOpen, sat.symtab ) ) { 208 // set up binding slot for recursive assertions 209 ast::UniqueId crntResnSlot = 0; 210 if ( ! newNeed.empty() ) { 211 crntResnSlot = ++globalResnSlot; 212 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } 213 } 214 215 matches.emplace_back( 216 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), 217 std::move( newOpen ), crntResnSlot ); 209 210 ast::OpenVarSet closed; 211 findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed ); 212 findOpenVars( adjType, newOpen, closed, newNeed, have, FirstOpen ); 213 if ( allowConversion ) { 214 if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) { 215 // set up binding slot for recursive assertions 216 ast::UniqueId crntResnSlot = 0; 217 if ( ! newNeed.empty() ) { 218 crntResnSlot = ++globalResnSlot; 219 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } 220 } 221 222 matches.emplace_back( 223 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), 224 std::move( newOpen ), crntResnSlot ); 225 } 226 } 227 else { 228 if ( unifyExact( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) { 229 // set up binding slot for recursive assertions 230 ast::UniqueId crntResnSlot = 0; 231 if ( ! newNeed.empty() ) { 232 crntResnSlot = ++globalResnSlot; 233 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } 234 } 235 236 matches.emplace_back( 237 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), 238 std::move( newOpen ), crntResnSlot ); 239 } 218 240 } 219 241 } … … 287 309 }; 288 310 289 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 311 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 290 312 /// threshold. 291 void finalizeAssertions( 292 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 293 CandidateList & out 313 void finalizeAssertions( 314 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 315 CandidateList & out 294 316 ) { 295 317 // prune if cheaper alternative for same key has already been generated … … 308 330 } 309 331 310 /// Combo iterator that combines candidates into an output list, merging their environments. 311 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 332 /// Combo iterator that combines candidates into an output list, merging their environments. 333 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 312 334 /// for description of "combo iterator". 313 335 class CandidateEnvMerger { … … 390 412 } // anonymous namespace 391 413 392 void satisfyAssertions( 393 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 414 void satisfyAssertions( 415 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 394 416 std::vector<std::string> & errors 395 417 ) { … … 413 435 // for each current mutually-compatible set of assertions 414 436 for ( SatState & sat : sats ) { 437 bool allowConversion = false; 415 438 // stop this branch if a better option is already found 416 439 auto it = thresholds.find( pruneKey( *sat.cand ) ); … … 418 441 419 442 // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen. 420 for (unsigned resetCount = 0; ; ++resetCount) { 443 444 for (unsigned resetCount = 0; ; ++resetCount) { 421 445 ast::AssertionList next; 422 446 resetTyVarRenaming(); … … 424 448 for ( auto & assn : sat.need ) { 425 449 // fail early if any assertion is not satisfiable 426 if ( ! satisfyAssertion( assn, sat ) ) {450 if ( ! satisfyAssertion( assn, sat, allowConversion, !next.empty() ) ) { 427 451 next.emplace_back(assn); 428 452 // goto nextSat; … … 433 457 // fail if nothing resolves 434 458 else if (next.size() == sat.need.size()) { 435 Indenter tabs{ 3 }; 436 std::ostringstream ss; 437 ss << tabs << "Unsatisfiable alternative:\n"; 438 print( ss, *sat.cand, ++tabs ); 439 ss << (tabs-1) << "Could not satisfy assertion:\n"; 440 ast::print( ss, next[0].first, tabs ); 441 442 errors.emplace_back( ss.str() ); 443 goto nextSat; 444 } 459 if (allowConversion) { 460 Indenter tabs{ 3 }; 461 std::ostringstream ss; 462 ss << tabs << "Unsatisfiable alternative:\n"; 463 print( ss, *sat.cand, ++tabs ); 464 ss << (tabs-1) << "Could not satisfy assertion:\n"; 465 ast::print( ss, next[0].first, tabs ); 466 467 errors.emplace_back( ss.str() ); 468 goto nextSat; 469 } 470 471 else { 472 allowConversion = true; 473 continue; 474 } 475 } 476 allowConversion = false; 445 477 sat.need = std::move(next); 446 478 } … … 449 481 // either add successful match or push back next state 450 482 if ( sat.newNeed.empty() ) { 451 finalizeAssertions( 483 finalizeAssertions( 452 484 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out ); 453 485 } else { … … 471 503 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos( 472 504 sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } ); 473 505 474 506 // fail early if no mutually-compatible assertion satisfaction 475 507 if ( compatible.empty() ) { … … 494 526 // set up next satisfaction state 495 527 CandidateRef nextCand = std::make_shared<Candidate>( 496 sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 528 sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 497 529 ast::AssertionSet{} /* need moved into satisfaction state */, 498 530 sat.cand->cost, sat.cand->cvtCost ); … … 500 532 ast::AssertionSet nextNewNeed{ sat.newNeed }; 501 533 InferCache nextInferred{ sat.inferred }; 502 534 503 535 CostVec nextCosts{ sat.costs }; 504 536 nextCosts.back() += compat.cost; 505 537 506 538 ast::SymbolTable nextSymtab{ sat.symtab }; 507 539 … … 517 549 // either add successful match or push back next state 518 550 if ( nextNewNeed.empty() ) { 519 finalizeAssertions( 551 finalizeAssertions( 520 552 nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); 521 553 } else { 522 nextSats.emplace_back( 523 std::move( nextCand ), std::move( nextNewNeed ), 524 std::move( nextInferred ), std::move( nextCosts ), 554 nextSats.emplace_back( 555 std::move( nextCand ), std::move( nextNewNeed ), 556 std::move( nextInferred ), std::move( nextCosts ), 525 557 std::move( nextSymtab ) ); 526 558 } … … 534 566 nextSats.clear(); 535 567 } 536 568 537 569 // exceeded recursion limit if reaches here 538 570 if ( out.empty() ) {
Note:
See TracChangeset
for help on using the changeset viewer.
