Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp @ 2ceb2bf

ADTast-experimental

Last change on this file since 2ceb2bf was 5bf3976, checked in by Andrew Beach <ajbeach@…>, 18 months ago
Header Clean-Up: Created new headers for new AST typeops and moved declarations.
Property mode set to `100644`
File size: 20.3 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats: