Context Navigation

source: src/ResolvExpr/TypeEnvironment.cc @ 933933c

ADTaaron-thesisarm-ehast-experimentalcleanup-dtorsdeferred_resnenumforall-pointer-decayjacob/cs343-translationjenkins-sandboxnew-astnew-ast-unique-exprno_listpersistent-indexerpthread-emulationqualifiedEnum

Last change on this file since 933933c was 51a455c, checked in by Rob Schluntz <rschlunt@…>, 6 years ago
Fix unhandled enum warning in TypeEnvironment?
Property mode set to `100644`
File size: 12.8 KB

Line
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	// TypeEnvironment.cc --
8	//
9	// Author : Richard C. Bilson
10	// Created On : Sun May 17 12:19:47 2015
11	// Last Modified By : Aaron B. Moss
12	// Last Modified On : Mon Jun 18 11:58:00 2018
13	// Update Count : 4
14	//
15
16	#include <cassert> // for assert
17	#include <algorithm> // for copy, set_intersection
18	#include <iterator> // for ostream_iterator, insert_iterator
19	#include <memory> // for unique_ptr
20	#include <utility> // for pair, move
21
22	#include "Common/utility.h" // for maybeClone
23	#include "SynTree/Type.h" // for Type, FunctionType, Type::Fora...
24	#include "SynTree/TypeSubstitution.h" // for TypeSubstitution
25	#include "Tuples/Tuples.h" // for isTtype
26	#include "TypeEnvironment.h"
27	#include "typeops.h" // for occurs
28	#include "Unify.h" // for unifyInexact
29
30	namespace ResolvExpr {
31	void printAssertionSet( const AssertionSet &assertions, std::ostream &os, int indent ) {
32	for ( AssertionSet::const_iterator i = assertions.begin(); i != assertions.end(); ++i ) {
33	i->first->print( os, indent );
34	if ( i->second.isUsed ) {
35	os << "(used)";
36	} else {
37	os << "(not used)";
38	} // if
39	} // for
40	}
41
42	void printOpenVarSet( const OpenVarSet &openVars, std::ostream &os, int indent ) {
43	os << std::string( indent, ' ' );
44	for ( OpenVarSet::const_iterator i = openVars.begin(); i != openVars.end(); ++i ) {
45	os << i->first << "(" << i->second << ") ";
46	} // for
47	}
48
49	void EqvClass::initialize( const EqvClass &src, EqvClass &dest ) {
50	initialize( src, dest, src.type );
51	}
52
53	void EqvClass::initialize( const EqvClass &src, EqvClass &dest, const Type *ty ) {
54	dest.vars = src.vars;
55	dest.type = maybeClone( ty );
56	dest.allowWidening = src.allowWidening;
57	dest.data = src.data;
58	}
59
60	EqvClass::EqvClass() : type( nullptr ), allowWidening( true ) {
61	}
62
63	EqvClass::EqvClass( const EqvClass &other ) {
64	initialize( other, *this );
65	}
66
67	EqvClass::EqvClass( const EqvClass &other, const Type *ty ) {
68	initialize( other, *this, ty );
69	}
70
71	EqvClass::EqvClass( EqvClass &&other )
72	: vars{std::move(other.vars)}, type{other.type},
73	allowWidening{std::move(other.allowWidening)}, data{std::move(other.data)} {
74	other.type = nullptr;
75	}
76
77	EqvClass &EqvClass::operator=( const EqvClass &other ) {
78	if ( this == &other ) return *this;
79	delete type;
80	initialize( other, *this );
81	return *this;
82	}
83
84	EqvClass &EqvClass::operator=( EqvClass &&other ) {
85	if ( this == &other ) return *this;
86	delete type;
87
88	vars = std::move(other.vars);
89	type = other.type;
90	other.type = nullptr;
91	allowWidening = std::move(other.allowWidening);
92	data = std::move(other.data);
93
94	return *this;
95	}
96
97	EqvClass::~EqvClass() {
98	delete type;
99	}
100
101	void EqvClass::set_type( Type* ty ) {
102	if ( ty == type ) return;
103	delete type;
104	type = ty;
105	}
106
107	void EqvClass::print( std::ostream &os, Indenter indent ) const {
108	os << "( ";
109	std::copy( vars.begin(), vars.end(), std::ostream_iterator< std::string >( os, " " ) );
110	os << ")";
111	if ( type ) {
112	os << " -> ";
113	type->print( os, indent+1 );
114	} // if
115	if ( ! allowWidening ) {
116	os << " (no widening)";
117	} // if
118	os << std::endl;
119	}
120
121	const EqvClass* TypeEnvironment::lookup( const std::string &var ) const {
122	for ( std::list< EqvClass >::const_iterator i = env.begin(); i != env.end(); ++i ) {
123	if ( i->vars.find( var ) != i->vars.end() ) return &*i;
124	} // for
125	return nullptr;
126	}
127
128	/// Removes any class from env that intersects eqvClass
129	void filterOverlappingClasses( std::list<EqvClass> &env, const EqvClass &eqvClass ) {
130	for ( auto i = env.begin(); i != env.end(); ) {
131	auto next = i;
132	++next;
133	std::set<std::string> intersection;
134	std::set_intersection( i->vars.begin(), i->vars.end(), eqvClass.vars.begin(), eqvClass.vars.end(),
135	std::inserter( intersection, intersection.begin() ) );
136	if ( ! intersection.empty() ) { env.erase( i ); }
137	i = next;
138	}
139	}
140
141	void TypeEnvironment::add( EqvClass &&eqvClass ) {
142	filterOverlappingClasses( env, eqvClass );
143	env.push_back( std::move(eqvClass) );
144	}
145
146	void TypeEnvironment::add( const Type::ForallList &tyDecls ) {
147	for ( Type::ForallList::const_iterator i = tyDecls.begin(); i != tyDecls.end(); ++i ) {
148	EqvClass newClass;
149	newClass.vars.insert( (*i)->get_name() );
150	newClass.data = TypeDecl::Data{ (*i) };
151	env.push_back( std::move(newClass) );
152	} // for
153	}
154
155	void TypeEnvironment::add( const TypeSubstitution & sub ) {
156	EqvClass newClass;
157	for ( auto p : sub ) {
158	newClass.vars.insert( p.first );
159	newClass.type = p.second->clone();
160	newClass.allowWidening = false;
161	// Minimal assumptions. Not technically correct, but might be good enough, and
162	// is the best we can do at the moment since information is lost in the
163	// transition to TypeSubstitution
164	newClass.data = TypeDecl::Data{ TypeDecl::Dtype, false };
165	add( std::move(newClass) );
166	}
167	}
168
169	void TypeEnvironment::makeSubstitution( TypeSubstitution &sub ) const {
170	for ( std::list< EqvClass >::const_iterator theClass = env.begin(); theClass != env.end(); ++theClass ) {
171	for ( std::set< std::string >::const_iterator theVar = theClass->vars.begin(); theVar != theClass->vars.end(); ++theVar ) {
172	if ( theClass->type ) {
173	sub.add( *theVar, theClass->type );
174	} else if ( theVar != theClass->vars.begin() ) {
175	TypeInstType newTypeInst = new TypeInstType( Type::Qualifiers(), theClass->vars.begin(), theClass->data.kind == TypeDecl::Ftype );
176	sub.add( *theVar, newTypeInst );
177	delete newTypeInst;
178	} // if
179	} // for
180	} // for
181	sub.normalize();
182	}
183
184	void TypeEnvironment::print( std::ostream &os, Indenter indent ) const {
185	for ( const EqvClass & theClass : env ) {
186	theClass.print( os, indent );
187	} // for
188	}
189
190	std::list< EqvClass >::iterator TypeEnvironment::internal_lookup( const std::string &var ) {
191	for ( std::list< EqvClass >::iterator i = env.begin(); i != env.end(); ++i ) {
192	if ( i->vars.count( var ) ) return i;
193	} // for
194	return env.end();
195	}
196
197	void TypeEnvironment::simpleCombine( const TypeEnvironment &second ) {
198	env.insert( env.end(), second.env.begin(), second.env.end() );
199	}
200
201	void TypeEnvironment::extractOpenVars( OpenVarSet &openVars ) const {
202	for ( std::list< EqvClass >::const_iterator eqvClass = env.begin(); eqvClass != env.end(); ++eqvClass ) {
203	for ( std::set< std::string >::const_iterator var = eqvClass->vars.begin(); var != eqvClass->vars.end(); ++var ) {
204	openVars[ *var ] = eqvClass->data;
205	} // for
206	} // for
207	}
208
209	void TypeEnvironment::addActual( const TypeEnvironment& actualEnv, OpenVarSet& openVars ) {
210	for ( const EqvClass& c : actualEnv ) {
211	EqvClass c2 = c;
212	c2.allowWidening = false;
213	for ( const std::string& var : c2.vars ) {
214	openVars[ var ] = c2.data;
215	}
216	env.push_back( std::move(c2) );
217	}
218	}
219
220	bool isFtype( Type *type ) {
221	if ( dynamic_cast< FunctionType* >( type ) ) {
222	return true;
223	} else if ( TypeInstType typeInst = dynamic_cast< TypeInstType >( type ) ) {
224	return typeInst->get_isFtype();
225	} // if
226	return false;
227	}
228
229	bool tyVarCompatible( const TypeDecl::Data & data, Type *type ) {
230	switch ( data.kind ) {
231	case TypeDecl::Dtype:
232	// to bind to an object type variable, the type must not be a function type.
233	// if the type variable is specified to be a complete type then the incoming
234	// type must also be complete
235	// xxx - should this also check that type is not a tuple type and that it's not a ttype?
236	return ! isFtype( type ) && (! data.isComplete \|\| type->isComplete() );
237	case TypeDecl::Ftype:
238	return isFtype( type );
239	case TypeDecl::Ttype:
240	// ttype unifies with any tuple type
241	return dynamic_cast< TupleType * >( type ) \|\| Tuples::isTtype( type );
242	default:
243	assertf(false, "Unhandled tyvar kind: %d", data.kind);
244	} // switch
245	return false;
246	}
247
248	bool TypeEnvironment::bindVar( TypeInstType typeInst, Type bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
249
250	// remove references from other, so that type variables can only bind to value types
251	bindTo = bindTo->stripReferences();
252	OpenVarSet::const_iterator tyvar = openVars.find( typeInst->get_name() );
253	assert( tyvar != openVars.end() );
254	if ( ! tyVarCompatible( tyvar->second, bindTo ) ) {
255	return false;
256	} // if
257	if ( occurs( bindTo, typeInst->get_name(), *this ) ) {
258	return false;
259	} // if
260	auto curClass = internal_lookup( typeInst->get_name() );
261	if ( curClass != env.end() ) {
262	if ( curClass->type ) {
263	Type *common = 0;
264	// attempt to unify equivalence class type (which has qualifiers stripped, so they must be restored) with the type to bind to
265	std::unique_ptr< Type > newType( curClass->type->clone() );
266	newType->get_qualifiers() = typeInst->get_qualifiers();
267	if ( unifyInexact( newType.get(), bindTo, *this, need, have, openVars, widenMode & WidenMode( curClass->allowWidening, true ), indexer, common ) ) {
268	if ( common ) {
269	common->get_qualifiers() = Type::Qualifiers{};
270	curClass->set_type( common );
271	} // if
272	} else return false;
273	} else {
274	Type* newType = bindTo->clone();
275	newType->get_qualifiers() = Type::Qualifiers{};
276	curClass->set_type( newType );
277	curClass->allowWidening = widenMode.widenFirst && widenMode.widenSecond;
278	} // if
279	} else {
280	EqvClass newClass;
281	newClass.vars.insert( typeInst->get_name() );
282	newClass.type = bindTo->clone();
283	newClass.type->get_qualifiers() = Type::Qualifiers();
284	newClass.allowWidening = widenMode.widenFirst && widenMode.widenSecond;
285	newClass.data = data;
286	env.push_back( std::move(newClass) );
287	} // if
288	return true;
289	}
290
291	bool TypeEnvironment::bindVarToVar( TypeInstType var1, TypeInstType var2, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
292
293	auto class1 = internal_lookup( var1->get_name() );
294	auto class2 = internal_lookup( var2->get_name() );
295
296	// exit early if variables already bound together
297	if ( class1 != env.end() && class1 == class2 ) {
298	class1->allowWidening &= widenMode;
299	return true;
300	}
301
302	bool widen1 = false, widen2 = false;
303	const Type type1 = nullptr, type2 = nullptr;
304
305	// check for existing bindings, perform occurs check
306	if ( class1 != env.end() ) {
307	if ( class1->type ) {
308	if ( occurs( class1->type, var2->get_name(), *this ) ) return false;
309	type1 = class1->type;
310	} // if
311	widen1 = widenMode.widenFirst && class1->allowWidening;
312	} // if
313	if ( class2 != env.end() ) {
314	if ( class2->type ) {
315	if ( occurs( class2->type, var1->get_name(), *this ) ) return false;
316	type2 = class2->type;
317	} // if
318	widen2 = widenMode.widenSecond && class2->allowWidening;
319	} // if
320
321	if ( type1 && type2 ) {
322	// both classes bound, merge if bound types can be unified
323	std::unique_ptr<Type> newType1{ type1->clone() }, newType2{ type2->clone() };
324	WidenMode newWidenMode{ widen1, widen2 };
325	Type *common = 0;
326	if ( unifyInexact( newType1.get(), newType2.get(), *this, need, have, openVars, newWidenMode, indexer, common ) ) {
327	class1->vars.insert( class2->vars.begin(), class2->vars.end() );
328	class1->allowWidening = widen1 && widen2;
329	if ( common ) {
330	common->get_qualifiers() = Type::Qualifiers{};
331	class1->set_type( common );
332	}
333	env.erase( class2 );
334	} else return false;
335	} else if ( class1 != env.end() && class2 != env.end() ) {
336	// both classes exist, at least one unbound, merge unconditionally
337	if ( type1 ) {
338	class1->vars.insert( class2->vars.begin(), class2->vars.end() );
339	class1->allowWidening = widen1;
340	env.erase( class2 );
341	} else {
342	class2->vars.insert( class1->vars.begin(), class1->vars.end() );
343	class2->allowWidening = widen2;
344	env.erase( class1 );
345	} // if
346	} else if ( class1 != env.end() ) {
347	// var2 unbound, add to class1
348	class1->vars.insert( var2->get_name() );
349	class1->allowWidening = widen1;
350	} else if ( class2 != env.end() ) {
351	// var1 unbound, add to class2
352	class2->vars.insert( var1->get_name() );
353	class2->allowWidening = widen2;
354	} else {
355	// neither var bound, create new class
356	EqvClass newClass;
357	newClass.vars.insert( var1->get_name() );
358	newClass.vars.insert( var2->get_name() );
359	newClass.allowWidening = widen1 && widen2;
360	newClass.data = data;
361	env.push_back( std::move(newClass) );
362	} // if
363	return true;
364	}
365
366	void TypeEnvironment::forbidWidening() {
367	for ( EqvClass& c : env ) c.allowWidening = false;
368	}
369
370	std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env ) {
371	env.print( out );
372	return out;
373	}
374	} // namespace ResolvExpr
375
376	// Local Variables: //
377	// tab-width: 4 //
378	// mode: c++ //
379	// compile-command: "make install" //
380	// End: //

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

Download in other formats: