Changes in src/ResolvExpr/SatisfyAssertions.cpp [1958fec:3e5dd913]

File:

• src/ResolvExpr/SatisfyAssertions.cpp (modified) (4 diffs)

src/ResolvExpr/SatisfyAssertions.cpp

@@ -202 +202 @@
                         ast::ptr< ast::Type > toType = assn.first->result;
                         ast::ptr< ast::Type > adjType = 
-                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
+                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
 
                         // only keep candidates which unify
@@ -385 +385 @@
 
         /// Limit to depth of recursion of assertion satisfaction
-        static const int recursionLimit = 8;
+        static const int recursionLimit = 4;
         /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
         static const int deferLimit = 10;
@@ -417 +417 @@
                         if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
 
-                        // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
-                        for (unsigned resetCount = 0; ; ++resetCount) { 
-                                ast::AssertionList next;
-                                resetTyVarRenaming();
-                                // make initial pass at matching assertions
-                                for ( auto & assn : sat.need ) {
-                                        // fail early if any assertion is not satisfiable
-                                        if ( ! satisfyAssertion( assn, sat ) ) {
-                                                next.emplace_back(assn);
-                                                // goto nextSat;
-                                        }
-                                }
-                                // success
-                                if (next.empty()) break;
-                                // fail if nothing resolves
-                                else if (next.size() == sat.need.size()) {
+                        // make initial pass at matching assertions
+                        for ( auto & assn : sat.need ) {
+                                // fail early if any assertion is not satisfiable
+                                if ( ! satisfyAssertion( assn, sat ) ) {
                                         Indenter tabs{ 3 };
                                         std::ostringstream ss;
@@ -438 +426 @@
                                         print( ss, *sat.cand, ++tabs );
                                         ss << (tabs-1) << "Could not satisfy assertion:\n";
-                                        ast::print( ss, next[0].first, tabs );
+                                        ast::print( ss, assn.first, tabs );
 
                                         errors.emplace_back( ss.str() );
                                         goto nextSat;
                                 }
-                                sat.need = std::move(next);
                         }