| 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: //
 | 
|---|