Ignore:
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ResolvExpr/RenameVars.cc

    r4e13e2a rf5edcb4  
    1919#include <utility>                 // for pair
    2020
    21 #include "AST/ForallSubstitutionTable.hpp"
    2221#include "AST/Pass.hpp"
    2322#include "AST/Type.hpp"
     
    3130#include "SynTree/Visitor.h"       // for acceptAll, maybeAccept
    3231
    33 #include "AST/Copy.hpp"
    34 
    3532namespace ResolvExpr {
    3633
     
    4037                int resetCount = 0;
    4138                ScopedMap< std::string, std::string > nameMap;
     39
    4240        public:
    43                 ast::ForallSubstitutionTable subs;
    44 
    4541                void reset() {
    4642                        level = 0;
     
    4844                }
    4945
     46                using mapConstIterator = ScopedMap< std::string, std::string >::const_iterator;
     47
    5048                void rename( TypeInstType * type ) {
    51                         auto it = nameMap.find( type->name );
     49                        mapConstIterator it = nameMap.find( type->name );
    5250                        if ( it != nameMap.end() ) {
    5351                                type->name = it->second;
     
    6765                                        // ditto for assertion names, the next level in
    6866                                        level++;
    69                                 }
    70                         }
     67                                        // acceptAll( td->assertions, *this );
     68                                } // for
     69                        } // if
    7170                }
    7271
     
    7877
    7978                const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
    80                         // re-linking of base type handled by WithForallSubstitutor
    81 
    82                         // rename
    83                         auto it = nameMap.find( type->name );
     79                        mapConstIterator it = nameMap.find( type->name );
    8480                        if ( it != nameMap.end() ) {
    85                                 // unconditionally mutate because map will *always* have different name,
    86                                 // if this mutates, will *always* have been mutated by ForallSubstitutor above
    87                                 ast::TypeInstType * mut = ast::mutate( type );
    88                                 mut->name = it->second;
    89                     type = mut;
     81                                ast::TypeInstType * mutType = ast::mutate( type );
     82                                mutType->name = it->second;
     83                    type = mutType;
    9084                        }
    91 
    9285                        return type;
    9386                }
     
    9588                template<typename NodeT>
    9689                const NodeT * openLevel( const NodeT * type ) {
    97                         if ( type->forall.empty() ) return type;
     90                        if ( !type->forall.empty() ) {
     91                                nameMap.beginScope();
     92                                // Load new names from this forall clause and perform renaming.
     93                                NodeT * mutType = ast::mutate( type );
     94                                for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
     95                                        std::ostringstream output;
     96                                        output << "_" << resetCount << "_" << level << "_" << td->name;
     97                                        std::string newname( output.str() );
     98                                        nameMap[ td->name ] = newname;
     99                                        ++level;
    98100
    99                         nameMap.beginScope();
    100 
    101                         // Load new names from this forall clause and perform renaming.
    102                         NodeT * mutType = ast::mutate( type );
    103                         assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
    104                         for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
    105                                 std::ostringstream output;
    106                                 output << "_" << resetCount << "_" << level << "_" << td->name;
    107                                 std::string newname =  output.str();
    108                                 nameMap[ td->name ] = newname;
    109                                 ++level;
    110 
    111                                 ast::TypeDecl * mutDecl = ast::mutate( td.get() );
    112                                 assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
    113                                 mutDecl->name = newname;
    114                                 // assertion above means `td = mutDecl;` is unnecessary
     101                                        ast::TypeDecl * decl = ast::mutate( td.get() );
     102                                        decl->name = newname;
     103                                        td = decl;
     104                                }
    115105                        }
    116                         // assertion above means `type = mutType;` is unnecessary
    117 
    118106                        return type;
    119107                }
    120108
    121                 void closeLevel( const ast::ParameterizedType * type ) {
    122                         if ( type->forall.empty() ) return;
    123 
    124                         nameMap.endScope();
     109                template<typename NodeT>
     110                const NodeT * closeLevel( const NodeT * type ) {
     111                        if ( !type->forall.empty() ) {
     112                                nameMap.endScope();
     113                        }
     114                        return type;
    125115                }
    126116        };
     
    129119        RenamingData renaming;
    130120
    131         struct RenameVars_old {
     121        struct RenameVars {
    132122                void previsit( TypeInstType * instType ) {
    133123                        renaming.openLevel( (Type*)instType );
     
    140130                        renaming.closeLevel( type );
    141131                }
    142         };
    143 
    144         struct RenameVars_new /*: public ast::WithForallSubstitutor*/ {
    145                 #warning when old RenameVars goes away, replace hack below with global pass inheriting from WithForallSubstitutor
    146                 ast::ForallSubstitutionTable & subs = renaming.subs;
    147132
    148133                const ast::FunctionType * previsit( const ast::FunctionType * type ) {
     
    161146                        return renaming.rename( renaming.openLevel( type ) );
    162147                }
    163                 void postvisit( const ast::ParameterizedType * type ) {
    164                         renaming.closeLevel( type );
     148                const ast::ParameterizedType * postvisit( const ast::ParameterizedType * type ) {
     149                        return renaming.closeLevel( type );
    165150                }
    166151        };
     
    169154
    170155void renameTyVars( Type * t ) {
    171         PassVisitor<RenameVars_old> renamer;
     156        PassVisitor<RenameVars> renamer;
    172157        t->accept( renamer );
    173158}
    174159
    175160const ast::Type * renameTyVars( const ast::Type * t ) {
    176         ast::Type *tc = ast::deepCopy(t);
    177         ast::Pass<RenameVars_new> renamer;
    178 //      return t->accept( renamer );
    179         return tc->accept( renamer );
     161        ast::Pass<RenameVars> renamer;
     162        return t->accept( renamer );
    180163}
    181164
Note: See TracChangeset for help on using the changeset viewer.