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/utility.h" // for maybeClone
|
---|
22 | #include "SynTree/Type.h" // for Type, FunctionType, Type::Fora...
|
---|
23 | #include "SynTree/TypeSubstitution.h" // for TypeSubstitution
|
---|
24 | #include "TypeEnvironment.h"
|
---|
25 |
|
---|
26 | namespace ResolvExpr {
|
---|
27 | void printAssertionSet( const AssertionSet &assertions, std::ostream &os, int indent ) {
|
---|
28 | for ( AssertionSet::const_iterator i = assertions.begin(); i != assertions.end(); ++i ) {
|
---|
29 | i->first->print( os, indent );
|
---|
30 | if ( i->second.isUsed ) {
|
---|
31 | os << "(used)";
|
---|
32 | } else {
|
---|
33 | os << "(not used)";
|
---|
34 | } // if
|
---|
35 | } // for
|
---|
36 | }
|
---|
37 |
|
---|
38 | void printOpenVarSet( const OpenVarSet &openVars, std::ostream &os, int indent ) {
|
---|
39 | os << std::string( indent, ' ' );
|
---|
40 | for ( OpenVarSet::const_iterator i = openVars.begin(); i != openVars.end(); ++i ) {
|
---|
41 | os << i->first << "(" << i->second << ") ";
|
---|
42 | } // for
|
---|
43 | }
|
---|
44 |
|
---|
45 | void EqvClass::initialize( const EqvClass &src, EqvClass &dest ) {
|
---|
46 | initialize( src, dest, src.type );
|
---|
47 | }
|
---|
48 |
|
---|
49 | void EqvClass::initialize( const EqvClass &src, EqvClass &dest, const Type *ty ) {
|
---|
50 | dest.vars = src.vars;
|
---|
51 | dest.type = maybeClone( ty );
|
---|
52 | dest.allowWidening = src.allowWidening;
|
---|
53 | dest.data = src.data;
|
---|
54 | }
|
---|
55 |
|
---|
56 | EqvClass::EqvClass() : type( nullptr ), allowWidening( true ) {
|
---|
57 | }
|
---|
58 |
|
---|
59 | EqvClass::EqvClass( const EqvClass &other ) {
|
---|
60 | initialize( other, *this );
|
---|
61 | }
|
---|
62 |
|
---|
63 | EqvClass::EqvClass( const EqvClass &other, const Type *ty ) {
|
---|
64 | initialize( other, *this, ty );
|
---|
65 | }
|
---|
66 |
|
---|
67 | EqvClass &EqvClass::operator=( const EqvClass &other ) {
|
---|
68 | if ( this == &other ) return *this;
|
---|
69 | delete type;
|
---|
70 | initialize( other, *this );
|
---|
71 | return *this;
|
---|
72 | }
|
---|
73 |
|
---|
74 | EqvClass::~EqvClass() {
|
---|
75 | delete type;
|
---|
76 | }
|
---|
77 |
|
---|
78 | void EqvClass::print( std::ostream &os, Indenter indent ) const {
|
---|
79 | os << "( ";
|
---|
80 | std::copy( vars.begin(), vars.end(), std::ostream_iterator< std::string >( os, " " ) );
|
---|
81 | os << ")";
|
---|
82 | if ( type ) {
|
---|
83 | os << " -> ";
|
---|
84 | type->print( os, indent+1 );
|
---|
85 | } // if
|
---|
86 | if ( ! allowWidening ) {
|
---|
87 | os << " (no widening)";
|
---|
88 | } // if
|
---|
89 | os << std::endl;
|
---|
90 | }
|
---|
91 |
|
---|
92 | const EqvClass* TypeEnvironment::lookup( const std::string &var ) const {
|
---|
93 | for ( std::list< EqvClass >::const_iterator i = env.begin(); i != env.end(); ++i ) {
|
---|
94 | if ( i->vars.find( var ) != i->vars.end() ) {
|
---|
95 | /// std::cout << var << " is in class ";
|
---|
96 | /// i->print( std::cout );
|
---|
97 | return &*i;
|
---|
98 | }
|
---|
99 | /// std::cout << var << " is not in class ";
|
---|
100 | /// i->print( std::cout );
|
---|
101 | } // for
|
---|
102 | return nullptr;
|
---|
103 | }
|
---|
104 |
|
---|
105 | /// Removes any class from env that intersects eqvClass
|
---|
106 | void filterOverlappingClasses( std::list<EqvClass> &env, const EqvClass &eqvClass ) {
|
---|
107 | for ( auto i = env.begin(); i != env.end(); ) {
|
---|
108 | auto next = i;
|
---|
109 | ++next;
|
---|
110 | std::set<std::string> intersection;
|
---|
111 | std::set_intersection( i->vars.begin(), i->vars.end(), eqvClass.vars.begin(), eqvClass.vars.end(),
|
---|
112 | std::inserter( intersection, intersection.begin() ) );
|
---|
113 | if ( ! intersection.empty() ) { env.erase( i ); }
|
---|
114 | i = next;
|
---|
115 | }
|
---|
116 | }
|
---|
117 |
|
---|
118 | void TypeEnvironment::add( const EqvClass &eqvClass ) {
|
---|
119 | filterOverlappingClasses( env, eqvClass );
|
---|
120 | env.push_back( eqvClass );
|
---|
121 | }
|
---|
122 |
|
---|
123 | void TypeEnvironment::add( EqvClass &&eqvClass ) {
|
---|
124 | filterOverlappingClasses( env, eqvClass );
|
---|
125 | env.push_back( std::move(eqvClass) );
|
---|
126 | }
|
---|
127 |
|
---|
128 | void TypeEnvironment::add( const Type::ForallList &tyDecls ) {
|
---|
129 | for ( Type::ForallList::const_iterator i = tyDecls.begin(); i != tyDecls.end(); ++i ) {
|
---|
130 | EqvClass newClass;
|
---|
131 | newClass.vars.insert( (*i)->get_name() );
|
---|
132 | newClass.data = TypeDecl::Data{ (*i) };
|
---|
133 | env.push_back( newClass );
|
---|
134 | } // for
|
---|
135 | }
|
---|
136 |
|
---|
137 | void TypeEnvironment::add( const TypeSubstitution & sub ) {
|
---|
138 | EqvClass newClass;
|
---|
139 | for ( auto p : sub ) {
|
---|
140 | newClass.vars.insert( p.first );
|
---|
141 | newClass.type = p.second->clone();
|
---|
142 | newClass.allowWidening = false;
|
---|
143 | // Minimal assumptions. Not technically correct, but might be good enough, and
|
---|
144 | // is the best we can do at the moment since information is lost in the
|
---|
145 | // transition to TypeSubstitution
|
---|
146 | newClass.data = TypeDecl::Data{ TypeDecl::Dtype, false };
|
---|
147 | add( newClass );
|
---|
148 | }
|
---|
149 | }
|
---|
150 |
|
---|
151 | void TypeEnvironment::makeSubstitution( TypeSubstitution &sub ) const {
|
---|
152 | for ( std::list< EqvClass >::const_iterator theClass = env.begin(); theClass != env.end(); ++theClass ) {
|
---|
153 | for ( std::set< std::string >::const_iterator theVar = theClass->vars.begin(); theVar != theClass->vars.end(); ++theVar ) {
|
---|
154 | /// std::cerr << "adding " << *theVar;
|
---|
155 | if ( theClass->type ) {
|
---|
156 | /// std::cerr << " bound to ";
|
---|
157 | /// theClass->type->print( std::cerr );
|
---|
158 | /// std::cerr << std::endl;
|
---|
159 | sub.add( *theVar, theClass->type );
|
---|
160 | } else if ( theVar != theClass->vars.begin() ) {
|
---|
161 | TypeInstType *newTypeInst = new TypeInstType( Type::Qualifiers(), *theClass->vars.begin(), theClass->data.kind == TypeDecl::Ftype );
|
---|
162 | /// std::cerr << " bound to variable " << *theClass->vars.begin() << std::endl;
|
---|
163 | sub.add( *theVar, newTypeInst );
|
---|
164 | delete newTypeInst;
|
---|
165 | } // if
|
---|
166 | } // for
|
---|
167 | } // for
|
---|
168 | /// std::cerr << "input env is:" << std::endl;
|
---|
169 | /// print( std::cerr, 8 );
|
---|
170 | /// std::cerr << "sub is:" << std::endl;
|
---|
171 | /// sub.print( std::cerr, 8 );
|
---|
172 | sub.normalize();
|
---|
173 | }
|
---|
174 |
|
---|
175 | void TypeEnvironment::print( std::ostream &os, Indenter indent ) const {
|
---|
176 | for ( const EqvClass & theClass : env ) {
|
---|
177 | theClass.print( os, indent );
|
---|
178 | } // for
|
---|
179 | }
|
---|
180 |
|
---|
181 | std::list< EqvClass >::iterator TypeEnvironment::internal_lookup( const std::string &var ) {
|
---|
182 | for ( std::list< EqvClass >::iterator i = env.begin(); i != env.end(); ++i ) {
|
---|
183 | if ( i->vars.find( var ) == i->vars.end() ) {
|
---|
184 | return i;
|
---|
185 | } // if
|
---|
186 | } // for
|
---|
187 | return env.end();
|
---|
188 | }
|
---|
189 |
|
---|
190 | void TypeEnvironment::simpleCombine( const TypeEnvironment &second ) {
|
---|
191 | env.insert( env.end(), second.env.begin(), second.env.end() );
|
---|
192 | }
|
---|
193 |
|
---|
194 | void TypeEnvironment::combine( const TypeEnvironment &second, Type *(*combineFunc)( Type*, Type* ) ) {
|
---|
195 | TypeEnvironment secondCopy( second );
|
---|
196 | for ( std::list< EqvClass >::iterator firstClass = env.begin(); firstClass != env.end(); ++firstClass ) {
|
---|
197 | EqvClass &newClass = *firstClass;
|
---|
198 | std::set< std::string > newVars;
|
---|
199 | for ( std::set< std::string >::const_iterator var = firstClass->vars.begin(); var != firstClass->vars.end(); ++var ) {
|
---|
200 | std::list< EqvClass >::iterator secondClass = secondCopy.internal_lookup( *var );
|
---|
201 | if ( secondClass != secondCopy.env.end() ) {
|
---|
202 | newVars.insert( secondClass->vars.begin(), secondClass->vars.end() );
|
---|
203 | if ( secondClass->type ) {
|
---|
204 | if ( newClass.type ) {
|
---|
205 | Type *newType = combineFunc( newClass.type, secondClass->type );
|
---|
206 | delete newClass.type;
|
---|
207 | newClass.type = newType;
|
---|
208 | newClass.allowWidening = newClass.allowWidening && secondClass->allowWidening;
|
---|
209 | } else {
|
---|
210 | newClass.type = secondClass->type->clone();
|
---|
211 | newClass.allowWidening = secondClass->allowWidening;
|
---|
212 | } // if
|
---|
213 | } // if
|
---|
214 | secondCopy.env.erase( secondClass );
|
---|
215 | } // if
|
---|
216 | } // for
|
---|
217 | newClass.vars.insert( newVars.begin(), newVars.end() );
|
---|
218 | } // for
|
---|
219 | for ( std::list< EqvClass >::iterator secondClass = secondCopy.env.begin(); secondClass != secondCopy.env.end(); ++secondClass ) {
|
---|
220 | env.push_back( *secondClass );
|
---|
221 | } // for
|
---|
222 | }
|
---|
223 |
|
---|
224 | void TypeEnvironment::extractOpenVars( OpenVarSet &openVars ) const {
|
---|
225 | for ( std::list< EqvClass >::const_iterator eqvClass = env.begin(); eqvClass != env.end(); ++eqvClass ) {
|
---|
226 | for ( std::set< std::string >::const_iterator var = eqvClass->vars.begin(); var != eqvClass->vars.end(); ++var ) {
|
---|
227 | openVars[ *var ] = eqvClass->data;
|
---|
228 | } // for
|
---|
229 | } // for
|
---|
230 | }
|
---|
231 |
|
---|
232 | void TypeEnvironment::addActual( const TypeEnvironment& actualEnv, OpenVarSet& openVars ) {
|
---|
233 | for ( const EqvClass& c : actualEnv ) {
|
---|
234 | EqvClass c2 = c;
|
---|
235 | c2.allowWidening = false;
|
---|
236 | for ( const std::string& var : c2.vars ) {
|
---|
237 | openVars[ var ] = c2.data;
|
---|
238 | }
|
---|
239 | env.push_back( std::move(c2) );
|
---|
240 | }
|
---|
241 | }
|
---|
242 |
|
---|
243 | std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env ) {
|
---|
244 | env.print( out );
|
---|
245 | return out;
|
---|
246 | }
|
---|
247 | } // namespace ResolvExpr
|
---|
248 |
|
---|
249 | // Local Variables: //
|
---|
250 | // tab-width: 4 //
|
---|
251 | // mode: c++ //
|
---|
252 | // compile-command: "make install" //
|
---|
253 | // End: //
|
---|