source: src/ResolvExpr/TypeEnvironment.cc@ 97397a26

new-env
Last change on this file since 97397a26 was 982f95d, checked in by Aaron Moss <a3moss@…>, 8 years ago

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