Changeset 53449a4 for src/AST

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/AST

Files:

• Convert.cpp (modified) (16 diffs)
• Decl.cpp (modified) (1 diff)
• Decl.hpp (modified) (3 diffs)
• Expr.cpp (modified) (1 diff)
• Expr.hpp (modified) (1 diff)
• ForallSubstitutionTable.cpp (deleted)
• ForallSubstitutionTable.hpp (deleted)
• ForallSubstitutor.hpp (deleted)
• Fwd.hpp (modified) (1 diff)
• Pass.hpp (modified) (5 diffs)
• Pass.impl.hpp (modified) (12 diffs)
• Pass.proto.hpp (modified) (3 diffs)
• Print.cpp (modified) (6 diffs)
• SymbolTable.cpp (modified) (1 diff)
• TranslationUnit.hpp (modified) (1 diff)
• Type.cpp (modified) (5 diffs)
• Type.hpp (modified) (9 diffs)
• TypeEnvironment.cpp (modified) (15 diffs)
• TypeEnvironment.hpp (modified) (7 diffs)
• TypeSubstitution.cpp (modified) (9 diffs)
• TypeSubstitution.hpp (modified) (7 diffs)
• module.mk (modified) (1 diff)

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 \