Changes in src/ResolvExpr/RenameVars.cc [7583c02:361bf01]

File:

• src/ResolvExpr/RenameVars.cc (modified) (8 diffs)

src/ResolvExpr/RenameVars.cc

@@ -19 +19 @@
 #include <utility>                 // for pair
 
+#include "AST/ForallSubstitutionTable.hpp"
 #include "AST/Pass.hpp"
 #include "AST/Type.hpp"
@@ -38 +39 @@
                 int level = 0;
                 int resetCount = 0;
+                ScopedMap< std::string, std::string > nameMap;
+        public:
+                ast::ForallSubstitutionTable subs;
 
-                int next_expr_id = 1;
-                int next_usage_id = 1;
-                ScopedMap< std::string, std::string > nameMap;
-                ScopedMap< std::string, ast::TypeInstType::TypeEnvKey > idMap;
-        public:
                 void reset() {
                         level = 0;
@@ -54 +53 @@
                                 type->name = it->second;
                         }
-                }
-
-                void nextUsage() {
-                        ++next_usage_id;
                 }
 
@@ -83 +78 @@
 
                 const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
+                        // re-linking of base type handled by WithForallSubstitutor
+
                         // rename
-                        auto it = idMap.find( type->name );
-                        if ( it != idMap.end() ) {
-                                // unconditionally mutate because map will *always* have different name
-                                ast::TypeInstType * mut = ast::shallowCopy( type );
-                                // reconcile base node since some copies might have been made
-                                mut->base = it->second.base;
-                                mut->formal_usage = it->second.formal_usage;
-                                mut->expr_id = it->second.expr_id;
+                        auto it = nameMap.find( type->name );
+                        if ( it != nameMap.end() ) {
+                                // unconditionally mutate because map will *always* have different name,
+                                // if this mutates, will *always* have been mutated by ForallSubstitutor above
+                                ast::TypeInstType * mut = ast::mutate( type );
+                                mut->name = it->second;
                     type = mut;
                         }
@@ -98 +93 @@
                 }
 
-                const ast::FunctionType * openLevel( const ast::FunctionType * type, RenameMode mode ) {
+                const ast::FunctionType * openLevel( const ast::FunctionType * type ) {
                         if ( type->forall.empty() ) return type;
-                        idMap.beginScope();
+
+                        nameMap.beginScope();
 
                         // Load new names from this forall clause and perform renaming.
-                        auto mutType = ast::shallowCopy( type );
-                        // assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
-                        for ( auto & td : mutType->forall ) {
-                                auto mut = ast::shallowCopy( td.get() );
-                                // assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
+                        auto mutType = ast::mutate( type );
+                        assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
+                        for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
+                                assertf(dynamic_cast<ast::FunctionType *>(mutType), "renaming vars in non-function type");
+                                std::ostringstream output;
+                                output << "_" << resetCount << "_" << level << "_" << td->name;
+                                std::string newname =  output.str();
+                                nameMap[ td->name ] = newname;
+                                ++level;
 
-                                if (mode == GEN_EXPR_ID) {
-                                        mut->expr_id = next_expr_id;
-                                        mut->formal_usage = -1;
-                                        ++next_expr_id;
-                                }
-                                else if (mode == GEN_USAGE) {
-                                        assertf(mut->expr_id, "unfilled expression id in generating candidate type");
-                                        mut->formal_usage = next_usage_id;
-                                }
-                                else {
-                                        assert(false);
-                                }
-                                idMap[ td->name ] = ast::TypeInstType::TypeEnvKey(*mut);
-                                
-                                td = mut;
+                                ast::TypeDecl * mutDecl = ast::mutate( td.get() );
+                                assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
+                                mutDecl->name = newname;
+                                // assertion above means `td = mutDecl;` is unnecessary
                         }
+                        // assertion above means `type = mutType;` is unnecessary
 
-                        return mutType;
+                        return type;
                 }
 
                 void closeLevel( const ast::FunctionType * type ) {
                         if ( type->forall.empty() ) return;
-                        idMap.endScope();
+
+                        nameMap.endScope();
                 }
         };
@@ -151 +142 @@
         };
 
-        struct RenameVars_new : public ast::PureVisitor /*: public ast::WithForallSubstitutor*/ {
-                RenameMode mode;
+        struct RenameVars_new /*: public ast::WithForallSubstitutor*/ {
+                #warning when old RenameVars goes away, replace hack below with global pass inheriting from WithForallSubstitutor
+                ast::ForallSubstitutionTable & subs = renaming.subs;
 
                 const ast::FunctionType * previsit( const ast::FunctionType * type ) {
-                        return renaming.openLevel( type, mode );
+                        return renaming.openLevel( type );
                 }
 
@@ -171 +163 @@
 
                 const ast::TypeInstType * previsit( const ast::TypeInstType * type ) {
-                        if (mode == GEN_USAGE && !type->formal_usage) return type; // do not rename an actual type
                         return renaming.rename( type );
                 }
@@ -186 +177 @@
 }
 
-const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode, bool reset ) {
-        // ast::Type *tc = ast::deepCopy(t);
+const ast::Type * renameTyVars( const ast::Type * t ) {
+        ast::Type *tc = ast::deepCopy(t);
         ast::Pass<RenameVars_new> renamer;
-        renamer.core.mode = mode;
-        if (mode == GEN_USAGE && reset) {
-                renaming.nextUsage();
-        }
-        return t->accept( renamer );
+//      return t->accept( renamer );
+        return tc->accept( renamer );
 }
 
 void resetTyVarRenaming() {
         renaming.reset();
-        renaming.nextUsage();
 }