| [a32b204] | 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 | // | 
|---|
| [8c49c0e] | 7 | // RenameVars.cc -- | 
|---|
| [a32b204] | 8 | // | 
|---|
|  | 9 | // Author           : Richard C. Bilson | 
|---|
|  | 10 | // Created On       : Sun May 17 12:05:18 2015 | 
|---|
| [f5edcb4] | 11 | // Last Modified By : Andrew Beach | 
|---|
|  | 12 | // Last Modified On : Thr Jun 20 17:39:00 2019 | 
|---|
|  | 13 | // Update Count     : 8 | 
|---|
| [a32b204] | 14 | // | 
|---|
| [51b73452] | 15 |  | 
|---|
| [ea6332d] | 16 | #include <ext/alloc_traits.h>      // for __alloc_traits<>::value_type | 
|---|
|  | 17 | #include <memory>                  // for allocator_traits<>::value_type | 
|---|
|  | 18 | #include <sstream>                 // for operator<<, basic_ostream, ostring... | 
|---|
|  | 19 | #include <utility>                 // for pair | 
|---|
| [51b73452] | 20 |  | 
|---|
| [f5edcb4] | 21 | #include "AST/Pass.hpp" | 
|---|
|  | 22 | #include "AST/Type.hpp" | 
|---|
| [ad51cc2] | 23 | #include "Common/PassVisitor.h" | 
|---|
| [f5edcb4] | 24 | #include "Common/ScopedMap.h" | 
|---|
| [ea6332d] | 25 | #include "Common/SemanticError.h"  // for SemanticError | 
|---|
| [51b73452] | 26 | #include "RenameVars.h" | 
|---|
| [ea6332d] | 27 | #include "SynTree/Declaration.h"   // for DeclarationWithType, TypeDecl, Dec... | 
|---|
|  | 28 | #include "SynTree/Expression.h"    // for Expression | 
|---|
|  | 29 | #include "SynTree/Type.h"          // for Type, TypeInstType, TraitInstType | 
|---|
|  | 30 | #include "SynTree/Visitor.h"       // for acceptAll, maybeAccept | 
|---|
| [51b73452] | 31 |  | 
|---|
| [99da267] | 32 | #include "AST/Copy.hpp" | 
|---|
|  | 33 |  | 
|---|
| [51b73452] | 34 | namespace ResolvExpr { | 
|---|
| [ad51cc2] | 35 |  | 
|---|
| [f5edcb4] | 36 | namespace { | 
|---|
|  | 37 | class RenamingData { | 
|---|
|  | 38 | int level = 0; | 
|---|
|  | 39 | int resetCount = 0; | 
|---|
| [3e5dd913] | 40 |  | 
|---|
|  | 41 | int next_expr_id = 1; | 
|---|
|  | 42 | int next_usage_id = 1; | 
|---|
| [f5edcb4] | 43 | ScopedMap< std::string, std::string > nameMap; | 
|---|
| [3e5dd913] | 44 | ScopedMap< std::string, ast::TypeInstType::TypeEnvKey > idMap; | 
|---|
| [f5edcb4] | 45 | public: | 
|---|
|  | 46 | void reset() { | 
|---|
| [ad51cc2] | 47 | level = 0; | 
|---|
| [f5edcb4] | 48 | ++resetCount; | 
|---|
| [ad51cc2] | 49 | } | 
|---|
|  | 50 |  | 
|---|
| [f5edcb4] | 51 | void rename( TypeInstType * type ) { | 
|---|
| [e0e9a0b] | 52 | auto it = nameMap.find( type->name ); | 
|---|
| [f5edcb4] | 53 | if ( it != nameMap.end() ) { | 
|---|
|  | 54 | type->name = it->second; | 
|---|
|  | 55 | } | 
|---|
| [ad51cc2] | 56 | } | 
|---|
|  | 57 |  | 
|---|
| [3e5dd913] | 58 | void nextUsage() { | 
|---|
|  | 59 | ++next_usage_id; | 
|---|
|  | 60 | } | 
|---|
|  | 61 |  | 
|---|
| [f5edcb4] | 62 | void openLevel( Type * type ) { | 
|---|
| [ad51cc2] | 63 | if ( ! type->forall.empty() ) { | 
|---|
| [f5edcb4] | 64 | nameMap.beginScope(); | 
|---|
| [ad51cc2] | 65 | // renames all "forall" type names to `_${level}_${name}' | 
|---|
|  | 66 | for ( auto td : type->forall ) { | 
|---|
|  | 67 | std::ostringstream output; | 
|---|
|  | 68 | output << "_" << resetCount << "_" << level << "_" << td->name; | 
|---|
|  | 69 | std::string newname( output.str() ); | 
|---|
| [f5edcb4] | 70 | nameMap[ td->get_name() ] = newname; | 
|---|
| [ad51cc2] | 71 | td->name = newname; | 
|---|
|  | 72 | // ditto for assertion names, the next level in | 
|---|
|  | 73 | level++; | 
|---|
| [e0e9a0b] | 74 | } | 
|---|
|  | 75 | } | 
|---|
| [ad51cc2] | 76 | } | 
|---|
|  | 77 |  | 
|---|
| [f5edcb4] | 78 | void closeLevel( Type * type ) { | 
|---|
|  | 79 | if ( !type->forall.empty() ) { | 
|---|
|  | 80 | nameMap.endScope(); | 
|---|
|  | 81 | } | 
|---|
|  | 82 | } | 
|---|
|  | 83 |  | 
|---|
|  | 84 | const ast::TypeInstType * rename( const ast::TypeInstType * type ) { | 
|---|
| [e0e9a0b] | 85 | // rename | 
|---|
| [3e5dd913] | 86 | auto it = idMap.find( type->name ); | 
|---|
|  | 87 | if ( it != idMap.end() ) { | 
|---|
|  | 88 | // unconditionally mutate because map will *always* have different name | 
|---|
|  | 89 | ast::TypeInstType * mut = ast::shallowCopy( type ); | 
|---|
|  | 90 | // reconcile base node since some copies might have been made | 
|---|
|  | 91 | mut->base = it->second.base; | 
|---|
|  | 92 | mut->formal_usage = it->second.formal_usage; | 
|---|
|  | 93 | mut->expr_id = it->second.expr_id; | 
|---|
| [e0e9a0b] | 94 | type = mut; | 
|---|
| [f5edcb4] | 95 | } | 
|---|
| [e0e9a0b] | 96 |  | 
|---|
| [f5edcb4] | 97 | return type; | 
|---|
|  | 98 | } | 
|---|
|  | 99 |  | 
|---|
| [3e5dd913] | 100 | const ast::FunctionType * openLevel( const ast::FunctionType * type, RenameMode mode ) { | 
|---|
| [e0e9a0b] | 101 | if ( type->forall.empty() ) return type; | 
|---|
| [3e5dd913] | 102 | idMap.beginScope(); | 
|---|
| [e0e9a0b] | 103 |  | 
|---|
|  | 104 | // Load new names from this forall clause and perform renaming. | 
|---|
| [3e5dd913] | 105 | auto mutType = ast::shallowCopy( type ); | 
|---|
|  | 106 | // assert( type == mutType && "mutated type must be unique from ForallSubstitutor" ); | 
|---|
|  | 107 | for ( auto & td : mutType->forall ) { | 
|---|
|  | 108 | auto mut = ast::shallowCopy( td.get() ); | 
|---|
|  | 109 | // assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" ); | 
|---|
|  | 110 |  | 
|---|
|  | 111 | if (mode == GEN_EXPR_ID) { | 
|---|
|  | 112 | mut->expr_id = next_expr_id; | 
|---|
|  | 113 | mut->formal_usage = -1; | 
|---|
|  | 114 | ++next_expr_id; | 
|---|
|  | 115 | } | 
|---|
|  | 116 | else if (mode == GEN_USAGE) { | 
|---|
|  | 117 | assertf(mut->expr_id, "unfilled expression id in generating candidate type"); | 
|---|
|  | 118 | mut->formal_usage = next_usage_id; | 
|---|
|  | 119 | } | 
|---|
|  | 120 | else { | 
|---|
|  | 121 | assert(false); | 
|---|
|  | 122 | } | 
|---|
|  | 123 | idMap[ td->name ] = ast::TypeInstType::TypeEnvKey(*mut); | 
|---|
|  | 124 |  | 
|---|
|  | 125 | td = mut; | 
|---|
| [f5edcb4] | 126 | } | 
|---|
| [e0e9a0b] | 127 |  | 
|---|
| [3e5dd913] | 128 | return mutType; | 
|---|
| [ad51cc2] | 129 | } | 
|---|
| [898ae07] | 130 |  | 
|---|
| [361bf01] | 131 | void closeLevel( const ast::FunctionType * type ) { | 
|---|
| [e0e9a0b] | 132 | if ( type->forall.empty() ) return; | 
|---|
| [3e5dd913] | 133 | idMap.endScope(); | 
|---|
| [f5edcb4] | 134 | } | 
|---|
|  | 135 | }; | 
|---|
|  | 136 |  | 
|---|
|  | 137 | // Global State: | 
|---|
|  | 138 | RenamingData renaming; | 
|---|
|  | 139 |  | 
|---|
| [e0e9a0b] | 140 | struct RenameVars_old { | 
|---|
| [f5edcb4] | 141 | void previsit( TypeInstType * instType ) { | 
|---|
|  | 142 | renaming.openLevel( (Type*)instType ); | 
|---|
|  | 143 | renaming.rename( instType ); | 
|---|
|  | 144 | } | 
|---|
|  | 145 | void previsit( Type * type ) { | 
|---|
|  | 146 | renaming.openLevel( type ); | 
|---|
|  | 147 | } | 
|---|
|  | 148 | void postvisit( Type * type ) { | 
|---|
|  | 149 | renaming.closeLevel( type ); | 
|---|
|  | 150 | } | 
|---|
| [e0e9a0b] | 151 | }; | 
|---|
| [4e13e2a] | 152 |  | 
|---|
| [3e5dd913] | 153 | struct RenameVars_new : public ast::PureVisitor /*: public ast::WithForallSubstitutor*/ { | 
|---|
|  | 154 | RenameMode mode; | 
|---|
| [f5edcb4] | 155 |  | 
|---|
|  | 156 | const ast::FunctionType * previsit( const ast::FunctionType * type ) { | 
|---|
| [3e5dd913] | 157 | return renaming.openLevel( type, mode ); | 
|---|
| [f5edcb4] | 158 | } | 
|---|
| [361bf01] | 159 |  | 
|---|
|  | 160 | /* | 
|---|
| [f5edcb4] | 161 | const ast::StructInstType * previsit( const ast::StructInstType * type ) { | 
|---|
|  | 162 | return renaming.openLevel( type ); | 
|---|
|  | 163 | } | 
|---|
|  | 164 | const ast::UnionInstType * previsit( const ast::UnionInstType * type ) { | 
|---|
|  | 165 | return renaming.openLevel( type ); | 
|---|
|  | 166 | } | 
|---|
|  | 167 | const ast::TraitInstType * previsit( const ast::TraitInstType * type ) { | 
|---|
|  | 168 | return renaming.openLevel( type ); | 
|---|
|  | 169 | } | 
|---|
| [361bf01] | 170 | */ | 
|---|
|  | 171 |  | 
|---|
| [f5edcb4] | 172 | const ast::TypeInstType * previsit( const ast::TypeInstType * type ) { | 
|---|
| [3e5dd913] | 173 | if (mode == GEN_USAGE && !type->formal_usage) return type; // do not rename an actual type | 
|---|
| [361bf01] | 174 | return renaming.rename( type ); | 
|---|
| [f5edcb4] | 175 | } | 
|---|
| [361bf01] | 176 | void postvisit( const ast::FunctionType * type ) { | 
|---|
| [e0e9a0b] | 177 | renaming.closeLevel( type ); | 
|---|
| [f5edcb4] | 178 | } | 
|---|
|  | 179 | }; | 
|---|
|  | 180 |  | 
|---|
|  | 181 | } // namespace | 
|---|
|  | 182 |  | 
|---|
|  | 183 | void renameTyVars( Type * t ) { | 
|---|
| [e0e9a0b] | 184 | PassVisitor<RenameVars_old> renamer; | 
|---|
| [f5edcb4] | 185 | t->accept( renamer ); | 
|---|
|  | 186 | } | 
|---|
|  | 187 |  | 
|---|
| [7583c02] | 188 | const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode, bool reset ) { | 
|---|
| [3e5dd913] | 189 | // ast::Type *tc = ast::deepCopy(t); | 
|---|
| [e0e9a0b] | 190 | ast::Pass<RenameVars_new> renamer; | 
|---|
| [3e5dd913] | 191 | renamer.core.mode = mode; | 
|---|
| [7583c02] | 192 | if (mode == GEN_USAGE && reset) { | 
|---|
| [3e5dd913] | 193 | renaming.nextUsage(); | 
|---|
|  | 194 | } | 
|---|
|  | 195 | return t->accept( renamer ); | 
|---|
| [f5edcb4] | 196 | } | 
|---|
|  | 197 |  | 
|---|
|  | 198 | void resetTyVarRenaming() { | 
|---|
|  | 199 | renaming.reset(); | 
|---|
| [7583c02] | 200 | renaming.nextUsage(); | 
|---|
| [f5edcb4] | 201 | } | 
|---|
|  | 202 |  | 
|---|
| [51b73452] | 203 | } // namespace ResolvExpr | 
|---|
| [a32b204] | 204 |  | 
|---|
|  | 205 | // Local Variables: // | 
|---|
|  | 206 | // tab-width: 4 // | 
|---|
|  | 207 | // mode: c++ // | 
|---|
|  | 208 | // compile-command: "make install" // | 
|---|
|  | 209 | // End: // | 
|---|