Changeset 53449a4 for src

Timestamp:

Dec 16, 2020, 4:01:57 PM (5 years ago)

Author:

Colby Alexander Parsons <caparsons@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, master, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

8ba363e, c8025a21

Parents:

b3c8496 (diff), 3e5dd913 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

Location:

src

Files:

• AST/Convert.cpp (modified) (16 diffs)
• AST/Decl.cpp (modified) (1 diff)
• AST/Decl.hpp (modified) (3 diffs)
• AST/Expr.cpp (modified) (1 diff)
• AST/Expr.hpp (modified) (1 diff)
• AST/ForallSubstitutionTable.cpp (deleted)
• AST/ForallSubstitutionTable.hpp (deleted)
• AST/ForallSubstitutor.hpp (deleted)
• AST/Fwd.hpp (modified) (1 diff)
• AST/Pass.hpp (modified) (5 diffs)
• AST/Pass.impl.hpp (modified) (12 diffs)
• AST/Pass.proto.hpp (modified) (3 diffs)
• AST/Print.cpp (modified) (6 diffs)
• AST/SymbolTable.cpp (modified) (1 diff)
• AST/TranslationUnit.hpp (modified) (1 diff)
• AST/Type.cpp (modified) (5 diffs)
• AST/Type.hpp (modified) (9 diffs)
• AST/TypeEnvironment.cpp (modified) (15 diffs)
• AST/TypeEnvironment.hpp (modified) (7 diffs)
• AST/TypeSubstitution.cpp (modified) (9 diffs)
• AST/TypeSubstitution.hpp (modified) (7 diffs)
• AST/module.mk (modified) (1 diff)
• Common/PassVisitor.impl.h (modified) (6 diffs)
• GenPoly/GenPoly.cc (modified) (4 diffs)
• Parser/TypeData.cc (modified) (1 diff)
• ResolvExpr/AdjustExprType.cc (modified) (1 diff)
• ResolvExpr/CandidateFinder.cpp (modified) (6 diffs)
• ResolvExpr/CastCost.cc (modified) (2 diffs)
• ResolvExpr/CommonType.cc (modified) (1 diff)
• ResolvExpr/ConversionCost.cc (modified) (2 diffs)
• ResolvExpr/FindOpenVars.cc (modified) (1 diff)
• ResolvExpr/PolyCost.cc (modified) (1 diff)
• ResolvExpr/PtrsAssignable.cc (modified) (2 diffs)
• ResolvExpr/PtrsCastable.cc (modified) (2 diffs)
• ResolvExpr/RenameVars.cc (modified) (8 diffs)
• ResolvExpr/RenameVars.h (modified) (1 diff)
• ResolvExpr/ResolveTypeof.cc (modified) (2 diffs)
• ResolvExpr/Resolver.cc (modified) (5 diffs)
• ResolvExpr/SatisfyAssertions.cpp (modified) (15 diffs)
• ResolvExpr/Unify.cc (modified) (5 diffs)
• SymTab/Mangler.cc (modified) (2 diffs)
• SymTab/Validate.cc (modified) (4 diffs)
• SynTree/Declaration.h (modified) (2 diffs)
• SynTree/NamedTypeDecl.cc (modified) (4 diffs)
• Tuples/TupleAssignment.cc (modified) (2 diffs)

src/AST/Convert.cpp

@@ -55 +55 @@
 
 // these need to be accessed in new FixInit now
-ast::Type * sizeType = nullptr;
-ast::FunctionDecl * dereferenceOperator = nullptr;
-ast::StructDecl   * dtorStruct = nullptr;
-ast::FunctionDecl * dtorStructDestroy = nullptr;
+ast::ptr<ast::Type> sizeType = nullptr;
+const ast::FunctionDecl * dereferenceOperator = nullptr;
+const ast::StructDecl   * dtorStruct = nullptr;
+const ast::FunctionDecl * dtorStructDestroy = nullptr;
 
 }
@@ -205 +205 @@
                 ftype->parameters = get<DeclarationWithType>().acceptL(node->params);
 
-                ftype->forall = get<TypeDecl>().acceptL( node->type->forall );
+                ftype->forall = get<TypeDecl>().acceptL( node->type_params );
+                if (!node->assertions.empty()) {
+                        assert(!ftype->forall.empty());
+                        // find somewhere to place assertions back, for convenience it is the last slot
+                        ftype->forall.back()->assertions = get<DeclarationWithType>().acceptL(node->assertions);
+                }
 
                 visitType(node->type, ftype);
