[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 | |
---|
[b69233ac] | 18 | #include <algorithm> |
---|
[396037d] | 19 | #include <cassert> |
---|
[b69233ac] | 20 | #include <sstream> |
---|
| 21 | #include <string> |
---|
| 22 | #include <unordered_map> |
---|
| 23 | #include <vector> |
---|
| 24 | |
---|
| 25 | #include "Candidate.hpp" |
---|
| 26 | #include "CandidateFinder.hpp" |
---|
| 27 | #include "Cost.h" |
---|
| 28 | #include "RenameVars.h" |
---|
| 29 | #include "typeops.h" |
---|
| 30 | #include "Unify.h" |
---|
| 31 | #include "AST/Decl.hpp" |
---|
| 32 | #include "AST/Expr.hpp" |
---|
| 33 | #include "AST/Node.hpp" |
---|
| 34 | #include "AST/Pass.hpp" |
---|
| 35 | #include "AST/Print.hpp" |
---|
| 36 | #include "AST/SymbolTable.hpp" |
---|
| 37 | #include "AST/TypeEnvironment.hpp" |
---|
| 38 | #include "Common/FilterCombos.h" |
---|
| 39 | #include "Common/Indenter.h" |
---|
| 40 | #include "GenPoly/GenPoly.h" |
---|
| 41 | #include "SymTab/Mangler.h" |
---|
[396037d] | 42 | |
---|
| 43 | namespace ResolvExpr { |
---|
| 44 | |
---|
[b69233ac] | 45 | // in CandidateFinder.cpp; unique ID for assertion satisfaction |
---|
| 46 | extern UniqueId globalResnSlot; |
---|
| 47 | |
---|
| 48 | namespace { |
---|
| 49 | /// Post-unification assertion satisfaction candidate |
---|
| 50 | struct AssnCandidate { |
---|
| 51 | ast::SymbolTable::IdData cdata; ///< Satisfying declaration |
---|
| 52 | ast::ptr< ast::Type > adjType; ///< Satisfying type |
---|
| 53 | ast::TypeEnvironment env; ///< Post-unification environment |
---|
| 54 | ast::AssertionSet have; ///< Post-unification have-set |
---|
| 55 | ast::AssertionSet need; ///< Post-unification need-set |
---|
| 56 | ast::OpenVarSet open; ///< Post-unification open-var-set |
---|
| 57 | ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs |
---|
| 58 | |
---|
| 59 | AssnCandidate( |
---|
| 60 | const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, |
---|
| 61 | ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) |
---|
| 62 | : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), |
---|
| 63 | need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {} |
---|
| 64 | }; |
---|
| 65 | |
---|
| 66 | /// List of assertion satisfaction candidates |
---|
| 67 | using AssnCandidateList = std::vector< AssnCandidate >; |
---|
| 68 | |
---|
| 69 | /// Reference to a single deferred item |
---|
| 70 | struct DeferRef { |
---|
| 71 | const ast::DeclWithType * decl; |
---|
| 72 | const ast::AssertionSetValue & info; |
---|
| 73 | const AssnCandidate & match; |
---|
| 74 | }; |
---|
| 75 | |
---|
| 76 | /// Wrapper for the deferred items from a single assertion satisfaction. |
---|
| 77 | /// Acts like an indexed list of DeferRef |
---|
| 78 | struct DeferItem { |
---|
| 79 | const ast::DeclWithType * decl; |
---|
| 80 | const ast::AssertionSetValue & info; |
---|
| 81 | AssnCandidateList matches; |
---|
| 82 | |
---|
| 83 | DeferItem( |
---|
| 84 | const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) |
---|
| 85 | : decl( d ), info( i ), matches( std::move( ms ) ) {} |
---|
| 86 | |
---|
| 87 | bool empty() const { return matches.empty(); } |
---|
| 88 | |
---|
| 89 | AssnCandidateList::size_type size() const { return matches.size(); } |
---|
| 90 | |
---|
| 91 | DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; } |
---|
| 92 | }; |
---|
| 93 | |
---|
| 94 | /// List of deferred satisfaction items |
---|
| 95 | using DeferList = std::vector< DeferItem >; |
---|
| 96 | |
---|
| 97 | /// Set of assertion satisfactions, grouped by resolution ID |
---|
| 98 | using InferCache = std::unordered_map< ast::UniqueId, ast::InferredParams >; |
---|
| 99 | |
---|
| 100 | /// Lexicographically-ordered vector of costs. |
---|
| 101 | /// Lexicographic order comes from default operator< on std::vector. |
---|
| 102 | using CostVec = std::vector< Cost >; |
---|
| 103 | |
---|
| 104 | /// Flag for state iteration |
---|
| 105 | enum IterateFlag { IterateState }; |
---|
| 106 | |
---|
| 107 | /// Intermediate state for satisfying a set of assertions |
---|
| 108 | struct SatState { |
---|
| 109 | CandidateRef cand; ///< Candidate assertion is rooted on |
---|
| 110 | ast::AssertionList need; ///< Assertions to find |
---|
| 111 | ast::AssertionSet newNeed; ///< Recursive assertions from current satisfied assertions |
---|
| 112 | DeferList deferred; ///< Deferred matches |
---|
| 113 | InferCache inferred; ///< Cache of already-inferred assertions |
---|
| 114 | CostVec costs; ///< Disambiguating costs of recursive assertion satisfaction |
---|
| 115 | ast::SymbolTable symtab; ///< Name lookup (depends on previous assertions) |
---|
| 116 | |
---|
| 117 | /// Initial satisfaction state for a candidate |
---|
| 118 | SatState( CandidateRef & c, const ast::SymbolTable & syms ) |
---|
| 119 | : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, |
---|
| 120 | symtab( syms ) { need.swap( c->need ); } |
---|
| 121 | |
---|
| 122 | /// Update satisfaction state for next step after previous state |
---|
| 123 | SatState( SatState && o, IterateFlag ) |
---|
| 124 | : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), |
---|
| 125 | deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), |
---|
| 126 | symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } |
---|
| 127 | |
---|
| 128 | /// Field-wise next step constructor |
---|
| 129 | SatState( |
---|
| 130 | CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, |
---|
| 131 | ast::SymbolTable && syms ) |
---|
| 132 | : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), |
---|
| 133 | inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) |
---|
| 134 | { costs.emplace_back( Cost::zero ); } |
---|
| 135 | }; |
---|
| 136 | |
---|
| 137 | /// Adds a captured assertion to the symbol table |
---|
| 138 | void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) { |
---|
| 139 | for ( auto & i : have ) { |
---|
| 140 | if ( i.second.isUsed ) { symtab.addId( i.first ); } |
---|
| 141 | } |
---|
| 142 | } |
---|
| 143 | |
---|
| 144 | /// Binds a single assertion, updating satisfaction state |
---|
| 145 | void bindAssertion( |
---|
| 146 | const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, |
---|
| 147 | AssnCandidate & match, InferCache & inferred |
---|
| 148 | ) { |
---|
| 149 | const ast::DeclWithType * candidate = match.cdata.id; |
---|
| 150 | assertf( candidate->uniqueId, |
---|
| 151 | "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); |
---|
| 152 | |
---|
| 153 | ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost ); |
---|
| 154 | varExpr->result = match.adjType; |
---|
| 155 | if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); } |
---|
| 156 | |
---|
| 157 | // place newly-inferred assertion in proper location in cache |
---|
| 158 | inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{ |
---|
| 159 | candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr }; |
---|
| 160 | } |
---|
| 161 | |
---|
| 162 | /// Satisfy a single assertion |
---|
| 163 | bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat ) { |
---|
| 164 | // skip unused assertions |
---|
| 165 | if ( ! assn.second.isUsed ) return true; |
---|
| 166 | |
---|
| 167 | // find candidates that unify with the desired type |
---|
| 168 | AssnCandidateList matches; |
---|
| 169 | for ( const ast::SymbolTable::IdData & cdata : sat.symtab.lookupId( assn.first->name ) ) { |
---|
| 170 | const ast::DeclWithType * candidate = cdata.id; |
---|
| 171 | |
---|
| 172 | // build independent unification context for candidate |
---|
| 173 | ast::AssertionSet have, newNeed; |
---|
| 174 | ast::TypeEnvironment newEnv{ sat.cand->env }; |
---|
| 175 | ast::OpenVarSet newOpen{ sat.cand->open }; |
---|
| 176 | ast::ptr< ast::Type > toType = assn.first->get_type(); |
---|
| 177 | ast::ptr< ast::Type > adjType = |
---|
| 178 | renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) ); |
---|
| 179 | |
---|
| 180 | // only keep candidates which unify |
---|
| 181 | if ( unify( toType, adjType, newEnv, newNeed, have, newOpen, sat.symtab ) ) { |
---|
| 182 | // set up binding slot for recursive assertions |
---|
| 183 | ast::UniqueId crntResnSlot = 0; |
---|
| 184 | if ( ! newNeed.empty() ) { |
---|
| 185 | crntResnSlot = ++globalResnSlot; |
---|
| 186 | for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; } |
---|
| 187 | } |
---|
| 188 | |
---|
| 189 | matches.emplace_back( |
---|
| 190 | cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ), |
---|
| 191 | std::move( newOpen ), crntResnSlot ); |
---|
| 192 | } |
---|
| 193 | } |
---|
| 194 | |
---|
| 195 | // break if no satisfying match |
---|
| 196 | if ( matches.empty() ) return false; |
---|
| 197 | |
---|
| 198 | // defer if too many satisfying matches |
---|
| 199 | if ( matches.size() > 1 ) { |
---|
| 200 | sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) ); |
---|
| 201 | return true; |
---|
| 202 | } |
---|
| 203 | |
---|
| 204 | // otherwise bind unique match in ongoing scope |
---|
| 205 | AssnCandidate & match = matches.front(); |
---|
| 206 | addToSymbolTable( match.have, sat.symtab ); |
---|
| 207 | sat.newNeed.insert( match.need.begin(), match.need.end() ); |
---|
| 208 | sat.cand->env = std::move( match.env ); |
---|
| 209 | sat.cand->open = std::move( match.open ); |
---|
| 210 | |
---|
| 211 | bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred ); |
---|
| 212 | return true; |
---|
| 213 | } |
---|
| 214 | |
---|
| 215 | /// Map of candidate return types to recursive assertion satisfaction costs |
---|
| 216 | using PruneMap = std::unordered_map< std::string, CostVec >; |
---|
| 217 | |
---|
| 218 | /// Gets the pruning key for a candidate (derived from environment-adjusted return type) |
---|
| 219 | std::string pruneKey( const Candidate & cand ) { |
---|
| 220 | ast::ptr< ast::Type > resType = cand.expr->result; |
---|
| 221 | cand.env.apply( resType ); |
---|
| 222 | return Mangle::mangle( resType, Mangle::typeMode() ); |
---|
| 223 | } |
---|
| 224 | |
---|
| 225 | /// Associates inferred parameters with an expression |
---|
| 226 | struct InferMatcher final { |
---|
| 227 | InferCache & inferred; |
---|
| 228 | |
---|
| 229 | InferMatcher( InferCache & inferred ) : inferred( inferred ) {} |
---|
| 230 | |
---|
[81da70a5] | 231 | const ast::Expr * postvisit( const ast::Expr * expr ) { |
---|
[b69233ac] | 232 | // Skip if no slots to find |
---|
| 233 | if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr; |
---|
| 234 | |
---|
| 235 | // find inferred parameters for resolution slots |
---|
| 236 | ast::InferredParams newInferred; |
---|
| 237 | for ( UniqueId slot : expr->inferred.resnSlots() ) { |
---|
| 238 | // fail if no matching assertions found |
---|
| 239 | auto it = inferred.find( slot ); |
---|
| 240 | if ( it == inferred.end() ) { |
---|
[81da70a5] | 241 | std::cerr << "missing assertion " << slot << std::endl; |
---|
| 242 | continue; |
---|
[b69233ac] | 243 | } |
---|
| 244 | |
---|
| 245 | // place inferred parameters into new map |
---|
| 246 | for ( auto & entry : it->second ) { |
---|
| 247 | // recurse on inferParams of resolved expressions |
---|
[81da70a5] | 248 | entry.second.expr = postvisit( entry.second.expr ); |
---|
[b69233ac] | 249 | auto res = newInferred.emplace( entry ); |
---|
| 250 | assert( res.second && "all assertions newly placed" ); |
---|
| 251 | } |
---|
| 252 | } |
---|
| 253 | |
---|
| 254 | ast::Expr * ret = mutate( expr ); |
---|
| 255 | ret->inferred.set_inferParams( std::move( newInferred ) ); |
---|
| 256 | return ret; |
---|
| 257 | } |
---|
| 258 | }; |
---|
| 259 | |
---|
| 260 | /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning |
---|
| 261 | /// threshold. |
---|
| 262 | void finalizeAssertions( |
---|
| 263 | CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, |
---|
| 264 | CandidateList & out |
---|
| 265 | ) { |
---|
| 266 | // prune if cheaper alternative for same key has already been generated |
---|
| 267 | std::string key = pruneKey( *cand ); |
---|
| 268 | auto it = thresholds.find( key ); |
---|
| 269 | if ( it != thresholds.end() ) { |
---|
| 270 | if ( it->second < costs ) return; |
---|
| 271 | } else { |
---|
| 272 | thresholds.emplace_hint( it, key, std::move( costs ) ); |
---|
| 273 | } |
---|
| 274 | |
---|
| 275 | // replace resolution slots with inferred parameters, add to output |
---|
| 276 | ast::Pass< InferMatcher > matcher{ inferred }; |
---|
| 277 | cand->expr = cand->expr->accept( matcher ); |
---|
| 278 | out.emplace_back( cand ); |
---|
| 279 | } |
---|
| 280 | |
---|
| 281 | /// Combo iterator that combines candidates into an output list, merging their environments. |
---|
| 282 | /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` |
---|
| 283 | /// for description of "combo iterator". |
---|
| 284 | class CandidateEnvMerger { |
---|
| 285 | /// Current list of merged candidates |
---|
| 286 | std::vector< DeferRef > crnt; |
---|
| 287 | /// Stack of environments to support backtracking |
---|
| 288 | std::vector< ast::TypeEnvironment > envs; |
---|
| 289 | /// Stack of open variables to support backtracking |
---|
| 290 | std::vector< ast::OpenVarSet > opens; |
---|
| 291 | /// Symbol table to use for merges |
---|
| 292 | const ast::SymbolTable & symtab; |
---|
| 293 | |
---|
| 294 | public: |
---|
| 295 | /// The merged environment/open variables and the list of candidates |
---|
| 296 | struct OutType { |
---|
| 297 | ast::TypeEnvironment env; |
---|
| 298 | ast::OpenVarSet open; |
---|
| 299 | std::vector< DeferRef > assns; |
---|
| 300 | Cost cost; |
---|
| 301 | |
---|
[cf32116] | 302 | OutType( |
---|
| 303 | const ast::TypeEnvironment & e, const ast::OpenVarSet & o, |
---|
[b69233ac] | 304 | const std::vector< DeferRef > & as, const ast::SymbolTable & symtab ) |
---|
| 305 | : env( e ), open( o ), assns( as ), cost( Cost::zero ) { |
---|
| 306 | // compute combined conversion cost |
---|
| 307 | for ( const DeferRef & assn : assns ) { |
---|
| 308 | // compute conversion cost from satisfying decl to assertion |
---|
[cf32116] | 309 | cost += computeConversionCost( |
---|
| 310 | assn.match.adjType, assn.decl->get_type(), false, symtab, env ); |
---|
| 311 | |
---|
[b69233ac] | 312 | // mark vars+specialization on function-type assertions |
---|
[cf32116] | 313 | const ast::FunctionType * func = |
---|
[b69233ac] | 314 | GenPoly::getFunctionType( assn.match.cdata.id->get_type() ); |
---|
| 315 | if ( ! func ) continue; |
---|
| 316 | |
---|
| 317 | for ( const ast::DeclWithType * param : func->params ) { |
---|
| 318 | cost.decSpec( specCost( param->get_type() ) ); |
---|
| 319 | } |
---|
[cf32116] | 320 | |
---|
[b69233ac] | 321 | cost.incVar( func->forall.size() ); |
---|
[cf32116] | 322 | |
---|
[b69233ac] | 323 | for ( const ast::TypeDecl * td : func->forall ) { |
---|
| 324 | cost.decSpec( td->assertions.size() ); |
---|
| 325 | } |
---|
| 326 | } |
---|
| 327 | } |
---|
| 328 | |
---|
| 329 | bool operator< ( const OutType & o ) const { return cost < o.cost; } |
---|
| 330 | }; |
---|
| 331 | |
---|
[cf32116] | 332 | CandidateEnvMerger( |
---|
| 333 | const ast::TypeEnvironment & env, const ast::OpenVarSet & open, |
---|
[b69233ac] | 334 | const ast::SymbolTable & syms ) |
---|
| 335 | : crnt(), envs{ env }, opens{ open }, symtab( syms ) {} |
---|
| 336 | |
---|
| 337 | bool append( DeferRef i ) { |
---|
| 338 | ast::TypeEnvironment env = envs.back(); |
---|
| 339 | ast::OpenVarSet open = opens.back(); |
---|
| 340 | mergeOpenVars( open, i.match.open ); |
---|
| 341 | |
---|
| 342 | if ( ! env.combine( i.match.env, open, symtab ) ) return false; |
---|
| 343 | |
---|
| 344 | crnt.emplace_back( i ); |
---|
| 345 | envs.emplace_back( std::move( env ) ); |
---|
| 346 | opens.emplace_back( std::move( open ) ); |
---|
| 347 | return true; |
---|
| 348 | } |
---|
| 349 | |
---|
| 350 | void backtrack() { |
---|
| 351 | crnt.pop_back(); |
---|
| 352 | envs.pop_back(); |
---|
| 353 | opens.pop_back(); |
---|
| 354 | } |
---|
| 355 | |
---|
| 356 | OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; } |
---|
| 357 | }; |
---|
| 358 | |
---|
| 359 | /// Limit to depth of recursion of assertion satisfaction |
---|
| 360 | static const int recursionLimit = 4; |
---|
| 361 | /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of |
---|
| 362 | static const int deferLimit = 10; |
---|
| 363 | } // anonymous namespace |
---|
| 364 | |
---|
[396037d] | 365 | void satisfyAssertions( |
---|
[b69233ac] | 366 | CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, |
---|
[396037d] | 367 | std::vector<std::string> & errors |
---|
| 368 | ) { |
---|
[b69233ac] | 369 | // finish early if no assertions to satisfy |
---|
| 370 | if ( cand->need.empty() ) { |
---|
| 371 | out.emplace_back( cand ); |
---|
| 372 | return; |
---|
| 373 | } |
---|
| 374 | |
---|
| 375 | // build list of possible combinations of satisfying declarations |
---|
| 376 | std::vector< SatState > sats{ SatState{ cand, symtab } }; |
---|
| 377 | std::vector< SatState > nextSats{}; |
---|
| 378 | |
---|
| 379 | // pruning thresholds by result type of output candidates. |
---|
| 380 | // Candidates *should* be generated in sorted order, so no need to retroactively prune |
---|
| 381 | PruneMap thresholds; |
---|
| 382 | |
---|
| 383 | // satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction. |
---|
| 384 | // Stop recursion at a limited number of levels deep to avoid infinite loops. |
---|
| 385 | for ( unsigned level = 0; level < recursionLimit; ++level ) { |
---|
| 386 | // for each current mutually-compatible set of assertions |
---|
| 387 | for ( SatState & sat : sats ) { |
---|
| 388 | // stop this branch if a better option is already found |
---|
| 389 | auto it = thresholds.find( pruneKey( *sat.cand ) ); |
---|
| 390 | if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat; |
---|
| 391 | |
---|
| 392 | // make initial pass at matching assertions |
---|
| 393 | for ( auto & assn : sat.need ) { |
---|
| 394 | // fail early if any assertion is not satisfiable |
---|
| 395 | if ( ! satisfyAssertion( assn, sat ) ) { |
---|
| 396 | Indenter tabs{ 3 }; |
---|
| 397 | std::ostringstream ss; |
---|
| 398 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 399 | print( ss, *sat.cand, ++tabs ); |
---|
| 400 | ss << (tabs-1) << "Could not satisfy assertion:\n"; |
---|
| 401 | ast::print( ss, assn.first, tabs ); |
---|
| 402 | |
---|
| 403 | errors.emplace_back( ss.str() ); |
---|
| 404 | goto nextSat; |
---|
| 405 | } |
---|
| 406 | } |
---|
| 407 | |
---|
| 408 | if ( sat.deferred.empty() ) { |
---|
| 409 | // either add successful match or push back next state |
---|
| 410 | if ( sat.newNeed.empty() ) { |
---|
| 411 | finalizeAssertions( |
---|
| 412 | sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out ); |
---|
| 413 | } else { |
---|
| 414 | nextSats.emplace_back( std::move( sat ), IterateState ); |
---|
| 415 | } |
---|
| 416 | } else if ( sat.deferred.size() > deferLimit ) { |
---|
| 417 | // too many deferred assertions to attempt mutual compatibility |
---|
| 418 | Indenter tabs{ 3 }; |
---|
| 419 | std::ostringstream ss; |
---|
| 420 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 421 | print( ss, *sat.cand, ++tabs ); |
---|
| 422 | ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n"; |
---|
| 423 | for ( const auto & d : sat.deferred ) { |
---|
| 424 | ast::print( ss, d.decl, tabs ); |
---|
| 425 | } |
---|
| 426 | |
---|
| 427 | errors.emplace_back( ss.str() ); |
---|
| 428 | goto nextSat; |
---|
| 429 | } else { |
---|
| 430 | // combine deferred assertions by mutual compatibility |
---|
| 431 | std::vector< CandidateEnvMerger::OutType > compatible = filterCombos( |
---|
| 432 | sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } ); |
---|
| 433 | |
---|
| 434 | // fail early if no mutually-compatible assertion satisfaction |
---|
| 435 | if ( compatible.empty() ) { |
---|
| 436 | Indenter tabs{ 3 }; |
---|
| 437 | std::ostringstream ss; |
---|
| 438 | ss << tabs << "Unsatisfiable alternative:\n"; |
---|
| 439 | print( ss, *sat.cand, ++tabs ); |
---|
| 440 | ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n"; |
---|
| 441 | for ( const auto& d : sat.deferred ) { |
---|
| 442 | ast::print( ss, d.decl, tabs ); |
---|
| 443 | } |
---|
| 444 | |
---|
| 445 | errors.emplace_back( ss.str() ); |
---|
| 446 | goto nextSat; |
---|
| 447 | } |
---|
| 448 | |
---|
| 449 | // sort by cost (for overall pruning order) |
---|
| 450 | std::sort( compatible.begin(), compatible.end() ); |
---|
| 451 | |
---|
| 452 | // process mutually-compatible combinations |
---|
| 453 | for ( auto & compat : compatible ) { |
---|
| 454 | // set up next satisfaction state |
---|
| 455 | CandidateRef nextCand = std::make_shared<Candidate>( |
---|
| 456 | sat.cand->expr, std::move( compat.env ), std::move( compat.open ), |
---|
| 457 | ast::AssertionSet{} /* need moved into satisfaction state */, |
---|
| 458 | sat.cand->cost, sat.cand->cvtCost ); |
---|
| 459 | |
---|
| 460 | ast::AssertionSet nextNewNeed{ sat.newNeed }; |
---|
| 461 | InferCache nextInferred{ sat.inferred }; |
---|
| 462 | |
---|
| 463 | CostVec nextCosts{ sat.costs }; |
---|
| 464 | nextCosts.back() += compat.cost; |
---|
| 465 | |
---|
| 466 | ast::SymbolTable nextSymtab{ sat.symtab }; |
---|
| 467 | |
---|
| 468 | // add compatible assertions to new satisfaction state |
---|
| 469 | for ( DeferRef r : compat.assns ) { |
---|
| 470 | AssnCandidate match = r.match; |
---|
| 471 | addToSymbolTable( match.have, nextSymtab ); |
---|
| 472 | nextNewNeed.insert( match.need.begin(), match.need.end() ); |
---|
| 473 | |
---|
| 474 | bindAssertion( r.decl, r.info, nextCand, match, nextInferred ); |
---|
| 475 | } |
---|
| 476 | |
---|
| 477 | // either add successful match or push back next state |
---|
| 478 | if ( nextNewNeed.empty() ) { |
---|
| 479 | finalizeAssertions( |
---|
| 480 | nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); |
---|
| 481 | } else { |
---|
| 482 | nextSats.emplace_back( |
---|
| 483 | std::move( nextCand ), std::move( nextNewNeed ), |
---|
| 484 | std::move( nextInferred ), std::move( nextCosts ), |
---|
| 485 | std::move( nextSymtab ) ); |
---|
| 486 | } |
---|
| 487 | } |
---|
| 488 | } |
---|
| 489 | nextSat:; } |
---|
| 490 | |
---|
| 491 | // finish or reset for next round |
---|
| 492 | if ( nextSats.empty() ) return; |
---|
| 493 | sats.swap( nextSats ); |
---|
| 494 | nextSats.clear(); |
---|
| 495 | } |
---|
| 496 | |
---|
| 497 | // exceeded recursion limit if reaches here |
---|
| 498 | if ( out.empty() ) { |
---|
| 499 | SemanticError( cand->expr->location, "Too many recursive assertions" ); |
---|
| 500 | } |
---|
[396037d] | 501 | } |
---|
| 502 | |
---|
| 503 | } // namespace ResolvExpr |
---|
| 504 | |
---|
| 505 | // Local Variables: // |
---|
| 506 | // tab-width: 4 // |
---|
| 507 | // mode: c++ // |
---|
| 508 | // compile-command: "make install" // |
---|
[cf32116] | 509 | // End: // |
---|