Changeset 46da46b for src/ResolvExpr/SatisfyAssertions.cpp
- Timestamp:
- May 2, 2023, 3:44:31 AM (15 months ago)
- Branches:
- ast-experimental, master
- Children:
- 0c840fc
- Parents:
- 1ab773e0
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ResolvExpr/SatisfyAssertions.cpp
r1ab773e0 r46da46b 16 16 #include "SatisfyAssertions.hpp" 17 17 18 #include <iostream> 18 19 #include <algorithm> 19 20 #include <cassert> … … 42 43 #include "SymTab/Mangler.h" 43 44 45 46 44 47 namespace ResolvExpr { 45 48 … … 62 65 ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) 63 66 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 64 need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {} 67 need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) { 68 if (!have.empty()) { 69 std::cerr << c.id->location << ':' << c.id->name << std::endl; 70 } 71 } 65 72 }; 66 73 … … 136 143 }; 137 144 138 /// Adds a captured assertion to the symbol table 139 void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) { 140 for ( auto & i : have ) { 141 if ( i.second.isUsed ) { symtab.addId( i.first->var ); } 142 } 143 } 145 144 146 145 147 /// Binds a single assertion, updating satisfaction state … … 152 154 "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); 153 155 154 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->c vtCost );156 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cost ); 155 157 varExpr->result = match.adjType; 156 158 if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); } … … 162 164 163 165 /// Satisfy a single assertion 164 bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool allowConversion = false, boolskipUnbound = false) {166 bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool skipUnbound = false) { 165 167 // skip unused assertions 168 static unsigned int cnt = 0; 166 169 if ( ! assn.second.isUsed ) return true; 167 170 171 if (assn.first->var->name[1] == '|') std::cerr << ++cnt << std::endl; 172 168 173 // find candidates that unify with the desired type 169 AssnCandidateList matches ;174 AssnCandidateList matches, inexactMatches; 170 175 171 176 std::vector<ast::SymbolTable::IdData> candidates; … … 209 214 210 215 ast::OpenVarSet closed; 211 findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed ); 212 findOpenVars( adjType, newOpen, closed, newNeed, have, FirstOpen ); 213 if ( allowConversion ) { 216 // findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed ); 217 findOpenVars( adjType, newOpen, closed, newNeed, have, newEnv, FirstOpen ); 218 ast::TypeEnvironment tempNewEnv {newEnv}; 219 220 if ( unifyExact( toType, adjType, tempNewEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) { 221 // set up binding slot for recursive assertions 222 ast::UniqueId crntResnSlot = 0; 223 if ( ! newNeed.empty() ) { 224 crntResnSlot = ++globalResnSlot; 225 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } 226 } 227 228 matches.emplace_back( 229 cdata, adjType, std::move( tempNewEnv ), std::move( have ), std::move( newNeed ), 230 std::move( newOpen ), crntResnSlot ); 231 } 232 else if ( matches.empty() ) { 233 // restore invalidated env 234 // newEnv = sat.cand->env; 235 // newNeed.clear(); 214 236 if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) { 215 237 // set up binding slot for recursive assertions … … 220 242 } 221 243 222 matches.emplace_back(244 inexactMatches.emplace_back( 223 245 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), 224 246 std::move( newOpen ), crntResnSlot ); 225 247 } 226 248 } 227 else {228 if ( unifyExact( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {229 // set up binding slot for recursive assertions230 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 }240 }241 249 } 242 250 243 251 // break if no satisfying match 252 if ( matches.empty() ) matches = std::move(inexactMatches); 244 253 if ( matches.empty() ) return false; 245 254 … … 252 261 // otherwise bind unique match in ongoing scope 253 262 AssnCandidate & match = matches.front(); 254 addToSymbolTable( match.have, sat.symtab );263 // addToSymbolTable( match.have, sat.symtab ); 255 264 sat.newNeed.insert( match.need.begin(), match.need.end() ); 256 265 sat.cand->env = std::move( match.env ); … … 435 444 // for each current mutually-compatible set of assertions 436 445 for ( SatState & sat : sats ) { 437 bool allowConversion = false;438 446 // stop this branch if a better option is already found 439 447 auto it = thresholds.find( pruneKey( *sat.cand ) ); … … 448 456 for ( auto & assn : sat.need ) { 449 457 // fail early if any assertion is not satisfiable 450 if ( ! satisfyAssertion( assn, sat, allowConversion,!next.empty() ) ) {458 if ( ! satisfyAssertion( assn, sat, !next.empty() ) ) { 451 459 next.emplace_back(assn); 452 460 // goto nextSat; … … 457 465 // fail if nothing resolves 458 466 else if (next.size() == sat.need.size()) { 459 if (allowConversion) {467 // if (allowConversion) { 460 468 Indenter tabs{ 3 }; 461 469 std::ostringstream ss; … … 467 475 errors.emplace_back( ss.str() ); 468 476 goto nextSat; 469 } 470 471 else { 472 allowConversion = true; 473 continue; 474 } 475 } 476 allowConversion = false; 477 // } 478 479 // else { 480 // allowConversion = true; 481 // continue; 482 // } 483 } 477 484 sat.need = std::move(next); 478 485 } … … 528 535 sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 529 536 ast::AssertionSet{} /* need moved into satisfaction state */, 530 sat.cand->cost , sat.cand->cvtCost);537 sat.cand->cost ); 531 538 532 539 ast::AssertionSet nextNewNeed{ sat.newNeed }; … … 541 548 for ( DeferRef r : compat.assns ) { 542 549 AssnCandidate match = r.match; 543 addToSymbolTable( match.have, nextSymtab );550 // addToSymbolTable( match.have, nextSymtab ); 544 551 nextNewNeed.insert( match.need.begin(), match.need.end() ); 545 552
Note: See TracChangeset
for help on using the changeset viewer.