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
|
---|
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 | dest.vars = src.vars;
|
---|
47 | dest.type = maybeClone( src.type );
|
---|
48 | dest.allowWidening = src.allowWidening;
|
---|
49 | dest.data = src.data;
|
---|
50 | }
|
---|
51 |
|
---|
52 | EqvClass::EqvClass() : type( 0 ), allowWidening( true ) {
|
---|
53 | }
|
---|
54 |
|
---|
55 | EqvClass::EqvClass( const EqvClass &other ) {
|
---|
56 | initialize( other, *this );
|
---|
57 | }
|
---|
58 |
|
---|
59 | EqvClass &EqvClass::operator=( const EqvClass &other ) {
|
---|
60 | if ( this == &other ) return *this;
|
---|
61 | delete type;
|
---|
62 | initialize( other, *this );
|
---|
63 | return *this;
|
---|
64 | }
|
---|
65 |
|
---|
66 | EqvClass::~EqvClass() {
|
---|
67 | delete type;
|
---|
68 | }
|
---|
69 |
|
---|
70 | void EqvClass::print( std::ostream &os, Indenter indent ) const {
|
---|
71 | os << "( ";
|
---|
72 | std::copy( vars.begin(), vars.end(), std::ostream_iterator< std::string >( os, " " ) );
|
---|
73 | os << ")";
|
---|
74 | if ( type ) {
|
---|
75 | os << " -> ";
|
---|
76 | type->print( os, indent+1 );
|
---|
77 | } // if
|
---|
78 | if ( ! allowWidening ) {
|
---|
79 | os << " (no widening)";
|
---|
80 | } // if
|
---|
81 | os << std::endl;
|
---|
82 | }
|
---|
83 |
|
---|
84 | bool TypeEnvironment::lookup( const std::string &var, EqvClass &eqvClass ) const {
|
---|
85 | for ( std::list< EqvClass >::const_iterator i = env.begin(); i != env.end(); ++i ) {
|
---|
86 | if ( i->vars.find( var ) != i->vars.end() ) {
|
---|
87 | /// std::cout << var << " is in class ";
|
---|
88 | /// i->print( std::cout );
|
---|
89 | eqvClass = *i;
|
---|
90 | return true;
|
---|
91 | }
|
---|
92 | /// std::cout << var << " is not in class ";
|
---|
93 | /// i->print( std::cout );
|
---|
94 | } // for
|
---|
95 | return false;
|
---|
96 | }
|
---|
97 |
|
---|
98 | void TypeEnvironment::add( const EqvClass &eqvClass ) {
|
---|
99 | std::list< EqvClass >::iterator i = env.begin();
|
---|
100 | while ( i != env.end() ) {
|
---|
101 | std::list< EqvClass >::iterator next = i;
|
---|
102 | next++;
|
---|
103 | std::set< std::string > intersection;
|
---|
104 | std::set_intersection( i->vars.begin(), i->vars.end(), eqvClass.vars.begin(), eqvClass.vars.end(), std::inserter( intersection, intersection.begin() ) );
|
---|
105 | if ( ! intersection.empty() ) {
|
---|
106 | env.erase( i );
|
---|
107 | } // if
|
---|
108 | i = next;
|
---|
109 | } // while
|
---|
110 | env.insert( env.end(), eqvClass );
|
---|
111 | }
|
---|
112 |
|
---|
113 | void TypeEnvironment::add( const Type::ForallList &tyDecls ) {
|
---|
114 | for ( Type::ForallList::const_iterator i = tyDecls.begin(); i != tyDecls.end(); ++i ) {
|
---|
115 | EqvClass newClass;
|
---|
116 | newClass.vars.insert( (*i)->get_name() );
|
---|
117 | newClass.data = TypeDecl::Data{ (*i) };
|
---|
118 | env.push_back( newClass );
|
---|
119 | } // for
|
---|
120 | }
|
---|
121 |
|
---|
122 | void TypeEnvironment::makeSubstitution( TypeSubstitution &sub ) const {
|
---|
123 | for ( std::list< EqvClass >::const_iterator theClass = env.begin(); theClass != env.end(); ++theClass ) {
|
---|
124 | for ( std::set< std::string >::const_iterator theVar = theClass->vars.begin(); theVar != theClass->vars.end(); ++theVar ) {
|
---|
125 | /// std::cerr << "adding " << *theVar;
|
---|
126 | if ( theClass->type ) {
|
---|
127 | /// std::cerr << " bound to ";
|
---|
128 | /// theClass->type->print( std::cerr );
|
---|
129 | /// std::cerr << std::endl;
|
---|
130 | sub.add( *theVar, theClass->type );
|
---|
131 | } else if ( theVar != theClass->vars.begin() ) {
|
---|
132 | TypeInstType *newTypeInst = new TypeInstType( Type::Qualifiers(), *theClass->vars.begin(), theClass->data.kind == TypeDecl::Ftype );
|
---|
133 | /// std::cerr << " bound to variable " << *theClass->vars.begin() << std::endl;
|
---|
134 | sub.add( *theVar, newTypeInst );
|
---|
135 | delete newTypeInst;
|
---|
136 | } // if
|
---|
137 | } // for
|
---|
138 | } // for
|
---|
139 | /// std::cerr << "input env is:" << std::endl;
|
---|
140 | /// print( std::cerr, 8 );
|
---|
141 | /// std::cerr << "sub is:" << std::endl;
|
---|
142 | /// sub.print( std::cerr, 8 );
|
---|
143 | sub.normalize();
|
---|
144 | }
|
---|
145 |
|
---|
146 | void TypeEnvironment::print( std::ostream &os, Indenter indent ) const {
|
---|
147 | for ( std::list< EqvClass >::const_iterator i = env.begin(); i != env.end(); ++i ) {
|
---|
148 | i->print( os, indent );
|
---|
149 | } // for
|
---|
150 | }
|
---|
151 |
|
---|
152 | std::list< EqvClass >::iterator TypeEnvironment::internal_lookup( const std::string &var ) {
|
---|
153 | for ( std::list< EqvClass >::iterator i = env.begin(); i != env.end(); ++i ) {
|
---|
154 | if ( i->vars.find( var ) == i->vars.end() ) {
|
---|
155 | return i;
|
---|
156 | } // if
|
---|
157 | } // for
|
---|
158 | return env.end();
|
---|
159 | }
|
---|
160 |
|
---|
161 | void TypeEnvironment::simpleCombine( const TypeEnvironment &second ) {
|
---|
162 | env.insert( env.end(), second.env.begin(), second.env.end() );
|
---|
163 | }
|
---|
164 |
|
---|
165 | void TypeEnvironment::combine( const TypeEnvironment &second, Type *(*combineFunc)( Type*, Type* ) ) {
|
---|
166 | TypeEnvironment secondCopy( second );
|
---|
167 | for ( std::list< EqvClass >::iterator firstClass = env.begin(); firstClass != env.end(); ++firstClass ) {
|
---|
168 | EqvClass &newClass = *firstClass;
|
---|
169 | std::set< std::string > newVars;
|
---|
170 | for ( std::set< std::string >::const_iterator var = firstClass->vars.begin(); var != firstClass->vars.end(); ++var ) {
|
---|
171 | std::list< EqvClass >::iterator secondClass = secondCopy.internal_lookup( *var );
|
---|
172 | if ( secondClass != secondCopy.env.end() ) {
|
---|
173 | newVars.insert( secondClass->vars.begin(), secondClass->vars.end() );
|
---|
174 | if ( secondClass->type ) {
|
---|
175 | if ( newClass.type ) {
|
---|
176 | Type *newType = combineFunc( newClass.type, secondClass->type );
|
---|
177 | delete newClass.type;
|
---|
178 | newClass.type = newType;
|
---|
179 | newClass.allowWidening = newClass.allowWidening && secondClass->allowWidening;
|
---|
180 | } else {
|
---|
181 | newClass.type = secondClass->type->clone();
|
---|
182 | newClass.allowWidening = secondClass->allowWidening;
|
---|
183 | } // if
|
---|
184 | } // if
|
---|
185 | secondCopy.env.erase( secondClass );
|
---|
186 | } // if
|
---|
187 | } // for
|
---|
188 | newClass.vars.insert( newVars.begin(), newVars.end() );
|
---|
189 | } // for
|
---|
190 | for ( std::list< EqvClass >::iterator secondClass = secondCopy.env.begin(); secondClass != secondCopy.env.end(); ++secondClass ) {
|
---|
191 | env.push_back( *secondClass );
|
---|
192 | } // for
|
---|
193 | }
|
---|
194 |
|
---|
195 | void TypeEnvironment::extractOpenVars( OpenVarSet &openVars ) const {
|
---|
196 | for ( std::list< EqvClass >::const_iterator eqvClass = env.begin(); eqvClass != env.end(); ++eqvClass ) {
|
---|
197 | for ( std::set< std::string >::const_iterator var = eqvClass->vars.begin(); var != eqvClass->vars.end(); ++var ) {
|
---|
198 | openVars[ *var ] = eqvClass->data;
|
---|
199 | } // for
|
---|
200 | } // for
|
---|
201 | }
|
---|
202 |
|
---|
203 | void TypeEnvironment::addActual( const TypeEnvironment& actualEnv, OpenVarSet& openVars ) {
|
---|
204 | for ( const EqvClass& c : actualEnv ) {
|
---|
205 | EqvClass c2 = c;
|
---|
206 | c2.allowWidening = false;
|
---|
207 | for ( const std::string& var : c2.vars ) {
|
---|
208 | openVars[ var ] = c2.data;
|
---|
209 | }
|
---|
210 | env.push_back( std::move(c2) );
|
---|
211 | }
|
---|
212 | }
|
---|
213 |
|
---|
214 | std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env ) {
|
---|
215 | env.print( out );
|
---|
216 | return out;
|
---|
217 | }
|
---|
218 | } // namespace ResolvExpr
|
---|
219 |
|
---|
220 | // Local Variables: //
|
---|
221 | // tab-width: 4 //
|
---|
222 | // mode: c++ //
|
---|
223 | // compile-command: "make install" //
|
---|
224 | // End: //
|
---|