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

File:

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

src/ResolvExpr/SatisfyAssertions.cpp

@@ -9 +9 @@
 // Author           : Aaron B. Moss
 // Created On       : Mon Jun 10 17:45:00 2019
-// Last Modified By : Aaron B. Moss
-// Last Modified On : Mon Jun 10 17:45:00 2019
-// Update Count     : 1
+// Last Modified By : Andrew Beach
+// Last Modified On : Tue Oct  1 13:56:00 2019
+// Update Count     : 2
 //
 
@@ -69 +69 @@
         /// Reference to a single deferred item
         struct DeferRef {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 const AssnCandidate & match;
@@ -77 +77 @@
         /// Acts like an indexed list of DeferRef
         struct DeferItem {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 AssnCandidateList matches;
 
                 DeferItem( 
-                        const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
-                : decl( d ), info( i ), matches( std::move( ms ) ) {}
+                        const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
+                : expr( d ), info( i ), matches( std::move( ms ) ) {}
 
                 bool empty() const { return matches.empty(); }
@@ -89 +89 @@
                 AssnCandidateList::size_type size() const { return matches.size(); }
 
-                DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+                DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
         };
 
@@ -138 +138 @@
         void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
                 for ( auto & i : have ) {
-                        if ( i.second.isUsed ) { symtab.addId( i.first ); }
+                        if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
                 }
         }
@@ -144 +144 @@
         /// Binds a single assertion, updating satisfaction state
         void bindAssertion( 
-                const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+                const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 
                 AssnCandidate & match, InferCache & inferred
         ) {
@@ -156 +156 @@
 
                 // place newly-inferred assertion in proper location in cache
-                inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{
-                        candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };
+                inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
+                        candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
         }
 
@@ -167 +167 @@
                 // find candidates that unify with the desired type
                 AssnCandidateList matches;
-                for ( const ast::SymbolTable::IdData & cdata : sat.symtab.lookupId( assn.first->name ) ) {
+
+                std::vector<ast::SymbolTable::IdData> candidates;
+                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
+                if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
+                        // prefilter special decls by argument type, if already known
+                        ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
+                                .strict_as<ast::FunctionType>()->params[0]
+                                .strict_as<ast::ReferenceType>()->base;
+                        sat.cand->env.apply(thisArgType);
+
+                        std::string otypeKey = "";
+                        if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer;
+                        else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams);
+
+                        candidates = sat.symtab.specialLookupId(kind, otypeKey);
+                }
+                else {
+                        candidates = sat.symtab.lookupId(assn.first->var->name);
+                }
+                for ( const ast::SymbolTable::IdData & cdata : candidates ) {
                         const ast::DeclWithType * candidate = cdata.id;
+
+                        // ignore deleted candidates.
+                        // NOTE: this behavior is different from main resolver.
+                        // further investigations might be needed to determine
+                        // if we should implement the same rule here
+                        // (i.e. error if unique best match is deleted)
+                        if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue;
 
                         // build independent unification context for candidate
@@ -174 +200 @@
                         ast::TypeEnvironment newEnv{ sat.cand->env };
                         ast::OpenVarSet newOpen{ sat.cand->open };
-                        ast::ptr< ast::Type > toType = assn.first->get_type();
+                        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
@@ -188 +214 @@
 
                                 matches.emplace_back( 
-                                        cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ), 
+                                        cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
                                         std::move( newOpen ), crntResnSlot );
                         }
@@ -229 +255 @@
                 InferMatcher( InferCache & inferred ) : inferred( inferred ) {}
 
-                const ast::Expr * postmutate( const ast::Expr * expr ) {
+                const ast::Expr * postvisit( const ast::Expr * expr ) {
                         // Skip if no slots to find
-                        if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
-
+                        if ( !expr->inferred.hasSlots() ) return expr;
+                        // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
+                        std::vector<UniqueId> missingSlots;
                         // find inferred parameters for resolution slots
-                        ast::InferredParams newInferred;
+                        ast::InferredParams * newInferred = new ast::InferredParams();
                         for ( UniqueId slot : expr->inferred.resnSlots() ) {
                                 // fail if no matching assertions found
                                 auto it = inferred.find( slot );
                                 if ( it == inferred.end() ) {
-                                        assert(!"missing assertion");
+                                        // std::cerr << "missing assertion " << slot << std::endl;
+                                        missingSlots.push_back(slot);
+                                        continue;
                                 }
 
@@ -245 +274 @@
                                 for ( auto & entry : it->second ) {
                                         // recurse on inferParams of resolved expressions
-                                        entry.second.expr = postmutate( entry.second.expr );
-                                        auto res = newInferred.emplace( entry );
+                                        entry.second.expr = postvisit( entry.second.expr );
+                                        auto res = newInferred->emplace( entry );
                                         assert( res.second && "all assertions newly placed" );
                                 }
@@ -252 +281 @@
 
                         ast::Expr * ret = mutate( expr );
-                        ret->inferred.set_inferParams( std::move( newInferred ) );
+                        ret->inferred.set_inferParams( newInferred );
+                        if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots;
                         return ret;
                 }
@@ -299 +329 @@
                         Cost cost;
 
-                        OutType( 
-                                const ast::TypeEnvironment & e, const ast::OpenVarSet & o, 
+                        OutType(
+                                const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
                                 const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
                         : env( e ), open( o ), assns( as ), cost( Cost::zero ) {
@@ -306 +336 @@
                                 for ( const DeferRef & assn : assns ) {
                                         // compute conversion cost from satisfying decl to assertion
-                                        cost += computeConversionCost( 
-                                                assn.match.adjType, assn.decl->get_type(), symtab, env );
-                                        
+                                        cost += computeConversionCost(
+                                                assn.match.adjType, assn.expr->result, false, symtab, env );
+
                                         // mark vars+specialization on function-type assertions
-                                        const ast::FunctionType * func = 
+                                        const ast::FunctionType * func =
                                                 GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
                                         if ( ! func ) continue;
 
-                                        for ( const ast::DeclWithType * param : func->params ) {
-                                                cost.decSpec( specCost( param->get_type() ) );
+                                        for ( const auto & param : func->params ) {
+                                                cost.decSpec( specCost( param ) );
                                         }
-                                        
+
                                         cost.incVar( func->forall.size() );
-                                        
-                                        for ( const ast::TypeDecl * td : func->forall ) {
-                                                cost.decSpec( td->assertions.size() );
-                                        }
+
+                                        cost.decSpec( func->assertions.size() );
                                 }
                         }
@@ -329 +357 @@
                 };
 
-                CandidateEnvMerger( 
-                        const ast::TypeEnvironment & env, const ast::OpenVarSet & open, 
+                CandidateEnvMerger(
+                        const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
                         const ast::SymbolTable & syms )
                 : crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
@@ -357 +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;
@@ -389 +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;
@@ -398 +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);
                         }
 
@@ -421 +462 @@
                                 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
                                 for ( const auto & d : sat.deferred ) {
-                                        ast::print( ss, d.decl, tabs );
+                                        ast::print( ss, d.expr, tabs );
                                 }
 
@@ -439 +480 @@
                                         ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
                                         for ( const auto& d : sat.deferred ) {
-                                                ast::print( ss, d.decl, tabs );
+                                                ast::print( ss, d.expr, tabs );
                                         }
 
@@ -471 +512 @@
                                                 nextNewNeed.insert( match.need.begin(), match.need.end() );
 
-                                                bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
+                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
                                         }