Index: src/ResolvExpr/ResolveAssertions.cc =================================================================== --- src/ResolvExpr/ResolveAssertions.cc (revision 1958fec9f9994b819ba4d3a3fde1aab2a6393be1) +++ src/ResolvExpr/ResolveAssertions.cc (revision a00bc5b670e302caf7b7a128c32475c702fd7890) @@ -397,5 +397,5 @@ /// Limit to depth of recursion of assertion satisfaction - static const int recursionLimit = 4; + static const int recursionLimit = 7; /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of static const int deferLimit = 10; Index: src/ResolvExpr/SatisfyAssertions.cpp =================================================================== --- src/ResolvExpr/SatisfyAssertions.cpp (revision 1958fec9f9994b819ba4d3a3fde1aab2a6393be1) +++ src/ResolvExpr/SatisfyAssertions.cpp (revision a00bc5b670e302caf7b7a128c32475c702fd7890) @@ -57,8 +57,8 @@ ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs - AssnCandidate( - const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, + AssnCandidate( + const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) - : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), + : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {} }; @@ -73,6 +73,6 @@ const AssnCandidate & match; }; - - /// Wrapper for the deferred items from a single assertion satisfaction. + + /// Wrapper for the deferred items from a single assertion satisfaction. /// Acts like an indexed list of DeferRef struct DeferItem { @@ -81,5 +81,5 @@ AssnCandidateList matches; - DeferItem( + DeferItem( const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) : expr( d ), info( i ), matches( std::move( ms ) ) {} @@ -117,18 +117,18 @@ /// Initial satisfaction state for a candidate SatState( CandidateRef & c, const ast::SymbolTable & syms ) - : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, + : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, symtab( syms ) { need.swap( c->need ); } - + /// Update satisfaction state for next step after previous state SatState( SatState && o, IterateFlag ) - : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), - deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), + : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), + deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } - + /// Field-wise next step constructor SatState( - CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, + CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, ast::SymbolTable && syms ) - : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), + : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) { costs.emplace_back( Cost::zero ); } @@ -143,12 +143,12 @@ /// Binds a single assertion, updating satisfaction state - void bindAssertion( - const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, + void bindAssertion( + const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, AssnCandidate & match, InferCache & inferred ) { const ast::DeclWithType * candidate = match.cdata.id; - assertf( candidate->uniqueId, + assertf( candidate->uniqueId, "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); - + ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost ); varExpr->result = match.adjType; @@ -201,5 +201,5 @@ ast::OpenVarSet newOpen{ sat.cand->open }; ast::ptr< ast::Type > toType = assn.first->result; - ast::ptr< ast::Type > adjType = + ast::ptr< ast::Type > adjType = renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false ); @@ -213,5 +213,5 @@ } - matches.emplace_back( + matches.emplace_back( cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), std::move( newOpen ), crntResnSlot ); @@ -287,9 +287,9 @@ }; - /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning + /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning /// threshold. - void finalizeAssertions( - CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, - CandidateList & out + void finalizeAssertions( + CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, + CandidateList & out ) { // prune if cheaper alternative for same key has already been generated @@ -308,6 +308,6 @@ } - /// Combo iterator that combines candidates into an output list, merging their environments. - /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` + /// Combo iterator that combines candidates into an output list, merging their environments. + /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` /// for description of "combo iterator". class CandidateEnvMerger { @@ -390,6 +390,6 @@ } // anonymous namespace -void satisfyAssertions( - CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, +void satisfyAssertions( + CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, std::vector & errors ) { @@ -418,5 +418,5 @@ // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen. - for (unsigned resetCount = 0; ; ++resetCount) { + for (unsigned resetCount = 0; ; ++resetCount) { ast::AssertionList next; resetTyVarRenaming(); @@ -449,5 +449,5 @@ // either add successful match or push back next state if ( sat.newNeed.empty() ) { - finalizeAssertions( + finalizeAssertions( sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out ); } else { @@ -471,5 +471,5 @@ std::vector< CandidateEnvMerger::OutType > compatible = filterCombos( sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } ); - + // fail early if no mutually-compatible assertion satisfaction if ( compatible.empty() ) { @@ -494,5 +494,5 @@ // set up next satisfaction state CandidateRef nextCand = std::make_shared( - sat.cand->expr, std::move( compat.env ), std::move( compat.open ), + sat.cand->expr, std::move( compat.env ), std::move( compat.open ), ast::AssertionSet{} /* need moved into satisfaction state */, sat.cand->cost, sat.cand->cvtCost ); @@ -500,8 +500,8 @@ ast::AssertionSet nextNewNeed{ sat.newNeed }; InferCache nextInferred{ sat.inferred }; - + CostVec nextCosts{ sat.costs }; nextCosts.back() += compat.cost; - + ast::SymbolTable nextSymtab{ sat.symtab }; @@ -517,10 +517,10 @@ // either add successful match or push back next state if ( nextNewNeed.empty() ) { - finalizeAssertions( + finalizeAssertions( nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); } else { - nextSats.emplace_back( - std::move( nextCand ), std::move( nextNewNeed ), - std::move( nextInferred ), std::move( nextCosts ), + nextSats.emplace_back( + std::move( nextCand ), std::move( nextNewNeed ), + std::move( nextInferred ), std::move( nextCosts ), std::move( nextSymtab ) ); } @@ -534,5 +534,5 @@ nextSats.clear(); } - + // exceeded recursion limit if reaches here if ( out.empty() ) {