- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ResolvExpr/SatisfyAssertions.cpp
r5b9a0ae r1958fec 69 69 /// Reference to a single deferred item 70 70 struct DeferRef { 71 const ast:: DeclWithType * decl;71 const ast::VariableExpr * expr; 72 72 const ast::AssertionSetValue & info; 73 73 const AssnCandidate & match; … … 77 77 /// Acts like an indexed list of DeferRef 78 78 struct DeferItem { 79 const ast:: DeclWithType * decl;79 const ast::VariableExpr * expr; 80 80 const ast::AssertionSetValue & info; 81 81 AssnCandidateList matches; 82 82 83 83 DeferItem( 84 const ast:: DeclWithType* d, const ast::AssertionSetValue & i, AssnCandidateList && ms )85 : decl( d ), info( i ), matches( std::move( ms ) ) {}84 const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) 85 : expr( d ), info( i ), matches( std::move( ms ) ) {} 86 86 87 87 bool empty() const { return matches.empty(); } … … 89 89 AssnCandidateList::size_type size() const { return matches.size(); } 90 90 91 DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }91 DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; } 92 92 }; 93 93 … … 138 138 void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) { 139 139 for ( auto & i : have ) { 140 if ( i.second.isUsed ) { symtab.addId( i.first ); }140 if ( i.second.isUsed ) { symtab.addId( i.first->var ); } 141 141 } 142 142 } … … 144 144 /// Binds a single assertion, updating satisfaction state 145 145 void bindAssertion( 146 const ast:: DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand,146 const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 147 147 AssnCandidate & match, InferCache & inferred 148 148 ) { … … 156 156 157 157 // place newly-inferred assertion in proper location in cache 158 inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{159 candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };158 inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{ 159 candidate->uniqueId, candidate, match.adjType, expr->result, varExpr }; 160 160 } 161 161 … … 169 169 170 170 std::vector<ast::SymbolTable::IdData> candidates; 171 auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first-> name);171 auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name); 172 172 if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) { 173 173 // prefilter special decls by argument type, if already known 174 ast::ptr<ast::Type> thisArgType = strict_dynamic_cast<const ast::PointerType *>(assn.first->get_type())->base174 ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base 175 175 .strict_as<ast::FunctionType>()->params[0] 176 176 .strict_as<ast::ReferenceType>()->base; … … 184 184 } 185 185 else { 186 candidates = sat.symtab.lookupId(assn.first-> name);186 candidates = sat.symtab.lookupId(assn.first->var->name); 187 187 } 188 188 for ( const ast::SymbolTable::IdData & cdata : candidates ) { … … 200 200 ast::TypeEnvironment newEnv{ sat.cand->env }; 201 201 ast::OpenVarSet newOpen{ sat.cand->open }; 202 ast::ptr< ast::Type > toType = assn.first-> get_type();202 ast::ptr< ast::Type > toType = assn.first->result; 203 203 ast::ptr< ast::Type > adjType = 204 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );204 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false ); 205 205 206 206 // only keep candidates which unify … … 337 337 // compute conversion cost from satisfying decl to assertion 338 338 cost += computeConversionCost( 339 assn.match.adjType, assn. decl->get_type(), false, symtab, env );339 assn.match.adjType, assn.expr->result, false, symtab, env ); 340 340 341 341 // mark vars+specialization on function-type assertions … … 350 350 cost.incVar( func->forall.size() ); 351 351 352 for ( const ast::TypeDecl * td : func->forall ) { 353 cost.decSpec( td->assertions.size() ); 354 } 352 cost.decSpec( func->assertions.size() ); 355 353 } 356 354 } … … 387 385 388 386 /// Limit to depth of recursion of assertion satisfaction 389 static const int recursionLimit = 4;387 static const int recursionLimit = 8; 390 388 /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of 391 389 static const int deferLimit = 10; … … 419 417 if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat; 420 418 421 // make initial pass at matching assertions 422 for ( auto & assn : sat.need ) { 423 // fail early if any assertion is not satisfiable 424 if ( ! satisfyAssertion( assn, sat ) ) { 419 // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen. 420 for (unsigned resetCount = 0; ; ++resetCount) { 421 ast::AssertionList next; 422 resetTyVarRenaming(); 423 // make initial pass at matching assertions 424 for ( auto & assn : sat.need ) { 425 // fail early if any assertion is not satisfiable 426 if ( ! satisfyAssertion( assn, sat ) ) { 427 next.emplace_back(assn); 428 // goto nextSat; 429 } 430 } 431 // success 432 if (next.empty()) break; 433 // fail if nothing resolves 434 else if (next.size() == sat.need.size()) { 425 435 Indenter tabs{ 3 }; 426 436 std::ostringstream ss; … … 428 438 print( ss, *sat.cand, ++tabs ); 429 439 ss << (tabs-1) << "Could not satisfy assertion:\n"; 430 ast::print( ss, assn.first, tabs );440 ast::print( ss, next[0].first, tabs ); 431 441 432 442 errors.emplace_back( ss.str() ); 433 443 goto nextSat; 434 444 } 445 sat.need = std::move(next); 435 446 } 436 447 … … 451 462 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n"; 452 463 for ( const auto & d : sat.deferred ) { 453 ast::print( ss, d. decl, tabs );464 ast::print( ss, d.expr, tabs ); 454 465 } 455 466 … … 469 480 ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n"; 470 481 for ( const auto& d : sat.deferred ) { 471 ast::print( ss, d. decl, tabs );482 ast::print( ss, d.expr, tabs ); 472 483 } 473 484 … … 501 512 nextNewNeed.insert( match.need.begin(), match.need.end() ); 502 513 503 bindAssertion( r. decl, r.info, nextCand, match, nextInferred );514 bindAssertion( r.expr, r.info, nextCand, match, nextInferred ); 504 515 } 505 516
Note: See TracChangeset
for help on using the changeset viewer.