@@ -233 +238 @@
         const ast::Decl * namedTypePostamble( NamedTypeDecl * decl, const ast::NamedTypeDecl * node ) {
                 // base comes from constructor
-                decl->parameters = get<TypeDecl>().acceptL( node->params );
                 decl->assertions = get<DeclarationWithType>().acceptL( node->assertions );
                 declPostamble( decl, node );
@@ -603 +607 @@
 
                 for (decltype(src->begin()) src_i = src->begin(); src_i != src->end(); src_i++) {
-                        rslt->add( src_i->first,
+                        rslt->add( src_i->first.typeString(),
                                    get<Type>().accept1(src_i->second) );
-                }
-
-                for (decltype(src->beginVar()) src_i = src->beginVar(); src_i != src->endVar(); src_i++) {
-                        rslt->addVar( src_i->first,
-                                      get<Expression>().accept1(src_i->second) );
                 }
 
@@ -1213 +1212 @@
                 // ty->returnVals = get<DeclarationWithType>().acceptL( node->returns );
                 // ty->parameters = get<DeclarationWithType>().acceptL( node->params );
-                ty->forall = get<TypeDecl>().acceptL( node->forall );
+
+                auto types = get<TypeInstType>().acceptL( node->forall );
+                for (auto t : types) {
+                        auto newT = new TypeDecl(*t->baseType);
+                        newT->name = t->name; // converted by typeString()
+                        for (auto asst : newT->assertions) delete asst;
+                        newT->assertions.clear();
+                        ty->forall.push_back(newT);
+                }
+                auto assts = get<VariableExpr>().acceptL( node->assertions );
+                if (!assts.empty()) {
+                        assert(!types.empty());
+                        for (auto asst : assts) {
+                                auto newDecl = new ObjectDecl(*strict_dynamic_cast<ObjectDecl*>(asst->var));
+                                delete newDecl->type;
+                                newDecl->type = asst->result->clone();
+                                newDecl->storageClasses.is_extern = true; // hack
+                                ty->forall.back()->assertions.push_back(newDecl);
+                        }
+                }
+
                 return visitType( node, ty );
         }
 
         const ast::Type * postvisit( const ast::BaseInstType * old, ReferenceToType * ty ) {
-                ty->forall = get<TypeDecl>().acceptL( old->forall );
                 ty->parameters = get<Expression>().acceptL( old->params );
                 ty->hoistType = old->hoistType;
@@ -1301 +1319 @@
                         ty = new TypeInstType{
                                 cv( node ),
-                                node->name,
+                                node->typeString(),
                                 get<TypeDecl>().accept1( node->base ),
                                 get<Attribute>().acceptL( node->attributes )
@@ -1308 +1326 @@
                         ty = new TypeInstType{
                                 cv( node ),
-                                node->name,
+                                node->typeString(),
                                 node->kind == ast::TypeDecl::Ftype,
                                 get<Attribute>().acceptL( node->attributes )
@@ -1433 +1451 @@
         /// at conversion stage, all created nodes are guaranteed to be unique, therefore
         /// const_casting out of smart pointers is permitted.
-        std::unordered_map< const BaseSyntaxNode *, ast::ptr<ast::Node> > cache = {};
+        std::unordered_map< const BaseSyntaxNode *, ast::readonly<ast::Node> > cache = {};
 
         // Local Utilities:
@@ -1567 +1585 @@
                 // can function type have attributes? seems not to be the case.
                 // visitType(old->type, ftype);
+
+                // collect assertions and put directly in FunctionDecl
+                std::vector<ast::ptr<ast::DeclWithType>> assertions;
+                for (auto & param: forall) {
+                        for (auto & asst: param->assertions) {
+                                assertf(asst->unique(), "newly converted decl must be unique");
+                                assertions.emplace_back(asst);
+                        }
+                        auto mut = param.get_and_mutate();
+                        assertf(mut == param, "newly converted decl must be unique");
+                        mut->assertions.clear();
+                }
 
                 auto decl = new ast::FunctionDecl{
@@ -1586 +1616 @@
                 cache.emplace( old, decl );
 
+                decl->assertions = std::move(assertions);
                 decl->withExprs = GET_ACCEPT_V(withExprs, Expr);
                 decl->stmts = GET_ACCEPT_1(statements, CompoundStmt);
@@ -1704 +1735 @@
                 cache.emplace( old, decl );
                 decl->assertions = GET_ACCEPT_V(assertions, DeclWithType);
-                decl->params     = GET_ACCEPT_V(parameters, TypeDecl);
                 decl->extension  = old->extension;
                 decl->uniqueId   = old->uniqueId;
@@ -1720 +1750 @@
                 );
                 decl->assertions = GET_ACCEPT_V(assertions, DeclWithType);
-                decl->params     = GET_ACCEPT_V(parameters, TypeDecl);
                 decl->extension  = old->extension;
                 decl->uniqueId   = old->uniqueId;
@@ -2070 +2099 @@
         }
 
+        // TypeSubstitution shouldn't exist yet in old.
         ast::TypeSubstitution * convertTypeSubstitution(const TypeSubstitution * old) {
-
+                
                 if (!old) return nullptr;
-
+                if (old->empty()) return nullptr;
+                assert(false);
+
+                /*
                 ast::TypeSubstitution *rslt = new ast::TypeSubstitution();
 
@@ -2081 +2114 @@
                 }
 
-                for (decltype(old->beginVar()) old_i = old->beginVar(); old_i != old->endVar(); old_i++) {
-                        rslt->addVar( old_i->first,
-                                      getAccept1<ast::Expr>(old_i->second) );
-                }
-
                 return rslt;
+                */
         }
 
@@ -2614 +2643 @@
                         ty->params.emplace_back(v->get_type());
                 }
-                ty->forall = GET_ACCEPT_V( forall, TypeDecl );
+                // xxx - when will this be non-null?
+                // will have to create dangling (no-owner) decls to be pointed to
+                auto foralls = GET_ACCEPT_V( forall, TypeDecl );
+
+                for (auto & param : foralls) {
+                        ty->forall.emplace_back(new ast::TypeInstType(param->name, param));
+                        for (auto asst : param->assertions) {
+                                ty->assertions.emplace_back(new ast::VariableExpr({}, asst));
+                        }
+                }
                 visitType( old, ty );
         }
 
         void postvisit( const ReferenceToType * old, ast::BaseInstType * ty ) {
-                ty->forall = GET_ACCEPT_V( forall, TypeDecl );
                 ty->params = GET_ACCEPT_V( parameters, Expr );
                 ty->hoistType = old->hoistType;
@@ -2807 +2844 @@
         ConverterOldToNew c;
         ast::TranslationUnit unit;
+        if (Validate::SizeType) {
+                // this should be a BasicType.
+                auto old = strict_dynamic_cast<BasicType *>(Validate::SizeType);
+                ast::sizeType = new ast::BasicType{ (ast::BasicType::Kind)(unsigned)old->kind };
+        }
+
         for(auto d : translationUnit) {
                 d->accept( c );

src/AST/Decl.cpp

@@ -50 +50 @@
 
 FunctionDecl::FunctionDecl( const CodeLocation & loc, const std::string & name, 
-                std::vector<ptr<TypeDecl>>&& forall,
-                std::vector<ptr<DeclWithType>>&& params, std::vector<ptr<DeclWithType>>&& returns,
-                CompoundStmt * stmts, Storage::Classes storage, Linkage::Spec linkage,
-                std::vector<ptr<Attribute>>&& attrs, Function::Specs fs, bool isVarArgs)
-        : DeclWithType( loc, name, storage, linkage, std::move(attrs), fs ), params(std::move(params)), returns(std::move(returns)),
-          stmts( stmts ) {
-                  FunctionType * ftype = new FunctionType(static_cast<ArgumentFlag>(isVarArgs));
-                  for (auto & param : this->params) {
-                          ftype->params.emplace_back(param->get_type());
-                  }
-                  for (auto & ret : this->returns) {
-                          ftype->returns.emplace_back(ret->get_type());
-                  }
-                  ftype->forall = std::move(forall);
-                  this->type = ftype;
-          }
+        std::vector<ptr<TypeDecl>>&& forall,
+        std::vector<ptr<DeclWithType>>&& params, std::vector<ptr<DeclWithType>>&& returns,
+        CompoundStmt * stmts, Storage::Classes storage, Linkage::Spec linkage,
+        std::vector<ptr<Attribute>>&& attrs, Function::Specs fs, bool isVarArgs)
+: DeclWithType( loc, name, storage, linkage, std::move(attrs), fs ), params(std::move(params)), returns(std::move(returns)),
+        type_params(std::move(forall)), stmts( stmts ) {
+        FunctionType * ftype = new FunctionType(static_cast<ArgumentFlag>(isVarArgs));
+        for (auto & param : this->params) {
+                ftype->params.emplace_back(param->get_type());
+        }
+        for (auto & ret : this->returns) {
+                ftype->returns.emplace_back(ret->get_type());
+        }
+        for (auto & tp : this->type_params) {
+                ftype->forall.emplace_back(new TypeInstType(tp->name, tp));
+        }
+        this->type = ftype;
+}
 
 

src/AST/Decl.hpp

@@ -132 +132 @@
         std::vector< ptr<Expr> > withExprs;
 
+        std::vector<ptr<TypeDecl>> type_params;
+        std::vector<ptr<DeclWithType>> assertions;
+
         FunctionDecl( const CodeLocation & loc, const std::string & name, std::vector<ptr<TypeDecl>>&& forall,
                 std::vector<ptr<DeclWithType>>&& params, std::vector<ptr<DeclWithType>>&& returns,
@@ -154 +157 @@
 public:
         ptr<Type> base;
-        std::vector<ptr<TypeDecl>> params;
         std::vector<ptr<DeclWithType>> assertions;
 
@@ -160 +162 @@
                 const CodeLocation & loc, const std::string & name, Storage::Classes storage,
                 const Type * b, Linkage::Spec spec = Linkage::Cforall )
-        : Decl( loc, name, storage, spec ), base( b ), params(), assertions() {}
+        : Decl( loc, name, storage, spec ), base( b ), assertions() {}
 
         /// Produces a name for the kind of alias

src/AST/Expr.cpp

@@ -206 +206 @@
         assert( aggregate->result );
 
-        // Deep copy on result type avoids mutation on transitively multiply referenced object.
-        //
-        // Example, adapted from parts of builtins and bootloader:
-        //
-        // forall(dtype T)
-        // struct __Destructor {
-        //   T * object;
-        //   void (*dtor)(T *);
-        // };
-        //
-        // forall(dtype S)
-        // void foo(__Destructor(S) &d) {
-        //   if (d.dtor) {  // here
-        //   }
-        // }
-        //
-        // Let e be the "d.dtor" guard espression, which is MemberExpr after resolve.  Let d be the
-        // declaration of member __Destructor.dtor (an ObjectDecl), as accessed via the top-level
-        // declaration of __Destructor.  Consider the types e.result and d.type.  In the old AST, one
-        // is a clone of the other.  Ordinary new-AST use would set them up as a multiply-referenced
-        // object.
-        //
-        // e.result: PointerType
-        // .base: FunctionType
-        // .params.front(): ObjectDecl, the anonymous parameter of type T*
-        // .type: PointerType
-        // .base: TypeInstType
-        // let x = that
-        // let y = similar, except start from d.type
-        //
-        // Consider two code lines down, genericSubstitution(...).apply(result).
-        //
-        // Applying this chosen-candidate's type substitution means modifying x, substituting
-        // S for T.  This mutation should affect x and not y.
-
-        result = deepCopy(mem->get_type());
+        result = mem->get_type();
 
         // substitute aggregate generic parameters into member type

src/AST/Expr.hpp

@@ -112 +112 @@
 
                 bool hasSlots() const { return data.resnSlots; }
+                bool hasParams() const { return data.inferParams; }
 
                 ResnSlots& resnSlots() {

src/AST/Fwd.hpp

@@ -139 +139 @@
 struct TranslationUnit;
 // TODO: Get from the TranslationUnit:
-extern Type * sizeType;
-extern FunctionDecl * dereferenceOperator;
-extern StructDecl   * dtorStruct;
-extern FunctionDecl * dtorStructDestroy;
+extern ptr<Type> sizeType;
+extern const FunctionDecl * dereferenceOperator;
+extern const StructDecl   * dtorStruct;
+extern const FunctionDecl * dtorStructDestroy;
 
 }

src/AST/Pass.hpp

@@ -34 +34 @@
 
 #include "AST/SymbolTable.hpp"
-
-#include "AST/ForallSubstitutionTable.hpp"
 
 // Private prelude header, needed for some of the magic tricks this class pulls off
@@ -66 +64 @@
 // | WithVisitorRef        - provides an pointer to the templated visitor wrapper
 // | WithSymbolTable       - provides symbol table functionality
-// | WithForallSubstitutor - maintains links between TypeInstType and TypeDecl under mutation
 //
 // Other Special Members:
@@ -258 +255 @@
         container_t< ptr<node_t> > call_accept( const container_t< ptr<node_t> > & container );
 
-        /// Mutate forall-list, accounting for presence of type substitution map
-        template<typename node_t>
-        void mutate_forall( const node_t *& );
-
 public:
         /// Logic to call the accept and mutate the parent if needed, delegates call to accept
@@ -287 +280 @@
         /// Internal RAII guard for forall substitutions
         struct guard_forall_subs {
-                guard_forall_subs( Pass<core_t> & pass, const ParameterizedType * type )
+                guard_forall_subs( Pass<core_t> & pass, const FunctionType * type )
                 : pass( pass ), type( type ) { __pass::forall::enter(pass.core, 0, type ); }
                 ~guard_forall_subs()         { __pass::forall::leave(pass.core, 0, type ); }
                 Pass<core_t> & pass;
-                const ParameterizedType * type;
+                const FunctionType * type;
         };
 
@@ -398 +391 @@
 };
 
-/// Use when the templated visitor needs to keep TypeInstType instances properly linked to TypeDecl
-struct WithForallSubstitutor {
-        ForallSubstitutionTable subs;
-};
-
 }
 

src/AST/Pass.impl.hpp

@@ -367 +367 @@
         }
 
-
-        template< typename core_t >
-        template< typename node_t >
-        void ast::Pass< core_t >::mutate_forall( const node_t *& node ) {
-                if ( auto subs = __pass::forall::subs( core, 0 ) ) {
-                        // tracking TypeDecl substitution, full clone
-                        if ( node->forall.empty() ) return;
-
-                        node_t * mut = __pass::mutate<core_t>( node );
-                        mut->forall = subs->clone( node->forall, *this );
-                        node = mut;
-                } else {
-                        // not tracking TypeDecl substitution, just mutate
-                        maybe_accept( node, &node_t::forall );
-                }
-        }
 }
 
