Changeset ed1a6374 for src

Timestamp:

Jan 5, 2021, 2:51:58 PM (5 years ago)

Author:

Thierry Delisle <tdelisle@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, master, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

f03209d3

Parents:

c4241b6 (diff), 95eec2c (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

Location:

src/ResolvExpr

Files:

• RenameVars.cc (modified) (2 diffs)
• RenameVars.h (modified) (1 diff)
• Resolver.cc (modified) (1 diff)
• SatisfyAssertions.cpp (modified) (4 diffs)

src/ResolvExpr/RenameVars.cc

@@ -186 +186 @@
 }
 
-const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode ) {
+const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode, bool reset ) {
         // ast::Type *tc = ast::deepCopy(t);
         ast::Pass<RenameVars_new> renamer;
         renamer.core.mode = mode;
-        if (mode == GEN_USAGE) {
+        if (mode == GEN_USAGE && reset) {
                 renaming.nextUsage();
         }
@@ -198 +198 @@
 void resetTyVarRenaming() {
         renaming.reset();
+        renaming.nextUsage();
 }
 

src/ResolvExpr/RenameVars.h

@@ -35 +35 @@
                 GEN_EXPR_ID // for type in decl
         };
-        const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE );
+        const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE, bool reset = true );
+        
 
         /// resets internal state of renamer to avoid overflow

src/ResolvExpr/Resolver.cc

@@ -1151 +1151 @@
                         const ast::Expr * untyped, const ast::SymbolTable & symtab
                 ) {
-                        resetTyVarRenaming();
                         ast::TypeEnvironment env;
                         ast::ptr< ast::Expr > newExpr = resolveInVoidContext( untyped, symtab, env );

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 ) );
+                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
 
                         // only keep candidates which unify
@@ -385 +385 @@
 
         /// Limit to depth of recursion of assertion satisfaction
-        static const int recursionLimit = 4;
+        static const int recursionLimit = 8;
         /// 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;
 
-                        // make initial pass at matching assertions
-                        for ( auto & assn : sat.need ) {
-                                // fail early if any assertion is not satisfiable
-                                if ( ! satisfyAssertion( assn, sat ) ) {
+                        // 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()) {
                                         Indenter tabs{ 3 };
                                         std::ostringstream ss;
@@ -426 +438 @@
                                         print( ss, *sat.cand, ++tabs );
                                         ss << (tabs-1) << "Could not satisfy assertion:\n";
-                                        ast::print( ss, assn.first, tabs );
+                                        ast::print( ss, next[0].first, tabs );
 
                                         errors.emplace_back( ss.str() );
                                         goto nextSat;
                                 }
+                                sat.need = std::move(next);
                         }