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 |
---|
11 | // Last Modified By : Andrew Beach |
---|
12 | // Last Modified On : Tue Oct 1 13:56:00 2019 |
---|
13 | // Update Count : 2 |
---|
14 | // |
---|
15 | |
---|
16 | #include "SatisfyAssertions.hpp" |
---|
17 | |
---|
18 | #include <iostream> |
---|
19 | #include <algorithm> |
---|
20 | #include <cassert> |
---|
21 | #include <sstream> |
---|
22 | #include <string> |
---|
23 | #include <unordered_map> |
---|
24 | #include <vector> |
---|
25 | |
---|
26 | #include "AdjustExprType.hpp" |
---|
27 | #include "Candidate.hpp" |
---|
28 | #include "CandidateFinder.hpp" |
---|
29 | #include "CommonType.hpp" |
---|
30 | #include "Cost.h" |
---|
31 | #include "RenameVars.h" |
---|
32 | #include "SpecCost.hpp" |
---|
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" |
---|
42 | #include "FindOpenVars.h" |
---|
43 | #include "Common/FilterCombos.h" |
---|
44 | #include "Common/Indenter.h" |
---|
45 | #include "GenPoly/GenPoly.h" |
---|
46 | #include "SymTab/Mangler.h" |
---|
47 | |
---|
48 | |
---|
49 | |
---|
50 | namespace ResolvExpr { |
---|
51 | |
---|
52 | // in CandidateFinder.cpp; unique ID for assertion satisfaction |
---|
53 | extern ast::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 | |
---|
66 | AssnCandidate( |
---|
67 | const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, |
---|
68 | ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) |
---|
69 | : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), |
---|
70 | need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) { |
---|
71 | if (!have.empty()) { |
---|
72 | // std::cerr << c.id->location << ':' << c.id->name << std::endl; // I think this was debugging code so I commented it |
---|
73 | } |
---|
74 | } |
---|
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 { |
---|
82 | const ast::VariableExpr * expr; |
---|
83 | const ast::AssertionSetValue & info; |
---|
84 | const AssnCandidate & match; |
---|
85 | }; |
---|
86 | |
---|
87 | /// Wrapper for the deferred items from a single assertion satisfaction. |
---|
88 | /// Acts like an indexed list of DeferRef |
---|
89 | struct DeferItem { |
---|
90 | const ast::VariableExpr * expr; |
---|
91 | const ast::AssertionSetValue & info; |
---|
92 | AssnCandidateList matches; |
---|
93 | |
---|
94 | DeferItem( |
---|
95 | const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) |
---|
96 | : expr( d ), info( i ), matches( std::move( ms ) ) {} |
---|
97 | |
---|
98 | bool empty() const { return matches.empty(); } |
---|
99 | |
---|
100 | AssnCandidateList::size_type size() const { return matches.size(); } |
---|
101 | |
---|
102 | DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; } |
---|
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 ) |
---|
130 | : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, |
---|
131 | symtab( syms ) { need.swap( c->need ); } |
---|
132 | |
---|
133 | /// Update satisfaction state for next step after previous state |
---|
134 | SatState( SatState && o, IterateFlag ) |
---|
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 ) ), |
---|
137 | symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } |
---|
138 | |
---|
139 | /// Field-wise next step constructor |
---|
140 | SatState( |
---|
141 | CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, |
---|
142 | ast::SymbolTable && syms ) |
---|
143 | : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), |
---|
144 | inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) |
---|
145 | { costs.emplace_back( Cost::zero ); } |
---|
146 | }; |
---|
147 | |
---|
148 | enum AssertionResult {Fail, Skip, Success} ; |
---|
149 | |
---|
150 | /// Binds a single assertion, updating satisfaction state |
---|
151 | void bindAssertion( |
---|
152 | const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, |
---|
153 | AssnCandidate & match, InferCache & inferred |
---|
154 | ) { |
---|
155 | const ast::DeclWithType * candidate = match.cdata.id; |
---|
156 | assertf( candidate->uniqueId, |
---|
157 | "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); |
---|
158 | |
---|
159 | ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cost ); |
---|
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 |
---|
164 | inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{ |
---|
165 | candidate->uniqueId, candidate, match.adjType, expr->result, varExpr }; |
---|
166 | } |
---|
167 | |
---|
168 | /// Satisfy a single assertion |
---|
169 | AssertionResult satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool skipUnbound = false) { |
---|
170 | // skip unused assertions |
---|
171 | // static unsigned int cnt = 0; // I think this was debugging code so I commented it |
---|
172 | if ( ! assn.second.isUsed ) return AssertionResult::Success; |
---|
173 | |
---|
174 | // if (assn.first->var->name[1] == '|') std::cerr << ++cnt << std::endl; // I think this was debugging code so I commented it |
---|
175 | |
---|
176 | // find candidates that unify with the desired type |
---|
177 | AssnCandidateList matches, inexactMatches; |
---|
178 | |
---|
179 | std::vector<ast::SymbolTable::IdData> candidates; |
---|
180 | auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name); |
---|
181 | if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) { |
---|
182 | // prefilter special decls by argument type, if already known |
---|
183 | ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base |
---|
184 | .strict_as<ast::FunctionType>()->params[0] |
---|
185 | .strict_as<ast::ReferenceType>()->base; |
---|
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 | } |
---|
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); |
---|
196 | else if (skipUnbound) return AssertionResult::Skip; |
---|
197 | |
---|
198 | candidates = sat.symtab.specialLookupId(kind, otypeKey); |
---|
199 | } |
---|
200 | else { |
---|
201 | candidates = sat.symtab.lookupId(assn.first->var->name); |
---|
202 | } |
---|
203 | for ( const ast::SymbolTable::IdData & cdata : candidates ) { |
---|
204 | const ast::DeclWithType * candidate = cdata.id; |
---|
205 | |
---|
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) |
---|
211 | if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue; |
---|
212 | |
---|
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 }; |
---|
217 | ast::ptr< ast::Type > toType = assn.first->result; |
---|
218 | ast::ptr< ast::Type > adjType = |
---|
219 | renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false ); |
---|
220 | |
---|
221 | // only keep candidates which unify |
---|
222 | |
---|
223 | ast::OpenVarSet closed; |
---|
224 | // findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed ); |
---|
225 | findOpenVars( adjType, newOpen, closed, newNeed, have, newEnv, FirstOpen ); |
---|
226 | ast::TypeEnvironment tempNewEnv {newEnv}; |
---|
227 | |
---|
228 | if ( unifyExact( toType, adjType, tempNewEnv, newNeed, have, newOpen, WidenMode {true, true} ) ) { |
---|
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; } |
---|
234 | } |
---|
235 | |
---|
236 | matches.emplace_back( |
---|
237 | cdata, adjType, std::move( tempNewEnv ), std::move( have ), std::move( newNeed ), |
---|
238 | std::move( newOpen ), crntResnSlot ); |
---|
239 | } |
---|
240 | else if ( matches.empty() ) { |
---|
241 | // restore invalidated env |
---|
242 | // newEnv = sat.cand->env; |
---|
243 | // newNeed.clear(); |
---|
244 | if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true} ) ) { |
---|
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 | } |
---|
251 | |
---|
252 | inexactMatches.emplace_back( |
---|
253 | cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ), |
---|
254 | std::move( newOpen ), crntResnSlot ); |
---|
255 | } |
---|
256 | } |
---|
257 | } |
---|
258 | |
---|
259 | // break if no satisfying match |
---|
260 | if ( matches.empty() ) matches = std::move(inexactMatches); |
---|
261 | if ( matches.empty() ) return AssertionResult::Fail; |
---|
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 ) ); |
---|
266 | return AssertionResult::Success; |
---|
267 | } |
---|
268 | |
---|
269 | // otherwise bind unique match in ongoing scope |
---|
270 | AssnCandidate & match = matches.front(); |
---|
271 | // addToSymbolTable( match.have, sat.symtab ); |
---|
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 ); |
---|
277 | return AssertionResult::Success; |
---|
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 ); |
---|
287 | return Mangle::mangleType( resType ); |
---|
288 | } |
---|
289 | |
---|
290 | /// Associates inferred parameters with an expression |
---|
291 | struct InferMatcher final { |
---|
292 | InferCache & inferred; |
---|
293 | |
---|
294 | InferMatcher( InferCache & inferred ) : inferred( inferred ) {} |
---|
295 | |
---|
296 | const ast::Expr * postvisit( const ast::Expr * expr ) { |
---|
297 | // Skip if no slots to find |
---|
298 | if ( !expr->inferred.hasSlots() ) return expr; |
---|
299 | // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr; |
---|
300 | std::vector<ast::UniqueId> missingSlots; |
---|
301 | // find inferred parameters for resolution slots |
---|
302 | ast::InferredParams * newInferred = new ast::InferredParams(); |
---|
303 | for ( ast::UniqueId slot : expr->inferred.resnSlots() ) { |
---|
304 | // fail if no matching assertions found |
---|
305 | auto it = inferred.find( slot ); |
---|
306 | if ( it == inferred.end() ) { |
---|
307 | // std::cerr << "missing assertion " << slot << std::endl; |
---|
308 | missingSlots.push_back(slot); |
---|
309 | continue; |
---|
310 | } |
---|
311 | |
---|
312 | // place inferred parameters into new map |
---|
313 | for ( auto & entry : it->second ) { |
---|
314 | // recurse on inferParams of resolved expressions |
---|
315 | entry.second.expr = postvisit( entry.second.expr ); |
---|
316 | auto res = newInferred->emplace( entry ); |
---|
317 | assert( res.second && "all assertions newly placed" ); |
---|
318 | } |
---|
319 | } |
---|
320 | |
---|
321 | ast::Expr * ret = mutate( expr ); |
---|
322 | ret->inferred.set_inferParams( newInferred ); |
---|
323 | if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots; |
---|
324 | return ret; |
---|
325 | } |
---|
326 | }; |
---|
327 | |
---|
328 | /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning |
---|
329 | /// threshold. |
---|
330 | void finalizeAssertions( |
---|
331 | CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, |
---|
332 | CandidateList & out |
---|
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 | |
---|
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` |
---|
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 | |
---|
370 | OutType( |
---|
371 | const ast::TypeEnvironment & e, const ast::OpenVarSet & o, |
---|
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 |
---|
377 | cost += computeConversionCost( |
---|
378 | assn.match.adjType, assn.expr->result, false, symtab, env ); |
---|
379 | |
---|
380 | // mark vars+specialization on function-type assertions |
---|
381 | const ast::FunctionType * func = |
---|
382 | GenPoly::getFunctionType( assn.match.cdata.id->get_type() ); |
---|
383 | if ( ! func ) continue; |
---|
384 | |
---|
385 | for ( const auto & param : func->params ) { |
---|
386 | cost.decSpec( specCost( param ) ); |
---|
387 | } |
---|
388 | |
---|
389 | cost.incVar( func->forall.size() ); |
---|
390 | |
---|
391 | cost.decSpec( func->assertions.size() ); |
---|
392 | } |
---|
393 | } |
---|
394 | |
---|
395 | bool operator< ( const OutType & o ) const { return cost < o.cost; } |
---|
396 | }; |
---|
397 | |
---|
398 | CandidateEnvMerger( |
---|
399 | const ast::TypeEnvironment & env, const ast::OpenVarSet & open, |
---|
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 | |
---|
408 | if ( ! env.combine( i.match.env, open ) ) return false; |
---|
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 |
---|
426 | static const int recursionLimit = 8; |
---|
427 | /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of |
---|
428 | static const int deferLimit = 10; |
---|
429 | } // anonymous namespace |
---|
430 | |
---|
431 | void satisfyAssertions( |
---|
432 | CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, |
---|
433 | std::vector<std::string> & errors |
---|
434 | ) { |
---|
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 | |
---|
458 | // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen. |
---|
459 | |
---|
460 | for (unsigned resetCount = 0; ; ++resetCount) { |
---|
461 | ast::AssertionList next; |
---|
462 | // make initial pass at matching assertions |
---|
463 | for ( auto & assn : sat.need ) { |
---|
464 | resetTyVarRenaming(); |
---|
465 | // fail early if any assertion is not satisfiable |
---|
466 | auto result = satisfyAssertion( assn, sat, !next.empty() ); |
---|
467 | if ( result == AssertionResult::Fail ) { |
---|
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"; |
---|
473 | ast::print( ss, assn.first, tabs ); |
---|
474 | |
---|
475 | errors.emplace_back( ss.str() ); |
---|
476 | goto nextSat; |
---|
477 | } |
---|
478 | else if ( result == AssertionResult::Skip ) { |
---|
479 | next.emplace_back(assn); |
---|
480 | // goto nextSat; |
---|
481 | } |
---|
482 | } |
---|
483 | // success |
---|
484 | if (next.empty()) break; |
---|
485 | |
---|
486 | sat.need = std::move(next); |
---|
487 | } |
---|
488 | |
---|
489 | if ( sat.deferred.empty() ) { |
---|
490 | // either add successful match or push back next state |
---|
491 | if ( sat.newNeed.empty() ) { |
---|
492 | finalizeAssertions( |
---|
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 ) { |
---|
505 | ast::print( ss, d.expr, tabs ); |
---|
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 } ); |
---|
514 | |
---|
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 ) { |
---|
523 | ast::print( ss, d.expr, tabs ); |
---|
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>( |
---|
537 | sat.cand->expr, std::move( compat.env ), std::move( compat.open ), |
---|
538 | ast::AssertionSet{} /* need moved into satisfaction state */, |
---|
539 | sat.cand->cost ); |
---|
540 | |
---|
541 | ast::AssertionSet nextNewNeed{ sat.newNeed }; |
---|
542 | InferCache nextInferred{ sat.inferred }; |
---|
543 | |
---|
544 | CostVec nextCosts{ sat.costs }; |
---|
545 | nextCosts.back() += compat.cost; |
---|
546 | |
---|
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; |
---|
552 | // addToSymbolTable( match.have, nextSymtab ); |
---|
553 | nextNewNeed.insert( match.need.begin(), match.need.end() ); |
---|
554 | |
---|
555 | bindAssertion( r.expr, r.info, nextCand, match, nextInferred ); |
---|
556 | } |
---|
557 | |
---|
558 | // either add successful match or push back next state |
---|
559 | if ( nextNewNeed.empty() ) { |
---|
560 | finalizeAssertions( |
---|
561 | nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); |
---|
562 | } else { |
---|
563 | nextSats.emplace_back( |
---|
564 | std::move( nextCand ), std::move( nextNewNeed ), |
---|
565 | std::move( nextInferred ), std::move( nextCosts ), |
---|
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 | } |
---|
577 | |
---|
578 | // exceeded recursion limit if reaches here |
---|
579 | if ( out.empty() ) { |
---|
580 | SemanticError( cand->expr->location, "Too many recursive assertions" ); |
---|
581 | } |
---|
582 | } |
---|
583 | |
---|
584 | } // namespace ResolvExpr |
---|
585 | |
---|
586 | // Local Variables: // |
---|
587 | // tab-width: 4 // |
---|
588 | // mode: c++ // |
---|
589 | // compile-command: "make install" // |
---|
590 | // End: // |
---|