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