[396037d] | 1 | // |
---|
| 2 | // Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo |
---|
| 3 | // |
---|
| 4 | // The contents of this file are covered under the licence agreement in the |
---|
| 5 | // file "LICENCE" distributed with Cforall. |
---|
| 6 | // |
---|
| 7 | // SatisfyAssertions.cpp -- |
---|
| 8 | // |
---|
| 9 | // Author : Aaron B. Moss |
---|
| 10 | // Created On : Mon Jun 10 17:45:00 2019 |
---|
[cf32116] | 11 | // Last Modified By : Andrew Beach |
---|
| 12 | // Last Modified On : Tue Oct 1 13:56:00 2019 |
---|
| 13 | // Update Count : 2 |
---|
[396037d] | 14 | // |
---|
| 15 | |
---|
| 16 | #include "SatisfyAssertions.hpp" |
---|
| 17 | |
---|
[46da46b] | 18 | #include <iostream> |
---|
[b69233ac] | 19 | #include <algorithm> |
---|
[396037d] | 20 | #include <cassert> |
---|
[b69233ac] | 21 | #include <sstream> |
---|
| 22 | #include <string> |
---|
| 23 | #include <unordered_map> |
---|
| 24 | #include <vector> |
---|
| 25 | |
---|
[5bf3976] | 26 | #include "AdjustExprType.hpp" |
---|
[b69233ac] | 27 | #include "Candidate.hpp" |
---|
| 28 | #include "CandidateFinder.hpp" |
---|
[5bf3976] | 29 | #include "CommonType.hpp" |
---|
[b69233ac] | 30 | #include "Cost.h" |
---|
| 31 | #include "RenameVars.h" |
---|
[5bf3976] | 32 | #include "SpecCost.hpp" |
---|
[b69233ac] | 33 | #include "typeops.h" |
---|
| 34 | #include "Unify.h" |
---|
| 35 | #include "AST/Decl.hpp" |
---|
| 36 | #include "AST/Expr.hpp" |
---|
| 37 | #include "AST/Node.hpp" |
---|
| 38 | #include "AST/Pass.hpp" |
---|
| 39 | #include "AST/Print.hpp" |
---|
| 40 | #include "AST/SymbolTable.hpp" |
---|
| 41 | #include "AST/TypeEnvironment.hpp" |
---|
[ef1da0e2] | 42 | #include "FindOpenVars.h" |
---|
[b69233ac] | 43 | #include "Common/FilterCombos.h" |
---|
| 44 | #include "Common/Indenter.h" |
---|
| 45 | #include "GenPoly/GenPoly.h" |
---|
| 46 | #include "SymTab/Mangler.h" |
---|
[396037d] | 47 | |
---|
[46da46b] | 48 | |
---|
| 49 | |
---|
[396037d] | 50 | namespace ResolvExpr { |
---|
| 51 | |
---|
[b69233ac] | 52 | // in CandidateFinder.cpp; unique ID for assertion satisfaction |
---|
| 53 | extern UniqueId globalResnSlot; |
---|
| 54 | |
---|
| 55 | namespace { |
---|
| 56 | /// Post-unification assertion satisfaction candidate |
---|
| 57 | struct AssnCandidate { |
---|
| 58 | ast::SymbolTable::IdData cdata; ///< Satisfying declaration |
---|
| 59 | ast::ptr< ast::Type > adjType; ///< Satisfying type |
---|
| 60 | ast::TypeEnvironment env; ///< Post-unification environment |
---|
| 61 | ast::AssertionSet have; ///< Post-unification have-set |
---|
| 62 | ast::AssertionSet need; ///< Post-unification need-set |
---|
| 63 | ast::OpenVarSet open; ///< Post-unification open-var-set |
---|
| 64 | ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs |
---|
| 65 | |
---|
[aca6a54c] | 66 | AssnCandidate( |
---|
| 67 | const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, |
---|
[b69233ac] | 68 | ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) |
---|
[aca6a54c] | 69 | : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), |
---|
[46da46b] | 70 | need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) { |
---|
| 71 | if (!have.empty()) { |
---|
[da4a570] | 72 | // std::cerr << c.id->location << ':' << c.id->name << std::endl; // I think this was debugging code so I commented it |
---|
[46da46b] | 73 | } |
---|
| 74 | } |
---|
[b69233ac] | 75 | }; |
---|
| 76 | |
---|
| 77 | /// List of assertion satisfaction candidates |
---|
| 78 | using AssnCandidateList = std::vector< AssnCandidate >; |
---|
| 79 | |
---|
| 80 | /// Reference to a single deferred item |
---|
| 81 | struct DeferRef { |
---|
[3e5dd913] | 82 | const ast::VariableExpr * expr; |
---|
[b69233ac] | 83 | const ast::AssertionSetValue & info; |
---|
| 84 | const AssnCandidate & match; |
---|
| 85 | }; |
---|
[aca6a54c] | 86 | |
---|
| 87 | /// Wrapper for the deferred items from a single assertion satisfaction. |
---|
[b69233ac] | 88 | /// Acts like an indexed list of DeferRef |
---|
| 89 | struct DeferItem { |
---|
[3e5dd913] | 90 | const ast::VariableExpr * expr; |
---|
[b69233ac] | 91 | const ast::AssertionSetValue & info; |
---|
| 92 | AssnCandidateList matches; |
---|
| 93 | |
---|
[aca6a54c] | 94 | DeferItem( |
---|
[3e5dd913] | 95 | const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) |
---|
| 96 | : expr( d ), info( i ), matches( std::move( ms ) ) {} |
---|
[b69233ac] | 97 | |
---|
| 98 | bool empty() const { return matches.empty(); } |
---|
| 99 | |
---|
| 100 | AssnCandidateList::size_type size() const { return matches.size(); } |
---|
| 101 | |
---|
[3e5dd913] | 102 | DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; } |
---|
[b69233ac] | 103 | }; |
---|
| 104 | |
---|
| 105 | /// List of deferred satisfaction items |
---|
| 106 | using DeferList = std::vector< DeferItem >; |
---|
| 107 | |
---|
| 108 | /// Set of assertion satisfactions, grouped by resolution ID |
---|
| 109 | using InferCache = std::unordered_map< ast::UniqueId, ast::InferredParams >; |
---|
| 110 | |
---|
| 111 | /// Lexicographically-ordered vector of costs. |
---|
| 112 | /// Lexicographic order comes from default operator< on std::vector. |
---|
| 113 | using CostVec = std::vector< Cost >; |
---|
| 114 | |
---|
| 115 | /// Flag for state iteration |
---|
| 116 | enum IterateFlag { IterateState }; |
---|
| 117 | |
---|
| 118 | /// Intermediate state for satisfying a set of assertions |
---|
| 119 | struct SatState { |
---|
| 120 | CandidateRef cand; ///< Candidate assertion is rooted on |
---|
| 121 | ast::AssertionList need; ///< Assertions to find |
---|
| 122 | ast::AssertionSet newNeed; ///< Recursive assertions from current satisfied assertions |
---|
| 123 | DeferList deferred; ///< Deferred matches |
---|
| 124 | InferCache inferred; ///< Cache of already-inferred assertions |
---|
| 125 | CostVec costs; ///< Disambiguating costs of recursive assertion satisfaction |
---|
| 126 | ast::SymbolTable symtab; ///< Name lookup (depends on previous assertions) |
---|
| 127 | |
---|
| 128 | /// Initial satisfaction state for a candidate |
---|
| 129 | SatState( CandidateRef & c, const ast::SymbolTable & syms ) |
---|
[aca6a54c] | 130 | : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, |
---|
[b69233ac] | 131 | symtab( syms ) { need.swap( c->need ); } |
---|
[aca6a54c] | 132 | |
---|
[b69233ac] | 133 | /// Update satisfaction state for next step after previous state |
---|
| 134 | SatState( SatState && o, IterateFlag ) |
---|
[aca6a54c] | 135 | : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), |
---|
| 136 | deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), |
---|
[b69233ac] | 137 | symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } |
---|
[aca6a54c] | 138 | |
---|
[b69233ac] | 139 | /// Field-wise next step constructor |
---|
| 140 | SatState( |
---|
[aca6a54c] | 141 | CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, |
---|
[b69233ac] | 142 | ast::SymbolTable && syms ) |
---|
[aca6a54c] | 143 | : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), |
---|
[b69233ac] | 144 | inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) |
---|
| 145 | { costs.emplace_back( Cost::zero ); } |
---|
| 146 | }; |
---|
| 147 | |
---|
[0c840fc] | 148 | enum AssertionResult {Fail, Skip, Success} ; |
---|
[b69233ac] | 149 | |
---|
| 150 | /// Binds a single assertion, updating satisfaction state |
---|
[aca6a54c] | 151 | void bindAssertion( |
---|
[eef8dfb] | 152 | const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, |
---|
[b69233ac] | 153 | AssnCandidate & match, InferCache & inferred |
---|
| 154 | ) { |
---|
| 155 | const ast::DeclWithType * candidate = match.cdata.id; |
---|
[aca6a54c] | 156 | assertf( candidate->uniqueId, |
---|
[b69233ac] | 157 | "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); |
---|
[aca6a54c] | 158 | |
---|
[46da46b] | 159 | ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cost ); |
---|
[b69233ac] | 160 | varExpr->result = match.adjType; |
---|
| 161 | if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); } |
---|
| 162 | |
---|
| 163 | // place newly-inferred assertion in proper location in cache |
---|
[3e5dd913] | 164 | inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{ |
---|
| 165 | candidate->uniqueId, candidate, match.adjType, expr->result, varExpr }; |
---|
[b69233ac] | 166 | } |
---|
| 167 | |
---|
| 168 | /// Satisfy a single assertion |
---|
[0c840fc] | 169 | AssertionResult satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool skipUnbound = false) { |
---|
[b69233ac] | 170 | // skip unused assertions |
---|
[da4a570] | 171 | // static unsigned int cnt = 0; // I think this was debugging code so I commented it |
---|
[0c840fc] | 172 | if ( ! assn.second.isUsed ) return AssertionResult::Success; |
---|
[b69233ac] | 173 | |
---|
[da4a570] | 174 | // if (assn.first->var->name[1] == '|') std::cerr << ++cnt << std::endl; // I think this was debugging code so I commented it |
---|
[46da46b] | 175 | |
---|
[b69233ac] | 176 | // find candidates that unify with the desired type |
---|
[46da46b] | 177 | AssnCandidateList matches, inexactMatches; |
---|
[e5c3811] | 178 | |
---|
| 179 | std::vector<ast::SymbolTable::IdData> candidates; |
---|
[3e5dd913] | 180 | auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name); |
---|
[e5c3811] | 181 | if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) { |
---|
| 182 | // prefilter special decls by argument type, if already known |
---|
[3e5dd913] | 183 | ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base |
---|
[e5c3811] | 184 | .strict_as<ast::FunctionType>()->params[0] |
---|
| 185 | .strict_as<ast::ReferenceType>()->base; |
---|
[24d6572] | 186 | // sat.cand->env.apply(thisArgType); |
---|
| 187 | |
---|
| 188 | if (auto inst = thisArgType.as<ast::TypeInstType>()) { |
---|
| 189 | auto cls = sat.cand->env.lookup(*inst); |
---|
| 190 | if (cls && cls->bound) thisArgType = cls->bound; |
---|
| 191 | } |
---|
[e5c3811] | 192 | |
---|
| 193 | std::string otypeKey = ""; |
---|
| 194 | if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer; |
---|
| 195 | else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams); |
---|
[0c840fc] | 196 | else if (skipUnbound) return AssertionResult::Skip; |
---|
[e5c3811] | 197 | |
---|
| 198 | candidates = sat.symtab.specialLookupId(kind, otypeKey); |
---|
| 199 | } |
---|
| 200 | else { |
---|
[3e5dd913] | 201 | candidates = sat.symtab.lookupId(assn.first->var->name); |
---|
[e5c3811] | 202 | } |
---|
| 203 | for ( const ast::SymbolTable::IdData & cdata : candidates ) { |
---|
[b69233ac] | 204 | const ast::DeclWithType * candidate = cdata.id; |
---|
| 205 | |
---|
[2fb35df] | 206 | // ignore deleted candidates. |
---|
| 207 | // NOTE: this behavior is different from main resolver. |
---|
| 208 | // further investigations might be needed to determine |
---|
| 209 | // if we should implement the same rule here |
---|
| 210 | // (i.e. error if unique best match is deleted) |
---|
[5b9a0ae] | 211 | if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue; |
---|
[2fb35df] | 212 | |
---|
[b69233ac] | 213 | // build independent unification context for candidate |
---|
| 214 | ast::AssertionSet have, newNeed; |
---|
| 215 | ast::TypeEnvironment newEnv{ sat.cand->env }; |
---|
| 216 | ast::OpenVarSet newOpen{ sat.cand->open }; |
---|
[3e5dd913] | 217 | ast::ptr< ast::Type > toType = assn.first->result; |
---|
[aca6a54c] | 218 | ast::ptr< ast::Type > adjType = |
---|
[7583c02] | 219 | renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false ); |
---|
[b69233ac] | 220 | |
---|
| 221 | // only keep candidates which unify |
---|
[ef1da0e2] | 222 | |
---|
| 223 | ast::OpenVarSet closed; |
---|
[46da46b] | 224 | // findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed ); |
---|
| 225 | findOpenVars( adjType, newOpen, closed, newNeed, have, newEnv, FirstOpen ); |
---|
| 226 | ast::TypeEnvironment tempNewEnv {newEnv}; |
---|
| 227 | |
---|
[24d6572] | 228 | if ( unifyExact( toType, adjType, tempNewEnv, newNeed, have, newOpen, WidenMode {true, true} ) ) { |
---|
[46da46b] | 229 | // set up binding slot for recursive assertions |
---|
| 230 | ast::UniqueId crntResnSlot = 0; |
---|
| 231 | if ( ! newNeed.empty() ) { |
---|
| 232 | crntResnSlot = ++globalResnSlot; |
---|
| 233 | for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } |
---|
[b69233ac] | 234 | } |
---|
[46da46b] | 235 | |
---|
| 236 | matches.emplace_back( |
---|
| 237 | cdata, adjType, std::move( tempNewEnv ), std::move( have ), std::move( newNeed ), |
---|
| 238 | std::move( newOpen ), crntResnSlot ); |
---|
[ef1da0e2] | 239 | } |
---|
[46da46b] | 240 | else if ( matches.empty() ) { |
---|
| 241 | // restore invalidated env |
---|
| 242 | // newEnv = sat.cand->env; |
---|
| 243 | // newNeed.clear(); |
---|
[24d6572] | 244 | if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true} ) ) { |
---|
[ef1da0e2] | 245 | // set up binding slot for recursive assertions |
---|
| 246 | ast::UniqueId crntResnSlot = 0; |
---|
| 247 | if ( ! newNeed.empty() ) { |
---|
| 248 | crntResnSlot = ++globalResnSlot; |
---|
| 249 | for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } |
---|
| 250 | } |
---|
[b69233ac] | 251 | |
---|
[46da46b] | 252 | inexactMatches.emplace_back( |
---|
[ef1da0e2] | 253 | cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), |
---|
| 254 | std::move( newOpen ), crntResnSlot ); |
---|
| 255 | } |
---|
[b69233ac] | 256 | } |
---|
| 257 | } |
---|
| 258 | |
---|
| 259 | // break if no satisfying match |
---|
[46da46b] | 260 | if ( matches.empty() ) matches = std::move(inexactMatches); |
---|
[0c840fc] | 261 | if ( matches.empty() ) return AssertionResult::Fail; |
---|
[b69233ac] | 262 | |
---|
| 263 | // defer if too many satisfying matches |
---|
| 264 | if ( matches.size() > 1 ) { |
---|
| 265 | sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) ); |
---|
[0c840fc] | 266 | return AssertionResult::Success; |
---|
[b69233ac] | 267 | } |
---|
| 268 | |
---|
| 269 | // otherwise bind unique match in ongoing scope |
---|
| 270 | AssnCandidate & match = matches.front(); |
---|
[46da46b] | 271 | // addToSymbolTable( match.have, sat.symtab ); |
---|
[b69233ac] | 272 | sat.newNeed.insert( match.need.begin(), match.need.end() ); |
---|
| 273 | sat.cand->env = std::move( match.env ); |
---|
| 274 | sat.cand->open = std::move( match.open ); |
---|
| 275 | |
---|
| 276 | bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred ); |
---|
[0c840fc] | 277 | return AssertionResult::Success; |
---|
[b69233ac] | 278 | } |
---|
| 279 | |
---|
| 280 | /// Map of candidate return types to recursive assertion satisfaction costs |
---|
| 281 | using PruneMap = std::unordered_map< std::string, CostVec >; |
---|
| 282 | |
---|
| 283 | /// Gets the pruning key for a candidate (derived from environment-adjusted return type) |
---|
| 284 | std::string pruneKey( const Candidate & cand ) { |
---|
| 285 | ast::ptr< ast::Type > resType = cand.expr->result; |
---|
| 286 | cand.env.apply( resType ); |
---|
[0026d67] | 287 | return Mangle::mangleType( resType ); |
---|
[b69233ac] | 288 | } |
---|
| 289 | |
---|
| 290 | /// Associates inferred parameters with an expression |
---|
| 291 | struct InferMatcher final { |
---|
| 292 | InferCache & inferred; |
---|
| 293 | |
---|
| 294 | InferMatcher( InferCache & inferred ) : inferred( inferred ) {} |
---|
| 295 | |
---|
[81da70a5] | 296 | const ast::Expr * postvisit( const ast::Expr * expr ) { |
---|
[b69233ac] | 297 | // Skip if no slots to find |
---|
[07d867b] | 298 | if ( !expr->inferred.hasSlots() ) return expr; |
---|
| 299 | // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr; |
---|
| 300 | std::vector<UniqueId> missingSlots; |
---|
[b69233ac] | 301 | // find inferred parameters for resolution slots |
---|
[07d867b] | 302 | ast::InferredParams * newInferred = new ast::InferredParams(); |
---|
[b69233ac] | 303 | for ( UniqueId slot : expr->inferred.resnSlots() ) { |
---|
| 304 | // fail if no matching assertions found |
---|
| 305 | auto it = inferred.find( slot ); |
---|
| 306 | if ( it == inferred.end() ) { |
---|
[cdacb73] | 307 | // std::cerr << "missing assertion " << slot << std::endl; |
---|
[07d867b] | 308 | missingSlots.push_back(slot); |
---|
[81da70a5] | 309 | continue; |
---|
[b69233ac] | 310 | } |
---|
| 311 | |
---|
| 312 | // place inferred parameters into new map |
---|
| 313 | for ( auto & entry : it->second ) { |
---|
| 314 | // recurse on inferParams of resolved expressions |
---|
[81da70a5] | 315 | entry.second.expr = postvisit( entry.second.expr ); |
---|
[07d867b] | 316 | auto res = newInferred->emplace( entry ); |
---|
[b69233ac] | 317 | assert( res.second && "all assertions newly placed" ); |
---|
| 318 | } |
---|
| 319 | } |
---|
| 320 | |
---|
| 321 | ast::Expr * ret = mutate( expr ); |
---|
[07d867b] | 322 | ret->inferred.set_inferParams( newInferred ); |
---|
| 323 | if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots; |
---|
[b69233ac] | 324 | return ret; |
---|
| 325 | } |
---|
| 326 | }; |
---|
| 327 | |
---|
[aca6a54c] | 328 | /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning |
---|
[b69233ac] | 329 | /// threshold. |
---|
[aca6a54c] | 330 | void finalizeAssertions( |
---|
| 331 | CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, |
---|
| 332 | CandidateList & out |
---|
[b69233ac] | 333 | ) { |
---|
| 334 | // prune if cheaper alternative for same key has already been generated |
---|
| 335 | std::string key = pruneKey( *cand ); |
---|
| 336 | auto it = thresholds.find( key ); |
---|
| 337 | if ( it != thresholds.end() ) { |
---|
| 338 | if ( it->second < costs ) return; |
---|
| 339 | } else { |
---|
| 340 | thresholds.emplace_hint( it, key, std::move( costs ) ); |
---|
| 341 | } |
---|
| 342 | |
---|
| 343 | // replace resolution slots with inferred parameters, add to output |
---|
| 344 | ast::Pass< InferMatcher > matcher{ inferred }; |
---|
| 345 | cand->expr = cand->expr->accept( matcher ); |
---|
| 346 | out.emplace_back( cand ); |
---|
| 347 | } |
---|
| 348 | |
---|
[aca6a54c] | 349 | /// Combo iterator that combines candidates into an output list, merging their environments. |
---|
| 350 | /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` |
---|
[b69233ac] | 351 | /// for description of "combo iterator". |
---|
| 352 | class CandidateEnvMerger { |
---|
| 353 | /// Current list of merged candidates |
---|
| 354 | std::vector< DeferRef > crnt; |
---|
| 355 | /// Stack of environments to support backtracking |
---|
| 356 | std::vector< ast::TypeEnvironment > envs; |
---|
| 357 | /// Stack of open variables to support backtracking |
---|
| 358 | std::vector< ast::OpenVarSet > opens; |
---|
| 359 | /// Symbol table to use for merges |
---|
| 360 | const ast::SymbolTable & symtab; |
---|
| 361 | |
---|
| 362 | public: |
---|
| 363 | /// The merged environment/open variables and the list of candidates |
---|
| 364 | struct OutType { |
---|
| 365 | ast::TypeEnvironment env; |
---|
| 366 | ast::OpenVarSet open; |
---|
| 367 | std::vector< DeferRef > assns; |
---|
| 368 | Cost cost; |
---|
| 369 | |
---|
[aca6a54c] | 370 | OutType( |
---|
| 371 | const ast::TypeEnvironment & e, const ast::OpenVarSet & o, |
---|
[b69233ac] | 372 | const std::vector< DeferRef > & as, const ast::SymbolTable & symtab ) |
---|
| 373 | : env( e ), open( o ), assns( as ), cost( Cost::zero ) { |
---|
| 374 | // compute combined conversion cost |
---|
| 375 | for ( const DeferRef & assn : assns ) { |
---|
| 376 | // compute conversion cost from satisfying decl to assertion |
---|
[aca6a54c] | 377 | cost += computeConversionCost( |
---|
[3e5dd913] | 378 | assn.match.adjType, assn.expr->result, false, symtab, env ); |
---|
[aca6a54c] | 379 | |
---|
[b69233ac] | 380 | // mark vars+specialization on function-type assertions |
---|
[aca6a54c] | 381 | const ast::FunctionType * func = |
---|
[b69233ac] | 382 | GenPoly::getFunctionType( assn.match.cdata.id->get_type() ); |
---|
| 383 | if ( ! func ) continue; |
---|
| 384 | |
---|
[954c954] | 385 | for ( const auto & param : func->params ) { |
---|
| 386 | cost.decSpec( specCost( param ) ); |
---|
[b69233ac] | 387 | } |
---|
[aca6a54c] | 388 | |
---|
[b69233ac] | 389 | cost.incVar( func->forall.size() ); |
---|
[aca6a54c] | 390 | |
---|
[3e5dd913] | 391 | cost.decSpec( func->assertions.size() ); |
---|
[b69233ac] | 392 | } |
---|
| 393 | } |
---|
| 394 | |
---|
| 395 | bool operator< ( const OutType & o ) const { return cost < o.cost; } |
---|
| 396 | }; |
---|
| 397 | |
---|
[aca6a54c] | 398 | CandidateEnvMerger( |
---|
| 399 | const ast::TypeEnvironment & env, const ast::OpenVarSet & open, |
---|
[b69233ac] | 400 | const ast::SymbolTable & syms ) |
---|
| 401 | : crnt(), envs{ env }, opens{ open }, symtab( syms ) {} |
---|
| 402 | |
---|
| 403 | bool append( DeferRef i ) { |
---|
| 404 | ast::TypeEnvironment env = envs.back(); |
---|
| 405 | ast::OpenVarSet open = opens.back(); |
---|
| 406 | mergeOpenVars( open, i.match.open ); |
---|
| 407 | |
---|
[251ce80] | 408 | if ( ! env.combine( i.match.env, open ) ) return false; |
---|
[b69233ac] | 409 | |
---|
| 410 | crnt.emplace_back( i ); |
---|
| 411 | envs.emplace_back( std::move( env ) ); |
---|
| 412 | opens.emplace_back( std::move( open ) ); |
---|
| 413 | return true; |
---|
| 414 | } |
---|
| 415 | |
---|
| 416 | void backtrack() { |
---|
| 417 | crnt.pop_back(); |
---|
| 418 | envs.pop_back(); |
---|
| 419 | opens.pop_back(); |
---|
| 420 | } |
---|
| 421 | |
---|
| 422 | OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; } |
---|
| 423 | }; |
---|
| 424 | |
---|
| 425 | /// Limit to depth of recursion of assertion satisfaction |
---|
[1958fec] | 426 | static const int recursionLimit = 8; |
---|
[b69233ac] | 427 | /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of |
---|
| 428 | static const int deferLimit = 10; |
---|
| 429 | } // anonymous namespace |
---|
| 430 | |
---|
[aca6a54c] | 431 | void satisfyAssertions( |
---|
| 432 | CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, |
---|
[396037d] | 433 | std::vector<std::string> & errors |
---|
| 434 | ) { |
---|
[b69233ac] | 435 | // finish early if no assertions to satisfy |
---|
| 436 | if ( cand->need.empty() ) { |
---|
| 437 | out.emplace_back( cand ); |
---|
| 438 | return; |
---|
| 439 | } |
---|
| 440 | |
---|
| 441 | // build list of possible combinations of satisfying declarations |
---|
| 442 | std::vector< SatState > sats{ SatState{ cand, symtab } }; |
---|
| 443 | std::vector< SatState > nextSats{}; |
---|
| 444 | |
---|
| 445 | // pruning thresholds by result type of output candidates. |
---|
| 446 | // Candidates *should* be generated in sorted order, so no need to retroactively prune |
---|
| 447 | PruneMap thresholds; |
---|
| 448 | |
---|
| 449 | // satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction. |
---|
| 450 | // Stop recursion at a limited number of levels deep to avoid infinite loops. |
---|
| 451 | for ( unsigned level = 0; level < recursionLimit; ++level ) { |
---|
| 452 | // for each current mutually-compatible set of assertions |
---|
| 453 | for ( SatState & sat : sats ) { |
---|
| 454 | // stop this branch if a better option is already found |
---|
| 455 | auto it = thresholds.find( pruneKey( *sat.cand ) ); |
---|
| 456 | if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat; |
---|
| 457 | |
---|
[7583c02] | 458 | // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen. |
---|
[ef1da0e2] | 459 | |
---|
[eef8dfb] | 460 | for (unsigned resetCount = 0; ; ++resetCount) { |
---|
[7583c02] | 461 | ast::AssertionList next; |
---|
| 462 | // make initial pass at matching assertions |
---|
| 463 | for ( auto & assn : sat.need ) { |
---|
[34b4268] | 464 | resetTyVarRenaming(); |
---|
[7583c02] | 465 | // fail early if any assertion is not satisfiable |
---|
[0c840fc] | 466 | auto result = satisfyAssertion( assn, sat, !next.empty() ); |
---|
| 467 | if ( result == AssertionResult::Fail ) { |
---|
[ef1da0e2] | 468 | Indenter tabs{ 3 }; |
---|
| 469 | std::ostringstream ss; |
---|
| 470 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 471 | print( ss, *sat.cand, ++tabs ); |
---|
| 472 | ss << (tabs-1) << "Could not satisfy assertion:\n"; |
---|
[0c840fc] | 473 | ast::print( ss, assn.first, tabs ); |
---|
[ef1da0e2] | 474 | |
---|
| 475 | errors.emplace_back( ss.str() ); |
---|
| 476 | goto nextSat; |
---|
[0c840fc] | 477 | } |
---|
| 478 | else if ( result == AssertionResult::Skip ) { |
---|
| 479 | next.emplace_back(assn); |
---|
| 480 | // goto nextSat; |
---|
| 481 | } |
---|
[b69233ac] | 482 | } |
---|
[0c840fc] | 483 | // success |
---|
| 484 | if (next.empty()) break; |
---|
| 485 | |
---|
[7583c02] | 486 | sat.need = std::move(next); |
---|
[b69233ac] | 487 | } |
---|
| 488 | |
---|
| 489 | if ( sat.deferred.empty() ) { |
---|
| 490 | // either add successful match or push back next state |
---|
| 491 | if ( sat.newNeed.empty() ) { |
---|
[aca6a54c] | 492 | finalizeAssertions( |
---|
[b69233ac] | 493 | sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out ); |
---|
| 494 | } else { |
---|
| 495 | nextSats.emplace_back( std::move( sat ), IterateState ); |
---|
| 496 | } |
---|
| 497 | } else if ( sat.deferred.size() > deferLimit ) { |
---|
| 498 | // too many deferred assertions to attempt mutual compatibility |
---|
| 499 | Indenter tabs{ 3 }; |
---|
| 500 | std::ostringstream ss; |
---|
| 501 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 502 | print( ss, *sat.cand, ++tabs ); |
---|
| 503 | ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n"; |
---|
| 504 | for ( const auto & d : sat.deferred ) { |
---|
[3e5dd913] | 505 | ast::print( ss, d.expr, tabs ); |
---|
[b69233ac] | 506 | } |
---|
| 507 | |
---|
| 508 | errors.emplace_back( ss.str() ); |
---|
| 509 | goto nextSat; |
---|
| 510 | } else { |
---|
| 511 | // combine deferred assertions by mutual compatibility |
---|
| 512 | std::vector< CandidateEnvMerger::OutType > compatible = filterCombos( |
---|
| 513 | sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } ); |
---|
[aca6a54c] | 514 | |
---|
[b69233ac] | 515 | // fail early if no mutually-compatible assertion satisfaction |
---|
| 516 | if ( compatible.empty() ) { |
---|
| 517 | Indenter tabs{ 3 }; |
---|
| 518 | std::ostringstream ss; |
---|
| 519 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 520 | print( ss, *sat.cand, ++tabs ); |
---|
| 521 | ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n"; |
---|
| 522 | for ( const auto& d : sat.deferred ) { |
---|
[3e5dd913] | 523 | ast::print( ss, d.expr, tabs ); |
---|
[b69233ac] | 524 | } |
---|
| 525 | |
---|
| 526 | errors.emplace_back( ss.str() ); |
---|
| 527 | goto nextSat; |
---|
| 528 | } |
---|
| 529 | |
---|
| 530 | // sort by cost (for overall pruning order) |
---|
| 531 | std::sort( compatible.begin(), compatible.end() ); |
---|
| 532 | |
---|
| 533 | // process mutually-compatible combinations |
---|
| 534 | for ( auto & compat : compatible ) { |
---|
| 535 | // set up next satisfaction state |
---|
| 536 | CandidateRef nextCand = std::make_shared<Candidate>( |
---|
[aca6a54c] | 537 | sat.cand->expr, std::move( compat.env ), std::move( compat.open ), |
---|
[b69233ac] | 538 | ast::AssertionSet{} /* need moved into satisfaction state */, |
---|
[46da46b] | 539 | sat.cand->cost ); |
---|
[b69233ac] | 540 | |
---|
| 541 | ast::AssertionSet nextNewNeed{ sat.newNeed }; |
---|
| 542 | InferCache nextInferred{ sat.inferred }; |
---|
[aca6a54c] | 543 | |
---|
[b69233ac] | 544 | CostVec nextCosts{ sat.costs }; |
---|
| 545 | nextCosts.back() += compat.cost; |
---|
[aca6a54c] | 546 | |
---|
[b69233ac] | 547 | ast::SymbolTable nextSymtab{ sat.symtab }; |
---|
| 548 | |
---|
| 549 | // add compatible assertions to new satisfaction state |
---|
| 550 | for ( DeferRef r : compat.assns ) { |
---|
| 551 | AssnCandidate match = r.match; |
---|
[46da46b] | 552 | // addToSymbolTable( match.have, nextSymtab ); |
---|
[b69233ac] | 553 | nextNewNeed.insert( match.need.begin(), match.need.end() ); |
---|
| 554 | |
---|
[3e5dd913] | 555 | bindAssertion( r.expr, r.info, nextCand, match, nextInferred ); |
---|
[b69233ac] | 556 | } |
---|
| 557 | |
---|
| 558 | // either add successful match or push back next state |
---|
| 559 | if ( nextNewNeed.empty() ) { |
---|
[aca6a54c] | 560 | finalizeAssertions( |
---|
[b69233ac] | 561 | nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); |
---|
| 562 | } else { |
---|
[aca6a54c] | 563 | nextSats.emplace_back( |
---|
| 564 | std::move( nextCand ), std::move( nextNewNeed ), |
---|
| 565 | std::move( nextInferred ), std::move( nextCosts ), |
---|
[b69233ac] | 566 | std::move( nextSymtab ) ); |
---|
| 567 | } |
---|
| 568 | } |
---|
| 569 | } |
---|
| 570 | nextSat:; } |
---|
| 571 | |
---|
| 572 | // finish or reset for next round |
---|
| 573 | if ( nextSats.empty() ) return; |
---|
| 574 | sats.swap( nextSats ); |
---|
| 575 | nextSats.clear(); |
---|
| 576 | } |
---|
[aca6a54c] | 577 | |
---|
[b69233ac] | 578 | // exceeded recursion limit if reaches here |
---|
| 579 | if ( out.empty() ) { |
---|
| 580 | SemanticError( cand->expr->location, "Too many recursive assertions" ); |
---|
| 581 | } |
---|
[396037d] | 582 | } |
---|
| 583 | |
---|
| 584 | } // namespace ResolvExpr |
---|
| 585 | |
---|
| 586 | // Local Variables: // |
---|
| 587 | // tab-width: 4 // |
---|
| 588 | // mode: c++ // |
---|
| 589 | // compile-command: "make install" // |
---|
[aca6a54c] | 590 | // End: // |
---|