source: src/ResolvExpr/SatisfyAssertions.cpp@ 0c840fc

ast-experimental
Last change on this file since 0c840fc was 0c840fc, checked in by Fangren Yu <f37yu@…>, 2 years ago

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