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

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"
@@ -39 +38 @@
                 int level = 0;
                 int resetCount = 0;
+
+                int next_expr_id = 1;
+                int next_usage_id = 1;
                 ScopedMap< std::string, std::string > nameMap;
+                ScopedMap< std::string, ast::TypeInstType::TypeEnvKey > idMap;
         public:
-                ast::ForallSubstitutionTable subs;
-
                 void reset() {
                         level = 0;
@@ -53 +54 @@
                                 type->name = it->second;
                         }
+                }
+
+                void nextUsage() {
+                        ++next_usage_id;
                 }
 
@@ -78 +83 @@
 
                 const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
-                        // re-linking of base type handled by WithForallSubstitutor
-
                         // rename
-                        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;
+                        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;
                     type = mut;
                         }
@@ -93 +98 @@
                 }
 
-                const ast::FunctionType * openLevel( const ast::FunctionType * type ) {
+                const ast::FunctionType * openLevel( const ast::FunctionType * type, RenameMode mode ) {
                         if ( type->forall.empty() ) return type;
-
-                        nameMap.beginScope();
+                        idMap.beginScope();
 
                         // Load new names from this forall clause and perform renaming.
-                        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;
-
-                                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 type;
+                        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" );
+
+                                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;
+                        }
+
+                        return mutType;
                 }
 
                 void closeLevel( const ast::FunctionType * type ) {
                         if ( type->forall.empty() ) return;
-
-                        nameMap.endScope();
+                        idMap.endScope();
                 }
         };
@@ -142 +151 @@
         };
 
-        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;
+        struct RenameVars_new : public ast::PureVisitor /*: public ast::WithForallSubstitutor*/ {
+                RenameMode mode;
 
                 const ast::FunctionType * previsit( const ast::FunctionType * type ) {
-                        return renaming.openLevel( type );
+                        return renaming.openLevel( type, mode );
                 }
 
@@ -163 +171 @@
 
                 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 );
                 }
@@ -177 +186 @@
 }
 
-const ast::Type * renameTyVars( const ast::Type * t ) {
-        ast::Type *tc = ast::deepCopy(t);
+const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode, bool reset ) {
+        // ast::Type *tc = ast::deepCopy(t);
         ast::Pass<RenameVars_new> renamer;
-//      return t->accept( renamer );
-        return tc->accept( renamer );
+        renamer.core.mode = mode;
+        if (mode == GEN_USAGE && reset) {
+                renaming.nextUsage();
+        }
+        return t->accept( renamer );
 }
 
 void resetTyVarRenaming() {
         renaming.reset();
+        renaming.nextUsage();
 }