Context Navigation

source: src/ResolvExpr/TypeEnvironment.cc @ 0e761e40

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

Last change on this file since 0e761e40 was d286cf68, checked in by Aaron Moss <a3moss@…>, 6 years ago
Fix TypeEnvironment? bind algorithms
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	} // switch
243	return false;
244	}
245
246	bool TypeEnvironment::bindVar( TypeInstType typeInst, Type bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
247
248	// remove references from other, so that type variables can only bind to value types
249	bindTo = bindTo->stripReferences();
250	OpenVarSet::const_iterator tyvar = openVars.find( typeInst->get_name() );
251	assert( tyvar != openVars.end() );
252	if ( ! tyVarCompatible( tyvar->second, bindTo ) ) {
253	return false;
254	} // if
255	if ( occurs( bindTo, typeInst->get_name(), *this ) ) {
256	return false;
257	} // if
258	auto curClass = internal_lookup( typeInst->get_name() );
259	if ( curClass != env.end() ) {
260	if ( curClass->type ) {
261	Type *common = 0;
262	// attempt to unify equivalence class type (which has qualifiers stripped, so they must be restored) with the type to bind to
263	std::unique_ptr< Type > newType( curClass->type->clone() );
264	newType->get_qualifiers() = typeInst->get_qualifiers();
265	if ( unifyInexact( newType.get(), bindTo, *this, need, have, openVars, widenMode & WidenMode( curClass->allowWidening, true ), indexer, common ) ) {
266	if ( common ) {
267	common->get_qualifiers() = Type::Qualifiers{};
268	curClass->set_type( common );
269	} // if
270	} else return false;
271	} else {
272	Type* newType = bindTo->clone();
273	newType->get_qualifiers() = Type::Qualifiers{};
274	curClass->set_type( newType );
275	curClass->allowWidening = widenMode.widenFirst && widenMode.widenSecond;
276	} // if
277	} else {
278	EqvClass newClass;
279	newClass.vars.insert( typeInst->get_name() );
280	newClass.type = bindTo->clone();
281	newClass.type->get_qualifiers() = Type::Qualifiers();
282	newClass.allowWidening = widenMode.widenFirst && widenMode.widenSecond;
283	newClass.data = data;
284	env.push_back( std::move(newClass) );
285	} // if
286	return true;
287	}
288
289	bool TypeEnvironment::bindVarToVar( TypeInstType var1, TypeInstType var2, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
290
291	auto class1 = internal_lookup( var1->get_name() );
292	auto class2 = internal_lookup( var2->get_name() );
293
294	// exit early if variables already bound together
295	if ( class1 != env.end() && class1 == class2 ) {
296	class1->allowWidening &= widenMode;
297	return true;
298	}
299
300	bool widen1 = false, widen2 = false;
301	const Type type1 = nullptr, type2 = nullptr;
302
303	// check for existing bindings, perform occurs check
304	if ( class1 != env.end() ) {
305	if ( class1->type ) {
306	if ( occurs( class1->type, var2->get_name(), *this ) ) return false;
307	type1 = class1->type;
308	} // if
309	widen1 = widenMode.widenFirst && class1->allowWidening;
310	} // if
311	if ( class2 != env.end() ) {
312	if ( class2->type ) {
313	if ( occurs( class2->type, var1->get_name(), *this ) ) return false;
314	type2 = class2->type;
315	} // if
316	widen2 = widenMode.widenSecond && class2->allowWidening;
317	} // if
318
319	if ( type1 && type2 ) {
320	// both classes bound, merge if bound types can be unified
321	std::unique_ptr<Type> newType1{ type1->clone() }, newType2{ type2->clone() };
322	WidenMode newWidenMode{ widen1, widen2 };
323	Type *common = 0;
324	if ( unifyInexact( newType1.get(), newType2.get(), *this, need, have, openVars, newWidenMode, indexer, common ) ) {
325	class1->vars.insert( class2->vars.begin(), class2->vars.end() );
326	class1->allowWidening = widen1 && widen2;
327	if ( common ) {
328	common->get_qualifiers() = Type::Qualifiers{};
329	class1->set_type( common );
330	}
331	env.erase( class2 );
332	} else return false;
333	} else if ( class1 != env.end() && class2 != env.end() ) {
334	// both classes exist, at least one unbound, merge unconditionally
335	if ( type1 ) {
336	class1->vars.insert( class2->vars.begin(), class2->vars.end() );
337	class1->allowWidening = widen1;
338	env.erase( class2 );
339	} else {
340	class2->vars.insert( class1->vars.begin(), class1->vars.end() );
341	class2->allowWidening = widen2;
342	env.erase( class1 );
343	} // if
344	} else if ( class1 != env.end() ) {
345	// var2 unbound, add to class1
346	class1->vars.insert( var2->get_name() );
347	class1->allowWidening = widen1;
348	} else if ( class2 != env.end() ) {
349	// var1 unbound, add to class2
350	class2->vars.insert( var1->get_name() );
351	class2->allowWidening = widen2;
352	} else {
353	// neither var bound, create new class
354	EqvClass newClass;
355	newClass.vars.insert( var1->get_name() );
356	newClass.vars.insert( var2->get_name() );
357	newClass.allowWidening = widen1 && widen2;
358	newClass.data = data;
359	env.push_back( std::move(newClass) );
360	} // if
361	return true;
362	}
363
364	void TypeEnvironment::forbidWidening() {
365	for ( EqvClass& c : env ) c.allowWidening = false;
366	}
367
368	std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env ) {
369	env.print( out );
370	return out;
371	}
372	} // namespace ResolvExpr
373
374	// Local Variables: //
375	// tab-width: 4 //
376	// mode: c++ //
377	// compile-command: "make install" //
378	// End: //

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

Download in other formats: