Changeset ef1da0e2 for src/ResolvExpr/SatisfyAssertions.cpp

Timestamp:

Sep 20, 2022, 6:34:55 PM (2 years ago)

Author:

Fangren Yu <f37yu@…>

Branches:

ADT, ast-experimental, master, pthread-emulation

Children:

79ae13d, a065f1f

Parents:

8f1e035

Message:

try to make parameter qualifier conversion work for assertions

File:

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

src/ResolvExpr/SatisfyAssertions.cpp

@@ -36 +36 @@
 #include "AST/SymbolTable.hpp"
 #include "AST/TypeEnvironment.hpp"
+#include "FindOpenVars.h"
 #include "Common/FilterCombos.h"
 #include "Common/Indenter.h"
@@ -161 +162 @@
 
         /// Satisfy a single assertion
-        bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat ) {
+        bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool allowConversion = false, bool skipUnbound = false) {
                 // skip unused assertions
                 if ( ! assn.second.isUsed ) return true;
@@ -180 +181 @@
                         if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer;
                         else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams);
+                        else if (skipUnbound) return false;
 
                         candidates = sat.symtab.specialLookupId(kind, otypeKey);
@@ -205 +207 @@
 
                         // only keep candidates which unify
-                        if ( unify( toType, adjType, newEnv, newNeed, have, newOpen, sat.symtab ) ) {
-                                // set up binding slot for recursive assertions
-                                ast::UniqueId crntResnSlot = 0;
-                                if ( ! newNeed.empty() ) {
-                                        crntResnSlot = ++globalResnSlot;
-                                        for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
-                                }
-
-                                matches.emplace_back(
-                                        cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
-                                        std::move( newOpen ), crntResnSlot );
+
+                        ast::OpenVarSet closed;
+                        findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed );
+                        findOpenVars( adjType, newOpen, closed, newNeed, have, FirstOpen );
+                        if ( allowConversion ) {
+                                if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
+                                        // set up binding slot for recursive assertions
+                                        ast::UniqueId crntResnSlot = 0;
+                                        if ( ! newNeed.empty() ) {
+                                                crntResnSlot = ++globalResnSlot;
+                                                for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
+                                        }
+
+                                        matches.emplace_back(
+                                                cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
+                                                std::move( newOpen ), crntResnSlot );
+                                }
+                        }
+                        else {
+                                if ( unifyExact( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
+                                        // set up binding slot for recursive assertions
+                                        ast::UniqueId crntResnSlot = 0;
+                                        if ( ! newNeed.empty() ) {
+                                                crntResnSlot = ++globalResnSlot;
+                                                for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
+                                        }
+
+                                        matches.emplace_back(
+                                                cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
+                                                std::move( newOpen ), crntResnSlot );
+                                }
                         }
                 }
@@ -413 +435 @@
                 // for each current mutually-compatible set of assertions
                 for ( SatState & sat : sats ) {
+                        bool allowConversion = false;
                         // stop this branch if a better option is already found
                         auto it = thresholds.find( pruneKey( *sat.cand ) );
@@ -418 +441 @@
 
                         // 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;
@@ -424 +448 @@
                                 for ( auto & assn : sat.need ) {
                                         // fail early if any assertion is not satisfiable
-                                        if ( ! satisfyAssertion( assn, sat ) ) {
+                                        if ( ! satisfyAssertion( assn, sat, allowConversion, !next.empty() ) ) {
                                                 next.emplace_back(assn);
                                                 // goto nextSat;
@@ -433 +457 @@
                                 // fail if nothing resolves
                                 else if (next.size() == sat.need.size()) {
-                                        Indenter tabs{ 3 };
-                                        std::ostringstream ss;
-                                        ss << tabs << "Unsatisfiable alternative:\n";
-                                        print( ss, *sat.cand, ++tabs );
-                                        ss << (tabs-1) << "Could not satisfy assertion:\n";
-                                        ast::print( ss, next[0].first, tabs );
-
-                                        errors.emplace_back( ss.str() );
-                                        goto nextSat;
-                                }
+                                        if (allowConversion) {
+                                                Indenter tabs{ 3 };
+                                                std::ostringstream ss;
+                                                ss << tabs << "Unsatisfiable alternative:\n";
+                                                print( ss, *sat.cand, ++tabs );
+                                                ss << (tabs-1) << "Could not satisfy assertion:\n";
+                                                ast::print( ss, next[0].first, tabs );
+
+                                                errors.emplace_back( ss.str() );
+                                                goto nextSat;
+                                        }
+
+                                        else {
+                                                allowConversion = true;
+                                                continue;
+                                        }
+                                }
+                                allowConversion = false;
                                 sat.need = std::move(next);
                         }