@@ -504 +488 @@
                         __pass::symtab::addId( core, 0, func );
                         VISIT(
-                                // parameter declarations are now directly here
+                                // parameter declarations
                                 maybe_accept( node, &FunctionDecl::params );
                                 maybe_accept( node, &FunctionDecl::returns );
-                                // foralls are still in function type
-                                maybe_accept( node, &FunctionDecl::type );
+                                // type params and assertions
+                                maybe_accept( node, &FunctionDecl::type_params );
+                                maybe_accept( node, &FunctionDecl::assertions );
                                 // First remember that we are now within a function.
                                 ValueGuard< bool > oldInFunction( inFunction );
@@ -609 +594 @@
         VISIT({
                 guard_symtab guard { *this };
-                maybe_accept( node, &TypeDecl::params );
                 maybe_accept( node, &TypeDecl::base   );
         })
@@ -638 +622 @@
         VISIT({
                 guard_symtab guard { *this };
-                maybe_accept( node, &TypedefDecl::params );
                 maybe_accept( node, &TypedefDecl::base   );
         })
@@ -1760 +1743 @@
 
         VISIT({
-                guard_forall_subs forall_guard { *this, node };
-                mutate_forall( node );
+                // guard_forall_subs forall_guard { *this, node };
+                // mutate_forall( node );
+                maybe_accept( node, &FunctionType::assertions );
                 maybe_accept( node, &FunctionType::returns );
                 maybe_accept( node, &FunctionType::params  );
@@ -1779 +1763 @@
         VISIT({
                 guard_symtab guard { *this };
-                guard_forall_subs forall_guard { *this, node };
-                mutate_forall( node );
                 maybe_accept( node, &StructInstType::params );
         })
@@ -1797 +1779 @@
         VISIT({
                 guard_symtab guard { *this };
-                guard_forall_subs forall_guard { *this, node };
-                mutate_forall( node );
                 maybe_accept( node, &UnionInstType::params );
         })
@@ -1812 +1792 @@
 
         VISIT({
-                guard_forall_subs forall_guard { *this, node };
-                mutate_forall( node );
                 maybe_accept( node, &EnumInstType::params );
         })
@@ -1827 +1805 @@
 
         VISIT({
-                guard_forall_subs forall_guard { *this, node };
-                mutate_forall( node );
                 maybe_accept( node, &TraitInstType::params );
         })
@@ -1843 +1819 @@
         VISIT(
                 {
-                        guard_forall_subs forall_guard { *this, node };
-                        mutate_forall( node );
                         maybe_accept( node, &TypeInstType::params );
                 }
@@ -1993 +1967 @@
                 {
                         bool mutated = false;
-                        std::unordered_map< std::string, ast::ptr< ast::Type > > new_map;
+                        std::unordered_map< ast::TypeInstType::TypeEnvKey, ast::ptr< ast::Type > > new_map;
                         for ( const auto & p : node->typeEnv ) {
                                 guard_symtab guard { *this };
@@ -2006 +1980 @@
                         }
                 }
-
-                {
-                        bool mutated = false;
-                        std::unordered_map< std::string, ast::ptr< ast::Expr > > new_map;
-                        for ( const auto & p : node->varEnv ) {
-                                guard_symtab guard { *this };
-                                auto new_node = p.second->accept( *this );
-                                if (new_node != p.second) mutated = true;
-                                new_map.insert({ p.first, new_node });
-                        }
-                        if (mutated) {
-                                auto new_node = __pass::mutate<core_t>( node );
-                                new_node->varEnv.swap( new_map );
-                                node = new_node;
-                        }
-                }
         )
 

src/AST/Pass.proto.hpp

@@ -396 +396 @@
                 // Some simple scoping rules
                 template<typename core_t>
-                static inline auto enter( core_t & core, int, const ast::ParameterizedType * type )
+                static inline auto enter( core_t & core, int, const ast::FunctionType * type )
                 -> decltype( core.subs, void() ) {
                         if ( ! type->forall.empty() ) core.subs.beginScope();
@@ -402 +402 @@
 
                 template<typename core_t>
-                static inline auto enter( core_t &, long, const ast::ParameterizedType * ) {}
-
-                template<typename core_t>
-                static inline auto leave( core_t & core, int, const ast::ParameterizedType * type )
+                static inline auto enter( core_t &, long, const ast::FunctionType * ) {}
+
+                template<typename core_t>
+                static inline auto leave( core_t & core, int, const ast::FunctionType * type )
                 -> decltype( core.subs, void() ) {
                         if ( ! type->forall.empty() ) { core.subs.endScope(); }
@@ -411 +411 @@
 
                 template<typename core_t>
-                static inline auto leave( core_t &, long, const ast::ParameterizedType * ) {}
-
-                // Get the substitution table, if present
-                template<typename core_t>
-                static inline auto subs( core_t & core, int ) -> decltype( &core.subs ) {
-                        return &core.subs;
-                }
-
-                template<typename core_t>
-                static inline ast::ForallSubstitutionTable * subs( core_t &, long ) { return nullptr; }
+                static inline auto leave( core_t &, long, const ast::FunctionType * ) {}
 
                 // Replaces a TypeInstType's base TypeDecl according to the table

src/AST/Print.cpp

@@ -146 +146 @@
         }
 
-        void print( const ast::ParameterizedType::ForallList & forall ) {
+        void print( const ast::FunctionType::ForallList & forall ) {
                 if ( forall.empty() ) return;
                 os << "forall" << endl;
                 ++indent;
                 printAll( forall );
+                os << indent;
+                --indent;
+        }
+
+        void print( const ast::FunctionType::AssertionList & assts ) {
+                if (assts.empty()) return;
+                os << "with assertions" << endl;
+                ++indent;
+                printAll(assts);
                 os << indent;
                 --indent;
@@ -206 +215 @@
         void preprint( const ast::NamedTypeDecl * node ) {
                 if ( ! node->name.empty() ) {
-                        if( deterministic_output && isUnboundType(node->name) ) os << "[unbound]:";
-                        else os << node->name << ": ";
+                        os << node->name << ": ";
                 }
 
@@ -224 +232 @@
                 }
 
-                if ( ! node->params.empty() ) {
-                        os << endl << indent << "... with parameters" << endl;
-                        ++indent;
-                        printAll( node->params );
-                        --indent;
-                }
-
                 if ( ! node->assertions.empty() ) {
                         os << endl << indent << "... with assertions" << endl;
@@ -266 +267 @@
         }
 
-        void preprint( const ast::ParameterizedType * node ) {
+        void preprint( const ast::FunctionType * node ) {
                 print( node->forall );
+                print( node->assertions );
                 print( node->qualifiers );
         }
 
         void preprint( const ast::BaseInstType * node ) {
-                print( node->forall );
                 print( node->attributes );
                 print( node->qualifiers );
@@ -1383 +1384 @@
         virtual const ast::Type * visit( const ast::TypeInstType * node ) override final {
                 preprint( node );
-                const auto & _name = deterministic_output && isUnboundType(node) ? "[unbound]" : node->name;
+                const auto & _name = deterministic_output && isUnboundType(node) ? "[unbound]" : node->typeString();
                 os << "instance of type " << _name
                    << " (" << (node->kind == ast::TypeDecl::Ftype ? "" : "not ") << "function type)";
@@ -1510 +1511 @@
                 os << indent << "Types:" << endl;
                 for ( const auto& i : *node ) {
-                        os << indent+1 << i.first << " -> ";
+                        os << indent+1 << i.first.typeString() << " -> ";
                         indent += 2;
                         safe_print( i.second );
-                        indent -= 2;
-                        os << endl;
-                }
-                os << indent << "Non-types:" << endl;
-                for ( auto i = node->beginVar(); i != node->endVar(); ++i ) {
-                        os << indent+1 << i->first << " -> ";
-                        indent += 2;
-                        safe_print( i->second );
                         indent -= 2;
                         os << endl;

src/AST/SymbolTable.cpp

@@ -414 +414 @@
 
 void SymbolTable::addFunction( const FunctionDecl * func ) {
-        addTypes( func->type->forall );
+        for (auto & td : func->type_params) {
+                addType(td);
+        }
+        for (auto & asst : func->assertions) {
+                addId(asst);
+        }
+        // addTypes( func->type->forall );
         addIds( func->returns );
         addIds( func->params );

src/AST/TranslationUnit.hpp

@@ -29 +29 @@
                 std::map< UniqueId, Decl * > idMap;
 
-                Type * sizeType;
-                FunctionDecl * dereference;
-                StructDecl * dtorStruct;
-                FunctionDecl * dtorDestroy;
+                const Type * sizeType;
+                const FunctionDecl * dereference;
+                const StructDecl * dtorStruct;
+                const FunctionDecl * dtorDestroy;
         } global;
 };

src/AST/Type.cpp

@@ -21 +21 @@
 
 #include "Decl.hpp"
-#include "ForallSubstitutor.hpp" // for substituteForall
 #include "Init.hpp"
 #include "Common/utility.h"      // for copy, move
@@ -92 +91 @@
 // GENERATED END
 
-// --- ParameterizedType
-
-void ParameterizedType::initWithSub(
-        const ParameterizedType & o, Pass< ForallSubstitutor > & sub
-) {
-        forall = sub.core( o.forall );
-}
-
 // --- FunctionType
-
-
-FunctionType::FunctionType( const FunctionType & o )
-: ParameterizedType( o.qualifiers, copy( o.attributes ) ), returns(), params(),
-  isVarArgs( o.isVarArgs ) {
-        Pass< ForallSubstitutor > sub;
-        initWithSub( o, sub );           // initialize substitution map
-        returns = sub.core( o.returns ); // apply to return and parameter types
-        params = sub.core( o.params );
-}
-
 namespace {
         bool containsTtype( const std::vector<ptr<Type>> & l ) {
@@ -123 +103 @@
 bool FunctionType::isTtype() const {
         return containsTtype( returns ) || containsTtype( params );
-}
-
-// --- BaseInstType
-
-void BaseInstType::initWithSub( const BaseInstType & o, Pass< ForallSubstitutor > & sub ) {
-        ParameterizedType::initWithSub( o, sub ); // initialize substitution
-        params = sub.core( o.params );            // apply to parameters
-}
-
-BaseInstType::BaseInstType( const BaseInstType & o )
-: ParameterizedType( o.qualifiers, copy( o.attributes ) ), params(), name( o.name ),
-  hoistType( o.hoistType ) {
-        Pass< ForallSubstitutor > sub;
-        initWithSub( o, sub );
 }
 
@@ -177 +143 @@
 : BaseInstType( b->name, q, move(as) ), base( b ) {}
 
-// --- TypeInstType
-
-TypeInstType::TypeInstType( const TypeInstType & o )
-: BaseInstType( o.name, o.qualifiers, copy( o.attributes ) ), base(), kind( o.kind ) {
-        Pass< ForallSubstitutor > sub;
-        initWithSub( o, sub );      // initialize substitution
-        base = sub.core( o.base );  // apply to base type
-}
-
 void TypeInstType::set_base( const TypeDecl * b ) {
         base = b;
@@ -222 +179 @@
                 // TODO: once TypeInstType representation is updated, it should properly check
                 // if the context id is filled. this is a temporary hack for now
-                return isUnboundType(typeInst->name);
-        }
-        return false;
-}
-
-bool isUnboundType(const std::string & tname) {
-        // xxx - look for a type name produced by renameTyVars.
-
-        // TODO: once TypeInstType representation is updated, it should properly check
-        // if the context id is filled. this is a temporary hack for now
-        if (std::count(tname.begin(), tname.end(), '_') >= 3) {
-                return true;
+                return typeInst->formal_usage > 0;
         }
         return false;

src/AST/Type.hpp

@@ -36 +36 @@
 
 template< typename T > class Pass;
-
-struct ForallSubstitutor;
 
 class Type : public Node {
@@ -267 +265 @@
 };
 
-/// Base type for potentially forall-qualified types
-class ParameterizedType : public Type {
-protected:
-        /// initializes forall with substitutor
-        void initWithSub( const ParameterizedType & o, Pass< ForallSubstitutor > & sub );
-public:
-        using ForallList = std::vector<ptr<TypeDecl>>;
-
-        ForallList forall;
-
-        ParameterizedType( ForallList&& fs = {}, CV::Qualifiers q = {},
-                std::vector<ptr<Attribute>> && as = {} )
-        : Type(q, std::move(as)), forall(std::move(fs)) {}
-
-        ParameterizedType( CV::Qualifiers q, std::vector<ptr<Attribute>> && as = {} )
-        : Type(q, std::move(as)), forall() {}
-
-        // enforce use of ForallSubstitutor to copy parameterized type
-        ParameterizedType( const ParameterizedType & ) = delete;
-
-        ParameterizedType( ParameterizedType && ) = default;
-
-        // no need to change destructor, and operator= deleted in Node
-
-private:
-        virtual ParameterizedType * clone() const override = 0;
-        MUTATE_FRIEND
-};
-
 /// Function variable arguments flag
 enum ArgumentFlag { FixedArgs, VariableArgs };
 
 /// Type of a function `[R1, R2](*)(P1, P2, P3)`
-class FunctionType final : public ParameterizedType {
-public:
+class FunctionType final : public Type {
+public:
+        using ForallList = std::vector<ptr<TypeInstType>>;
+        using AssertionList = std::vector<ptr<VariableExpr>>;
+        ForallList forall;
+        AssertionList assertions;
+
         std::vector<ptr<Type>> returns;
         std::vector<ptr<Type>> params;
@@ -313 +287 @@
 
         FunctionType( ArgumentFlag va = FixedArgs, CV::Qualifiers q = {} )
-        : ParameterizedType(q), returns(), params(), isVarArgs(va) {}
-
-        FunctionType( const FunctionType & o );
+        : Type(q), returns(), params(), isVarArgs(va) {}
+
+        FunctionType( const FunctionType & o ) = default;
 
         /// true if either the parameters or return values contain a tttype
@@ -329 +303 @@
 
 /// base class for types that refer to types declared elsewhere (aggregates and typedefs)
-class BaseInstType : public ParameterizedType {
-protected:
-        /// Initializes forall and parameters based on substitutor
-        void initWithSub( const BaseInstType & o, Pass< ForallSubstitutor > & sub );
+class BaseInstType : public Type {
 public:
         std::vector<ptr<Expr>> params;
@@ -340 +311 @@
         BaseInstType(
                 const std::string& n, CV::Qualifiers q = {}, std::vector<ptr<Attribute>> && as = {} )
-        : ParameterizedType(q, std::move(as)), params(), name(n) {}
+        : Type(q, std::move(as)), params(), name(n) {}
 
         BaseInstType(
                 const std::string& n, std::vector<ptr<Expr>> && params,
                 CV::Qualifiers q = {}, std::vector<ptr<Attribute>> && as = {} )
-        : ParameterizedType(q, std::move(as)), params(std::move(params)), name(n) {}
-
-        BaseInstType( const BaseInstType & o );
+        : Type(q, std::move(as)), params(std::move(params)), name(n) {}
+
+        BaseInstType( const BaseInstType & o ) = default;
 
         /// Gets aggregate declaration this type refers to
@@ -423 +394 @@
 public:
         readonly<TypeDecl> base;
+        // previously from renameTyVars; now directly use integer fields instead of synthesized strings
+        // a nonzero value of formal_usage indicates a formal type (only used in function type)
+        // a zero value of formal_usage indicates an actual type (referenced inside body of parametric structs and functions)
         TypeDecl::Kind kind;
+        int formal_usage;
+        int expr_id;
+
+        // compact representation used for map lookups.
+        struct TypeEnvKey { 
+                const TypeDecl * base;
+                int formal_usage;
+                int expr_id;
+
+                TypeEnvKey() = default;
+                TypeEnvKey(const TypeDecl * base, int formal_usage = 0, int expr_id = 0): base(base), formal_usage(formal_usage), expr_id(expr_id) {}
+                TypeEnvKey(const TypeInstType & inst): base(inst.base), formal_usage(inst.formal_usage), expr_id(inst.expr_id) {}
+                std::string typeString() const { return std::string("_") + std::to_string(formal_usage) + "_" + std::to_string(expr_id) + "_" + base->name; }
+                bool operator==(const TypeEnvKey & other) const { return base == other.base && formal_usage == other.formal_usage && expr_id == other.expr_id; }
+
+        };
+
+        bool operator==(const TypeInstType & other) const { return base == other.base && formal_usage == other.formal_usage && expr_id == other.expr_id; }
 
         TypeInstType(
@@ -433 +425 @@
         : BaseInstType( n, q, std::move(as) ), base(), kind( k ) {}
 
-        TypeInstType( const TypeInstType & o );
+        TypeInstType( const TypeInstType & o ) = default;
+
+        TypeInstType( const TypeEnvKey & key )
+        : BaseInstType(key.base->name), base(key.base), kind(key.base->kind), formal_usage(key.formal_usage), expr_id(key.expr_id) {}
 
         /// sets `base`, updating `kind` correctly
@@ -444 +439 @@
 
         const Type * accept( Visitor & v ) const override { return v.visit( this ); }
+
+        std::string typeString() const { 
+                if (formal_usage > 0) return std::string("_") + std::to_string(formal_usage) + "_" + std::to_string(expr_id) + "_" + name; 
+                else return name;
+        }
 private:
         TypeInstType * clone() const override { return new TypeInstType{ *this }; }
@@ -536 +536 @@
 
 bool isUnboundType(const Type * type);
-bool isUnboundType(const std::string & tname);
-
+
+}
+
+namespace std {
+        template<>
+        struct hash<typename ast::TypeInstType::TypeEnvKey> {
+                size_t operator() (const ast::TypeInstType::TypeEnvKey & x) const {
+                        const size_t p = 1000007;
+                        size_t res = reinterpret_cast<size_t>(x.base);
+                        res = p * res + x.formal_usage;
+                        res = p * res + x.expr_id;
+                        return res;
+                } 
+        };
 }
 

src/AST/TypeEnvironment.cpp

@@ -52 +52 @@
         for ( const auto & i : open ) {
                 if ( first ) { first = false; } else { out << ' '; }
-                out << i.first << "(" << i.second << ")";
+                out << i.first.typeString() << "(" << i.second << ")";
         }
 }
@@ -62 +62 @@
                 if(first) first = false;
                 else out << " ";
-                if( deterministic_output && isUnboundType(var) ) out << "[unbound]";
-                else out << var;
+
+                if( deterministic_output ) out << "[unbound]";
+                else out << "_" << var.formal_usage << "_" << var.expr_id << "_";
+
+                out << var.base->name;
         }
         out << ")";
@@ -79 +82 @@
 }
 
-const EqvClass * TypeEnvironment::lookup( const std::string & var ) const {
+const EqvClass * TypeEnvironment::lookup( const TypeInstType::TypeEnvKey & var ) const {
         for ( ClassList::const_iterator i = env.begin(); i != env.end(); ++i ) {
                 if ( i->vars.find( var ) != i->vars.end() ) return &*i;
@@ -105 +108 @@
 }
 
-void TypeEnvironment::add( const ParameterizedType::ForallList & tyDecls ) {
-        for ( const TypeDecl * tyDecl : tyDecls ) {
+void TypeEnvironment::add( const FunctionType::ForallList & tyDecls ) {
+        for ( auto & tyDecl : tyDecls ) {
                 env.emplace_back( tyDecl );
         }
@@ -119 +122 @@
 void TypeEnvironment::writeToSubstitution( TypeSubstitution & sub ) const {
         for ( const auto & clz : env ) {
-                std::string clzRep;
+                TypeInstType::TypeEnvKey clzRep;
+                bool first = true;
                 for ( const auto & var : clz.vars ) {
                         if ( clz.bound ) {
                                 sub.add( var, clz.bound );
-                        } else if ( clzRep.empty() ) {
+                        } else if ( first ) {
                                 clzRep = var;
+                                first = false;
                         } else {
-                                sub.add( var, new TypeInstType{ clzRep, clz.data.kind } );
+                                sub.add( var, new TypeInstType{ clzRep } );
                         }
                 }
@@ -141 +146 @@
         struct Occurs : public ast::WithVisitorRef<Occurs> {
                 bool result;
-                std::set< std::string > vars;
+                std::unordered_set< TypeInstType::TypeEnvKey > vars;
                 const TypeEnvironment & tenv;
 
-                Occurs( const std::string & var, const TypeEnvironment & env )
+                Occurs( const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env )
                 : result( false ), vars(), tenv( env ) {
                         if ( const EqvClass * clz = tenv.lookup( var ) ) {
@@ -154 +159 @@
 
                 void previsit( const TypeInstType * typeInst ) {
-                        if ( vars.count( typeInst->name ) ) {
+                        if ( vars.count( *typeInst ) ) {
                                 result = true;
-                        } else if ( const EqvClass * clz = tenv.lookup( typeInst->name ) ) {
+                        } else if ( const EqvClass * clz = tenv.lookup( *typeInst ) ) {
                                 if ( clz->bound ) {
                                         clz->bound->accept( *visitor );
@@ -165 +170 @@
 
         /// true if `var` occurs in `ty` under `env`
-        bool occurs( const Type * ty, const std::string & var, const TypeEnvironment & env ) {
+        bool occurs( const Type * ty, const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env ) {
                 Pass<Occurs> occur{ var, env };
                 maybe_accept( ty, occur );
@@ -280 +285 @@
         // remove references from bound type, so that type variables can only bind to value types
         ptr<Type> target = bindTo->stripReferences();
-        auto tyvar = open.find( typeInst->name );
+        auto tyvar = open.find( *typeInst );
         assert( tyvar != open.end() );
         if ( ! tyVarCompatible( tyvar->second, target ) ) return false;
-        if ( occurs( target, typeInst->name, *this ) ) return false;
-
-        auto it = internal_lookup( typeInst->name );
+        if ( occurs( target, *typeInst, *this ) ) return false;
+
+        auto it = internal_lookup( *typeInst );
         if ( it != env.end() ) {
                 if ( it->bound ) {
@@ -308 +313 @@
         } else {
                 env.emplace_back(
-                        typeInst->name, target, widen.first && widen.second, data );
+                        *typeInst, target, widen.first && widen.second, data );
         }
         return true;
@@ -318 +323 @@
                 WidenMode widen, const SymbolTable & symtab
 ) {
-        auto c1 = internal_lookup( var1->name );
-        auto c2 = internal_lookup( var2->name );
+        auto c1 = internal_lookup( *var1 );
+        auto c2 = internal_lookup( *var2 );
 
         // exit early if variables already bound together
@@ -333 +338 @@
         if ( c1 != env.end() ) {
                 if ( c1->bound ) {
-                        if ( occurs( c1->bound, var2->name, *this ) ) return false;
+                        if ( occurs( c1->bound, *var2, *this ) ) return false;
                         type1 = c1->bound;
                 }
@@ -340 +345 @@
         if ( c2 != env.end() ) {
                 if ( c2->bound ) {
-                        if ( occurs( c2->bound, var1->name, *this ) ) return false;
+                        if ( occurs( c2->bound, *var1, *this ) ) return false;
                         type2 = c2->bound;
                 }
@@ -378 +383 @@
         } else if ( c1 != env.end() ) {
                 // var2 unbound, add to env[c1]
-                c1->vars.emplace( var2->name );
+                c1->vars.emplace( *var2 );
                 c1->allowWidening = widen1;
                 c1->data.isComplete |= data.isComplete;
         } else if ( c2 != env.end() ) {
                 // var1 unbound, add to env[c2]
-                c2->vars.emplace( var1->name );
+                c2->vars.emplace( *var1 );
                 c2->allowWidening = widen2;
                 c2->data.isComplete |= data.isComplete;
         } else {
                 // neither var bound, create new class
-                env.emplace_back( var1->name, var2->name, widen1 && widen2, data );
+                env.emplace_back( *var1, *var2, widen1 && widen2, data );
         }
 
@@ -452 +457 @@
 }
 
-TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const std::string & var ) {
+TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const TypeInstType::TypeEnvKey & var ) {
         for ( ClassList::iterator i = env.begin(); i != env.end(); ++i ) {
                 if ( i->vars.count( var ) ) return i;

src/AST/TypeEnvironment.hpp

@@ -55 +55 @@
 /// recorded. More investigation is needed.
 struct AssertCompare {
-        bool operator()( const DeclWithType * d1, const DeclWithType * d2 ) const {
-                int cmp = d1->name.compare( d2->name );
-                return cmp < 0 || ( cmp == 0 && d1->get_type() < d2->get_type() );
+        bool operator()( const VariableExpr * d1, const VariableExpr * d2 ) const {
+                int cmp = d1->var->name.compare( d2->var->name );
+                return cmp < 0 || ( cmp == 0 && d1->result < d2->result );
         }
 };
@@ -70 +70 @@
 
 /// Set of assertions pending satisfaction
-using AssertionSet = std::map< readonly<DeclWithType>, AssertionSetValue, AssertCompare >;
+using AssertionSet = std::map< const VariableExpr *, AssertionSetValue, AssertCompare >;
 
 /// Set of open variables
-using OpenVarSet = std::unordered_map< std::string, TypeDecl::Data >;
+using OpenVarSet = std::unordered_map< TypeInstType::TypeEnvKey, TypeDecl::Data >;
 
 /// Merges one set of open vars into another
@@ -89 +89 @@
 /// they bind to.
 struct EqvClass {
-        std::set< std::string > vars;
+        std::unordered_set< TypeInstType::TypeEnvKey > vars;
         ptr<Type> bound;
         bool allowWidening;
@@ -101 +101 @@
 
         /// Singleton class constructor from TypeDecl
-        EqvClass( const TypeDecl * decl )
-        : vars{ decl->name }, bound(), allowWidening( true ), data( decl ) {}
+        EqvClass( const TypeInstType * inst )
+        : vars{ *inst }, bound(), allowWidening( true ), data( inst->base ) {}
 
         /// Singleton class constructor from substitution
-        EqvClass( const std::string & v, const Type * b )
+        EqvClass( const TypeInstType::TypeEnvKey & v, const Type * b )
         : vars{ v }, bound( b ), allowWidening( false ), data( TypeDecl::Dtype, false ) {}
 
         /// Single-var constructor (strips qualifiers from bound type)
-        EqvClass( const std::string & v, const Type * b, bool w, const TypeDecl::Data & d )
+        EqvClass( const TypeInstType::TypeEnvKey & v, const Type * b, bool w, const TypeDecl::Data & d )
         : vars{ v }, bound( b ), allowWidening( w ), data( d ) {
                 reset_qualifiers( bound );
@@ -115 +115 @@
 
         /// Double-var constructor
-        EqvClass( const std::string & v, const std::string & u, bool w, const TypeDecl::Data & d )
+        EqvClass( const TypeInstType::TypeEnvKey & v, const TypeInstType::TypeEnvKey & u, bool w, const TypeDecl::Data & d )
         : vars{ v, u }, bound(), allowWidening( w ), data( d ) {}
 
@@ -131 +131 @@
 public:
         /// Finds the equivalence class containing a variable; nullptr for none such
-        const EqvClass * lookup( const std::string & var ) const;
+        const EqvClass * lookup( const TypeInstType::TypeEnvKey & var ) const;
 
         /// Add a new equivalence class for each type variable
-        void add( const ParameterizedType::ForallList & tyDecls );
+        void add( const FunctionType::ForallList & tyDecls );
 
         /// Add a new equivalence class for each branch of the substitution, checking for conflicts
@@ -207 +207 @@
 
         /// Private lookup API; returns array index of string, or env.size() for not found
-        ClassList::iterator internal_lookup( const std::string & );
+        ClassList::iterator internal_lookup( const TypeInstType::TypeEnvKey & );
 };
 

src/AST/TypeSubstitution.cpp

@@ -39 +39 @@
 void TypeSubstitution::initialize( const TypeSubstitution &src, TypeSubstitution &dest ) {
         dest.typeEnv.clear();
-        dest.varEnv.clear();
         dest.add( src );
 }
@@ -47 +46 @@
                 typeEnv[ i->first ] = i->second;
         } // for
-        for ( VarEnvType::const_iterator i = other.varEnv.begin(); i != other.varEnv.end(); ++i ) {
-                varEnv[ i->first ] = i->second;
-        } // for
 }
 
-void TypeSubstitution::add( std::string formalType, const Type *actualType ) {
-        typeEnv[ formalType ] = actualType;
+void TypeSubstitution::add( const TypeInstType * formalType, const Type *actualType ) {
+        typeEnv[ *formalType ] = actualType;
 }
 
-void TypeSubstitution::addVar( std::string formalExpr, const Expr *actualExpr ) {
-        varEnv[ formalExpr ] = actualExpr;
+void TypeSubstitution::add( const TypeInstType::TypeEnvKey & key, const Type * actualType) {
+        typeEnv[ key ] = actualType;
 }
 
-void TypeSubstitution::remove( std::string formalType ) {
-        TypeEnvType::iterator i = typeEnv.find( formalType );
+void TypeSubstitution::remove( const TypeInstType * formalType ) {
+        TypeEnvType::iterator i = typeEnv.find( *formalType );
         if ( i != typeEnv.end() ) {
-                typeEnv.erase( formalType );
+                typeEnv.erase( *formalType );
         } // if
 }
 
-const Type *TypeSubstitution::lookup( std::string formalType ) const {
-        TypeEnvType::const_iterator i = typeEnv.find( formalType );
+const Type *TypeSubstitution::lookup( const TypeInstType * formalType ) const {
+        TypeEnvType::const_iterator i = typeEnv.find( *formalType );
 
         // break on not in substitution set
@@ -75 +71 @@
         // attempt to transitively follow TypeInstType links.
         while ( const TypeInstType *actualType = i->second.as<TypeInstType>()) {
-                const std::string& typeName = actualType->name;
-
                 // break cycles in the transitive follow
-                if ( formalType == typeName ) break;
+                if ( *formalType == *actualType ) break;
 
                 // Look for the type this maps to, returning previous mapping if none-such
-                i = typeEnv.find( typeName );
+                i = typeEnv.find( *actualType );
                 if ( i == typeEnv.end() ) return actualType;
         }
@@ -90 +84 @@
 
 bool TypeSubstitution::empty() const {
-        return typeEnv.empty() && varEnv.empty();
+        return typeEnv.empty();
 }
 
@@ -98 +92 @@
                 TypeSubstitution * newEnv;
                 EnvTrimmer( const TypeSubstitution * env, TypeSubstitution * newEnv ) : env( env ), newEnv( newEnv ){}
-                void previsit( TypeDecl * tyDecl ) {
+                void previsit( FunctionType * ftype ) {
                         // transfer known bindings for seen type variables
-                        if ( const Type * t = env->lookup( tyDecl->name ) ) {
-                                newEnv->add( tyDecl->name, t );
+                        for (auto & formal : ftype->forall) {
+                                if ( const Type * t = env->lookup( formal ) ) {
+                                        newEnv->add( formal, t );
+                                }
                         }
                 }
@@ -130 +126 @@
 
 const Type * TypeSubstitution::Substituter::postvisit( const TypeInstType *inst ) {
-        BoundVarsType::const_iterator bound = boundVars.find( inst->name );
+        BoundVarsType::const_iterator bound = boundVars.find( *inst );
         if ( bound != boundVars.end() ) return inst;
 
-        TypeEnvType::const_iterator i = sub.typeEnv.find( inst->name );
+        TypeEnvType::const_iterator i = sub.typeEnv.find( *inst );
         if ( i == sub.typeEnv.end() ) {
                 return inst;
@@ -141 +137 @@
                 // TODO: investigate preventing type variables from being bound to themselves in the first place.
                 if ( const TypeInstType * replacement = i->second.as<TypeInstType>() ) {
-                        if ( inst->name == replacement->name ) {
+                        if ( *inst == *replacement ) {
                                 return inst;
                         }
@@ -156 +152 @@
 }
 
-const Expr * TypeSubstitution::Substituter::postvisit( const NameExpr * nameExpr ) {
-        VarEnvType::const_iterator i = sub.varEnv.find( nameExpr->name );
-        if ( i == sub.varEnv.end() ) {
-                return nameExpr;
-        } else {
-                subCount++;
-                return i->second;
-        } // if
-}
-
-void TypeSubstitution::Substituter::previsit( const ParameterizedType * ptype ) {
+void TypeSubstitution::Substituter::previsit( const FunctionType * ptype ) {
         GuardValue( boundVars );
         // bind type variables from forall-qualifiers
         if ( freeOnly ) {
-                for ( const TypeDecl * tyvar : ptype->forall ) {
-                                boundVars.insert( tyvar->name );
+                for ( auto & tyvar : ptype->forall ) {
+                                boundVars.insert( *tyvar );
                 } // for
         } // if
 }
 
+/*
 void TypeSubstitution::Substituter::handleAggregateType( const BaseInstType * type ) {
         GuardValue( boundVars );
         // bind type variables from forall-qualifiers
         if ( freeOnly ) {
-                for ( const TypeDecl * tyvar : type->forall ) {
-                        boundVars.insert( tyvar->name );
-                } // for
                 // bind type variables from generic type instantiations
                 if ( auto decl = type->aggr() ) {
                         if ( ! type->params.empty() ) {
                                 for ( const TypeDecl * tyvar : decl->params ) {
-                                        boundVars.insert( tyvar->name );
+                                        boundVars.insert( *tyvar );
                                 } // for
                         } // if
@@ -201 +185 @@
         handleAggregateType( aggregateUseType );
 }
+*/
 
 } // namespace ast

src/AST/TypeSubstitution.hpp

@@ -69 +69 @@
         }
 
-        void add( std::string formalType, const Type *actualType );
+        void add( const TypeInstType * formalType, const Type *actualType );
+        void add( const TypeInstType::TypeEnvKey & key, const Type *actualType );
         void add( const TypeSubstitution &other );
-        void remove( std::string formalType );
-        const Type *lookup( std::string formalType ) const;
+        void remove( const TypeInstType * formalType );
+        const Type *lookup( const TypeInstType * formalType ) const;
         bool empty() const;
-
-        void addVar( std::string formalExpr, const Expr *actualExpr );
 
         template< typename FormalIterator, typename ActualIterator >
@@ -101 +100 @@
         friend class Pass;
 
-        typedef std::unordered_map< std::string, ptr<Type> > TypeEnvType;
-        typedef std::unordered_map< std::string, ptr<Expr> > VarEnvType;
+        typedef std::unordered_map< TypeInstType::TypeEnvKey, ptr<Type> > TypeEnvType;
         TypeEnvType typeEnv;
-        VarEnvType varEnv;
 
   public:
@@ -113 +110 @@
         auto   end() const -> decltype( typeEnv.  end() ) { return typeEnv.  end(); }
 
-        auto beginVar()       -> decltype( varEnv.begin() ) { return varEnv.begin(); }
-        auto   endVar()       -> decltype( varEnv.  end() ) { return varEnv.  end(); }
-        auto beginVar() const -> decltype( varEnv.begin() ) { return varEnv.begin(); }
-        auto   endVar() const -> decltype( varEnv.  end() ) { return varEnv.  end(); }
 };
 
+// this is the only place where type parameters outside a function formal may be substituted.
 template< typename FormalIterator, typename ActualIterator >
 void TypeSubstitution::add( FormalIterator formalBegin, FormalIterator formalEnd, ActualIterator actualBegin ) {
@@ -129 +123 @@
                         if ( const TypeExpr *actual = actualIt->template as<TypeExpr>() ) {
                                 if ( formal->name != "" ) {
-                                        typeEnv[ formal->name ] = actual->type;
+                                        typeEnv[ formal ] = actual->type;
                                 } // if
                         } else {
@@ -135 +129 @@
                         } // if
                 } else {
-                        // TODO: type check the formal and actual parameters
-                        if ( (*formalIt)->name != "" ) {
-                                varEnv[ (*formalIt)->name ] = *actualIt;
-                        } // if
+                        
                 } // if
         } // for
 }
+
+
 
 template< typename FormalIterator, typename ActualIterator >
@@ -147 +140 @@
         add( formalBegin, formalEnd, actualBegin );
 }
+
 
 } // namespace ast
@@ -164 +158 @@
 
                 const Type * postvisit( const TypeInstType * aggregateUseType );
-                const Expr * postvisit( const NameExpr * nameExpr );
 
                 /// Records type variable bindings from forall-statements
-                void previsit( const ParameterizedType * type );
+                void previsit( const FunctionType * type );
                 /// Records type variable bindings from forall-statements and instantiations of generic types
-                void handleAggregateType( const BaseInstType * type );
+                // void handleAggregateType( const BaseInstType * type );
 
-                void previsit( const StructInstType * aggregateUseType );
-                void previsit( const UnionInstType * aggregateUseType );
+                // void previsit( const StructInstType * aggregateUseType );
+                // void previsit( const UnionInstType * aggregateUseType );
 
                 const TypeSubstitution & sub;
                 int subCount = 0;
                 bool freeOnly;
-                typedef std::unordered_set< std::string > BoundVarsType;
+                typedef std::unordered_set< TypeInstType::TypeEnvKey > BoundVarsType;
                 BoundVarsType boundVars;
 

src/AST/module.mk

@@ -33 +33 @@
         AST/Expr.cpp \
         AST/Expr.hpp \
-        AST/ForallSubstitutionTable.cpp \
-        AST/ForallSubstitutionTable.hpp \
-        AST/ForallSubstitutor.hpp \
         AST/FunctionSpec.hpp \
         AST/Fwd.hpp \

src/Common/PassVisitor.impl.h

@@ -835 +835 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeAccept_impl( node->parameters, *this );
                 maybeAccept_impl( node->base      , *this );
         }
@@ -858 +857 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeAccept_impl( node->parameters, *this );
                 maybeAccept_impl( node->base      , *this );
         }
@@ -880 +878 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeMutate_impl( node->parameters, *this );
                 maybeMutate_impl( node->base      , *this );
         }
@@ -904 +901 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeAccept_impl( node->parameters, *this );
                 maybeAccept_impl( node->base      , *this );
         }
@@ -921 +917 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeAccept_impl( node->parameters, *this );
                 maybeAccept_impl( node->base      , *this );
         }
@@ -938 +933 @@
         {
                 auto guard = makeFuncGuard( [this]() { indexerScopeEnter(); }, [this]() { indexerScopeLeave(); } );
-                maybeMutate_impl( node->parameters, *this );
                 maybeMutate_impl( node->base      , *this );
         }

src/GenPoly/GenPoly.cc

@@ -115 +115 @@
                 if (!env) return type;
                 if (auto typeInst = dynamic_cast<const ast::TypeInstType*> (type)) {
-                        auto newType = env->lookup(typeInst->name);
+                        auto newType = env->lookup(typeInst);
                         if (newType) return newType;
                 }
@@ -172 +172 @@
 
                 if ( auto typeInst = dynamic_cast< const ast::TypeInstType * >( type ) ) {
-                        return tyVars.find(typeInst->name) != tyVars.end() ? type : nullptr;
+                        return tyVars.find(typeInst->typeString()) != tyVars.end() ? type : nullptr;
                 } else if ( auto arrayType = dynamic_cast< const ast::ArrayType * >( type ) ) {
                         return isPolyType( arrayType->base, env );
@@ -552 +552 @@
         }
 
-        void addToTyVarMap( const ast::TypeDecl * tyVar, TyVarMap & tyVarMap) {
-                tyVarMap.insert(tyVar->name, convData(ast::TypeDecl::Data{tyVar}));
+        void addToTyVarMap( const ast::TypeInstType * tyVar, TyVarMap & tyVarMap) {
+                tyVarMap.insert(tyVar->typeString(), convData(ast::TypeDecl::Data{tyVar->base}));
         }
 
@@ -567 +567 @@
 
         void makeTyVarMap(const ast::Type * type, TyVarMap & tyVarMap) {
-                if (auto ptype = dynamic_cast<const ast::ParameterizedType *>(type)) {
+                if (auto ptype = dynamic_cast<const ast::FunctionType *>(type)) {
                         for (auto & tyVar : ptype->forall) {
                                 assert (tyVar);

src/Parser/TypeData.cc

@@ -900 +900 @@
                 ret = new TypeDecl( name, scs, typebuild( td->base ), TypeDecl::Dtype, true );
         } // if
-        buildList( td->symbolic.params, ret->get_parameters() );
         buildList( td->symbolic.assertions, ret->get_assertions() );
         ret->base->attributes.splice( ret->base->attributes.end(), attributes );

src/ResolvExpr/AdjustExprType.cc

@@ -133 +133 @@
                 const ast::Type * postvisit( const ast::TypeInstType * inst ) {
                         // replace known function-type-variables with pointer-to-function
-                        if ( const ast::EqvClass * eqvClass = tenv.lookup( inst->name ) ) {
+                        if ( const ast::EqvClass * eqvClass = tenv.lookup( *inst ) ) {
                                 if ( eqvClass->data.kind == ast::TypeDecl::Ftype ) {
                                         return new ast::PointerType{ inst };

src/ResolvExpr/CandidateFinder.cpp

@@ -212 +212 @@
                 // mark type variable and specialization cost of forall clause
                 convCost.incVar( function->forall.size() );
-                for ( const ast::TypeDecl * td : function->forall ) {
-                        convCost.decSpec( td->assertions.size() );
-                }
+                convCost.decSpec( function->assertions.size() );
 
                 return convCost;
@@ -220 +218 @@
 
         void makeUnifiableVars(
-                const ast::ParameterizedType * type, ast::OpenVarSet & unifiableVars,
+                const ast::FunctionType * type, ast::OpenVarSet & unifiableVars,
                 ast::AssertionSet & need
         ) {
-                for ( const ast::TypeDecl * tyvar : type->forall ) {
-                        unifiableVars[ tyvar->name ] = ast::TypeDecl::Data{ tyvar };
-                        for ( const ast::DeclWithType * assn : tyvar->assertions ) {
-                                need[ assn ].isUsed = true;
-                        }
+                for ( auto & tyvar : type->forall ) {
+                        unifiableVars[ *tyvar ] = ast::TypeDecl::Data{ tyvar->base };
+                }
+                for ( auto & assn : type->assertions ) {
+                        need[ assn ].isUsed = true;
                 }
         }
@@ -953 +951 @@
                                                 auto inst = dynamic_cast< const ast::TypeInstType * >( funcResult )
                                         ) {
-                                                if ( const ast::EqvClass * clz = func->env.lookup( inst->name ) ) {
+                                                if ( const ast::EqvClass * clz = func->env.lookup( *inst ) ) {
                                                         if ( auto function = clz->bound.as< ast::FunctionType >() ) {
                                                                 CandidateRef newFunc{ new Candidate{ *func } };
@@ -1077 +1075 @@
                         assert( toType );
                         toType = resolveTypeof( toType, symtab );
-                        toType = SymTab::validateType( castExpr->location, toType, symtab );
+                        // toType = SymTab::validateType( castExpr->location, toType, symtab );
                         toType = adjustExprType( toType, tenv, symtab );
 
@@ -1162 +1160 @@
 
                                         if(auto insttype = dynamic_cast<const ast::TypeInstType*>(expr)) {
-                                                auto td = cand->env.lookup(insttype->name);
+                                                auto td = cand->env.lookup(*insttype);
                                                 if(!td) { continue; }
                                                 expr = td->bound.get();
@@ -1568 +1566 @@
                                 // calculate target type
                                 const ast::Type * toType = resolveTypeof( initAlt.type, symtab );
-                                toType = SymTab::validateType( initExpr->location, toType, symtab );
+                                // toType = SymTab::validateType( initExpr->location, toType, symtab );
                                 toType = adjustExprType( toType, tenv, symtab );
                                 // The call to find must occur inside this loop, otherwise polymorphic return

src/ResolvExpr/CastCost.cc

@@ -165 +165 @@
                                 } else {
                                         ast::TypeEnvironment newEnv{ env };
-                                        if ( auto wParams = pointerType->base.as< ast::ParameterizedType >() ) {
+                                        if ( auto wParams = pointerType->base.as< ast::FunctionType >() ) {
                                                 newEnv.add( wParams->forall );
                                         }
@@ -202 +202 @@
 ) {
         if ( auto typeInst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-                if ( const ast::EqvClass * eqvClass = env.lookup( typeInst->name ) ) {
+                if ( const ast::EqvClass * eqvClass = env.lookup( *typeInst ) ) {
                         // check cast cost against bound type, if present
                         if ( eqvClass->bound ) {

src/ResolvExpr/CommonType.cc

@@ -713 +713 @@
                         const ast::Type * base = oPtr->base;
                         if ( auto var = dynamic_cast< const ast::TypeInstType * >( base ) ) {
-                                auto entry = open.find( var->name );
+                                auto entry = open.find( *var );
                                 if ( entry != open.end() ) {
                                         ast::AssertionSet need, have;

src/ResolvExpr/ConversionCost.cc

@@ -498 +498 @@
 ) {
         if ( const ast::TypeInstType * inst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-                if ( const ast::EqvClass * eqv = env.lookup( inst->name ) ) {
+                if ( const ast::EqvClass * eqv = env.lookup( *inst ) ) {
                         if ( eqv->bound ) {
                                 return conversionCost(src, eqv->bound, srcIsLvalue, symtab, env );
@@ -675 +675 @@
 
 void ConversionCost_new::postvisit( const ast::TypeInstType * typeInstType ) {
-        if ( const ast::EqvClass * eqv = env.lookup( typeInstType->name ) ) {
+        if ( const ast::EqvClass * eqv = env.lookup( *typeInstType ) ) {
                 cost = costCalc( eqv->bound, dst, srcIsLvalue, symtab, env );
         } else if ( const ast::TypeInstType * dstAsInst =
                         dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-                if ( typeInstType->name == dstAsInst->name ) {
+                if ( *typeInstType == *dstAsInst ) {
                         cost = Cost::zero;
                 }

src/ResolvExpr/FindOpenVars.cc

@@ -112 +112 @@
                                 // mark open/closed variables
                                 if ( nextIsOpen ) {
-                                        for ( const ast::TypeDecl * decl : type->forall ) {
-                                                open[ decl->name ] = ast::TypeDecl::Data{ decl };
-                                                for ( const ast::DeclWithType * assert : decl->assertions ) {
-                                                        need[ assert ].isUsed = false;
-                                                }
+                                        for ( auto & decl : type->forall ) {
+                                                open[ *decl ] = ast::TypeDecl::Data{ decl->base };
+                                        }
+                                        for ( auto & assert : type->assertions ) {
+                                                need[ assert ].isUsed = false;
                                         }
                                 } else {
-                                        for ( const ast::TypeDecl * decl : type->forall ) {
-                                                closed[ decl->name ] = ast::TypeDecl::Data{ decl };
-                                                for ( const ast::DeclWithType * assert : decl->assertions ) {
-                                                        have[ assert ].isUsed = false;
-                                                }
+                                        for ( auto & decl : type->forall ) {
+                                                closed[ *decl ] = ast::TypeDecl::Data{ decl->base };    
+                                        }
+                                        for ( auto & assert : type->assertions ) {
+                                                have[ assert ].isUsed = false;
                                         }
                                 }

src/ResolvExpr/PolyCost.cc

@@ -68 +68 @@
 
         void previsit( const ast::TypeInstType * type ) {
-                if ( const ast::EqvClass * eqv = env_.lookup( type->name ) ) /* && */ if ( eqv->bound ) {
+                if ( const ast::EqvClass * eqv = env_.lookup( *type ) ) /* && */ if ( eqv->bound ) {
                         if ( const ast::TypeInstType * otherType = eqv->bound.as< ast::TypeInstType >() ) {
                                 if ( symtab.lookupType( otherType->name ) ) {

src/ResolvExpr/PtrsAssignable.cc

@@ -134 +134 @@
         }
         void postvisit( const ast::TypeInstType * inst ) {
-                if ( const ast::EqvClass * eqv = typeEnv.lookup( inst->name ) ) {
+                if ( const ast::EqvClass * eqv = typeEnv.lookup( *inst ) ) {
                         if ( eqv->bound ) {
                                 // T * = S * for any S depends on the type bound to T
@@ -146 +146 @@
                 const ast::TypeEnvironment & env ) {
         if ( const ast::TypeInstType * dstAsInst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-                if ( const ast::EqvClass * eqv = env.lookup( dstAsInst->name ) ) {
+                if ( const ast::EqvClass * eqv = env.lookup( *dstAsInst ) ) {
                         return ptrsAssignable( src, eqv->bound, env );
                 }

src/ResolvExpr/PtrsCastable.cc

@@ -180 +180 @@
                                         }
                                 }
-                        } else if ( const ast::EqvClass * eqvClass = env.lookup( inst->name ) ) {
+                        } else if ( const ast::EqvClass * eqvClass = env.lookup( *inst ) ) {
                                 if ( eqvClass->data.kind == ast::TypeDecl::Ftype ) {
                                         return -1;
@@ -283 +283 @@
 ) {
         if ( auto inst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-                if ( const ast::EqvClass * eqvClass = env.lookup( inst->name ) ) {
+                if ( const ast::EqvClass * eqvClass = env.lookup( *inst ) ) {
                         return ptrsAssignable( src, eqvClass->bound, env );
                 }

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 @@
                 }
 
-                template<typename NodeT>
-                const NodeT * openLevel( const NodeT * 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.
-                        NodeT * mutType = ast::mutate( type );
-                        assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
-                        for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
-                                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;
-                }
-
-                void closeLevel( const ast::ParameterizedType * 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 );
+                }
+
+                /*
                 const ast::StructInstType * previsit( const ast::StructInstType * type ) {
                         return renaming.openLevel( type );
@@ -158 +168 @@
                         return renaming.openLevel( type );
                 }
+                */
+
                 const ast::TypeInstType * previsit( const ast::TypeInstType * type ) {
-                        return renaming.rename( renaming.openLevel( type ) );
-                }
-                void postvisit( const ast::ParameterizedType * type ) {
+                        if (mode == GEN_USAGE && !type->formal_usage) return type; // do not rename an actual type
+                        return renaming.rename( type );
+                }
+                void postvisit( const ast::FunctionType * type ) {
                         renaming.closeLevel( type );
                 }
@@ -173 +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 ) {
+        // 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) {
+                renaming.nextUsage();
+        }
+        return t->accept( renamer );
 }
 

src/ResolvExpr/RenameVars.h

@@ -30 +30 @@
         /// Provides a consistent renaming of forall type names in a hierarchy by prefixing them with a unique "level" ID
         void renameTyVars( Type * );
-        const ast::Type * renameTyVars( const ast::Type * );
+
+        enum RenameMode {
+                GEN_USAGE, // for type in VariableExpr
+                GEN_EXPR_ID // for type in decl
+        };
+        const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE );
 
         /// resets internal state of renamer to avoid overflow
         void resetTyVarRenaming();
+
+        
 } // namespace ResolvExpr
 

src/ResolvExpr/ResolveTypeof.cc

@@ -15 +15 @@
 
 #include "ResolveTypeof.h"
+#include "RenameVars.h"
 
 #include <cassert>               // for assert
@@ -218 +219 @@
                         mutDecl->mangleName = Mangle::mangle(mutDecl); // do not mangle unnamed variables
                 
+                mutDecl->type = renameTyVars(mutDecl->type, RenameMode::GEN_EXPR_ID);
                 mutDecl->isTypeFixed = true;
                 return mutDecl;

src/ResolvExpr/Resolver.cc

@@ -968 +968 @@
         namespace {
                 /// Finds deleted expressions in an expression tree
-                struct DeleteFinder_new final : public ast::WithShortCircuiting {
+                struct DeleteFinder_new final : public ast::WithShortCircuiting, public ast::WithVisitorRef<DeleteFinder_new> {
                         const ast::DeletedExpr * result = nullptr;
 
@@ -976 +976 @@
                         }
 
-                        void previsit( const ast::Expr * ) {
+                        void previsit( const ast::Expr * expr ) {
                                 if ( result ) { visit_children = false; }
+                                if (expr->inferred.hasParams()) {
+                                        for (auto & imp : expr->inferred.inferParams() ) {
+                                                imp.second.expr->accept(*visitor);
+                                        }
+                                }
                         }
                 };
         } // anonymous namespace
-
         /// Check if this expression is or includes a deleted expression
         const ast::DeletedExpr * findDeletedExpr( const ast::Expr * expr ) {
@@ -1370 +1374 @@
                         }
 
-                        // handle assertions. (seems deep)
+                        // handle assertions
 
                         symtab.enterScope();
-                        for (auto & typeParam : mutType->forall) {
-                                auto mutParam = typeParam.get_and_mutate();
-                                symtab.addType(mutParam);
-                                for (auto & asst : mutParam->assertions) {
-                                        asst = fixObjectType(asst.strict_as<ast::ObjectDecl>(), symtab);
-                                        symtab.addId(asst);
-                                }
-                                typeParam = mutParam;
+                        mutType->forall.clear();
+                        mutType->assertions.clear();
+                        for (auto & typeParam : mutDecl->type_params) {
+                                symtab.addType(typeParam);
+                                mutType->forall.emplace_back(new ast::TypeInstType(typeParam->name, typeParam));
+                        }
+                        for (auto & asst : mutDecl->assertions) {
+                                asst = fixObjectType(asst.strict_as<ast::ObjectDecl>(), symtab);
+                                symtab.addId(asst);
+                                mutType->assertions.emplace_back(new ast::VariableExpr(functionDecl->location, asst));
                         }
 
@@ -1402 +1408 @@
                         mutType->returns = std::move(returnTypes);
 
+                        auto renamedType = strict_dynamic_cast<const ast::FunctionType *>(renameTyVars(mutType, RenameMode::GEN_EXPR_ID));
+
                         std::list<ast::ptr<ast::Stmt>> newStmts;
                         resolveWithExprs (mutDecl->withExprs, newStmts);
@@ -1413 +1421 @@
                         symtab.leaveScope();
 
+                        mutDecl->type = renamedType;
                         mutDecl->mangleName = Mangle::mangle(mutDecl);
                         mutDecl->isTypeFixed = true;

src/ResolvExpr/SatisfyAssertions.cpp

@@ -69 +69 @@
         /// Reference to a single deferred item
         struct DeferRef {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 const AssnCandidate & match;
@@ -77 +77 @@
         /// Acts like an indexed list of DeferRef
         struct DeferItem {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 AssnCandidateList matches;
 
                 DeferItem( 
-                        const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
-                : decl( d ), info( i ), matches( std::move( ms ) ) {}
+                        const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
+                : expr( d ), info( i ), matches( std::move( ms ) ) {}
 
                 bool empty() const { return matches.empty(); }
@@ -89 +89 @@
                 AssnCandidateList::size_type size() const { return matches.size(); }
 
-                DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+                DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
         };
 
@@ -138 +138 @@
         void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
                 for ( auto & i : have ) {
-                        if ( i.second.isUsed ) { symtab.addId( i.first ); }
+                        if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
                 }
         }
@@ -144 +144 @@
         /// Binds a single assertion, updating satisfaction state
         void bindAssertion( 
-                const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+                const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 
                 AssnCandidate & match, InferCache & inferred
         ) {
@@ -156 +156 @@
 
                 // place newly-inferred assertion in proper location in cache
-                inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{
-                        candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };
+                inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
+                        candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
         }
 
@@ -169 +169 @@
 
                 std::vector<ast::SymbolTable::IdData> candidates;
-                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->name);
+                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
                 if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
                         // prefilter special decls by argument type, if already known
-                        ast::ptr<ast::Type> thisArgType = strict_dynamic_cast<const ast::PointerType *>(assn.first->get_type())->base
+                        ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
                                 .strict_as<ast::FunctionType>()->params[0]
                                 .strict_as<ast::ReferenceType>()->base;
@@ -184 +184 @@
                 }
                 else {
-                        candidates = sat.symtab.lookupId(assn.first->name);
+                        candidates = sat.symtab.lookupId(assn.first->var->name);
                 }
                 for ( const ast::SymbolTable::IdData & cdata : candidates ) {
@@ -194 +194 @@
                         // if we should implement the same rule here
                         // (i.e. error if unique best match is deleted)
-                        if (candidate->isDeleted) continue;
+                        if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue;
 
                         // build independent unification context for candidate
@@ -200 +200 @@
                         ast::TypeEnvironment newEnv{ sat.cand->env };
                         ast::OpenVarSet newOpen{ sat.cand->open };
-                        ast::ptr< ast::Type > toType = assn.first->get_type();
+                        ast::ptr< ast::Type > toType = assn.first->result;
                         ast::ptr< ast::Type > adjType = 
                                 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
@@ -337 +337 @@
                                         // compute conversion cost from satisfying decl to assertion
                                         cost += computeConversionCost(
-                                                assn.match.adjType, assn.decl->get_type(), false, symtab, env );
+                                                assn.match.adjType, assn.expr->result, false, symtab, env );
 
                                         // mark vars+specialization on function-type assertions
@@ -350 +350 @@
                                         cost.incVar( func->forall.size() );
 
-                                        for ( const ast::TypeDecl * td : func->forall ) {
-                                                cost.decSpec( td->assertions.size() );
-                                        }
+                                        cost.decSpec( func->assertions.size() );
                                 }
                         }
@@ -451 +449 @@
                                 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
                                 for ( const auto & d : sat.deferred ) {
-                                        ast::print( ss, d.decl, tabs );
+                                        ast::print( ss, d.expr, tabs );
                                 }
 
@@ -469 +467 @@
                                         ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
                                         for ( const auto& d : sat.deferred ) {
-                                                ast::print( ss, d.decl, tabs );
+                                                ast::print( ss, d.expr, tabs );
                                         }
 
@@ -501 +499 @@
                                                 nextNewNeed.insert( match.need.begin(), match.need.end() );
 
-                                                bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
+                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
                                         }
 

src/ResolvExpr/Unify.cc

@@ -773 +773 @@
 
                         const ast::Type * postvisit( const ast::TypeInstType * typeInst ) {
-                                if ( const ast::EqvClass * clz = tenv.lookup( typeInst->name ) ) {
+                                if ( const ast::EqvClass * clz = tenv.lookup( *typeInst ) ) {
                                         // expand ttype parameter into its actual type
                                         if ( clz->data.kind == ast::TypeDecl::Ttype && clz->bound ) {
@@ -888 +888 @@
                 }
 
-                static void markAssertionSet( ast::AssertionSet & assns, const ast::DeclWithType * assn ) {
+                static void markAssertionSet( ast::AssertionSet & assns, const ast::VariableExpr * assn ) {
                         auto i = assns.find( assn );
                         if ( i != assns.end() ) {
@@ -898 +898 @@
                 static void markAssertions(
                         ast::AssertionSet & assn1, ast::AssertionSet & assn2,
-                        const ast::ParameterizedType * type
+                        const ast::FunctionType * type
                 ) {
-                        for ( const auto & tyvar : type->forall ) {
-                                for ( const ast::DeclWithType * assert : tyvar->assertions ) {
-                                        markAssertionSet( assn1, assert );
-                                        markAssertionSet( assn2, assert );
-                                }
+                        for ( auto & assert : type->assertions ) {
+                                markAssertionSet( assn1, assert );
+                                markAssertionSet( assn2, assert );
                         }
                 }
@@ -1030 +1028 @@
 
                 void postvisit( const ast::TypeInstType * typeInst ) {
-                        assert( open.find( typeInst->name ) == open.end() );
+                        assert( open.find( *typeInst ) == open.end() );
                         handleRefType( typeInst, type2 );
                 }
@@ -1171 +1169 @@
                 auto var2 = dynamic_cast< const ast::TypeInstType * >( type2 );
                 ast::OpenVarSet::const_iterator
-                        entry1 = var1 ? open.find( var1->name ) : open.end(),
-                        entry2 = var2 ? open.find( var2->name ) : open.end();
+                        entry1 = var1 ? open.find( *var1 ) : open.end(),
+                        entry2 = var2 ? open.find( *var2 ) : open.end();
                 bool isopen1 = entry1 != open.end();
                 bool isopen2 = entry2 != open.end();

src/SymTab/Mangler.cc

@@ -666 +666 @@
                         // skip if not including qualifiers
                         if ( typeMode ) return;
-                        if ( auto ptype = dynamic_cast< const ast::ParameterizedType * >(type) ) {
+                        if ( auto ptype = dynamic_cast< const ast::FunctionType * >(type) ) {
                                 if ( ! ptype->forall.empty() ) {
                                         std::list< std::string > assertionNames;
                                         int dcount = 0, fcount = 0, vcount = 0, acount = 0;
                                         mangleName += Encoding::forall;
-                                        for ( const ast::TypeDecl * decl : ptype->forall ) {
+                                        for ( auto & decl : ptype->forall ) {
                                                 switch ( decl->kind ) {
                                                 case ast::TypeDecl::Kind::Dtype:
@@ -686 +686 @@
                                                 } // switch
                                                 varNums[ decl->name ] = std::make_pair( nextVarNum, (int)decl->kind );
-                                                for ( const ast::DeclWithType * assert : decl->assertions ) {
-                                                        ast::Pass<Mangler_new> sub_mangler(
-                                                                mangleOverridable, typeMode, mangleGenericParams, nextVarNum, varNums );
-                                                        assert->accept( sub_mangler );
-                                                        assertionNames.push_back( sub_mangler.core.get_mangleName() );
-                                                        acount++;
-                                                } // for
+                                        } // for
+                                        for ( auto & assert : ptype->assertions ) {
+                                                ast::Pass<Mangler_new> sub_mangler(
+                                                        mangleOverridable, typeMode, mangleGenericParams, nextVarNum, varNums );
+                                                assert->var->accept( sub_mangler );
+                                                assertionNames.push_back( sub_mangler.core.get_mangleName() );
+                                                acount++;
                                         } // for
                                         mangleName += std::to_string( dcount ) + "_" + std::to_string( fcount ) + "_" + std::to_string( vcount ) + "_" + std::to_string( acount ) + "_";

src/SymTab/Validate.cc

@@ -1463 +1463 @@
         }
 
+        /*
+
         /// Associates forward declarations of aggregates with their definitions
         class LinkReferenceToTypes_new final
@@ -1793 +1795 @@
                 static const node_t * forallFixer(
                         const CodeLocation & loc, const node_t * node,
-                        ast::ParameterizedType::ForallList parent_t::* forallField
+                        ast::FunctionType::ForallList parent_t::* forallField
                 ) {
                         for ( unsigned i = 0; i < (node->* forallField).size(); ++i ) {
@@ -1844 +1846 @@
                 }
         };
+        */
 } // anonymous namespace
 
+/*
 const ast::Type * validateType(
                 const CodeLocation & loc, const ast::Type * type, const ast::SymbolTable & symtab ) {
@@ -1854 +1858 @@
         return type->accept( lrt )->accept( fpd );
 }
+*/
 
 } // namespace SymTab

src/SynTree/Declaration.h

@@ -181 +181 @@
   public:
         Type * base;
-        std::list< TypeDecl * > parameters;
         std::list< DeclarationWithType * > assertions;
 
@@ -190 +189 @@
         Type * get_base() const { return base; }
         void set_base( Type * newValue ) { base = newValue; }
-        std::list< TypeDecl* > & get_parameters() { return parameters; }
         std::list< DeclarationWithType * >& get_assertions() { return assertions; }
 

src/SynTree/NamedTypeDecl.cc

@@ -29 +29 @@
 NamedTypeDecl::NamedTypeDecl( const NamedTypeDecl &other )
         : Parent( other ), base( maybeClone( other.base ) ) {
-        cloneAll( other.parameters, parameters );
         cloneAll( other.assertions, assertions );
 }
@@ -35 +34 @@
 NamedTypeDecl::~NamedTypeDecl() {
         delete base;
-        deleteAll( parameters );
         deleteAll( assertions );
 }
@@ -56 +54 @@
                 base->print( os, indent+1 );
         } // if
-        if ( ! parameters.empty() ) {
-                os << endl << indent << "... with parameters" << endl;
-                printAll( parameters, os, indent+1 );
-        } // if
         if ( ! assertions.empty() ) {
                 os << endl << indent << "... with assertions" << endl;
@@ -76 +70 @@
                 base->print( os, indent+1 );
         } // if
-        if ( ! parameters.empty() ) {
-                os << endl << indent << "... with parameters" << endl;
-                printAll( parameters, os, indent+1 );
-        } // if
 }
 

src/Tuples/TupleAssignment.cc

@@ -504 +504 @@
 
                         std::vector< ast::ptr< ast::Expr > > match() override {
-                                // temporary workaround for new and old ast to coexist and avoid name collision
-                                static UniqueName lhsNamer( "__massassign_Ln" );
-                                static UniqueName rhsNamer( "__massassign_Rn" );
+                                static UniqueName lhsNamer( "__massassign_L" );
+                                static UniqueName rhsNamer( "__massassign_R" );
                                 // empty tuple case falls into this matcher
                                 assert( lhs.empty() ? rhs.empty() : rhs.size() <= 1 );
@@ -535 +534 @@
 
                         std::vector< ast::ptr< ast::Expr > > match() override {
-                                // temporary workaround for new and old ast to coexist and avoid name collision
-                                static UniqueName lhsNamer( "__multassign_Ln" );
-                                static UniqueName rhsNamer( "__multassign_Rn" );
+                                static UniqueName lhsNamer( "__multassign_L" );
+                                static UniqueName rhsNamer( "__multassign_R" );
 
                                 if ( lhs.size() != rhs.size() ) return {};