source: src/AST/TypeEnvironment.cpp @ 3e5dd913

arm-ehjacob/cs343-translationnew-ast-unique-expr
Last change on this file since 3e5dd913 was 3e5dd913, checked in by Fangren Yu <f37yu@…>, 10 months ago

reimplement function type and eliminate deep copy

  • Property mode set to 100644
File size: 13.5 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.cpp --
8//
9// Author           : Aaron B. Moss
10// Created On       : Wed May 29 11:00:00 2019
11// Last Modified By : Peter A. Buhr
12// Last Modified On : Wed Dec 11 21:49:13 2019
13// Update Count     : 4
14//
15
16#include "TypeEnvironment.hpp"
17
18#include <algorithm>  // for copy
19#include <cassert>
20#include <iterator>   // for ostream_iterator
21#include <iostream>
22#include <string>
23#include <utility>    // for move
24#include <vector>
25
26#include "Decl.hpp"
27#include "Node.hpp"
28#include "Pass.hpp"
29#include "Print.hpp"
30#include "Type.hpp"
31#include "Common/Indenter.h"
32#include "ResolvExpr/typeops.h"    // for occurs
33#include "ResolvExpr/WidenMode.h"
34#include "ResolvExpr/Unify.h"      // for unifyInexact
35#include "Tuples/Tuples.h"         // for isTtype
36#include "CompilationState.h"
37
38using ResolvExpr::WidenMode;
39
40namespace ast {
41
42void print( std::ostream & out, const AssertionSet & assns, Indenter indent ) {
43        for ( const auto & i : assns ) {
44                print( out, i.first, indent );
45                out << ( i.second.isUsed ? " (used)" : " (not used)" );
46        }
47}
48
49void print( std::ostream & out, const OpenVarSet & open, Indenter indent ) {
50        out << indent;
51        bool first = true;
52        for ( const auto & i : open ) {
53                if ( first ) { first = false; } else { out << ' '; }
54                out << i.first.typeString() << "(" << i.second << ")";
55        }
56}
57
58void print( std::ostream & out, const EqvClass & clz, Indenter indent ) {
59        out << "(";
60        bool first = true;
61        for(const auto & var : clz.vars) {
62                if(first) first = false;
63                else out << " ";
64
65                if( deterministic_output ) out << "[unbound]";
66                else out << "_" << var.formal_usage << "_" << var.expr_id << "_";
67
68                out << var.base->name;
69        }
70        out << ")";
71
72        if ( clz.bound ) {
73                out << " -> ";
74                print( out, clz.bound, indent+1 );
75        }
76
77        if ( ! clz.allowWidening ) {
78                out << " (no widening)";
79        }
80
81        out << std::endl;
82}
83
84const EqvClass * TypeEnvironment::lookup( const TypeInstType::TypeEnvKey & var ) const {
85        for ( ClassList::const_iterator i = env.begin(); i != env.end(); ++i ) {
86                if ( i->vars.find( var ) != i->vars.end() ) return &*i;
87        }
88        return nullptr;
89}
90
91namespace {
92        /// Removes any class from env that intersects eqvClass
93        void filterOverlappingClasses( std::list<EqvClass> & env, const EqvClass & eqvClass ) {
94                auto i = env.begin();
95                while ( i != env.end() ) {
96                        auto next = i; ++next;  // save next node in case of erasure
97
98                        for ( const auto & v : eqvClass.vars ) {
99                                if ( i->vars.count( v ) ) {
100                                        env.erase( i );  // remove overlapping class
101                                        break;           // done with this class
102                                }
103                        }
104
105                        i = next;  // go to next node even if this removed
106                }
107        }
108}
109
110void TypeEnvironment::add( const FunctionType::ForallList & tyDecls ) {
111        for ( auto & tyDecl : tyDecls ) {
112                env.emplace_back( tyDecl );
113        }
114}
115
116void TypeEnvironment::add( const TypeSubstitution & sub ) {
117        for ( const auto p : sub ) {
118                add( EqvClass{ p.first, p.second } );
119        }
120}
121
122void TypeEnvironment::writeToSubstitution( TypeSubstitution & sub ) const {
123        for ( const auto & clz : env ) {
124                TypeInstType::TypeEnvKey clzRep;
125                bool first = true;
126                for ( const auto & var : clz.vars ) {
127                        if ( clz.bound ) {
128                                sub.add( var, clz.bound );
129                        } else if ( first ) {
130                                clzRep = var;
131                                first = false;
132                        } else {
133                                sub.add( var, new TypeInstType{ clzRep } );
134                        }
135                }
136        }
137        sub.normalize();
138}
139
140void TypeEnvironment::simpleCombine( const TypeEnvironment & o ) {
141        env.insert( env.end(), o.env.begin(), o.env.end() );
142}
143
144namespace {
145        /// Implements occurs check by traversing type
146        struct Occurs : public ast::WithVisitorRef<Occurs> {
147                bool result;
148                std::unordered_set< TypeInstType::TypeEnvKey > vars;
149                const TypeEnvironment & tenv;
150
151                Occurs( const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env )
152                : result( false ), vars(), tenv( env ) {
153                        if ( const EqvClass * clz = tenv.lookup( var ) ) {
154                                vars = clz->vars;
155                        } else {
156                                vars.emplace( var );
157                        }
158                }
159
160                void previsit( const TypeInstType * typeInst ) {
161                        if ( vars.count( *typeInst ) ) {
162                                result = true;
163                        } else if ( const EqvClass * clz = tenv.lookup( *typeInst ) ) {
164                                if ( clz->bound ) {
165                                        clz->bound->accept( *visitor );
166                                }
167                        }
168                }
169        };
170
171        /// true if `var` occurs in `ty` under `env`
172        bool occurs( const Type * ty, const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env ) {
173                Pass<Occurs> occur{ var, env };
174                maybe_accept( ty, occur );
175                return occur.core.result;
176        }
177}
178
179bool TypeEnvironment::combine(
180                const TypeEnvironment & o, OpenVarSet & open, const SymbolTable & symtab ) {
181        // short-circuit easy cases
182        if ( o.empty() ) return true;
183        if ( empty() ) {
184                simpleCombine( o );
185                return true;
186        }
187
188        // merge classes
189        for ( const EqvClass & c : o.env ) {
190                // index of typeclass in local environment bound to c
191                auto rt = env.end();
192
193                // look for first existing bound variable
194                auto vt = c.vars.begin();
195                for ( ; vt != c.vars.end(); ++vt ) {
196                        rt = internal_lookup( *vt );
197                        if ( rt != env.end() ) break;
198                }
199
200                if ( rt != env.end() ) {  // c needs to be merged into *rt
201                        EqvClass & r = *rt;
202                        // merge bindings
203                        if ( ! mergeBound( r, c, open, symtab ) ) return false;
204                        // merge previous unbound variables into this class, checking occurs if needed
205                        if ( r.bound ) for ( const auto & u : c.vars ) {
206                                if ( occurs( r.bound, u, *this ) ) return false;
207                                r.vars.emplace( u );
208                        } else { r.vars.insert( c.vars.begin(), vt ); }
209                        // merge subsequent variables into this class (skipping *vt, already there)
210                        while ( ++vt != c.vars.end() ) {
211                                auto st = internal_lookup( *vt );
212                                if ( st == env.end() ) {
213                                        // unbound, safe to add if occurs
214                                        if ( r.bound && occurs( r.bound, *vt, *this ) ) return false;
215                                        r.vars.emplace( *vt );
216                                } else if ( st != rt ) {
217                                        // bound, but not to the same class
218                                        if ( ! mergeClasses( rt, st, open, symtab ) ) return false;
219                                }       // ignore bound into the same class
220                        }
221                } else {  // no variables in c bound; just copy up
222                        env.emplace_back( c );
223                }
224        }
225
226        // merged all classes
227        return true;
228}
229
230void TypeEnvironment::extractOpenVars( OpenVarSet & open ) const {
231        for ( const auto & clz : env ) {
232                for ( const auto & var : clz.vars ) {
233                        open[ var ] = clz.data;
234                }
235        }
236}
237
238void TypeEnvironment::addActual( const TypeEnvironment & actualEnv, OpenVarSet & open ) {
239        for ( const auto & clz : actualEnv ) {
240                EqvClass c = clz;
241                c.allowWidening = false;
242                for ( const auto & var : c.vars ) {
243                        open[ var ] = c.data;
244                }
245                env.emplace_back( std::move(c) );
246        }
247}
248
249/// true if a type is a function type
250bool isFtype( const Type * type ) {
251        if ( dynamic_cast< const FunctionType * >( type ) ) {
252                return true;
253        } else if ( auto typeInst = dynamic_cast< const TypeInstType * >( type ) ) {
254                return typeInst->kind == TypeDecl::Ftype;
255        } else return false;
256}
257
258namespace {
259        /// true if the given type can be bound to the given type variable
260        bool tyVarCompatible( const TypeDecl::Data & data, const Type * type ) {
261                switch ( data.kind ) {
262                  case TypeDecl::Dtype:
263                        // to bind to an object type variable, the type must not be a function type.
264                        // if the type variable is specified to be a complete type then the incoming
265                        // type must also be complete
266                        // xxx - should this also check that type is not a tuple type and that it's not a ttype?
267                        return ! isFtype( type ) && ( ! data.isComplete || type->isComplete() );
268                  case TypeDecl::Ftype:
269                        return isFtype( type );
270                  case TypeDecl::Ttype:
271                        // ttype unifies with any tuple type
272                        return dynamic_cast< const TupleType * >( type ) || Tuples::isTtype( type );
273                  default:
274                        assertf(false, "Unhandled tyvar kind: %d", data.kind);
275                        return false;
276                }
277        }
278}
279
280bool TypeEnvironment::bindVar(
281                const TypeInstType * typeInst, const Type * bindTo, const TypeDecl::Data & data,
282                AssertionSet & need, AssertionSet & have, const OpenVarSet & open, WidenMode widen,
283                const SymbolTable & symtab
284) {
285        // remove references from bound type, so that type variables can only bind to value types
286        ptr<Type> target = bindTo->stripReferences();
287        auto tyvar = open.find( *typeInst );
288        assert( tyvar != open.end() );
289        if ( ! tyVarCompatible( tyvar->second, target ) ) return false;
290        if ( occurs( target, *typeInst, *this ) ) return false;
291
292        auto it = internal_lookup( *typeInst );
293        if ( it != env.end() ) {
294                if ( it->bound ) {
295                        // attempt to unify equivalence class type with type to bind to.
296                        // equivalence class type has stripped qualifiers which must be restored
297                        ptr<Type> common;
298                        ptr<Type> newType = it->bound;
299                        reset_qualifiers( newType, typeInst->qualifiers );
300                        if ( unifyInexact(
301                                        newType, target, *this, need, have, open,
302                                        widen & WidenMode{ it->allowWidening, true }, symtab, common ) ) {
303                                if ( common ) {
304                                        it->bound = std::move(common);
305                                        reset_qualifiers( it->bound );
306                                }
307                        } else return false;
308                } else {
309                        it->bound = std::move(target);
310                        reset_qualifiers( it->bound );
311                        it->allowWidening = widen.first && widen.second;
312                }
313        } else {
314                env.emplace_back(
315                        *typeInst, target, widen.first && widen.second, data );
316        }
317        return true;
318}
319
320bool TypeEnvironment::bindVarToVar(
321                const TypeInstType * var1, const TypeInstType * var2, TypeDecl::Data && data,
322                AssertionSet & need, AssertionSet & have, const OpenVarSet & open,
323                WidenMode widen, const SymbolTable & symtab
324) {
325        auto c1 = internal_lookup( *var1 );
326        auto c2 = internal_lookup( *var2 );
327
328        // exit early if variables already bound together
329        if ( c1 != env.end() && c1 == c2 ) {
330                c1->allowWidening &= widen;
331                return true;
332        }
333
334        bool widen1 = false, widen2 = false;
335        const Type * type1 = nullptr, * type2 = nullptr;
336
337        // check for existing bindings, perform occurs check
338        if ( c1 != env.end() ) {
339                if ( c1->bound ) {
340                        if ( occurs( c1->bound, *var2, *this ) ) return false;
341                        type1 = c1->bound;
342                }
343                widen1 = widen.first && c1->allowWidening;
344        }
345        if ( c2 != env.end() ) {
346                if ( c2->bound ) {
347                        if ( occurs( c2->bound, *var1, *this ) ) return false;
348                        type2 = c2->bound;
349                }
350                widen2 = widen.second && c2->allowWidening;
351        }
352
353        if ( type1 && type2 ) {
354                // both classes bound, merge if bound types can be unified
355                ptr<Type> newType1{ type1 }, newType2{ type2 };
356                WidenMode newWidenMode{ widen1, widen2 };
357                ptr<Type> common;
358
359                if ( unifyInexact(
360                                newType1, newType2, *this, need, have, open, newWidenMode, symtab, common ) ) {
361                        c1->vars.insert( c2->vars.begin(), c2->vars.end() );
362                        c1->allowWidening = widen1 && widen2;
363                        if ( common ) {
364                                c1->bound = std::move(common);
365                                reset_qualifiers( c1->bound );
366                        }
367                        c1->data.isComplete |= data.isComplete;
368                        env.erase( c2 );
369                } else return false;
370        } else if ( c1 != env.end() && c2 != env.end() ) {
371                // both classes exist, at least one unbound, merge unconditionally
372                if ( type1 ) {
373                        c1->vars.insert( c2->vars.begin(), c2->vars.end() );
374                        c1->allowWidening = widen1;
375                        c1->data.isComplete |= data.isComplete;
376                        env.erase( c2 );
377                } else {
378                        c2->vars.insert( c1->vars.begin(), c1->vars.end() );
379                        c2->allowWidening = widen2;
380                        c2->data.isComplete |= data.isComplete;
381                        env.erase( c1 );
382                }
383        } else if ( c1 != env.end() ) {
384                // var2 unbound, add to env[c1]
385                c1->vars.emplace( *var2 );
386                c1->allowWidening = widen1;
387                c1->data.isComplete |= data.isComplete;
388        } else if ( c2 != env.end() ) {
389                // var1 unbound, add to env[c2]
390                c2->vars.emplace( *var1 );
391                c2->allowWidening = widen2;
392                c2->data.isComplete |= data.isComplete;
393        } else {
394                // neither var bound, create new class
395                env.emplace_back( *var1, *var2, widen1 && widen2, data );
396        }
397
398        return true;
399}
400
401void TypeEnvironment::forbidWidening() {
402        for ( EqvClass& c : env ) c.allowWidening = false;
403}
404
405void TypeEnvironment::add( EqvClass && eqvClass ) {
406        filterOverlappingClasses( env, eqvClass );
407        env.emplace_back( std::move(eqvClass) );
408}
409
410bool TypeEnvironment::mergeBound(
411                EqvClass & to, const EqvClass & from, OpenVarSet & open, const SymbolTable & symtab ) {
412        if ( from.bound ) {
413                if ( to.bound ) {
414                        // attempt to unify bound types
415                        ptr<Type> toType{ to.bound }, fromType{ from.bound };
416                        WidenMode widen{ to.allowWidening, from.allowWidening };
417                        ptr<Type> common;
418                        AssertionSet need, have;
419
420                        if ( unifyInexact(
421                                        toType, fromType, *this, need, have, open, widen, symtab, common ) ) {
422                                // unifies, set common type if necessary
423                                if ( common ) {
424                                        to.bound = std::move(common);
425                                        reset_qualifiers( to.bound );
426                                }
427                        } else return false; // cannot unify
428                } else {
429                        to.bound = from.bound;
430                }
431        }
432
433        // unify widening if matches
434        to.allowWidening &= from.allowWidening;
435        return true;
436}
437
438bool TypeEnvironment::mergeClasses(
439        ClassList::iterator to, ClassList::iterator from, OpenVarSet & open, const SymbolTable & symtab
440) {
441        EqvClass & r = *to, & s = *from;
442
443        // ensure bounds match
444        if ( ! mergeBound( r, s, open, symtab ) ) return false;
445
446        // check safely bindable
447        if ( r.bound ) {
448                for ( const auto & v : s.vars ) if ( occurs( r.bound, v, *this ) ) return false;
449        }
450
451        // merge classes
452        r.vars.insert( s.vars.begin(), s.vars.end() );
453        r.allowWidening &= s.allowWidening;
454        env.erase( from );
455
456        return true;
457}
458
459TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const TypeInstType::TypeEnvKey & var ) {
460        for ( ClassList::iterator i = env.begin(); i != env.end(); ++i ) {
461                if ( i->vars.count( var ) ) return i;
462        }
463        return env.end();
464}
465
466void print( std::ostream & out, const TypeEnvironment & env, Indenter indent ) {
467        for ( const auto & clz : env ) {
468                print( out, clz, indent );
469        }
470}
471
472std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env ) {
473        print( out, env );
474        return out;
475}
476
477}
478
479// Local Variables: //
480// tab-width: 4 //
481// mode: c++ //
482// compile-command: "make install" //
483// End: //
Note: See TracBrowser for help on using the repository browser.